Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eluzle | Unicode version |
Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) |
Ref | Expression |
---|---|
eluzle |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz2 9486 | . 2 | |
2 | 1 | simp3bi 1009 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2141 class class class wbr 3987 cfv 5196 cle 7948 cz 9205 cuz 9480 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-14 2144 ax-ext 2152 ax-sep 4105 ax-pow 4158 ax-pr 4192 ax-cnex 7858 ax-resscn 7859 |
This theorem depends on definitions: df-bi 116 df-3or 974 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-rex 2454 df-rab 2457 df-v 2732 df-sbc 2956 df-un 3125 df-in 3127 df-ss 3134 df-pw 3566 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-br 3988 df-opab 4049 df-mpt 4050 df-id 4276 df-xp 4615 df-rel 4616 df-cnv 4617 df-co 4618 df-dm 4619 df-rn 4620 df-res 4621 df-ima 4622 df-iota 5158 df-fun 5198 df-fn 5199 df-f 5200 df-fv 5204 df-ov 5854 df-neg 8086 df-z 9206 df-uz 9481 |
This theorem is referenced by: uztrn 9496 uzneg 9498 uzss 9500 uz11 9502 eluzp1l 9504 uzm1 9510 uzin 9512 uzind4 9540 elfz5 9966 elfzle1 9976 elfzle2 9977 elfzle3 9979 uzsplit 10041 uzdisj 10042 uznfz 10052 elfz2nn0 10061 uzsubfz0 10078 nn0disj 10087 fzouzdisj 10129 elfzonelfzo 10179 mulp1mod1 10314 m1modge3gt1 10320 uzennn 10385 seq3split 10428 seq3f1olemqsumk 10448 seq3f1o 10453 seq3coll 10770 seq3shft 10795 cvg1nlemcau 10941 resqrexlemcvg 10976 resqrexlemga 10980 summodclem2a 11337 fsum3 11343 fsum3cvg3 11352 fsumadd 11362 sumsnf 11365 fsummulc2 11404 isumshft 11446 divcnv 11453 geolim2 11468 cvgratnnlemseq 11482 cvgratnnlemsumlt 11484 cvgratz 11488 mertenslemi1 11491 prodmodclem3 11531 prodmodclem2a 11532 fprodntrivap 11540 prodsnf 11548 fprodeq0 11573 efcllemp 11614 infssuzex 11897 suprzubdc 11900 dvdsbnd 11904 uzwodc 11985 ncoprmgcdne1b 12036 isprm5 12089 hashdvds 12168 pcmpt2 12289 pcfaclem 12294 pcfac 12295 nninfdclemp1 12398 lgslem1 13660 lgsdirprm 13694 cvgcmp2nlemabs 14029 |
Copyright terms: Public domain | W3C validator |