Theorem eluzelz 9765

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

Syntax hints:   → wi 4   ∈ wcel 2202   class class class wbr 4088  ‘cfv 5326   ≤ cle 8215  ℤcz 9479  ℤ_≥cuz 9755

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 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-cnex 8123  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480  df-uz 9756

This theorem is referenced by:  eluzelre  9766  uztrn  9773  uzneg  9775  uzssz  9776  uzss  9777  eluzp1l  9781  eluzaddi  9783  eluzsubi  9784  eluzadd  9785  eluzsub  9786  uzm1  9787  uzin  9789  uzind4  9822  uz2mulcl  9842  elfz5  10252  elfzel2  10258  elfzelz  10260  eluzfz2  10267  peano2fzr  10272  fzsplit2  10285  fzopth  10296  fzsuc  10304  elfzp1  10307  fzdifsuc  10316  uzsplit  10327  uzdisj  10328  fzm1  10335  fzneuz  10336  uznfz  10338  nn0disj  10373  elfzo3  10399  fzoss2  10409  fzouzsplit  10416  fzoun  10418  eluzgtdifelfzo  10443  fzosplitsnm1  10455  fzofzp1b  10474  elfzonelfzo  10476  fzosplitsn  10479  fzisfzounsn  10483  zsupcllemstep  10490  infssuzex  10494  suprzubdc  10497  fldiv4lem1div2uz2  10567  mulp1mod1  10628  m1modge3gt1  10634  frec2uzltd  10666  frecfzen2  10690  uzennn  10699  uzsinds  10707  seq3fveq2  10738  seq3feq2  10739  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seq3f1olemqsumk  10775  seq3f1olemp  10778  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  seq3id  10788  seq3z  10791  fser0const  10798  leexp2a  10855  expnlbnd2  10928  hashfz  11086  hashfzo  11087  hashfzp1  11089  seq3coll  11107  swrdfv2  11248  pfxccatin12  11318  seq3shft  11403  rexuz3  11555  r19.2uz  11558  cau4  11681  caubnd2  11682  clim  11846  climshft2  11871  climaddc1  11894  climmulc2  11896  climsubc1  11897  climsubc2  11898  clim2ser  11902  clim2ser2  11903  iserex  11904  climlec2  11906  climub  11909  climcau  11912  climcaucn  11916  serf0  11917  sumrbdclem  11943  fsum3cvg  11944  summodclem2a  11947  zsumdc  11950  fsum3  11953  fisumss  11958  fsum3cvg2  11960  fsum3ser  11963  fsumcl2lem  11964  fsumadd  11972  fsumm1  11982  fzosump1  11983  fsum1p  11984  fsump1  11986  fsummulc2  12014  telfsumo  12032  fsumparts  12036  iserabs  12041  binomlem  12049  isumshft  12056  isumsplit  12057  isumrpcl  12060  divcnv  12063  trireciplem  12066  geosergap  12072  geolim2  12078  cvgratnnlemseq  12092  cvgratnnlemabsle  12093  cvgratnnlemsumlt  12094  cvgratnnlemrate  12096  cvgratz  12098  cvgratgt0  12099  mertenslemi1  12101  clim2divap  12106  prodrbdclem  12137  fproddccvg  12138  prodmodclem3  12141  prodmodclem2a  12142  zproddc  12145  fprodntrivap  12150  fprodssdc  12156  fprodm1  12164  fprod1p  12165  fprodp1  12166  fprodabs  12182  fprodeq0  12183  efgt1p2  12261  modm1div  12366  dvdsbnd  12532  uzwodc  12613  ncoprmgcdne1b  12666  isprm3  12695  prmind2  12697  nprm  12700  dvdsprm  12714  exprmfct  12715  isprm5lem  12718  isprm5  12719  phibndlem  12793  phibnd  12794  dfphi2  12797  hashdvds  12798  pclemdc  12866  pcaddlem  12917  pcmptdvds  12923  pcfac  12928  expnprm  12931  fngsum  13476  igsumvalx  13477  gsumval2  13485  gsumsplit1r  13486  gsumfzz  13583  plycoeid3  15487  relogbval  15681  relogbzcl  15682  nnlogbexp  15689  logblt  15692  logbgcd1irr  15697  lgsne0  15773  gausslemma2dlem4  15799  lgsquad2lem2  15817  2sqlem6  15855  2sqlem8a  15857  2sqlem8  15858  supfz  16702  gsumgfsumlem  16710