MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluzelz Structured version   Unicode version

Theorem eluzelz 10488
Description: A member of a set of upper integers is an integer. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
eluzelz  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )

Proof of Theorem eluzelz
StepHypRef Expression
1 eluz2 10486 . 2  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
21simp2bi 973 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   class class class wbr 4204   ` cfv 5446    <_ cle 9113   ZZcz 10274   ZZ>=cuz 10480
This theorem is referenced by:  eluzelre  10489  uztrn  10494  uzneg  10496  uzss  10498  eluzp1l  10502  eluzaddi  10504  eluzsubi  10505  uzm1  10508  uzin  10510  uzp1  10511  peano2uzr  10524  uzaddcl  10525  uzind4  10526  uzwo  10531  uzwoOLD  10532  uz2mulcl  10545  uzsupss  10560  elfz5  11043  elfzel2  11049  elfzelz  11051  eluzfz2  11057  peano2fzr  11061  fzsplit2  11068  fzopth  11081  fzsuc  11088  uzsplit  11110  uzdisj  11111  fzm1  11119  uznfz  11122  elfzo3  11147  fzoss2  11155  fzouzsplit  11160  fzofzp1b  11182  fzosplitsn  11187  om2uzlti  11282  om2uzf1oi  11285  uzrdgxfr  11298  fzen2  11300  seqm1  11332  seqfveq2  11337  seqfeq2  11338  seqshft2  11341  monoord  11345  monoord2  11346  sermono  11347  seqsplit  11348  seqf1olem1  11354  seqf1olem2  11355  seqid  11360  seqz  11363  leexp2a  11427  expnlbnd2  11502  expmulnbnd  11503  bcval5  11601  hashfz  11684  fzsdom2  11685  hashfzo  11686  seqcoll  11704  shftuz  11876  seqshft  11892  rexuz3  12144  r19.2uz  12147  rexuzre  12148  cau4  12152  caubnd2  12153  clim  12280  climrlim2  12333  climshftlem  12360  climshft  12362  climshft2  12368  climaddc1  12420  climmulc2  12422  climsubc1  12423  climsubc2  12424  clim2ser  12440  clim2ser2  12441  iserex  12442  climlec2  12444  climub  12447  isercolllem2  12451  isercoll  12453  isercoll2  12454  climcau  12456  caurcvg2  12463  caucvgb  12465  serf0  12466  iseraltlem1  12467  iseraltlem2  12468  iseralt  12470  sumrblem  12497  fsumcvg  12498  summolem2a  12501  fsumcvg2  12513  fsumm1  12529  fzosump1  12530  fsump1  12532  fsumrev2  12557  fsumtscopo  12573  fsumparts  12577  isumshft  12611  isumsplit  12612  isumrpcl  12615  isumsup2  12618  cvgrat  12652  mertenslem1  12653  dvdsexp  12897  isprm3  13080  nprm  13085  dvdsprm  13091  exprmfct  13102  isprm5  13104  maxprmfct  13105  phibndlem  13151  dfphi2  13155  hashdvds  13156  pclem  13204  pcaddlem  13249  pcfac  13260  expnprm  13263  prmreclem4  13279  vdwlem8  13348  gsumval2a  14774  efgtlen  15350  efgs1b  15360  iscau4  19224  caucfil  19228  iscmet3lem3  19235  iscmet3lem1  19236  iscmet3lem2  19237  lmle  19246  uniioombllem3  19469  mbflimsup  19550  mbfi1fseqlem6  19604  dvfsumle  19897  dvfsumge  19898  dvfsumabs  19899  aaliou3lem1  20251  aaliou3lem2  20252  ulmres  20296  ulmshftlem  20297  ulmshft  20298  ulmcaulem  20302  ulmcau  20303  ulmdvlem1  20308  radcnvlem1  20321  dvradcnv  20329  muval1  20908  chtdif  20933  ppidif  20938  chtub  20988  bcmono  21053  bpos1lem  21058  lgsquad2lem2  21135  2sqlem6  21145  2sqlem8a  21147  2sqlem8  21148  chebbnd1lem1  21155  dchrisumlem2  21176  dchrisum0lem1  21202  ostthlem2  21314  ostth2  21323  constr3trllem3  21631  fzspl  24141  logblt  24398  supfz  25191  divcnvlin  25204  clim2div  25209  prodeq2ii  25231  fprodcvg  25248  prodmolem2a  25252  zprod  25255  fprodntriv  25260  fprodser  25267  fprodm1  25282  fprodp1  25284  fprodeq0  25291  preduz  25467  axlowdimlem3  25875  axlowdimlem6  25878  axlowdimlem7  25879  axlowdimlem16  25888  axlowdimlem17  25889  axlowdim  25892  nn0prpwlem  26316  fdc  26440  mettrifi  26454  caushft  26458  rmspecsqrnq  26960  rmspecnonsq  26961  rmspecfund  26963  rmxyadd  26975  rmxy1  26976  rmxm1  26988  rmxluc  26990  rmyluc2  26992  jm2.17a  27016  jm2.18  27050  jm2.22  27057  jm2.15nn0  27065  jm2.16nn0  27066  jm2.27a  27067  jm2.27c  27069  jm3.1lem2  27080  jm3.1lem3  27081  jm3.1  27082  expdiophlem1  27083  fmul01  27677  fmul01lt1lem1  27681  fmul01lt1lem2  27682  climsuselem1  27700  climsuse  27701  itgsinexp  27716  fzosplitsnm1  28114  elfzonelfzo  28115  iswrd0i  28146  swrdccatin12  28180
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-cnex 9038  ax-resscn 9039
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-fv 5454  df-ov 6076  df-neg 9286  df-z 10275  df-uz 10481
  Copyright terms: Public domain W3C validator