Theorem eluzelz 9809

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

Syntax hints:   → wi 4   ∈ wcel 2202   class class class wbr 4093  ‘cfv 5333   ≤ cle 8257  ℤcz 9523  ℤ_≥cuz 9799

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-cnex 8166  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341  df-ov 6031  df-neg 8395  df-z 9524  df-uz 9800

This theorem is referenced by:  eluzelre  9810  uztrn  9817  uzneg  9819  uzssz  9820  uzss  9821  eluzp1l  9825  eluzaddi  9827  eluzsubi  9828  eluzadd  9829  eluzsub  9830  uzm1  9831  uzin  9833  uzind4  9866  uz2mulcl  9886  elfz5  10297  elfzel2  10303  elfzelz  10305  eluzfz2  10312  peano2fzr  10317  fzsplit2  10330  fzopth  10341  fzsuc  10349  elfzp1  10352  fzdifsuc  10361  uzsplit  10372  uzdisj  10373  fzm1  10380  fzneuz  10381  uznfz  10383  nn0disj  10418  elfzo3  10444  fzoss2  10454  fzouzsplit  10461  fzoun  10463  eluzgtdifelfzo  10488  fzosplitsnm1  10500  fzofzp1b  10519  elfzonelfzo  10521  fzosplitsn  10524  fzisfzounsn  10528  zsupcllemstep  10535  infssuzex  10539  suprzubdc  10542  fldiv4lem1div2uz2  10612  mulp1mod1  10673  m1modge3gt1  10679  frec2uzltd  10711  frecfzen2  10735  uzennn  10744  uzsinds  10752  seq3fveq2  10783  seq3feq2  10784  seqfveq2g  10785  seq3shft2  10789  seqshft2g  10790  monoord  10793  monoord2  10794  ser3mono  10795  seq3split  10796  seqsplitg  10797  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  seq3f1olemqsumk  10820  seq3f1olemp  10823  seq3f1oleml  10824  seq3f1o  10825  seqf1oglem1  10827  seqf1oglem2  10828  seqf1og  10829  seq3id  10833  seq3z  10836  fser0const  10843  leexp2a  10900  expnlbnd2  10973  hashfz  11131  hashfzo  11132  hashfzp1  11134  seq3coll  11152  swrdfv2  11293  pfxccatin12  11363  seq3shft  11461  rexuz3  11613  r19.2uz  11616  cau4  11739  caubnd2  11740  clim  11904  climshft2  11929  climaddc1  11952  climmulc2  11954  climsubc1  11955  climsubc2  11956  clim2ser  11960  clim2ser2  11961  iserex  11962  climlec2  11964  climub  11967  climcau  11970  climcaucn  11974  serf0  11975  sumrbdclem  12001  fsum3cvg  12002  summodclem2a  12005  zsumdc  12008  fsum3  12011  fisumss  12016  fsum3cvg2  12018  fsum3ser  12021  fsumcl2lem  12022  fsumadd  12030  fsumm1  12040  fzosump1  12041  fsum1p  12042  fsump1  12044  fsummulc2  12072  telfsumo  12090  fsumparts  12094  iserabs  12099  binomlem  12107  isumshft  12114  isumsplit  12115  isumrpcl  12118  divcnv  12121  trireciplem  12124  geosergap  12130  geolim2  12136  cvgratnnlemseq  12150  cvgratnnlemabsle  12151  cvgratnnlemsumlt  12152  cvgratnnlemrate  12154  cvgratz  12156  cvgratgt0  12157  mertenslemi1  12159  clim2divap  12164  prodrbdclem  12195  fproddccvg  12196  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodntrivap  12208  fprodssdc  12214  fprodm1  12222  fprod1p  12223  fprodp1  12224  fprodabs  12240  fprodeq0  12241  efgt1p2  12319  modm1div  12424  dvdsbnd  12590  uzwodc  12671  ncoprmgcdne1b  12724  isprm3  12753  prmind2  12755  nprm  12758  dvdsprm  12772  exprmfct  12773  isprm5lem  12776  isprm5  12777  phibndlem  12851  phibnd  12852  dfphi2  12855  hashdvds  12856  pclemdc  12924  pcaddlem  12975  pcmptdvds  12981  pcfac  12986  expnprm  12989  fngsum  13534  igsumvalx  13535  gsumval2  13543  gsumsplit1r  13544  gsumfzz  13641  plycoeid3  15551  relogbval  15745  relogbzcl  15746  nnlogbexp  15753  logblt  15756  logbgcd1irr  15761  lgsne0  15840  gausslemma2dlem4  15866  lgsquad2lem2  15884  2sqlem6  15922  2sqlem8a  15924  2sqlem8  15925  supfz  16787  gsumgfsumlem  16795