Theorem eluzel2 12798

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

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4563  dom cdm 5638  ‘cfv 6511  ℤcz 12529  ℤ_≥cuz 12793

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-cnex 11124  ax-resscn 11125

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530  df-uz 12794

This theorem is referenced by:  eluz2  12799  uztrn  12811  uzneg  12813  uzss  12816  uz11  12818  eluzadd  12822  eluzaddOLD  12828  subeluzsub  12830  uzm1  12831  uzin  12833  uzind4  12865  uzsupss  12899  elfz5  13477  elfzel1  13484  eluzfz1  13492  fzsplit2  13510  fzopth  13522  ssfzunsn  13531  fzpred  13533  fzpreddisj  13534  uzsplit  13557  uzdisj  13558  fzdif1  13566  fzm1  13568  uznfz  13571  nn0disj  13605  preduz  13611  fzolb  13626  fzoss2  13648  fzouzdisj  13656  fzoun  13657  ige2m2fzo  13689  fzen2  13934  seqp1  13981  seqcl  13987  seqfeq2  13990  seqfveq  13991  seqshft2  13993  seqsplit  14000  seqcaopr3  14002  seqf1olem2a  14005  seqf1olem1  14006  seqf1olem2  14007  seqid  14012  seqhomo  14014  seqz  14015  leexp2a  14137  hashfz  14392  fzsdom2  14393  hashfzo  14394  hashfzp1  14396  seqcoll  14429  rexanuz2  15316  cau4  15323  clim2ser  15621  clim2ser2  15622  climserle  15629  caurcvg  15643  caucvg  15645  fsumcvg  15678  fsumcvg2  15693  fsumsers  15694  fsumm1  15717  fsum1p  15719  fsumrev2  15748  telfsumo  15768  fsumparts  15772  cvgcmp  15782  cvgcmpub  15783  cvgcmpce  15784  isumsplit  15806  clim2prod  15854  clim2div  15855  prodfrec  15861  ntrivcvgtail  15866  fprodcvg  15896  fprodser  15915  fprodm1  15933  fprodeq0  15941  pcaddlem  16859  vdwnnlem2  16967  prmlem0  17076  gsumval2a  18612  telgsumfzs  19919  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  coeid3  26145  ulmres  26297  ulmss  26306  chtdif  27068  ppidif  27073  bcmono  27188  axlowdimlem6  28874  inffz  35717  mettrifi  37751  jm2.25  42988  jm2.16nn0  42993  dvgrat  44301  ssinc  45081  ssdec  45082  fzdifsuc2  45308  iuneqfzuzlem  45330  ssuzfz  45345  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  carageniuncllem1  46519  caratheodorylem1  46524