![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eluzel2 | Structured version Visualization version GIF version |
Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Ref | Expression |
---|---|
eluzel2 | β’ (π β (β€β₯βπ) β π β β€) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfvdm 6899 | . 2 β’ (π β (β€β₯βπ) β π β dom β€β₯) | |
2 | uzf 12790 | . . 3 β’ β€β₯:β€βΆπ« β€ | |
3 | 2 | fdmi 6700 | . 2 β’ dom β€β₯ = β€ |
4 | 1, 3 | eleqtrdi 2842 | 1 β’ (π β (β€β₯βπ) β π β β€) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wcel 2106 π« cpw 4580 dom cdm 5653 βcfv 6516 β€cz 12523 β€β₯cuz 12787 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5276 ax-nul 5283 ax-pr 5404 ax-cnex 11131 ax-resscn 11132 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3419 df-v 3461 df-dif 3931 df-un 3933 df-in 3935 df-ss 3945 df-nul 4303 df-if 4507 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4886 df-br 5126 df-opab 5188 df-mpt 5209 df-id 5551 df-xp 5659 df-rel 5660 df-cnv 5661 df-co 5662 df-dm 5663 df-rn 5664 df-res 5665 df-ima 5666 df-iota 6468 df-fun 6518 df-fn 6519 df-f 6520 df-fv 6524 df-ov 7380 df-neg 11412 df-z 12524 df-uz 12788 |
This theorem is referenced by: eluz2 12793 uztrn 12805 uzneg 12807 uzss 12810 uz11 12812 eluzadd 12816 eluzaddOLD 12822 subeluzsub 12824 uzm1 12825 uzin 12827 uzind4 12855 uzsupss 12889 elfz5 13458 elfzel1 13465 eluzfz1 13473 fzsplit2 13491 fzopth 13503 ssfzunsn 13512 fzpred 13514 fzpreddisj 13515 uzsplit 13538 uzdisj 13539 fzm1 13546 uznfz 13549 nn0disj 13582 preduz 13588 fzolb 13603 fzoss2 13625 fzouzdisj 13633 fzoun 13634 ige2m2fzo 13660 fzen2 13899 seqp1 13946 seqcl 13953 seqfeq2 13956 seqfveq 13957 seqshft2 13959 seqsplit 13966 seqcaopr3 13968 seqf1olem2a 13971 seqf1olem1 13972 seqf1olem2 13973 seqid 13978 seqhomo 13980 seqz 13981 leexp2a 14102 hashfz 14352 fzsdom2 14353 hashfzo 14354 hashfzp1 14356 seqcoll 14390 rexanuz2 15261 cau4 15268 clim2ser 15566 clim2ser2 15567 climserle 15574 caurcvg 15588 caucvg 15590 fsumcvg 15623 fsumcvg2 15638 fsumsers 15639 fsumm1 15662 fsum1p 15664 fsumrev2 15693 telfsumo 15713 fsumparts 15717 cvgcmp 15727 cvgcmpub 15728 cvgcmpce 15729 isumsplit 15751 clim2prod 15799 clim2div 15800 prodfrec 15806 ntrivcvgtail 15811 fprodcvg 15839 fprodser 15858 fprodm1 15876 fprodeq0 15884 pcaddlem 16786 vdwnnlem2 16894 prmlem0 17004 gsumval2a 18569 telgsumfzs 19795 dvfsumle 25437 dvfsumge 25438 dvfsumabs 25439 coeid3 25653 ulmres 25799 ulmss 25808 chtdif 26559 ppidif 26564 bcmono 26677 axlowdimlem6 27993 inffz 34422 mettrifi 36323 jm2.25 41414 jm2.16nn0 41419 dvgrat 42747 ssinc 43452 ssdec 43453 fzdifsuc2 43698 iuneqfzuzlem 43722 ssuzfz 43737 ioodvbdlimc1lem2 44326 ioodvbdlimc2lem 44328 carageniuncllem1 44915 caratheodorylem1 44920 |
Copyright terms: Public domain | W3C validator |