Theorem eluzelz 9601

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

Syntax hints:   → wi 4   ∈ wcel 2164   class class class wbr 4029  ‘cfv 5254   ≤ cle 8055  ℤcz 9317  ℤ_≥cuz 9592

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-cnex 7963  ax-resscn 7964

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-sbc 2986  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-fv 5262  df-ov 5921  df-neg 8193  df-z 9318  df-uz 9593

This theorem is referenced by:  eluzelre  9602  uztrn  9609  uzneg  9611  uzssz  9612  uzss  9613  eluzp1l  9617  eluzaddi  9619  eluzsubi  9620  eluzadd  9621  eluzsub  9622  uzm1  9623  uzin  9625  uzind4  9653  uz2mulcl  9673  elfz5  10083  elfzel2  10089  elfzelz  10091  eluzfz2  10098  peano2fzr  10103  fzsplit2  10116  fzopth  10127  fzsuc  10135  elfzp1  10138  fzdifsuc  10147  uzsplit  10158  uzdisj  10159  fzm1  10166  fzneuz  10167  uznfz  10169  nn0disj  10204  elfzo3  10230  fzoss2  10239  fzouzsplit  10246  eluzgtdifelfzo  10264  fzosplitsnm1  10276  fzofzp1b  10295  elfzonelfzo  10297  fzosplitsn  10300  fzisfzounsn  10303  fldiv4lem1div2uz2  10375  mulp1mod1  10436  m1modge3gt1  10442  frec2uzltd  10474  frecfzen2  10498  uzennn  10507  uzsinds  10515  seq3fveq2  10546  seq3feq2  10547  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord  10556  monoord2  10557  ser3mono  10558  seq3split  10559  seqsplitg  10560  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  seq3f1olemqsumk  10583  seq3f1olemp  10586  seq3f1oleml  10587  seq3f1o  10588  seqf1oglem1  10590  seqf1oglem2  10591  seqf1og  10592  seq3id  10596  seq3z  10599  fser0const  10606  leexp2a  10663  expnlbnd2  10736  hashfz  10892  hashfzo  10893  hashfzp1  10895  seq3coll  10913  seq3shft  10982  rexuz3  11134  r19.2uz  11137  cau4  11260  caubnd2  11261  clim  11424  climshft2  11449  climaddc1  11472  climmulc2  11474  climsubc1  11475  climsubc2  11476  clim2ser  11480  clim2ser2  11481  iserex  11482  climlec2  11484  climub  11487  climcau  11490  climcaucn  11494  serf0  11495  sumrbdclem  11520  fsum3cvg  11521  summodclem2a  11524  zsumdc  11527  fsum3  11530  fisumss  11535  fsum3cvg2  11537  fsum3ser  11540  fsumcl2lem  11541  fsumadd  11549  fsumm1  11559  fzosump1  11560  fsum1p  11561  fsump1  11563  fsummulc2  11591  telfsumo  11609  fsumparts  11613  iserabs  11618  binomlem  11626  isumshft  11633  isumsplit  11634  isumrpcl  11637  divcnv  11640  trireciplem  11643  geosergap  11649  geolim2  11655  cvgratnnlemseq  11669  cvgratnnlemabsle  11670  cvgratnnlemsumlt  11671  cvgratnnlemrate  11673  cvgratz  11675  cvgratgt0  11676  mertenslemi1  11678  clim2divap  11683  prodrbdclem  11714  fproddccvg  11715  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodntrivap  11727  fprodssdc  11733  fprodm1  11741  fprod1p  11742  fprodp1  11743  fprodabs  11759  fprodeq0  11760  efgt1p2  11838  modm1div  11943  zsupcllemstep  12082  infssuzex  12086  suprzubdc  12089  dvdsbnd  12093  uzwodc  12174  ncoprmgcdne1b  12227  isprm3  12256  prmind2  12258  nprm  12261  dvdsprm  12275  exprmfct  12276  isprm5lem  12279  isprm5  12280  phibndlem  12354  phibnd  12355  dfphi2  12358  hashdvds  12359  pclemdc  12426  pcaddlem  12477  pcmptdvds  12483  pcfac  12488  expnprm  12491  fngsum  12971  igsumvalx  12972  gsumval2  12980  gsumsplit1r  12981  gsumfzz  13067  relogbval  15083  relogbzcl  15084  nnlogbexp  15091  logblt  15094  logbgcd1irr  15099  lgsne0  15154  gausslemma2dlem4  15180  2sqlem6  15207  2sqlem8a  15209  2sqlem8  15210  supfz  15561