Theorem eluzel2 12768

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

Syntax hints:   → wi 4   ∈ wcel 2114  𝒫 cpw 4556  dom cdm 5632  ‘cfv 6500  ℤcz 12500  ℤ_≥cuz 12763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501  df-uz 12764

This theorem is referenced by:  eluz2  12769  uztrn  12781  uzneg  12783  uzss  12786  uz11  12788  eluzadd  12792  subeluzsub  12796  uzm1  12797  uzin  12799  uzind4  12831  uzsupss  12865  elfz5  13444  elfzel1  13451  eluzfz1  13459  fzsplit2  13477  fzopth  13489  ssfzunsn  13498  fzpred  13500  fzpreddisj  13501  uzsplit  13524  uzdisj  13525  fzdif1  13533  fzm1  13535  uznfz  13538  nn0disj  13572  preduz  13578  fzolb  13593  fzoss2  13615  fzouzdisj  13623  fzoun  13624  ige2m2fzo  13656  fzen2  13904  seqp1  13951  seqcl  13957  seqfeq2  13960  seqfveq  13961  seqshft2  13963  seqsplit  13970  seqcaopr3  13972  seqf1olem2a  13975  seqf1olem1  13976  seqf1olem2  13977  seqid  13982  seqhomo  13984  seqz  13985  leexp2a  14107  hashfz  14362  fzsdom2  14363  hashfzo  14364  hashfzp1  14366  seqcoll  14399  rexanuz2  15285  cau4  15292  clim2ser  15590  clim2ser2  15591  climserle  15598  caurcvg  15612  caucvg  15614  fsumcvg  15647  fsumcvg2  15662  fsumsers  15663  fsumm1  15686  fsum1p  15688  fsumrev2  15717  telfsumo  15737  fsumparts  15741  cvgcmp  15751  cvgcmpub  15752  cvgcmpce  15753  isumsplit  15775  clim2prod  15823  clim2div  15824  prodfrec  15830  ntrivcvgtail  15835  fprodcvg  15865  fprodser  15884  fprodm1  15902  fprodeq0  15910  pcaddlem  16828  vdwnnlem2  16936  prmlem0  17045  gsumval2a  18622  telgsumfzs  19933  dvfsumle  25997  dvfsumleOLD  25998  dvfsumge  25999  dvfsumabs  26000  coeid3  26216  ulmres  26368  ulmss  26377  chtdif  27139  ppidif  27144  bcmono  27259  axlowdimlem6  29036  inffz  35950  mettrifi  38012  jm2.25  43360  jm2.16nn0  43365  dvgrat  44672  ssinc  45450  ssdec  45451  fzdifsuc2  45676  iuneqfzuzlem  45697  ssuzfz  45712  ioodvbdlimc1lem2  46294  ioodvbdlimc2lem  46296  carageniuncllem1  46883  caratheodorylem1  46888