Theorem eluzel2 12980

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 12978	. . 3 ⊢ ℤ≥:ℤ⟶𝒫 ℤ
3	2	fdmi 6729	. 2 ⊢ dom ℤ≥ = ℤ
4	1, 3	eleqtrdi 2873	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  𝒫 cpw 4559  dom cdm 5654  ‘cfv 6546  ℤcz 12703  ℤ_≥cuz 12975

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-cnex 11266  ax-resscn 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7430  df-neg 11554  df-z 12704  df-uz 12976

This theorem is used by:  eluz2  12981  uztrn  12993  uzneg  12995  uzss  12998  uz11  13000  eluzadd  13004  subeluzsub  13008  uzm1  13009  uzin  13011  uzind4  13043  uzsupss  13077  elfz5  13658  elfzel1  13665  eluzfz1  13674  fzsplit2  13693  fzopth  13705  ssfzunsn  13714  fzpred  13716  fzpreddisj  13717  uzsplit  13740  uzdisj  13741  fzdif1  13749  fzm1  13751  uznfz  13754  nn0disj  13788  preduz  13794  fzolb  13810  fzoss2  13832  fzouzdisj  13840  fzoun  13841  ige2m2fzo  13873  fzen2  14122  seqp1  14169  seqcl  14175  seqfeq2  14178  seqfveq  14179  seqshft2  14181  seqsplit  14188  seqcaopr3  14190  seqf1olem2a  14193  seqf1olem1  14194  seqf1olem2  14195  seqid  14200  seqhomo  14202  seqz  14203  leexp2a  14325  hashfz  14582  fzsdom2  14583  hashfzo  14584  hashfzp1  14586  seqcoll  14619  rexanuz2  15529  cau4  15536  clim2ser  15834  clim2ser2  15835  climserle  15842  caurcvg  15856  caucvg  15858  fsumcvg  15890  fsumcvg2  15905  fsumsers  15906  fsumm1  15929  fsum1p  15931  fsumrev2  15960  telfsumo  15981  fsumparts  15985  cvgcmp  15995  cvgcmpub  15996  cvgcmpce  15997  isumsplit  16021  clim2prod  16069  clim2div  16070  prodfrec  16076  ntrivcvgtail  16081  fprodcvg  16109  fprodser  16128  fprodm1  16146  fprodeq0  16154  pcaddlem  17078  vdwnnlem2  17186  prmlem0  17295  gsumval2a  18886  telgsumfzs  20215  dvfsumle  26353  dvfsumge  26354  dvfsumabs  26355  coeid3  26571  ulmres  26727  ulmss  26736  chtdif  27497  ppidif  27502  bcmono  27616  axlowdimlem6  29537  inffz  36622  mettrifi  38831  jm2.25  44146  jm2.16nn0  44151  dvgrat  45436  ssinc  46241  ssdec  46242  fzdifsuc2  46465  iuneqfzuzlem  46485  ssuzfz  46500  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  carageniuncllem1  47670  caratheodorylem1  47675