Theorem eluzel2 12831

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

Syntax hints:   → wi 4   ∈ wcel 2104  𝒫 cpw 4601  dom cdm 5675  ‘cfv 6542  ℤcz 12562  ℤ_≥cuz 12826

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-cnex 11168  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7414  df-neg 11451  df-z 12563  df-uz 12827

This theorem is referenced by:  eluz2  12832  uztrn  12844  uzneg  12846  uzss  12849  uz11  12851  eluzadd  12855  eluzaddOLD  12861  subeluzsub  12863  uzm1  12864  uzin  12866  uzind4  12894  uzsupss  12928  elfz5  13497  elfzel1  13504  eluzfz1  13512  fzsplit2  13530  fzopth  13542  ssfzunsn  13551  fzpred  13553  fzpreddisj  13554  uzsplit  13577  uzdisj  13578  fzm1  13585  uznfz  13588  nn0disj  13621  preduz  13627  fzolb  13642  fzoss2  13664  fzouzdisj  13672  fzoun  13673  ige2m2fzo  13699  fzen2  13938  seqp1  13985  seqcl  13992  seqfeq2  13995  seqfveq  13996  seqshft2  13998  seqsplit  14005  seqcaopr3  14007  seqf1olem2a  14010  seqf1olem1  14011  seqf1olem2  14012  seqid  14017  seqhomo  14019  seqz  14020  leexp2a  14141  hashfz  14391  fzsdom2  14392  hashfzo  14393  hashfzp1  14395  seqcoll  14429  rexanuz2  15300  cau4  15307  clim2ser  15605  clim2ser2  15606  climserle  15613  caurcvg  15627  caucvg  15629  fsumcvg  15662  fsumcvg2  15677  fsumsers  15678  fsumm1  15701  fsum1p  15703  fsumrev2  15732  telfsumo  15752  fsumparts  15756  cvgcmp  15766  cvgcmpub  15767  cvgcmpce  15768  isumsplit  15790  clim2prod  15838  clim2div  15839  prodfrec  15845  ntrivcvgtail  15850  fprodcvg  15878  fprodser  15897  fprodm1  15915  fprodeq0  15923  pcaddlem  16825  vdwnnlem2  16933  prmlem0  17043  gsumval2a  18610  telgsumfzs  19898  dvfsumle  25773  dvfsumge  25774  dvfsumabs  25775  coeid3  25989  ulmres  26136  ulmss  26145  chtdif  26898  ppidif  26903  bcmono  27016  axlowdimlem6  28472  inffz  35003  gg-dvfsumle  35468  mettrifi  36928  jm2.25  42040  jm2.16nn0  42045  dvgrat  43373  ssinc  44077  ssdec  44078  fzdifsuc2  44318  iuneqfzuzlem  44342  ssuzfz  44357  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  carageniuncllem1  45535  caratheodorylem1  45540