Theorem eluzelz 9946

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   class class class wbr 4131  ‘cfv 5380   ≤ cle 8367  ℤcz 9653  ℤ_≥cuz 9936

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-cnex 8276  ax-resscn 8277

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-mpt 4195  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9654  df-uz 9937

This theorem is used by:  eluzelre  9947  uztrn  9954  uzneg  9956  uzssz  9957  uzss  9958  eluzp1l  9962  eluzaddi  9964  eluzsubi  9965  eluzadd  9966  eluzsub  9967  uzm1  9968  uzin  9970  uzind4  10003  uz2mulcl  10023  elfz5  10436  elfzel2  10442  elfzelz  10444  eluzfz2  10452  peano2fzr  10457  fzsplit2  10471  fzopth  10483  fzsuc  10491  fzspl  10492  elfzp1  10495  fzdifsuc  10504  uzsplit  10515  uzdisj  10516  fzm1  10523  fzneuz  10524  uznfz  10526  nn0disj  10561  elfzo3  10587  fzoss2  10597  fzouzsplit  10604  fzoun  10606  eluzgtdifelfzo  10631  fzosplitsnm1  10643  fzofzp1b  10662  elfzonelfzo  10664  fzosplitsn  10667  fzisfzounsn  10671  zsupcllemstep  10678  infssuzex  10682  infssfzcldc  10685  infssfzledc  10686  suprzubdc  10687  fldiv4lem1div2uz2  10761  mulp1mod1  10822  m1modge3gt1  10828  frec2uzltd  10860  frecfzen2  10884  uzennn  10893  uzsinds  10901  seq3fveq2  10932  seq3feq2  10933  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  monoord  10942  monoord2  10943  ser3mono  10944  seq3split  10945  seqsplitg  10946  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  seq3f1olemqsumk  10969  seq3f1olemp  10972  seq3f1oleml  10973  seq3f1o  10974  seqf1oglem1  10976  seqf1oglem2  10977  seqf1og  10978  seq3id  10982  seq3z  10985  fser0const  10992  leexp2a  11049  expnlbnd2  11123  hashfz  11283  hashfzo  11284  hashfzp1  11286  seq3coll  11315  swrdfv2  11456  pfxccatin12  11526  seq3shft  11624  rexuz3  11777  r19.2uz  11780  cau4  11904  caubnd2  11905  clim  12071  climshft2  12096  climaddc1  12119  climmulc2  12121  climsubc1  12122  climsubc2  12123  clim2ser  12127  clim2ser2  12128  iserex  12129  climlec2  12131  climub  12134  climcau  12137  climcaucn  12141  serf0  12142  sumrbdclem  12168  fsum3cvg  12169  summodclem2a  12172  zsumdc  12175  fsum3  12178  fisumss  12183  fsum3cvg2  12185  fsum3ser  12188  fsumcl2lem  12189  fsumadd  12197  fsumm1  12207  fzosump1  12208  fsum1p  12209  fsump1  12211  fsummulc2  12239  telfsumo  12257  fsumparts  12261  iserabs  12266  binomlem  12274  isumshft  12281  isumsplit  12282  isumrpcl  12285  divcnv  12288  trireciplem  12291  geosergap  12297  geolim2  12303  cvgratnnlemseq  12317  cvgratnnlemabsle  12318  cvgratnnlemsumlt  12319  cvgratnnlemrate  12321  cvgratz  12323  cvgratgt0  12324  mertenslemi1  12326  clim2divap  12331  prodrbdclem  12362  fproddccvg  12363  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodntrivap  12375  fprodssdc  12381  fprodm1  12389  fprod1p  12390  fprodp1  12391  fprodabs  12407  fprodeq0  12408  efgt1p2  12486  modm1div  12591  dvdsbnd  12757  uzwodc  12838  ncoprmgcdne1b  12891  isprm3  12920  prmind2  12922  nprm  12925  dvdsprm  12940  exprmfct  12941  isprm5lem  12944  isprm5  12945  phibndlem  13022  phibnd  13023  dfphi2  13026  hashdvds  13027  pclemdc  13095  pcaddlem  13146  pcmptdvds  13152  pcfac  13157  expnprm  13160  prmlem1  13250  prmlem2  13262  fngzsum  13766  gzsumvalx  13767  gzsumval2  13772  gzsumsplit1r  13773  gzsumshift  14238  plycoeid3  16000  logfac  16143  relogbval  16204  relogbzcl  16205  nnlogbexp  16212  logblt  16215  logbgcd1irr  16220  chtdif  16281  ppidif  16286  prmorcht  16299  chtqub  16313  bcmono  16321  bpos1lem  16326  bpos1  16327  lgsne0  16379  gausslemma2dlem4  16405  lgsquad2lem2  16423  2sqlem6  16461  2sqlem8a  16463  2sqlem8  16464  supfz  17345