Theorem eluzel2 12867

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

Syntax hints:   → wi 4   ∈ wcel 2149  𝒫 cpw 4567  dom cdm 5662  ‘cfv 6537  ℤcz 12591  ℤ_≥cuz 12862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-cnex 11156  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-neg 11444  df-z 12592  df-uz 12863

This theorem is referenced by:  eluz2  12868  uztrn  12880  uzneg  12882  uzss  12885  uz11  12887  eluzadd  12891  subeluzsub  12895  uzm1  12896  uzin  12898  uzind4  12930  uzsupss  12964  elfz5  13544  elfzel1  13551  eluzfz1  13559  fzsplit2  13577  fzopth  13589  ssfzunsn  13598  fzpred  13600  fzpreddisj  13601  uzsplit  13624  uzdisj  13625  fzdif1  13633  fzm1  13635  uznfz  13638  nn0disj  13672  preduz  13678  fzolb  13694  fzoss2  13716  fzouzdisj  13724  fzoun  13725  ige2m2fzo  13757  fzen2  14005  seqp1  14052  seqcl  14058  seqfeq2  14061  seqfveq  14062  seqshft2  14064  seqsplit  14071  seqcaopr3  14073  seqf1olem2a  14076  seqf1olem1  14077  seqf1olem2  14078  seqid  14083  seqhomo  14085  seqz  14086  leexp2a  14208  hashfz  14464  fzsdom2  14465  hashfzo  14466  hashfzp1  14468  seqcoll  14501  rexanuz2  15401  cau4  15408  clim2ser  15706  clim2ser2  15707  climserle  15714  caurcvg  15728  caucvg  15730  fsumcvg  15763  fsumcvg2  15778  fsumsers  15779  fsumm1  15802  fsum1p  15804  fsumrev2  15833  telfsumo  15854  fsumparts  15858  cvgcmp  15868  cvgcmpub  15869  cvgcmpce  15870  isumsplit  15894  clim2prod  15942  clim2div  15943  prodfrec  15949  ntrivcvgtail  15954  fprodcvg  15984  fprodser  16003  fprodm1  16021  fprodeq0  16029  pcaddlem  16948  vdwnnlem2  17056  prmlem0  17165  gsumval2a  18743  telgsumfzs  20059  dvfsumle  26149  dvfsumge  26150  dvfsumabs  26151  coeid3  26366  ulmres  26517  ulmss  26526  chtdif  27288  ppidif  27293  bcmono  27407  axlowdimlem6  29238  inffz  36121  mettrifi  38296  jm2.25  43618  jm2.16nn0  43623  dvgrat  44914  ssinc  45697  ssdec  45698  fzdifsuc2  45921  iuneqfzuzlem  45942  ssuzfz  45957  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  carageniuncllem1  47127  caratheodorylem1  47132