Theorem eluzel2 12970

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  𝒫 cpw 4557  dom cdm 5651  ‘cfv 6538  ℤcz 12693  ℤ_≥cuz 12965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-cnex 11256  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694  df-uz 12966

This theorem is used by:  eluz2  12971  uztrn  12983  uzneg  12985  uzss  12988  uz11  12990  eluzadd  12994  subeluzsub  12998  uzm1  12999  uzin  13001  uzind4  13033  uzsupss  13067  elfz5  13648  elfzel1  13655  eluzfz1  13664  fzsplit2  13683  fzopth  13695  ssfzunsn  13704  fzpred  13706  fzpreddisj  13707  uzsplit  13730  uzdisj  13731  fzdif1  13739  fzm1  13741  uznfz  13744  nn0disj  13778  preduz  13784  fzolb  13800  fzoss2  13822  fzouzdisj  13830  fzoun  13831  ige2m2fzo  13863  fzen2  14112  seqp1  14159  seqcl  14165  seqfeq2  14168  seqfveq  14169  seqshft2  14171  seqsplit  14178  seqcaopr3  14180  seqf1olem2a  14183  seqf1olem1  14184  seqf1olem2  14185  seqid  14190  seqhomo  14192  seqz  14193  leexp2a  14315  hashfz  14572  fzsdom2  14573  hashfzo  14574  hashfzp1  14576  seqcoll  14609  rexanuz2  15517  cau4  15524  clim2ser  15822  clim2ser2  15823  climserle  15830  caurcvg  15844  caucvg  15846  fsumcvg  15878  fsumcvg2  15893  fsumsers  15894  fsumm1  15917  fsum1p  15919  fsumrev2  15948  telfsumo  15969  fsumparts  15973  cvgcmp  15983  cvgcmpub  15984  cvgcmpce  15985  isumsplit  16009  clim2prod  16057  clim2div  16058  prodfrec  16064  ntrivcvgtail  16069  fprodcvg  16097  fprodser  16116  fprodm1  16134  fprodeq0  16142  pcaddlem  17066  vdwnnlem2  17174  prmlem0  17283  gsumval2a  18874  telgsumfzs  20203  dvfsumle  26341  dvfsumge  26342  dvfsumabs  26343  coeid3  26559  ulmres  26715  ulmss  26724  chtdif  27485  ppidif  27490  bcmono  27604  axlowdimlem6  29525  inffz  36495  mettrifi  38691  jm2.25  44005  jm2.16nn0  44010  dvgrat  45295  ssinc  46101  ssdec  46102  fzdifsuc2  46325  iuneqfzuzlem  46345  ssuzfz  46360  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  carageniuncllem1  47530  caratheodorylem1  47535