Theorem eluzelz 12854

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

Syntax hints:   → wi 4   ∈ wcel 2099   class class class wbr 5142  ‘cfv 6542   ≤ cle 11271  ℤcz 12580  ℤ_≥cuz 12844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-cnex 11186  ax-resscn 11187

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7417  df-neg 11469  df-z 12581  df-uz 12845

This theorem is referenced by:  eluzelre  12855  uztrn  12862  uzneg  12864  uzss  12867  eluzp1l  12871  eluzadd  12873  eluzsub  12874  eluzaddiOLD  12876  eluzsubiOLD  12878  subeluzsub  12881  uzm1  12882  uzin  12884  uzind4  12912  uzwo  12917  uz2mulcl  12932  uzsupss  12946  elfz5  13517  elfzel2  13523  elfzelz  13525  eluzfz2  13533  peano2fzr  13538  fzsplit2  13550  fzopth  13562  ssfzunsn  13571  fzsuc  13572  elfz1uz  13595  uzsplit  13597  uzdisj  13598  fzm1  13605  uznfz  13608  nn0disj  13641  preduz  13647  elfzo3  13673  fzoss2  13684  fzouzsplit  13691  fzoun  13693  eluzgtdifelfzo  13718  fzosplitsnm1  13731  fzofzp1b  13754  elfzonelfzo  13758  fzosplitsn  13764  fzisfzounsn  13768  fldiv4lem1div2uz2  13825  m1modge3gt1  13907  modaddmodup  13923  om2uzlti  13939  om2uzf1oi  13942  uzrdgxfr  13956  fzen2  13958  seqfveq2  14013  seqfeq2  14014  seqshft2  14017  monoord  14021  monoord2  14022  sermono  14023  seqsplit  14024  seqf1olem1  14030  seqf1olem2  14031  seqid  14036  leexp2a  14160  expnlbnd2  14220  expmulnbnd  14221  hashfz  14410  fzsdom2  14411  hashfzo  14412  hashfzp1  14414  seqcoll  14449  swrdfv2  14635  pfxccatin12  14707  rexuz3  15319  r19.2uz  15322  rexuzre  15323  cau4  15327  caubnd2  15328  clim  15462  climrlim2  15515  climshft2  15550  climaddc1  15603  climmulc2  15605  climsubc1  15606  climsubc2  15607  clim2ser  15625  clim2ser2  15626  iserex  15627  climlec2  15629  climub  15632  isercolllem2  15636  isercoll  15638  isercoll2  15639  climcau  15641  caurcvg2  15648  caucvgb  15650  serf0  15651  iseraltlem1  15652  iseraltlem2  15653  iseralt  15655  sumrblem  15681  fsumcvg  15682  summolem2a  15685  fsumcvg2  15697  fsumm1  15721  fzosump1  15722  fsump1  15726  fsumrev2  15752  telfsumo  15772  fsumparts  15776  isumsplit  15810  isumrpcl  15813  isumsup2  15816  cvgrat  15853  mertenslem1  15854  clim2div  15859  prodeq2ii  15881  fprodcvg  15898  prodmolem2a  15902  zprod  15905  fprodntriv  15910  fprodser  15917  fprodm1  15935  fprodp1  15937  fprodeq0  15943  isprm3  16645  nprm  16650  dvdsprm  16665  exprmfct  16666  isprm5  16669  maxprmfct  16671  prmdvdsncoprmbd  16690  ncoprmlnprm  16691  phibndlem  16730  dfphi2  16734  hashdvds  16735  pcaddlem  16848  pcfac  16859  expnprm  16862  prmreclem4  16879  vdwlem8  16948  gsumval2a  18636  efgs1b  19682  telgsumfzs  19935  iscau4  25194  caucfil  25198  iscmet3lem3  25205  iscmet3lem1  25206  iscmet3lem2  25207  lmle  25216  uniioombllem3  25501  mbflimsup  25582  mbfi1fseqlem6  25637  dvfsumle  25941  dvfsumleOLD  25942  dvfsumge  25943  dvfsumabs  25944  aaliou3lem1  26264  aaliou3lem2  26265  ulmres  26311  ulmshftlem  26312  ulmshft  26313  ulmcaulem  26317  ulmcau  26318  ulmdvlem1  26323  radcnvlem1  26336  logblt  26703  logbgcd1irr  26713  muval1  27052  chtdif  27077  ppidif  27082  chtub  27132  bcmono  27197  bpos1lem  27202  lgsquad2lem2  27305  2sqlem6  27343  2sqlem8a  27345  2sqlem8  27346  chebbnd1lem1  27389  dchrisumlem2  27410  dchrisum0lem1  27436  ostthlem2  27548  ostth2  27557  axlowdimlem3  28742  axlowdimlem6  28745  axlowdimlem7  28746  axlowdimlem16  28755  axlowdimlem17  28756  axlowdim  28759  clwwnrepclwwn  30141  fzspl  32542  fzdif2  32543  supfz  35259  divcnvlin  35263  nn0prpwlem  35742  fdc  37153  mettrifi  37165  caushft  37169  aks4d1lem1  41470  aks4d1p1  41484  aks4d1p2  41485  aks4d1p3  41486  aks4d1p5  41488  aks4d1p6  41489  aks4d1p7d1  41490  aks4d1p7  41491  aks4d1p8  41495  aks4d1p9  41496  fzosumm1  41654  dffltz  41980  rmspecnonsq  42249  rmspecfund  42251  rmxyadd  42264  rmxy1  42265  jm2.18  42331  jm2.22  42338  jm2.15nn0  42346  jm2.16nn0  42347  jm2.27a  42348  jm2.27c  42350  jm3.1lem2  42361  jm3.1lem3  42362  jm3.1  42363  expdiophlem1  42364  dvgrat  43672  cvgdvgrat  43673  hashnzfz  43680  uzwo4  44340  ssinc  44376  ssdec  44377  rexanuz3  44385  monoords  44602  fzdifsuc2  44615  iuneqfzuzlem  44639  eluzelzd  44680  allbutfi  44698  eluzelz2  44708  uzid2  44710  monoordxrv  44787  monoord2xrv  44789  fmul01  44891  fmul01lt1lem1  44895  fmul01lt1lem2  44896  climsuselem1  44918  climsuse  44919  climf  44933  climresmpt  44970  climf2  44977  limsupequzlem  45033  limsupmnfuzlem  45037  limsupre3uzlem  45046  itgsinexp  45266  iblspltprt  45284  itgspltprt  45290  iundjiun  45771  smflimsuplem2  46132  smflimsuplem4  46134  smflimsuplem5  46135  fzopredsuc  46626  smonoord  46634  iccpartiltu  46685  fmtnoprmfac2lem1  46829  fmtnofac2lem  46831  lighneallem2  46869  lighneallem4a  46871  lighneallem4b  46872  fppr2odd  46994  fpprwpprb  47003  gboge9  47027  nnsum3primesle9  47057  nnsum4primesevenALTV  47064  wtgoldbnnsum4prm  47065  bgoldbnnsum3prm  47067  bgoldbtbndlem2  47069  m1modmmod  47517  fllogbd  47556  fllog2  47564  dignn0ldlem  47598  dignnld  47599  digexp  47603  dignn0flhalf  47614  nn0sumshdiglemB  47616