Theorem eluzelz 9692

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

Syntax hints:   → wi 4   ∈ wcel 2178   class class class wbr 4059  ‘cfv 5290   ≤ cle 8143  ℤcz 9407  ℤ_≥cuz 9683

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-cnex 8051  ax-resscn 8052

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-sbc 3006  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-mpt 4123  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-res 4705  df-ima 4706  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-fv 5298  df-ov 5970  df-neg 8281  df-z 9408  df-uz 9684

This theorem is referenced by:  eluzelre  9693  uztrn  9700  uzneg  9702  uzssz  9703  uzss  9704  eluzp1l  9708  eluzaddi  9710  eluzsubi  9711  eluzadd  9712  eluzsub  9713  uzm1  9714  uzin  9716  uzind4  9744  uz2mulcl  9764  elfz5  10174  elfzel2  10180  elfzelz  10182  eluzfz2  10189  peano2fzr  10194  fzsplit2  10207  fzopth  10218  fzsuc  10226  elfzp1  10229  fzdifsuc  10238  uzsplit  10249  uzdisj  10250  fzm1  10257  fzneuz  10258  uznfz  10260  nn0disj  10295  elfzo3  10321  fzoss2  10331  fzouzsplit  10338  fzoun  10340  eluzgtdifelfzo  10363  fzosplitsnm1  10375  fzofzp1b  10394  elfzonelfzo  10396  fzosplitsn  10399  fzisfzounsn  10402  zsupcllemstep  10409  infssuzex  10413  suprzubdc  10416  fldiv4lem1div2uz2  10486  mulp1mod1  10547  m1modge3gt1  10553  frec2uzltd  10585  frecfzen2  10609  uzennn  10618  uzsinds  10626  seq3fveq2  10657  seq3feq2  10658  seqfveq2g  10659  seq3shft2  10663  seqshft2g  10664  monoord  10667  monoord2  10668  ser3mono  10669  seq3split  10670  seqsplitg  10671  iseqf1olemjpcl  10690  iseqf1olemqpcl  10691  seq3f1olemqsumk  10694  seq3f1olemp  10697  seq3f1oleml  10698  seq3f1o  10699  seqf1oglem1  10701  seqf1oglem2  10702  seqf1og  10703  seq3id  10707  seq3z  10710  fser0const  10717  leexp2a  10774  expnlbnd2  10847  hashfz  11003  hashfzo  11004  hashfzp1  11006  seq3coll  11024  swrdfv2  11154  pfxccatin12  11224  seq3shft  11264  rexuz3  11416  r19.2uz  11419  cau4  11542  caubnd2  11543  clim  11707  climshft2  11732  climaddc1  11755  climmulc2  11757  climsubc1  11758  climsubc2  11759  clim2ser  11763  clim2ser2  11764  iserex  11765  climlec2  11767  climub  11770  climcau  11773  climcaucn  11777  serf0  11778  sumrbdclem  11803  fsum3cvg  11804  summodclem2a  11807  zsumdc  11810  fsum3  11813  fisumss  11818  fsum3cvg2  11820  fsum3ser  11823  fsumcl2lem  11824  fsumadd  11832  fsumm1  11842  fzosump1  11843  fsum1p  11844  fsump1  11846  fsummulc2  11874  telfsumo  11892  fsumparts  11896  iserabs  11901  binomlem  11909  isumshft  11916  isumsplit  11917  isumrpcl  11920  divcnv  11923  trireciplem  11926  geosergap  11932  geolim2  11938  cvgratnnlemseq  11952  cvgratnnlemabsle  11953  cvgratnnlemsumlt  11954  cvgratnnlemrate  11956  cvgratz  11958  cvgratgt0  11959  mertenslemi1  11961  clim2divap  11966  prodrbdclem  11997  fproddccvg  11998  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodntrivap  12010  fprodssdc  12016  fprodm1  12024  fprod1p  12025  fprodp1  12026  fprodabs  12042  fprodeq0  12043  efgt1p2  12121  modm1div  12226  dvdsbnd  12392  uzwodc  12473  ncoprmgcdne1b  12526  isprm3  12555  prmind2  12557  nprm  12560  dvdsprm  12574  exprmfct  12575  isprm5lem  12578  isprm5  12579  phibndlem  12653  phibnd  12654  dfphi2  12657  hashdvds  12658  pclemdc  12726  pcaddlem  12777  pcmptdvds  12783  pcfac  12788  expnprm  12791  fngsum  13335  igsumvalx  13336  gsumval2  13344  gsumsplit1r  13345  gsumfzz  13442  plycoeid3  15344  relogbval  15538  relogbzcl  15539  nnlogbexp  15546  logblt  15549  logbgcd1irr  15554  lgsne0  15630  gausslemma2dlem4  15656  lgsquad2lem2  15674  2sqlem6  15712  2sqlem8a  15714  2sqlem8  15715  supfz  16212