Theorem eluzelz 9089

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

Syntax hints:   → wi 4   ∈ wcel 1439   class class class wbr 3851  ‘cfv 5028   ≤ cle 7584  ℤcz 8811  ℤ_≥cuz 9080

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-pow 4015  ax-pr 4045  ax-cnex 7497  ax-resscn 7498

This theorem depends on definitions:  df-bi 116  df-3or 926  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-rab 2369  df-v 2622  df-sbc 2842  df-un 3004  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-opab 3906  df-mpt 3907  df-id 4129  df-xp 4458  df-rel 4459  df-cnv 4460  df-co 4461  df-dm 4462  df-rn 4463  df-res 4464  df-ima 4465  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-fv 5036  df-ov 5669  df-neg 7717  df-z 8812  df-uz 9081

This theorem is referenced by:  eluzelre  9090  uztrn  9096  uzneg  9098  uzssz  9099  uzss  9100  eluzp1l  9104  eluzaddi  9106  eluzsubi  9107  eluzadd  9108  eluzsub  9109  uzm1  9110  uzin  9112  uzind4  9137  uz2mulcl  9156  elfz5  9493  elfzel2  9499  elfzelz  9501  eluzfz2  9507  peano2fzr  9512  fzsplit2  9525  fzopth  9536  fzsuc  9544  elfzp1  9547  fzdifsuc  9556  uzsplit  9567  uzdisj  9568  fzm1  9575  fzneuz  9576  uznfz  9578  nn0disj  9610  elfzo3  9635  fzoss2  9644  fzouzsplit  9651  eluzgtdifelfzo  9669  fzosplitsnm1  9681  fzofzp1b  9700  elfzonelfzo  9702  fzosplitsn  9705  fzisfzounsn  9708  mulp1mod1  9833  m1modge3gt1  9839  frec2uzltd  9871  frecfzen2  9895  uzsinds  9909  iseqfveq2  9951  iseqfeq2  9952  seq3fveq2  9953  seq3feq2  9954  iseqshft2  9959  monoord  9965  monoord2  9966  isermono  9967  seq3split  9968  iseqsplit  9969  iseqf1olemjpcl  9985  iseqf1olemqpcl  9986  seq3f1olemqsumk  9989  seq3f1olemp  9992  seq3f1oleml  9993  seq3f1o  9994  iseqid  10000  iseqz  10004  fser0const  10012  leexp2a  10069  expnlbnd2  10140  hashfz  10290  hashfzo  10291  hashfzp1  10293  iseqcoll  10308  seq3shft  10333  rexuz3  10484  r19.2uz  10487  cau4  10610  caubnd2  10611  clim  10730  climshft2  10756  climaddc1  10778  climmulc2  10780  climsubc1  10781  climsubc2  10782  clim2ser  10786  clim2ser2  10787  iserex  10788  climlec2  10791  climub  10794  climcau  10797  climcaucn  10801  serf0  10802  isumrblem  10826  fisumcvg  10827  fsum3cvg  10828  isummolem2a  10832  zisum  10835  fisum  10839  fsum3  10840  fisumss  10845  fisumcvg2  10847  fsum3cvg2  10848  fisumser  10851  fsumcl2lem  10853  fsumadd  10861  fsumm1  10871  fzosump1  10872  fsum1p  10873  fsump1  10875  fsummulc2  10903  telfsumo  10921  fsumparts  10925  iserabs  10930  binomlem  10938  isumshft  10945  isumsplit  10946  isumrpcl  10949  divcnv  10952  trireciplem  10955  geosergap  10961  geolim2  10967  cvgratnnlemseq  10981  cvgratnnlemabsle  10982  cvgratnnlemsumlt  10983  cvgratnnlemrate  10985  cvgratz  10987  cvgratgt0  10988  mertenslemi1  10990  efgt1p2  11046  zsupcllemstep  11280  infssuzex  11284  dvdsbnd  11287  ncoprmgcdne1b  11410  isprm3  11439  prmind2  11441  nprm  11444  dvdsprm  11457  exprmfct  11458  phibndlem  11531  phibnd  11532  dfphi2  11535  hashdvds  11536  supfz  12188