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 6130 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥) | |
2 | uzf 11566 | . . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
3 | 2 | fdmi 5965 | . 2 ⊢ dom ℤ≥ = ℤ |
4 | 1, 3 | syl6eleq 2698 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 𝒫 cpw 4108 dom cdm 5038 ‘cfv 5804 ℤcz 11254 ℤ≥cuz 11563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-cnex 9871 ax-resscn 9872 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-fv 5812 df-ov 6552 df-neg 10148 df-z 11255 df-uz 11564 |
This theorem is referenced by: eluz2 11569 uztrn 11580 uzneg 11582 uzss 11584 uz11 11586 eluzadd 11592 uzm1 11594 uzin 11596 uzind4 11622 uzsupss 11656 elfz5 12205 elfzel1 12212 eluzfz1 12219 fzsplit2 12237 fzopth 12249 ssfzunsn 12257 fzpred 12259 fzpreddisj 12260 uzsplit 12281 uzdisj 12282 fzm1 12289 uznfz 12292 nn0disj 12324 preduz 12330 fzolb 12345 fzoss2 12365 fzouzdisj 12373 ige2m2fzo 12398 fzen2 12630 seqp1 12678 seqcl 12683 seqfeq2 12686 seqfveq 12687 seqshft2 12689 seqsplit 12696 seqcaopr3 12698 seqf1olem2a 12701 seqf1olem1 12702 seqf1olem2 12703 seqid 12708 seqhomo 12710 seqz 12711 leexp2a 12778 hashfz 13074 fzsdom2 13075 hashfzo 13076 hashfzp1 13078 seqcoll 13105 rexanuz2 13937 cau4 13944 clim2ser 14233 clim2ser2 14234 climserle 14241 caurcvg 14255 caucvg 14257 fsumcvg 14290 fsumcvg2 14305 fsumsers 14306 fsumm1 14324 fsum1p 14326 fsumrev2 14356 telfsumo 14375 fsumparts 14379 cvgcmp 14389 cvgcmpub 14390 cvgcmpce 14391 isumsplit 14411 clim2prod 14459 clim2div 14460 prodfrec 14466 ntrivcvgtail 14471 fprodcvg 14499 fprodser 14518 fprodm1 14536 fprodeq0 14544 pcaddlem 15430 vdwnnlem2 15538 prmlem0 15650 gsumval2a 17102 telgsumfzs 18209 dvfsumle 23588 dvfsumge 23589 dvfsumabs 23590 coeid3 23800 ulmres 23946 ulmss 23955 chtdif 24684 ppidif 24689 bcmono 24802 axlowdimlem6 25627 extwwlkfablem2 26605 inffz 30867 inffzOLD 30868 mettrifi 32723 jm2.25 36584 jm2.16nn0 36589 dvgrat 37533 ssinc 38292 ssdec 38293 fzdifsuc2 38466 iuneqfzuzlem 38491 ssuzfz 38506 ioodvbdlimc1lem2 38822 ioodvbdlimc2lem 38824 carageniuncllem1 39411 caratheodorylem1 39416 av-extwwlkfablem2 41510 |
Copyright terms: Public domain | W3C validator |