Theorem eluzelz 9940

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   class class class wbr 4130  ‘cfv 5377   ≤ cle 8361  ℤcz 9648  ℤ_≥cuz 9930

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 4249  ax-pow 4311  ax-pr 4346  ax-cnex 8270  ax-resscn 8271

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 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-fv 5385  df-ov 6088  df-neg 8501  df-z 9649  df-uz 9931

This theorem is used by:  eluzelre  9941  uztrn  9948  uzneg  9950  uzssz  9951  uzss  9952  eluzp1l  9956  eluzaddi  9958  eluzsubi  9959  eluzadd  9960  eluzsub  9961  uzm1  9962  uzin  9964  uzind4  9997  uz2mulcl  10017  elfz5  10430  elfzel2  10436  elfzelz  10438  eluzfz2  10446  peano2fzr  10451  fzsplit2  10465  fzopth  10477  fzsuc  10485  fzspl  10486  elfzp1  10489  fzdifsuc  10498  uzsplit  10509  uzdisj  10510  fzm1  10517  fzneuz  10518  uznfz  10520  nn0disj  10555  elfzo3  10581  fzoss2  10591  fzouzsplit  10598  fzoun  10600  eluzgtdifelfzo  10625  fzosplitsnm1  10637  fzofzp1b  10656  elfzonelfzo  10658  fzosplitsn  10661  fzisfzounsn  10665  zsupcllemstep  10672  infssuzex  10676  infssfzcldc  10679  infssfzledc  10680  suprzubdc  10681  fldiv4lem1div2uz2  10754  mulp1mod1  10815  m1modge3gt1  10821  frec2uzltd  10853  frecfzen2  10877  uzennn  10886  uzsinds  10894  seq3fveq2  10925  seq3feq2  10926  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  monoord  10935  monoord2  10936  ser3mono  10937  seq3split  10938  seqsplitg  10939  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  seq3f1olemqsumk  10962  seq3f1olemp  10965  seq3f1oleml  10966  seq3f1o  10967  seqf1oglem1  10969  seqf1oglem2  10970  seqf1og  10971  seq3id  10975  seq3z  10978  fser0const  10985  leexp2a  11042  expnlbnd2  11116  hashfz  11276  hashfzo  11277  hashfzp1  11279  seq3coll  11308  swrdfv2  11449  pfxccatin12  11519  seq3shft  11617  rexuz3  11770  r19.2uz  11773  cau4  11897  caubnd2  11898  clim  12063  climshft2  12088  climaddc1  12111  climmulc2  12113  climsubc1  12114  climsubc2  12115  clim2ser  12119  clim2ser2  12120  iserex  12121  climlec2  12123  climub  12126  climcau  12129  climcaucn  12133  serf0  12134  sumrbdclem  12160  fsum3cvg  12161  summodclem2a  12164  zsumdc  12167  fsum3  12170  fisumss  12175  fsum3cvg2  12177  fsum3ser  12180  fsumcl2lem  12181  fsumadd  12189  fsumm1  12199  fzosump1  12200  fsum1p  12201  fsump1  12203  fsummulc2  12231  telfsumo  12249  fsumparts  12253  iserabs  12258  binomlem  12266  isumshft  12273  isumsplit  12274  isumrpcl  12277  divcnv  12280  trireciplem  12283  geosergap  12289  geolim2  12295  cvgratnnlemseq  12309  cvgratnnlemabsle  12310  cvgratnnlemsumlt  12311  cvgratnnlemrate  12313  cvgratz  12315  cvgratgt0  12316  mertenslemi1  12318  clim2divap  12323  prodrbdclem  12354  fproddccvg  12355  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodntrivap  12367  fprodssdc  12373  fprodm1  12381  fprod1p  12382  fprodp1  12383  fprodabs  12399  fprodeq0  12400  efgt1p2  12478  modm1div  12583  dvdsbnd  12749  uzwodc  12830  ncoprmgcdne1b  12883  isprm3  12912  prmind2  12914  nprm  12917  dvdsprm  12932  exprmfct  12933  isprm5lem  12936  isprm5  12937  phibndlem  13014  phibnd  13015  dfphi2  13018  hashdvds  13019  pclemdc  13087  pcaddlem  13138  pcmptdvds  13144  pcfac  13149  expnprm  13152  prmlem1  13242  prmlem2  13254  fngzsum  13757  gzsumvalx  13758  gzsumval2  13763  gzsumsplit1r  13764  gzsumshift  14198  plycoeid3  15907  logfac  16048  relogbval  16106  relogbzcl  16107  nnlogbexp  16114  logblt  16117  logbgcd1irr  16122  ppidif  16175  bcmono  16202  bpos1lem  16207  bpos1  16208  lgsne0  16255  gausslemma2dlem4  16281  lgsquad2lem2  16299  2sqlem6  16337  2sqlem8a  16339  2sqlem8  16340  supfz  17219