Theorem eluzelz 9941

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

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

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 8271  ax-resscn 8272

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 8502  df-z 9650  df-uz 9932

This theorem is used by:  eluzelre  9942  uztrn  9949  uzneg  9951  uzssz  9952  uzss  9953  eluzp1l  9957  eluzaddi  9959  eluzsubi  9960  eluzadd  9961  eluzsub  9962  uzm1  9963  uzin  9965  uzind4  9998  uz2mulcl  10018  elfz5  10431  elfzel2  10437  elfzelz  10439  eluzfz2  10447  peano2fzr  10452  fzsplit2  10466  fzopth  10478  fzsuc  10486  fzspl  10487  elfzp1  10490  fzdifsuc  10499  uzsplit  10510  uzdisj  10511  fzm1  10518  fzneuz  10519  uznfz  10521  nn0disj  10556  elfzo3  10582  fzoss2  10592  fzouzsplit  10599  fzoun  10601  eluzgtdifelfzo  10626  fzosplitsnm1  10638  fzofzp1b  10657  elfzonelfzo  10659  fzosplitsn  10662  fzisfzounsn  10666  zsupcllemstep  10673  infssuzex  10677  infssfzcldc  10680  infssfzledc  10681  suprzubdc  10682  fldiv4lem1div2uz2  10756  mulp1mod1  10817  m1modge3gt1  10823  frec2uzltd  10855  frecfzen2  10879  uzennn  10888  uzsinds  10896  seq3fveq2  10927  seq3feq2  10928  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  monoord2  10938  ser3mono  10939  seq3split  10940  seqsplitg  10941  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  seq3f1olemqsumk  10964  seq3f1olemp  10967  seq3f1oleml  10968  seq3f1o  10969  seqf1oglem1  10971  seqf1oglem2  10972  seqf1og  10973  seq3id  10977  seq3z  10980  fser0const  10987  leexp2a  11044  expnlbnd2  11118  hashfz  11278  hashfzo  11279  hashfzp1  11281  seq3coll  11310  swrdfv2  11451  pfxccatin12  11521  seq3shft  11619  rexuz3  11772  r19.2uz  11775  cau4  11899  caubnd2  11900  clim  12066  climshft2  12091  climaddc1  12114  climmulc2  12116  climsubc1  12117  climsubc2  12118  clim2ser  12122  clim2ser2  12123  iserex  12124  climlec2  12126  climub  12129  climcau  12132  climcaucn  12136  serf0  12137  sumrbdclem  12163  fsum3cvg  12164  summodclem2a  12167  zsumdc  12170  fsum3  12173  fisumss  12178  fsum3cvg2  12180  fsum3ser  12183  fsumcl2lem  12184  fsumadd  12192  fsumm1  12202  fzosump1  12203  fsum1p  12204  fsump1  12206  fsummulc2  12234  telfsumo  12252  fsumparts  12256  iserabs  12261  binomlem  12269  isumshft  12276  isumsplit  12277  isumrpcl  12280  divcnv  12283  trireciplem  12286  geosergap  12292  geolim2  12298  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratnnlemrate  12316  cvgratz  12318  cvgratgt0  12319  mertenslemi1  12321  clim2divap  12326  prodrbdclem  12357  fproddccvg  12358  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodntrivap  12370  fprodssdc  12376  fprodm1  12384  fprod1p  12385  fprodp1  12386  fprodabs  12402  fprodeq0  12403  efgt1p2  12481  modm1div  12586  dvdsbnd  12752  uzwodc  12833  ncoprmgcdne1b  12886  isprm3  12915  prmind2  12917  nprm  12920  dvdsprm  12935  exprmfct  12936  isprm5lem  12939  isprm5  12940  phibndlem  13017  phibnd  13018  dfphi2  13021  hashdvds  13022  pclemdc  13090  pcaddlem  13141  pcmptdvds  13147  pcfac  13152  expnprm  13155  prmlem1  13245  prmlem2  13257  fngzsum  13761  gzsumvalx  13762  gzsumval2  13767  gzsumsplit1r  13768  gzsumshift  14233  plycoeid3  15949  logfac  16090  relogbval  16148  relogbzcl  16149  nnlogbexp  16156  logblt  16159  logbgcd1irr  16164  chtdif  16225  ppidif  16230  prmorcht  16243  chtqub  16257  bcmono  16265  bpos1lem  16270  bpos1  16271  lgsne0  16323  gausslemma2dlem4  16349  lgsquad2lem2  16367  2sqlem6  16405  2sqlem8a  16407  2sqlem8  16408  supfz  17288