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 6702 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥) | |
2 | uzf 12247 | . . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
3 | 2 | fdmi 6524 | . 2 ⊢ dom ℤ≥ = ℤ |
4 | 1, 3 | eleqtrdi 2923 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 𝒫 cpw 4539 dom cdm 5555 ‘cfv 6355 ℤcz 11982 ℤ≥cuz 12244 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-cnex 10593 ax-resscn 10594 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-fv 6363 df-ov 7159 df-neg 10873 df-z 11983 df-uz 12245 |
This theorem is referenced by: eluz2 12250 uztrn 12262 uzneg 12264 uzss 12266 uz11 12268 eluzadd 12274 subeluzsub 12276 uzm1 12277 uzin 12279 uzind4 12307 uzsupss 12341 elfz5 12901 elfzel1 12908 eluzfz1 12915 fzsplit2 12933 fzopth 12945 ssfzunsn 12954 fzpred 12956 fzpreddisj 12957 uzsplit 12980 uzdisj 12981 fzm1 12988 uznfz 12991 nn0disj 13024 preduz 13030 fzolb 13045 fzoss2 13066 fzouzdisj 13074 fzoun 13075 ige2m2fzo 13101 fzen2 13338 seqp1 13385 seqcl 13391 seqfeq2 13394 seqfveq 13395 seqshft2 13397 seqsplit 13404 seqcaopr3 13406 seqf1olem2a 13409 seqf1olem1 13410 seqf1olem2 13411 seqid 13416 seqhomo 13418 seqz 13419 leexp2a 13537 hashfz 13789 fzsdom2 13790 hashfzo 13791 hashfzp1 13793 seqcoll 13823 rexanuz2 14709 cau4 14716 clim2ser 15011 clim2ser2 15012 climserle 15019 caurcvg 15033 caucvg 15035 fsumcvg 15069 fsumcvg2 15084 fsumsers 15085 fsumm1 15106 fsum1p 15108 fsumrev2 15137 telfsumo 15157 fsumparts 15161 cvgcmp 15171 cvgcmpub 15172 cvgcmpce 15173 isumsplit 15195 clim2prod 15244 clim2div 15245 prodfrec 15251 ntrivcvgtail 15256 fprodcvg 15284 fprodser 15303 fprodm1 15321 fprodeq0 15329 pcaddlem 16224 vdwnnlem2 16332 prmlem0 16439 gsumval2a 17895 telgsumfzs 19109 dvfsumle 24618 dvfsumge 24619 dvfsumabs 24620 coeid3 24830 ulmres 24976 ulmss 24985 chtdif 25735 ppidif 25740 bcmono 25853 axlowdimlem6 26733 inffz 32961 mettrifi 35047 jm2.25 39645 jm2.16nn0 39650 dvgrat 40693 ssinc 41402 ssdec 41403 fzdifsuc2 41626 iuneqfzuzlem 41651 ssuzfz 41666 ioodvbdlimc1lem2 42266 ioodvbdlimc2lem 42268 carageniuncllem1 42852 caratheodorylem1 42857 |
Copyright terms: Public domain | W3C validator |