Theorem eluzelz 9657

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

Syntax hints:   → wi 4   ∈ wcel 2176   class class class wbr 4044  ‘cfv 5271   ≤ cle 8108  ℤcz 9372  ℤ_≥cuz 9648

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-cnex 8016  ax-resscn 8017

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-mpt 4107  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-res 4687  df-ima 4688  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279  df-ov 5947  df-neg 8246  df-z 9373  df-uz 9649

This theorem is referenced by:  eluzelre  9658  uztrn  9665  uzneg  9667  uzssz  9668  uzss  9669  eluzp1l  9673  eluzaddi  9675  eluzsubi  9676  eluzadd  9677  eluzsub  9678  uzm1  9679  uzin  9681  uzind4  9709  uz2mulcl  9729  elfz5  10139  elfzel2  10145  elfzelz  10147  eluzfz2  10154  peano2fzr  10159  fzsplit2  10172  fzopth  10183  fzsuc  10191  elfzp1  10194  fzdifsuc  10203  uzsplit  10214  uzdisj  10215  fzm1  10222  fzneuz  10223  uznfz  10225  nn0disj  10260  elfzo3  10286  fzoss2  10296  fzouzsplit  10303  eluzgtdifelfzo  10326  fzosplitsnm1  10338  fzofzp1b  10357  elfzonelfzo  10359  fzosplitsn  10362  fzisfzounsn  10365  zsupcllemstep  10372  infssuzex  10376  suprzubdc  10379  fldiv4lem1div2uz2  10449  mulp1mod1  10510  m1modge3gt1  10516  frec2uzltd  10548  frecfzen2  10572  uzennn  10581  uzsinds  10589  seq3fveq2  10620  seq3feq2  10621  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord  10630  monoord2  10631  ser3mono  10632  seq3split  10633  seqsplitg  10634  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  seq3f1olemqsumk  10657  seq3f1olemp  10660  seq3f1oleml  10661  seq3f1o  10662  seqf1oglem1  10664  seqf1oglem2  10665  seqf1og  10666  seq3id  10670  seq3z  10673  fser0const  10680  leexp2a  10737  expnlbnd2  10810  hashfz  10966  hashfzo  10967  hashfzp1  10969  seq3coll  10987  swrdfv2  11116  seq3shft  11149  rexuz3  11301  r19.2uz  11304  cau4  11427  caubnd2  11428  clim  11592  climshft2  11617  climaddc1  11640  climmulc2  11642  climsubc1  11643  climsubc2  11644  clim2ser  11648  clim2ser2  11649  iserex  11650  climlec2  11652  climub  11655  climcau  11658  climcaucn  11662  serf0  11663  sumrbdclem  11688  fsum3cvg  11689  summodclem2a  11692  zsumdc  11695  fsum3  11698  fisumss  11703  fsum3cvg2  11705  fsum3ser  11708  fsumcl2lem  11709  fsumadd  11717  fsumm1  11727  fzosump1  11728  fsum1p  11729  fsump1  11731  fsummulc2  11759  telfsumo  11777  fsumparts  11781  iserabs  11786  binomlem  11794  isumshft  11801  isumsplit  11802  isumrpcl  11805  divcnv  11808  trireciplem  11811  geosergap  11817  geolim2  11823  cvgratnnlemseq  11837  cvgratnnlemabsle  11838  cvgratnnlemsumlt  11839  cvgratnnlemrate  11841  cvgratz  11843  cvgratgt0  11844  mertenslemi1  11846  clim2divap  11851  prodrbdclem  11882  fproddccvg  11883  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodntrivap  11895  fprodssdc  11901  fprodm1  11909  fprod1p  11910  fprodp1  11911  fprodabs  11927  fprodeq0  11928  efgt1p2  12006  modm1div  12111  dvdsbnd  12277  uzwodc  12358  ncoprmgcdne1b  12411  isprm3  12440  prmind2  12442  nprm  12445  dvdsprm  12459  exprmfct  12460  isprm5lem  12463  isprm5  12464  phibndlem  12538  phibnd  12539  dfphi2  12542  hashdvds  12543  pclemdc  12611  pcaddlem  12662  pcmptdvds  12668  pcfac  12673  expnprm  12676  fngsum  13220  igsumvalx  13221  gsumval2  13229  gsumsplit1r  13230  gsumfzz  13327  plycoeid3  15229  relogbval  15423  relogbzcl  15424  nnlogbexp  15431  logblt  15434  logbgcd1irr  15439  lgsne0  15515  gausslemma2dlem4  15541  lgsquad2lem2  15559  2sqlem6  15597  2sqlem8a  15599  2sqlem8  15600  supfz  16010