Theorem eluzel2 12885

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)

Assertion

Ref	Expression
eluzel2	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

Proof of Theorem eluzel2

Step	Hyp	Ref	Expression
1		elfvdm 6919	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
2		uzf 12883	. . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
3	2	fdmi 6721	. 2 ⊢ dom ℤ≥ = ℤ
4	1, 3	eleqtrdi 2875	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  𝒫 cpw 4564  dom cdm 5663  ‘cfv 6540  ℤcz 12608  ℤ_≥cuz 12880

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-cnex 11173  ax-resscn 11174

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422  df-neg 11461  df-z 12609  df-uz 12881

This theorem is used by:  eluz2  12886  uztrn  12898  uzneg  12900  uzss  12903  uz11  12905  eluzadd  12909  subeluzsub  12913  uzm1  12914  uzin  12916  uzind4  12948  uzsupss  12982  elfz5  13562  elfzel1  13569  eluzfz1  13577  fzsplit2  13596  fzopth  13608  ssfzunsn  13617  fzpred  13619  fzpreddisj  13620  uzsplit  13643  uzdisj  13644  fzdif1  13652  fzm1  13654  uznfz  13657  nn0disj  13691  preduz  13697  fzolb  13713  fzoss2  13735  fzouzdisj  13743  fzoun  13744  ige2m2fzo  13776  fzen2  14025  seqp1  14072  seqcl  14078  seqfeq2  14081  seqfveq  14082  seqshft2  14084  seqsplit  14091  seqcaopr3  14093  seqf1olem2a  14096  seqf1olem1  14097  seqf1olem2  14098  seqid  14103  seqhomo  14105  seqz  14106  leexp2a  14228  hashfz  14484  fzsdom2  14485  hashfzo  14486  hashfzp1  14488  seqcoll  14521  rexanuz2  15427  cau4  15434  clim2ser  15732  clim2ser2  15733  climserle  15740  caurcvg  15754  caucvg  15756  fsumcvg  15788  fsumcvg2  15803  fsumsers  15804  fsumm1  15827  fsum1p  15829  fsumrev2  15858  telfsumo  15879  fsumparts  15883  cvgcmp  15893  cvgcmpub  15894  cvgcmpce  15895  isumsplit  15919  clim2prod  15967  clim2div  15968  prodfrec  15974  ntrivcvgtail  15979  fprodcvg  16009  fprodser  16028  fprodm1  16046  fprodeq0  16054  pcaddlem  16972  vdwnnlem2  17080  prmlem0  17189  gsumval2a  18777  telgsumfzs  20105  dvfsumle  26233  dvfsumge  26234  dvfsumabs  26235  coeid3  26450  ulmres  26604  ulmss  26613  chtdif  27375  ppidif  27380  bcmono  27494  axlowdimlem6  29354  inffz  36261  mettrifi  38468  jm2.25  43786  jm2.16nn0  43791  dvgrat  45082  ssinc  45865  ssdec  45866  fzdifsuc2  46089  iuneqfzuzlem  46110  ssuzfz  46125  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  carageniuncllem1  47295  caratheodorylem1  47300