Theorem eluzel2 12844

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

Syntax hints:   → wi 4   ∈ wcel 2142  𝒫 cpw 4555  dom cdm 5647  ‘cfv 6521  ℤcz 12568  ℤ_≥cuz 12839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-neg 11417  df-z 12569  df-uz 12840

This theorem is referenced by:  eluz2  12845  uztrn  12857  uzneg  12859  uzss  12862  uz11  12864  eluzadd  12868  subeluzsub  12872  uzm1  12873  uzin  12875  uzind4  12907  uzsupss  12941  elfz5  13521  elfzel1  13528  eluzfz1  13536  fzsplit2  13554  fzopth  13566  ssfzunsn  13575  fzpred  13577  fzpreddisj  13578  uzsplit  13601  uzdisj  13602  fzdif1  13610  fzm1  13612  uznfz  13615  nn0disj  13649  preduz  13655  fzolb  13671  fzoss2  13693  fzouzdisj  13701  fzoun  13702  ige2m2fzo  13734  fzen2  13982  seqp1  14029  seqcl  14035  seqfeq2  14038  seqfveq  14039  seqshft2  14041  seqsplit  14048  seqcaopr3  14050  seqf1olem2a  14053  seqf1olem1  14054  seqf1olem2  14055  seqid  14060  seqhomo  14062  seqz  14063  leexp2a  14185  hashfz  14440  fzsdom2  14441  hashfzo  14442  hashfzp1  14444  seqcoll  14477  rexanuz2  15377  cau4  15384  clim2ser  15682  clim2ser2  15683  climserle  15690  caurcvg  15704  caucvg  15706  fsumcvg  15739  fsumcvg2  15754  fsumsers  15755  fsumm1  15778  fsum1p  15780  fsumrev2  15809  telfsumo  15830  fsumparts  15834  cvgcmp  15844  cvgcmpub  15845  cvgcmpce  15846  isumsplit  15870  clim2prod  15918  clim2div  15919  prodfrec  15925  ntrivcvgtail  15930  fprodcvg  15960  fprodser  15979  fprodm1  15997  fprodeq0  16005  pcaddlem  16924  vdwnnlem2  17032  prmlem0  17141  gsumval2a  18719  telgsumfzs  20029  dvfsumle  26083  dvfsumge  26084  dvfsumabs  26085  coeid3  26300  ulmres  26451  ulmss  26460  chtdif  27222  ppidif  27227  bcmono  27341  axlowdimlem6  29148  inffz  36080  mettrifi  38256  jm2.25  43576  jm2.16nn0  43581  dvgrat  44888  ssinc  45665  ssdec  45666  fzdifsuc2  45889  iuneqfzuzlem  45910  ssuzfz  45925  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  carageniuncllem1  47095  caratheodorylem1  47100