Theorem eluzelz 9572

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

Syntax hints:   → wi 4   ∈ wcel 2160   class class class wbr 4021  ‘cfv 5238   ≤ cle 8028  ℤcz 9288  ℤ_≥cuz 9563

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 2163  ax-ext 2171  ax-sep 4139  ax-pow 4195  ax-pr 4230  ax-cnex 7937  ax-resscn 7938

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 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-br 4022  df-opab 4083  df-mpt 4084  df-id 4314  df-xp 4653  df-rel 4654  df-cnv 4655  df-co 4656  df-dm 4657  df-rn 4658  df-res 4659  df-ima 4660  df-iota 5199  df-fun 5240  df-fn 5241  df-f 5242  df-fv 5246  df-ov 5903  df-neg 8166  df-z 9289  df-uz 9564

This theorem is referenced by:  eluzelre  9573  uztrn  9580  uzneg  9582  uzssz  9583  uzss  9584  eluzp1l  9588  eluzaddi  9590  eluzsubi  9591  eluzadd  9592  eluzsub  9593  uzm1  9594  uzin  9596  uzind4  9624  uz2mulcl  9644  elfz5  10053  elfzel2  10059  elfzelz  10061  eluzfz2  10068  peano2fzr  10073  fzsplit2  10086  fzopth  10097  fzsuc  10105  elfzp1  10108  fzdifsuc  10117  uzsplit  10128  uzdisj  10129  fzm1  10136  fzneuz  10137  uznfz  10139  nn0disj  10174  elfzo3  10199  fzoss2  10208  fzouzsplit  10215  eluzgtdifelfzo  10233  fzosplitsnm1  10245  fzofzp1b  10264  elfzonelfzo  10266  fzosplitsn  10269  fzisfzounsn  10272  mulp1mod1  10402  m1modge3gt1  10408  frec2uzltd  10440  frecfzen2  10464  uzennn  10473  uzsinds  10481  seq3fveq2  10508  seq3feq2  10509  seq3shft2  10512  monoord  10515  monoord2  10516  ser3mono  10517  seq3split  10518  iseqf1olemjpcl  10534  iseqf1olemqpcl  10535  seq3f1olemqsumk  10538  seq3f1olemp  10541  seq3f1oleml  10542  seq3f1o  10543  seq3id  10547  seq3z  10550  fser0const  10556  leexp2a  10613  expnlbnd2  10686  hashfz  10842  hashfzo  10843  hashfzp1  10845  seq3coll  10863  seq3shft  10888  rexuz3  11040  r19.2uz  11043  cau4  11166  caubnd2  11167  clim  11330  climshft2  11355  climaddc1  11378  climmulc2  11380  climsubc1  11381  climsubc2  11382  clim2ser  11386  clim2ser2  11387  iserex  11388  climlec2  11390  climub  11393  climcau  11396  climcaucn  11400  serf0  11401  sumrbdclem  11426  fsum3cvg  11427  summodclem2a  11430  zsumdc  11433  fsum3  11436  fisumss  11441  fsum3cvg2  11443  fsum3ser  11446  fsumcl2lem  11447  fsumadd  11455  fsumm1  11465  fzosump1  11466  fsum1p  11467  fsump1  11469  fsummulc2  11497  telfsumo  11515  fsumparts  11519  iserabs  11524  binomlem  11532  isumshft  11539  isumsplit  11540  isumrpcl  11543  divcnv  11546  trireciplem  11549  geosergap  11555  geolim2  11561  cvgratnnlemseq  11575  cvgratnnlemabsle  11576  cvgratnnlemsumlt  11577  cvgratnnlemrate  11579  cvgratz  11581  cvgratgt0  11582  mertenslemi1  11584  clim2divap  11589  prodrbdclem  11620  fproddccvg  11621  prodmodclem3  11624  prodmodclem2a  11625  zproddc  11628  fprodntrivap  11633  fprodssdc  11639  fprodm1  11647  fprod1p  11648  fprodp1  11649  fprodabs  11665  fprodeq0  11666  efgt1p2  11744  modm1div  11848  zsupcllemstep  11987  infssuzex  11991  suprzubdc  11994  dvdsbnd  11998  uzwodc  12079  ncoprmgcdne1b  12132  isprm3  12161  prmind2  12163  nprm  12166  dvdsprm  12180  exprmfct  12181  isprm5lem  12184  isprm5  12185  phibndlem  12259  phibnd  12260  dfphi2  12263  hashdvds  12264  pclemdc  12331  pcaddlem  12382  pcmptdvds  12388  pcfac  12393  expnprm  12396  fngsum  12875  igsumvalx  12876  gsumval2  12883  gsumsplit1r  12884  relogbval  14854  relogbzcl  14855  nnlogbexp  14862  logblt  14865  logbgcd1irr  14870  lgsne0  14925  2sqlem6  14953  2sqlem8a  14955  2sqlem8  14956  supfz  15307