Theorem eluzelz 9770

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 9766	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1039	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2201   class class class wbr 4089  ‘cfv 5328   ≤ cle 8220  ℤcz 9484  ℤ_≥cuz 9760

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-cnex 8128  ax-resscn 8129

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-rab 2518  df-v 2803  df-sbc 3031  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-opab 4152  df-mpt 4153  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-fv 5336  df-ov 6026  df-neg 8358  df-z 9485  df-uz 9761

This theorem is referenced by:  eluzelre  9771  uztrn  9778  uzneg  9780  uzssz  9781  uzss  9782  eluzp1l  9786  eluzaddi  9788  eluzsubi  9789  eluzadd  9790  eluzsub  9791  uzm1  9792  uzin  9794  uzind4  9827  uz2mulcl  9847  elfz5  10257  elfzel2  10263  elfzelz  10265  eluzfz2  10272  peano2fzr  10277  fzsplit2  10290  fzopth  10301  fzsuc  10309  elfzp1  10312  fzdifsuc  10321  uzsplit  10332  uzdisj  10333  fzm1  10340  fzneuz  10341  uznfz  10343  nn0disj  10378  elfzo3  10404  fzoss2  10414  fzouzsplit  10421  fzoun  10423  eluzgtdifelfzo  10448  fzosplitsnm1  10460  fzofzp1b  10479  elfzonelfzo  10481  fzosplitsn  10484  fzisfzounsn  10488  zsupcllemstep  10495  infssuzex  10499  suprzubdc  10502  fldiv4lem1div2uz2  10572  mulp1mod1  10633  m1modge3gt1  10639  frec2uzltd  10671  frecfzen2  10695  uzennn  10704  uzsinds  10712  seq3fveq2  10743  seq3feq2  10744  seqfveq2g  10745  seq3shft2  10749  seqshft2g  10750  monoord  10753  monoord2  10754  ser3mono  10755  seq3split  10756  seqsplitg  10757  iseqf1olemjpcl  10776  iseqf1olemqpcl  10777  seq3f1olemqsumk  10780  seq3f1olemp  10783  seq3f1oleml  10784  seq3f1o  10785  seqf1oglem1  10787  seqf1oglem2  10788  seqf1og  10789  seq3id  10793  seq3z  10796  fser0const  10803  leexp2a  10860  expnlbnd2  10933  hashfz  11091  hashfzo  11092  hashfzp1  11094  seq3coll  11112  swrdfv2  11253  pfxccatin12  11323  seq3shft  11421  rexuz3  11573  r19.2uz  11576  cau4  11699  caubnd2  11700  clim  11864  climshft2  11889  climaddc1  11912  climmulc2  11914  climsubc1  11915  climsubc2  11916  clim2ser  11920  clim2ser2  11921  iserex  11922  climlec2  11924  climub  11927  climcau  11930  climcaucn  11934  serf0  11935  sumrbdclem  11961  fsum3cvg  11962  summodclem2a  11965  zsumdc  11968  fsum3  11971  fisumss  11976  fsum3cvg2  11978  fsum3ser  11981  fsumcl2lem  11982  fsumadd  11990  fsumm1  12000  fzosump1  12001  fsum1p  12002  fsump1  12004  fsummulc2  12032  telfsumo  12050  fsumparts  12054  iserabs  12059  binomlem  12067  isumshft  12074  isumsplit  12075  isumrpcl  12078  divcnv  12081  trireciplem  12084  geosergap  12090  geolim2  12096  cvgratnnlemseq  12110  cvgratnnlemabsle  12111  cvgratnnlemsumlt  12112  cvgratnnlemrate  12114  cvgratz  12116  cvgratgt0  12117  mertenslemi1  12119  clim2divap  12124  prodrbdclem  12155  fproddccvg  12156  prodmodclem3  12159  prodmodclem2a  12160  zproddc  12163  fprodntrivap  12168  fprodssdc  12174  fprodm1  12182  fprod1p  12183  fprodp1  12184  fprodabs  12200  fprodeq0  12201  efgt1p2  12279  modm1div  12384  dvdsbnd  12550  uzwodc  12631  ncoprmgcdne1b  12684  isprm3  12713  prmind2  12715  nprm  12718  dvdsprm  12732  exprmfct  12733  isprm5lem  12736  isprm5  12737  phibndlem  12811  phibnd  12812  dfphi2  12815  hashdvds  12816  pclemdc  12884  pcaddlem  12935  pcmptdvds  12941  pcfac  12946  expnprm  12949  fngsum  13494  igsumvalx  13495  gsumval2  13503  gsumsplit1r  13504  gsumfzz  13601  plycoeid3  15510  relogbval  15704  relogbzcl  15705  nnlogbexp  15712  logblt  15715  logbgcd1irr  15720  lgsne0  15796  gausslemma2dlem4  15822  lgsquad2lem2  15840  2sqlem6  15878  2sqlem8a  15880  2sqlem8  15881  supfz  16743  gsumgfsumlem  16751