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 6704 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥) | |
2 | uzf 12249 | . . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
3 | 2 | fdmi 6526 | . 2 ⊢ dom ℤ≥ = ℤ |
4 | 1, 3 | eleqtrdi 2925 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 𝒫 cpw 4541 dom cdm 5557 ‘cfv 6357 ℤcz 11984 ℤ≥cuz 12246 |
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 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-cnex 10595 ax-resscn 10596 |
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 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-sbc 3775 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-fv 6365 df-ov 7161 df-neg 10875 df-z 11985 df-uz 12247 |
This theorem is referenced by: eluz2 12252 uztrn 12264 uzneg 12266 uzss 12268 uz11 12270 eluzadd 12276 subeluzsub 12278 uzm1 12279 uzin 12281 uzind4 12309 uzsupss 12343 elfz5 12903 elfzel1 12910 eluzfz1 12917 fzsplit2 12935 fzopth 12947 ssfzunsn 12956 fzpred 12958 fzpreddisj 12959 uzsplit 12982 uzdisj 12983 fzm1 12990 uznfz 12993 nn0disj 13026 preduz 13032 fzolb 13047 fzoss2 13068 fzouzdisj 13076 fzoun 13077 ige2m2fzo 13103 fzen2 13340 seqp1 13387 seqcl 13393 seqfeq2 13396 seqfveq 13397 seqshft2 13399 seqsplit 13406 seqcaopr3 13408 seqf1olem2a 13411 seqf1olem1 13412 seqf1olem2 13413 seqid 13418 seqhomo 13420 seqz 13421 leexp2a 13539 hashfz 13791 fzsdom2 13792 hashfzo 13793 hashfzp1 13795 seqcoll 13825 rexanuz2 14711 cau4 14718 clim2ser 15013 clim2ser2 15014 climserle 15021 caurcvg 15035 caucvg 15037 fsumcvg 15071 fsumcvg2 15086 fsumsers 15087 fsumm1 15108 fsum1p 15110 fsumrev2 15139 telfsumo 15159 fsumparts 15163 cvgcmp 15173 cvgcmpub 15174 cvgcmpce 15175 isumsplit 15197 clim2prod 15246 clim2div 15247 prodfrec 15253 ntrivcvgtail 15258 fprodcvg 15286 fprodser 15305 fprodm1 15323 fprodeq0 15331 pcaddlem 16226 vdwnnlem2 16334 prmlem0 16441 gsumval2a 17897 telgsumfzs 19111 dvfsumle 24620 dvfsumge 24621 dvfsumabs 24622 coeid3 24832 ulmres 24978 ulmss 24987 chtdif 25737 ppidif 25742 bcmono 25855 axlowdimlem6 26735 inffz 32963 mettrifi 35034 jm2.25 39603 jm2.16nn0 39608 dvgrat 40651 ssinc 41360 ssdec 41361 fzdifsuc2 41584 iuneqfzuzlem 41609 ssuzfz 41624 ioodvbdlimc1lem2 42224 ioodvbdlimc2lem 42226 carageniuncllem1 42810 caratheodorylem1 42815 |
Copyright terms: Public domain | W3C validator |