![]() |
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 6929 | . 2 β’ (π β (β€β₯βπ) β π β dom β€β₯) | |
2 | uzf 12825 | . . 3 β’ β€β₯:β€βΆπ« β€ | |
3 | 2 | fdmi 6730 | . 2 β’ dom β€β₯ = β€ |
4 | 1, 3 | eleqtrdi 2844 | 1 β’ (π β (β€β₯βπ) β π β β€) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wcel 2107 π« cpw 4603 dom cdm 5677 βcfv 6544 β€cz 12558 β€β₯cuz 12822 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 ax-cnex 11166 ax-resscn 11167 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-fv 6552 df-ov 7412 df-neg 11447 df-z 12559 df-uz 12823 |
This theorem is referenced by: eluz2 12828 uztrn 12840 uzneg 12842 uzss 12845 uz11 12847 eluzadd 12851 eluzaddOLD 12857 subeluzsub 12859 uzm1 12860 uzin 12862 uzind4 12890 uzsupss 12924 elfz5 13493 elfzel1 13500 eluzfz1 13508 fzsplit2 13526 fzopth 13538 ssfzunsn 13547 fzpred 13549 fzpreddisj 13550 uzsplit 13573 uzdisj 13574 fzm1 13581 uznfz 13584 nn0disj 13617 preduz 13623 fzolb 13638 fzoss2 13660 fzouzdisj 13668 fzoun 13669 ige2m2fzo 13695 fzen2 13934 seqp1 13981 seqcl 13988 seqfeq2 13991 seqfveq 13992 seqshft2 13994 seqsplit 14001 seqcaopr3 14003 seqf1olem2a 14006 seqf1olem1 14007 seqf1olem2 14008 seqid 14013 seqhomo 14015 seqz 14016 leexp2a 14137 hashfz 14387 fzsdom2 14388 hashfzo 14389 hashfzp1 14391 seqcoll 14425 rexanuz2 15296 cau4 15303 clim2ser 15601 clim2ser2 15602 climserle 15609 caurcvg 15623 caucvg 15625 fsumcvg 15658 fsumcvg2 15673 fsumsers 15674 fsumm1 15697 fsum1p 15699 fsumrev2 15728 telfsumo 15748 fsumparts 15752 cvgcmp 15762 cvgcmpub 15763 cvgcmpce 15764 isumsplit 15786 clim2prod 15834 clim2div 15835 prodfrec 15841 ntrivcvgtail 15846 fprodcvg 15874 fprodser 15893 fprodm1 15911 fprodeq0 15919 pcaddlem 16821 vdwnnlem2 16929 prmlem0 17039 gsumval2a 18604 telgsumfzs 19857 dvfsumle 25538 dvfsumge 25539 dvfsumabs 25540 coeid3 25754 ulmres 25900 ulmss 25909 chtdif 26662 ppidif 26667 bcmono 26780 axlowdimlem6 28205 inffz 34699 gg-dvfsumle 35182 mettrifi 36625 jm2.25 41738 jm2.16nn0 41743 dvgrat 43071 ssinc 43776 ssdec 43777 fzdifsuc2 44020 iuneqfzuzlem 44044 ssuzfz 44059 ioodvbdlimc1lem2 44648 ioodvbdlimc2lem 44650 carageniuncllem1 45237 caratheodorylem1 45242 |
Copyright terms: Public domain | W3C validator |