MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zre Structured version   Visualization version   GIF version

Theorem zre 11974
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre
StepHypRef Expression
1 elz 11972 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 498 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1078   = wceq 1528  wcel 2105  cr 10525  0cc0 10526  -cneg 10860  cn 11627  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148  df-neg 10862  df-z 11971
This theorem is referenced by:  zcn  11975  zrei  11976  zssre  11977  elnn0z  11983  elnnz1  11997  znnnlt1  11998  zletr  12015  znnsub  12017  znn0sub  12018  nzadd  12019  zltp1le  12021  zleltp1  12022  nn0ge0div  12040  zextle  12044  btwnnz  12047  suprzcl  12051  msqznn  12053  peano2uz2  12059  uzind  12063  fzind  12069  fnn0ind  12070  eluzuzle  12241  uzid  12247  uzneg  12252  uztric  12255  uz11  12256  eluzp1m1  12257  eluzp1p1  12259  eluzaddi  12260  eluzsubi  12261  subeluzsub  12264  uzin  12267  uz3m2nn  12280  peano2uz  12290  nn0pzuz  12294  uzwo  12300  eluz2b2  12310  uz2mulcl  12315  uzinfi  12317  eqreznegel  12323  lbzbi  12325  uzsupss  12329  nn01to3  12330  zmin  12333  zmax  12334  zbtwnre  12335  rebtwnz  12336  qre  12342  elpq  12364  rpnnen1lem2  12366  rpnnen1lem1  12367  rpnnen1lem3  12368  rpnnen1lem5  12370  z2ge  12581  qbtwnre  12582  zltaddlt1le  12880  elfz1eq  12908  fzn  12913  fzen  12914  uzsubsubfz  12919  fzaddel  12931  fzadd2  12932  ssfzunsnext  12942  ssfzunsn  12943  fzsuc2  12955  fzrev  12960  elfz1b  12966  fznuz  12979  uznfz  12980  fzp1nel  12981  elfz0fzfz0  13002  fz0fzelfz0  13003  fznn0sub2  13004  fz0fzdiffz0  13006  elfzmlbp  13008  difelfznle  13011  nelfzo  13033  elfzouz2  13042  fzo0n  13049  fzonlt0  13050  fzossrbm1  13056  fzospliti  13059  elfzo0z  13069  fzofzim  13074  fzo1fzo0n0  13078  eluzgtdifelfzo  13089  fzossfzop1  13105  ssfzoulel  13121  ssfzo12bi  13122  elfzonelfzo  13129  elfzomelpfzo  13131  elfznelfzob  13133  fzostep1  13143  fllt  13166  flid  13168  flbi2  13177  2tnp1ge0ge0  13189  flhalf  13190  fldiv4p1lem1div2  13195  fldiv4lem1div2uz2  13196  dfceil2  13199  ceile  13207  ceilid  13209  quoremz  13213  intfracq  13217  uzsup  13221  mulmod0  13235  zmod10  13245  zmodcl  13249  zmodfz  13251  zmodid2  13257  modcyc  13264  mulp1mod1  13270  modmuladd  13271  modmuladdim  13272  modmul1  13282  modaddmodup  13292  modaddmodlo  13293  modaddmulmod  13296  zsqcl2  13492  leexp2  13525  iexpcyc  13559  fi1uzind  13845  ccatsymb  13926  ccatval21sw  13929  lswccatn0lsw  13935  swrdnd  14006  swrdnnn0nd  14008  swrd0  14010  swrdswrdlem  14056  swrdswrd  14057  swrdccatin2  14081  pfxccatin12lem2  14083  pfxccatin12lem3  14084  repswswrd  14136  cshwmodn  14147  cshwsublen  14148  cshwidxmod  14155  cshwidxmodr  14156  cshwidxm1  14159  repswcshw  14164  2cshw  14165  cshweqrep  14173  cshw1  14174  swrd2lsw  14304  nn0abscl  14662  rexuzre  14702  dvdsval3  15601  p1modz1  15604  moddvds  15608  absdvdsb  15618  dvdsabsb  15619  dvdsle  15650  alzdvds  15660  mod2eq1n2dvds  15686  evennn02n  15689  evennn2n  15690  ltoddhalfle  15700  divalgmod  15747  fldivndvdslt  15755  flodddiv4t2lthalf  15757  bitsp1o  15772  gcdabs  15867  gcdabs1  15868  modgcd  15870  bezoutlem1  15877  dfgcd2  15884  algcvga  15913  lcmabs  15939  isprm3  16017  dvdsnprmd  16024  2mulprm  16027  oddprmgt2  16033  sqnprm  16036  zgcdsq  16083  hashdvds  16102  vfermltlALT  16129  powm2modprm  16130  modprm0  16132  modprmn0modprm0  16134  fldivp1  16223  zgz  16259  4sqlem4  16278  prmgaplem5  16381  prmgaplem7  16383  cshwshashlem2  16420  setsstruct  16513  mulgmodid  18206  gexdvds  18640  zringunit  20565  prmirred  20572  znf1o  20628  chfacfscmul0  21396  chfacfscmulgsum  21398  chfacfpmmul0  21400  chfacfpmmulgsum  21402  dyadf  24121  dyadovol  24123  degltlem1  24595  coskpi  25037  cosne0  25041  relogexp  25106  cxpeq  25265  relogbzexp  25281  ppival2  25633  ppival2g  25634  ppiprm  25656  chtprm  25658  chtnprm  25659  ppip1le  25666  efexple  25785  zabsle1  25800  lgsdir2lem4  25832  lgsne0  25839  gausslemma2dlem1a  25869  gausslemma2dlem3  25872  gausslemma2dlem4  25873  lgsquadlem1  25884  lgsquadlem2  25885  2lgslem1a1  25893  2lgslem1a2  25894  2sqlem2  25922  rplogsumlem2  25989  pntrsumbnd  26070  axlowdim  26675  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  crctcshwlkn0  27527  crctcsh  27530  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a  27704  clwwisshclwwslemlem  27719  clwwlkinwwlk  27746  clwwlkext2edg  27763  wwlksubclwwlk  27765  numclwwlk5  28095  topnfbey  28176  uzssico  30434  rezh  31112  zrhre  31160  hashf2  31243  ballotlemfc0  31650  ballotlemfcc  31651  chpvalz  31799  chtvalz  31800  zltp1ne  32246  0nn0m1nnn0  32249  elfzm12  32816  nn0prpwlem  33568  poimirlem24  34798  mblfinlem1  34811  mblfinlem2  34812  itg2addnclem2  34826  fzmul  34899  incsequz2  34907  ellz1  39244  lzunuz  39245  lzenom  39247  nerabdioph  39286  pell14qrgt0  39336  rmxycomplete  39394  monotuz  39418  monotoddzzfi  39419  oddcomabszz  39421  zindbi  39423  jm2.24  39440  congrep  39450  fzneg  39459  jm2.19  39470  oddfl  41423  fzdifsuc2  41457  climsuse  41769  stoweidlem26  42192  stoweidlem34  42200  fourierdlem20  42293  fourierdlem42  42315  fourierdlem51  42323  fourierdlem64  42336  fourierdlem76  42348  fourierdlem94  42366  fourierdlem97  42369  fourierdlem113  42385  zm1nn  43383  zgeltp1eq  43390  eluzge0nn0  43393  elfz2z  43396  2elfz2melfz  43399  elfzlble  43401  elfzelfzlble  43402  fzopredsuc  43404  smonoord  43412  fsummmodsndifre  43415  iccpartipre  43428  iccpartiltu  43429  iccpartigtl  43430  icceuelpartlem  43442  fmtno4prmfac  43581  lighneallem4b  43621  dfeven3  43670  dfodd4  43671  nn0o1gt2ALTV  43706  nnoALTV  43707  fpprel2  43753  gbegt5  43773  gbowgt5  43774  sbgoldbwt  43789  nnsum3primesle9  43806  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  evengpop3  43810  evengpoap3  43811  nnsum4primesevenALTV  43813  bgoldbtbndlem1  43817  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbndlem4  43820  cznnring  44125  elfzolborelfzop1  44472  zgtp1leeq  44474  mod0mul  44477  modn0mul  44478  m1modmmod  44479  difmodm1lt  44480  rege1logbzge0  44517  fllog2  44526  dignn0ldlem  44560  dignn0flhalflem1  44573  dignn0flhalflem2  44574
  Copyright terms: Public domain W3C validator