Theorem eluzelz 9881

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzelz	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Proof of Theorem eluzelz

Step	Hyp	Ref	Expression
1		eluz2 9877	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1040	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2205   class class class wbr 4114  ‘cfv 5357   ≤ cle 8325  ℤcz 9594  ℤ_≥cuz 9871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-cnex 8234  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-sbc 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-fv 5365  df-ov 6061  df-neg 8463  df-z 9595  df-uz 9872

This theorem is referenced by:  eluzelre  9882  uztrn  9889  uzneg  9891  uzssz  9892  uzss  9893  eluzp1l  9897  eluzaddi  9899  eluzsubi  9900  eluzadd  9901  eluzsub  9902  uzm1  9903  uzin  9905  uzind4  9938  uz2mulcl  9958  elfz5  10370  elfzel2  10376  elfzelz  10378  eluzfz2  10386  peano2fzr  10391  fzsplit2  10404  fzopth  10416  fzsuc  10424  fzspl  10425  elfzp1  10428  fzdifsuc  10437  uzsplit  10448  uzdisj  10449  fzm1  10456  fzneuz  10457  uznfz  10459  nn0disj  10494  elfzo3  10520  fzoss2  10530  fzouzsplit  10537  fzoun  10539  eluzgtdifelfzo  10564  fzosplitsnm1  10576  fzofzp1b  10595  elfzonelfzo  10597  fzosplitsn  10600  fzisfzounsn  10604  zsupcllemstep  10611  infssuzex  10615  infssfzcldc  10618  infssfzledc  10619  suprzubdc  10620  fldiv4lem1div2uz2  10690  mulp1mod1  10751  m1modge3gt1  10757  frec2uzltd  10789  frecfzen2  10813  uzennn  10822  uzsinds  10830  seq3fveq2  10861  seq3feq2  10862  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  monoord2  10872  ser3mono  10873  seq3split  10874  seqsplitg  10875  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seq3f1olemqsumk  10898  seq3f1olemp  10901  seq3f1oleml  10902  seq3f1o  10903  seqf1oglem1  10905  seqf1oglem2  10906  seqf1og  10907  seq3id  10911  seq3z  10914  fser0const  10921  leexp2a  10978  expnlbnd2  11052  hashfz  11211  hashfzo  11212  hashfzp1  11214  seq3coll  11239  swrdfv2  11380  pfxccatin12  11450  seq3shft  11548  rexuz3  11700  r19.2uz  11703  cau4  11826  caubnd2  11827  clim  11991  climshft2  12016  climaddc1  12039  climmulc2  12041  climsubc1  12042  climsubc2  12043  clim2ser  12047  clim2ser2  12048  iserex  12049  climlec2  12051  climub  12054  climcau  12057  climcaucn  12061  serf0  12062  sumrbdclem  12088  fsum3cvg  12089  summodclem2a  12092  zsumdc  12095  fsum3  12098  fisumss  12103  fsum3cvg2  12105  fsum3ser  12108  fsumcl2lem  12109  fsumadd  12117  fsumm1  12127  fzosump1  12128  fsum1p  12129  fsump1  12131  fsummulc2  12159  telfsumo  12177  fsumparts  12181  iserabs  12186  binomlem  12194  isumshft  12201  isumsplit  12202  isumrpcl  12205  divcnv  12208  trireciplem  12211  geosergap  12217  geolim2  12223  cvgratnnlemseq  12237  cvgratnnlemabsle  12238  cvgratnnlemsumlt  12239  cvgratnnlemrate  12241  cvgratz  12243  cvgratgt0  12244  mertenslemi1  12246  clim2divap  12251  prodrbdclem  12282  fproddccvg  12283  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodntrivap  12295  fprodssdc  12301  fprodm1  12309  fprod1p  12310  fprodp1  12311  fprodabs  12327  fprodeq0  12328  efgt1p2  12406  modm1div  12511  dvdsbnd  12677  uzwodc  12758  ncoprmgcdne1b  12811  isprm3  12840  prmind2  12842  nprm  12845  dvdsprm  12859  exprmfct  12860  isprm5lem  12863  isprm5  12864  phibndlem  12938  phibnd  12939  dfphi2  12942  hashdvds  12943  pclemdc  13011  pcaddlem  13062  pcmptdvds  13068  pcfac  13073  expnprm  13076  fngsum  13651  igsumvalx  13652  gsumval2  13660  gsumsplit1r  13661  gsumfzz  13750  gsumshift  14105  plycoeid3  15748  relogbval  15942  relogbzcl  15943  nnlogbexp  15950  logblt  15953  logbgcd1irr  15958  lgsne0  16037  gausslemma2dlem4  16063  lgsquad2lem2  16081  2sqlem6  16119  2sqlem8a  16121  2sqlem8  16122  supfz  16983