Theorem eluzelz 9755

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

Syntax hints:   → wi 4   ∈ wcel 2200   class class class wbr 4086  ‘cfv 5324   ≤ cle 8205  ℤcz 9469  ℤ_≥cuz 9745

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-cnex 8113  ax-resscn 8114

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-fv 5332  df-ov 6016  df-neg 8343  df-z 9470  df-uz 9746

This theorem is referenced by:  eluzelre  9756  uztrn  9763  uzneg  9765  uzssz  9766  uzss  9767  eluzp1l  9771  eluzaddi  9773  eluzsubi  9774  eluzadd  9775  eluzsub  9776  uzm1  9777  uzin  9779  uzind4  9812  uz2mulcl  9832  elfz5  10242  elfzel2  10248  elfzelz  10250  eluzfz2  10257  peano2fzr  10262  fzsplit2  10275  fzopth  10286  fzsuc  10294  elfzp1  10297  fzdifsuc  10306  uzsplit  10317  uzdisj  10318  fzm1  10325  fzneuz  10326  uznfz  10328  nn0disj  10363  elfzo3  10389  fzoss2  10399  fzouzsplit  10406  fzoun  10408  eluzgtdifelfzo  10432  fzosplitsnm1  10444  fzofzp1b  10463  elfzonelfzo  10465  fzosplitsn  10468  fzisfzounsn  10472  zsupcllemstep  10479  infssuzex  10483  suprzubdc  10486  fldiv4lem1div2uz2  10556  mulp1mod1  10617  m1modge3gt1  10623  frec2uzltd  10655  frecfzen2  10679  uzennn  10688  uzsinds  10696  seq3fveq2  10727  seq3feq2  10728  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  monoord  10737  monoord2  10738  ser3mono  10739  seq3split  10740  seqsplitg  10741  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  seq3f1olemqsumk  10764  seq3f1olemp  10767  seq3f1oleml  10768  seq3f1o  10769  seqf1oglem1  10771  seqf1oglem2  10772  seqf1og  10773  seq3id  10777  seq3z  10780  fser0const  10787  leexp2a  10844  expnlbnd2  10917  hashfz  11075  hashfzo  11076  hashfzp1  11078  seq3coll  11096  swrdfv2  11234  pfxccatin12  11304  seq3shft  11389  rexuz3  11541  r19.2uz  11544  cau4  11667  caubnd2  11668  clim  11832  climshft2  11857  climaddc1  11880  climmulc2  11882  climsubc1  11883  climsubc2  11884  clim2ser  11888  clim2ser2  11889  iserex  11890  climlec2  11892  climub  11895  climcau  11898  climcaucn  11902  serf0  11903  sumrbdclem  11928  fsum3cvg  11929  summodclem2a  11932  zsumdc  11935  fsum3  11938  fisumss  11943  fsum3cvg2  11945  fsum3ser  11948  fsumcl2lem  11949  fsumadd  11957  fsumm1  11967  fzosump1  11968  fsum1p  11969  fsump1  11971  fsummulc2  11999  telfsumo  12017  fsumparts  12021  iserabs  12026  binomlem  12034  isumshft  12041  isumsplit  12042  isumrpcl  12045  divcnv  12048  trireciplem  12051  geosergap  12057  geolim2  12063  cvgratnnlemseq  12077  cvgratnnlemabsle  12078  cvgratnnlemsumlt  12079  cvgratnnlemrate  12081  cvgratz  12083  cvgratgt0  12084  mertenslemi1  12086  clim2divap  12091  prodrbdclem  12122  fproddccvg  12123  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodntrivap  12135  fprodssdc  12141  fprodm1  12149  fprod1p  12150  fprodp1  12151  fprodabs  12167  fprodeq0  12168  efgt1p2  12246  modm1div  12351  dvdsbnd  12517  uzwodc  12598  ncoprmgcdne1b  12651  isprm3  12680  prmind2  12682  nprm  12685  dvdsprm  12699  exprmfct  12700  isprm5lem  12703  isprm5  12704  phibndlem  12778  phibnd  12779  dfphi2  12782  hashdvds  12783  pclemdc  12851  pcaddlem  12902  pcmptdvds  12908  pcfac  12913  expnprm  12916  fngsum  13461  igsumvalx  13462  gsumval2  13470  gsumsplit1r  13471  gsumfzz  13568  plycoeid3  15471  relogbval  15665  relogbzcl  15666  nnlogbexp  15673  logblt  15676  logbgcd1irr  15681  lgsne0  15757  gausslemma2dlem4  15783  lgsquad2lem2  15801  2sqlem6  15839  2sqlem8a  15841  2sqlem8  15842  supfz  16611