Theorem eluzel2 13010

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 6950	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ dom ℤ≥)
2		uzf 13008	. . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
3	2	fdmi 6751	. 2 ⊢ dom ℤ≥ = ℤ
4	1, 3	eleqtrdi 2874	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  𝒫 cpw 4560  dom cdm 5658  ‘cfv 6566  ℤcz 12733  ℤ_≥cuz 13005

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-cnex 11295  ax-resscn 11296

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-neg 11583  df-z 12734  df-uz 13006

This theorem is used by:  eluz2  13011  uztrn  13023  uzneg  13025  uzss  13028  uz11  13030  eluzadd  13034  subeluzsub  13038  uzm1  13039  uzin  13041  uzind4  13073  uzsupss  13107  elfz5  13688  elfzel1  13695  eluzfz1  13704  fzsplit2  13723  fzopth  13735  ssfzunsn  13744  fzpred  13746  fzpreddisj  13747  uzsplit  13770  uzdisj  13771  fzdif1  13779  fzm1  13781  uznfz  13784  nn0disj  13818  preduz  13824  fzolb  13840  fzoss2  13862  fzouzdisj  13870  fzoun  13871  ige2m2fzo  13903  fzen2  14152  seqp1  14199  seqcl  14205  seqfeq2  14208  seqfveq  14209  seqshft2  14211  seqsplit  14218  seqcaopr3  14220  seqf1olem2a  14223  seqf1olem1  14224  seqf1olem2  14225  seqid  14230  seqhomo  14232  seqz  14233  leexp2a  14355  hashfz  14613  fzsdom2  14614  hashfzo  14615  hashfzp1  14617  seqcoll  14650  rexanuz2  15561  cau4  15568  clim2ser  15866  clim2ser2  15867  climserle  15874  caurcvg  15888  caucvg  15890  fsumcvg  15922  fsumcvg2  15937  fsumsers  15938  fsumm1  15961  fsum1p  15963  fsumrev2  15992  telfsumo  16013  fsumparts  16017  cvgcmp  16027  cvgcmpub  16028  cvgcmpce  16029  isumsplit  16053  clim2prod  16101  clim2div  16102  prodfrec  16108  ntrivcvgtail  16113  fprodcvg  16141  fprodser  16160  fprodm1  16178  fprodeq0  16186  pcaddlem  17110  vdwnnlem2  17218  prmlem0  17327  gsumval2a  18924  telgsumfzs  20254  dvfsumle  26396  dvfsumge  26397  dvfsumabs  26398  coeid3  26614  ulmres  26772  ulmss  26781  chtdif  27542  ppidif  27547  bcmono  27661  axlowdimlem6  29582  inffz  36710  mettrifi  38957  jm2.25  44272  jm2.16nn0  44277  dvgrat  45557  ssinc  46375  ssdec  46376  fzdifsuc2  46599  iuneqfzuzlem  46619  ssuzfz  46634  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  carageniuncllem1  47804  caratheodorylem1  47809