![]() |
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 6465 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥) | |
2 | uzf 11971 | . . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ | |
3 | 2 | fdmi 6288 | . 2 ⊢ dom ℤ≥ = ℤ |
4 | 1, 3 | syl6eleq 2916 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2164 𝒫 cpw 4378 dom cdm 5342 ‘cfv 6123 ℤcz 11704 ℤ≥cuz 11968 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pow 5065 ax-pr 5127 ax-cnex 10308 ax-resscn 10309 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3or 1112 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-sbc 3663 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-mpt 4953 df-id 5250 df-xp 5348 df-rel 5349 df-cnv 5350 df-co 5351 df-dm 5352 df-rn 5353 df-res 5354 df-ima 5355 df-iota 6086 df-fun 6125 df-fn 6126 df-f 6127 df-fv 6131 df-ov 6908 df-neg 10588 df-z 11705 df-uz 11969 |
This theorem is referenced by: eluz2 11974 uztrn 11985 uzneg 11987 uzss 11989 uz11 11991 eluzadd 11997 subeluzsub 11999 uzm1 12000 uzin 12002 uzind4 12028 uzsupss 12063 elfz5 12627 elfzel1 12634 eluzfz1 12641 fzsplit2 12659 fzopth 12671 ssfzunsn 12680 fzpred 12682 fzpreddisj 12683 uzsplit 12706 uzdisj 12707 fzm1 12714 uznfz 12717 nn0disj 12750 preduz 12756 fzolb 12771 fzoss2 12791 fzouzdisj 12799 fzoun 12800 ige2m2fzo 12826 fzen2 13063 seqp1 13110 seqcl 13115 seqfeq2 13118 seqfveq 13119 seqshft2 13121 seqsplit 13128 seqcaopr3 13130 seqf1olem2a 13133 seqf1olem1 13134 seqf1olem2 13135 seqid 13140 seqhomo 13142 seqz 13143 leexp2a 13210 hashfz 13503 fzsdom2 13504 hashfzo 13505 hashfzp1 13507 seqcoll 13537 rexanuz2 14466 cau4 14473 clim2ser 14762 clim2ser2 14763 climserle 14770 caurcvg 14784 caucvg 14786 fsumcvg 14820 fsumcvg2 14835 fsumsers 14836 fsumm1 14857 fsum1p 14859 fsumrev2 14888 telfsumo 14908 fsumparts 14912 cvgcmp 14922 cvgcmpub 14923 cvgcmpce 14924 isumsplit 14946 clim2prod 14993 clim2div 14994 prodfrec 15000 ntrivcvgtail 15005 fprodcvg 15033 fprodser 15052 fprodm1 15070 fprodeq0 15078 pcaddlem 15963 vdwnnlem2 16071 prmlem0 16178 gsumval2a 17632 telgsumfzs 18740 dvfsumle 24183 dvfsumge 24184 dvfsumabs 24185 coeid3 24395 ulmres 24541 ulmss 24550 chtdif 25297 ppidif 25302 bcmono 25415 axlowdimlem6 26246 inffz 32146 mettrifi 34088 jm2.25 38402 jm2.16nn0 38407 dvgrat 39344 ssinc 40074 ssdec 40075 fzdifsuc2 40315 iuneqfzuzlem 40340 ssuzfz 40355 ioodvbdlimc1lem2 40935 ioodvbdlimc2lem 40937 carageniuncllem1 41522 caratheodorylem1 41527 |
Copyright terms: Public domain | W3C validator |