![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluzelz | Unicode version |
Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.) |
Ref | Expression |
---|---|
eluzelz |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz2 9532 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simp2bi 1013 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-14 2151 ax-ext 2159 ax-sep 4121 ax-pow 4174 ax-pr 4209 ax-cnex 7901 ax-resscn 7902 |
This theorem depends on definitions: df-bi 117 df-3or 979 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-rab 2464 df-v 2739 df-sbc 2963 df-un 3133 df-in 3135 df-ss 3142 df-pw 3577 df-sn 3598 df-pr 3599 df-op 3601 df-uni 3810 df-br 4004 df-opab 4065 df-mpt 4066 df-id 4293 df-xp 4632 df-rel 4633 df-cnv 4634 df-co 4635 df-dm 4636 df-rn 4637 df-res 4638 df-ima 4639 df-iota 5178 df-fun 5218 df-fn 5219 df-f 5220 df-fv 5224 df-ov 5877 df-neg 8129 df-z 9252 df-uz 9527 |
This theorem is referenced by: eluzelre 9536 uztrn 9542 uzneg 9544 uzssz 9545 uzss 9546 eluzp1l 9550 eluzaddi 9552 eluzsubi 9553 eluzadd 9554 eluzsub 9555 uzm1 9556 uzin 9558 uzind4 9586 uz2mulcl 9606 elfz5 10014 elfzel2 10020 elfzelz 10022 eluzfz2 10029 peano2fzr 10034 fzsplit2 10047 fzopth 10058 fzsuc 10066 elfzp1 10069 fzdifsuc 10078 uzsplit 10089 uzdisj 10090 fzm1 10097 fzneuz 10098 uznfz 10100 nn0disj 10135 elfzo3 10160 fzoss2 10169 fzouzsplit 10176 eluzgtdifelfzo 10194 fzosplitsnm1 10206 fzofzp1b 10225 elfzonelfzo 10227 fzosplitsn 10230 fzisfzounsn 10233 mulp1mod1 10362 m1modge3gt1 10368 frec2uzltd 10400 frecfzen2 10424 uzennn 10433 uzsinds 10439 seq3fveq2 10466 seq3feq2 10467 seq3shft2 10470 monoord 10473 monoord2 10474 ser3mono 10475 seq3split 10476 iseqf1olemjpcl 10492 iseqf1olemqpcl 10493 seq3f1olemqsumk 10496 seq3f1olemp 10499 seq3f1oleml 10500 seq3f1o 10501 seq3id 10505 seq3z 10508 fser0const 10513 leexp2a 10570 expnlbnd2 10642 hashfz 10796 hashfzo 10797 hashfzp1 10799 seq3coll 10817 seq3shft 10842 rexuz3 10994 r19.2uz 10997 cau4 11120 caubnd2 11121 clim 11284 climshft2 11309 climaddc1 11332 climmulc2 11334 climsubc1 11335 climsubc2 11336 clim2ser 11340 clim2ser2 11341 iserex 11342 climlec2 11344 climub 11347 climcau 11350 climcaucn 11354 serf0 11355 sumrbdclem 11380 fsum3cvg 11381 summodclem2a 11384 zsumdc 11387 fsum3 11390 fisumss 11395 fsum3cvg2 11397 fsum3ser 11400 fsumcl2lem 11401 fsumadd 11409 fsumm1 11419 fzosump1 11420 fsum1p 11421 fsump1 11423 fsummulc2 11451 telfsumo 11469 fsumparts 11473 iserabs 11478 binomlem 11486 isumshft 11493 isumsplit 11494 isumrpcl 11497 divcnv 11500 trireciplem 11503 geosergap 11509 geolim2 11515 cvgratnnlemseq 11529 cvgratnnlemabsle 11530 cvgratnnlemsumlt 11531 cvgratnnlemrate 11533 cvgratz 11535 cvgratgt0 11536 mertenslemi1 11538 clim2divap 11543 prodrbdclem 11574 fproddccvg 11575 prodmodclem3 11578 prodmodclem2a 11579 zproddc 11582 fprodntrivap 11587 fprodssdc 11593 fprodm1 11601 fprod1p 11602 fprodp1 11603 fprodabs 11619 fprodeq0 11620 efgt1p2 11698 modm1div 11802 zsupcllemstep 11940 infssuzex 11944 suprzubdc 11947 dvdsbnd 11951 uzwodc 12032 ncoprmgcdne1b 12083 isprm3 12112 prmind2 12114 nprm 12117 dvdsprm 12131 exprmfct 12132 isprm5lem 12135 isprm5 12136 phibndlem 12210 phibnd 12211 dfphi2 12214 hashdvds 12215 pclemdc 12282 pcaddlem 12332 pcmptdvds 12337 pcfac 12342 expnprm 12345 relogbval 14300 relogbzcl 14301 nnlogbexp 14308 logblt 14311 logbgcd1irr 14316 lgsne0 14370 2sqlem6 14387 2sqlem8a 14389 2sqlem8 14390 supfz 14738 |
Copyright terms: Public domain | W3C validator |