Theorem eluzel2 12805

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

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4566  dom cdm 5641  ‘cfv 6514  ℤcz 12536  ℤ_≥cuz 12800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537  df-uz 12801

This theorem is referenced by:  eluz2  12806  uztrn  12818  uzneg  12820  uzss  12823  uz11  12825  eluzadd  12829  eluzaddOLD  12835  subeluzsub  12837  uzm1  12838  uzin  12840  uzind4  12872  uzsupss  12906  elfz5  13484  elfzel1  13491  eluzfz1  13499  fzsplit2  13517  fzopth  13529  ssfzunsn  13538  fzpred  13540  fzpreddisj  13541  uzsplit  13564  uzdisj  13565  fzdif1  13573  fzm1  13575  uznfz  13578  nn0disj  13612  preduz  13618  fzolb  13633  fzoss2  13655  fzouzdisj  13663  fzoun  13664  ige2m2fzo  13696  fzen2  13941  seqp1  13988  seqcl  13994  seqfeq2  13997  seqfveq  13998  seqshft2  14000  seqsplit  14007  seqcaopr3  14009  seqf1olem2a  14012  seqf1olem1  14013  seqf1olem2  14014  seqid  14019  seqhomo  14021  seqz  14022  leexp2a  14144  hashfz  14399  fzsdom2  14400  hashfzo  14401  hashfzp1  14403  seqcoll  14436  rexanuz2  15323  cau4  15330  clim2ser  15628  clim2ser2  15629  climserle  15636  caurcvg  15650  caucvg  15652  fsumcvg  15685  fsumcvg2  15700  fsumsers  15701  fsumm1  15724  fsum1p  15726  fsumrev2  15755  telfsumo  15775  fsumparts  15779  cvgcmp  15789  cvgcmpub  15790  cvgcmpce  15791  isumsplit  15813  clim2prod  15861  clim2div  15862  prodfrec  15868  ntrivcvgtail  15873  fprodcvg  15903  fprodser  15922  fprodm1  15940  fprodeq0  15948  pcaddlem  16866  vdwnnlem2  16974  prmlem0  17083  gsumval2a  18619  telgsumfzs  19926  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  coeid3  26152  ulmres  26304  ulmss  26313  chtdif  27075  ppidif  27080  bcmono  27195  axlowdimlem6  28881  inffz  35724  mettrifi  37758  jm2.25  42995  jm2.16nn0  43000  dvgrat  44308  ssinc  45088  ssdec  45089  fzdifsuc2  45315  iuneqfzuzlem  45337  ssuzfz  45352  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  carageniuncllem1  46526  caratheodorylem1  46531