Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > uzid | Unicode version |
Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
Ref | Expression |
---|---|
uzid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre 9209 | . . . 4 | |
2 | 1 | leidd 8426 | . . 3 |
3 | 2 | ancli 321 | . 2 |
4 | eluz1 9484 | . 2 | |
5 | 3, 4 | mpbird 166 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 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-in1 609 ax-in2 610 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-13 2143 ax-14 2144 ax-ext 2152 ax-sep 4105 ax-pow 4158 ax-pr 4192 ax-un 4416 ax-setind 4519 ax-cnex 7858 ax-resscn 7859 ax-pre-ltirr 7879 |
This theorem depends on definitions: df-bi 116 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 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-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-rab 2457 df-v 2732 df-sbc 2956 df-dif 3123 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-iota 5158 df-fun 5198 df-fv 5204 df-ov 5854 df-pnf 7949 df-mnf 7950 df-xr 7951 df-ltxr 7952 df-le 7953 df-neg 8086 df-z 9206 df-uz 9481 |
This theorem is referenced by: uzn0 9495 uz11 9502 eluzfz1 9980 eluzfz2 9981 elfz3 9983 elfz1end 10004 fzssp1 10016 fzpred 10019 fzp1ss 10022 fzpr 10026 fztp 10027 elfz0add 10069 fzolb 10102 zpnn0elfzo 10156 fzosplitsnm1 10158 fzofzp1 10176 fzosplitsn 10182 fzostep1 10186 frec2uzuzd 10351 frecuzrdgrrn 10357 frec2uzrdg 10358 frecuzrdgrcl 10359 frecuzrdgsuc 10363 frecuzrdgrclt 10364 frecuzrdgg 10365 frecuzrdgsuctlem 10372 uzsinds 10391 seq3val 10407 seqvalcd 10408 seq3-1 10409 seqf 10410 seq3p1 10411 seq3fveq 10420 seq3-1p 10429 seq3caopr3 10430 iseqf1olemjpcl 10444 iseqf1olemqpcl 10445 seq3f1oleml 10452 seq3f1o 10453 seq3homo 10459 faclbnd3 10670 bcm1k 10687 bcn2 10691 seq3coll 10770 rexuz3 10947 r19.2uz 10950 resqrexlemcvg 10976 resqrexlemgt0 10977 resqrexlemoverl 10978 cau3lem 11071 caubnd2 11074 climconst 11246 climuni 11249 climcau 11303 serf0 11308 fsumparts 11426 isum1p 11448 isumrpcl 11450 cvgratz 11488 mertenslemi1 11491 ntrivcvgap0 11505 fprodabs 11572 eftlub 11646 zsupcllemstep 11893 zsupcllemex 11894 ialgr0 11991 eucalg 12006 pw2dvds 12113 eulerthlemrprm 12176 oddprm 12206 pcfac 12295 pcbc 12296 ennnfonelem1 12355 lmconst 12975 2logb9irr 13648 sqrt2cxp2logb9e3 13652 2logb9irrap 13654 cvgcmp2nlemabs 14029 trilpolemlt1 14038 |
Copyright terms: Public domain | W3C validator |