Thanks Glauco for showing this example. I didn’t expect that |- 0 < k implies |- 0 < -u 1 .
- Igor On Saturday, October 19, 2024 at 8:29:25 PM UTC+2 Glauco wrote: > Hi Igor, > > as Mario pointed out, we'd better be careful with free setvars in hyps. > > For instance, from hyp > > |- 0 < k > > you can derive everything. Here's an example > > h1::temp4.1 |- 0 < k > 2::negex |- -u 1 e. _V > 3::breq2 |- ( k = -u 1 -> ( 0 < k <-> 0 < -u 1 ) ) > 4:2,3,1:vtocl |- 0 < -u 1 > 5::lenlt |- ( ( -u 1 e. RR /\ 0 e. RR ) -> ( -u 1 <_ 0 <-> > -. 0 < -u 1 ) ) > 6::neg1rr |- -u 1 e. RR > 7::0re |- 0 e. RR > 8::neg1lt0 |- -u 1 < 0 > 9:6,7,8:ltleii |- -u 1 <_ 0 > 10::neg1rr |- -u 1 e. RR > 11::0re |- 0 e. RR > 12:10,11,5:mp2an |- ( -u 1 <_ 0 <-> -. 0 < -u 1 ) > 13:12:biimpi |- ( -u 1 <_ 0 -> -. 0 < -u 1 ) > 14:9,13:ax-mp |- -. 0 < -u 1 > qed:4,14:pm2.24ii |- 1 e. (/) > > $= ( cc0 c1 cneg clt wbr c0 wcel cv negex breq2 vtocl cle wn neg1rr 0re > neg1lt0 > ltleii cr wb lenlt mp2an biimpi ax-mp pm2.24ii ) > CDEZFGZDHICAJZFGUHAUGDKUIUG > CFLBMUGCNGZUHOZUGCPQRSUJUKUGTICTIUJUKUAPQUGCUBUCUDUEUF $. > > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3bf568bf-cae2-4853-9735-555598676ef5n%40googlegroups.com.
