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 1080   = wceq 1530  wcel 2107  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 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6312  df-fv 6360  df-ov 7151  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  18196  gexdvds  18629  zringunit  20551  prmirred  20558  znf1o  20614  chfacfscmul0  21382  chfacfscmulgsum  21384  chfacfpmmul0  21386  chfacfpmmulgsum  21388  dyadf  24107  dyadovol  24109  degltlem1  24581  coskpi  25023  cosne0  25027  relogexp  25092  cxpeq  25251  relogbzexp  25267  ppival2  25619  ppival2g  25620  ppiprm  25642  chtprm  25644  chtnprm  25645  ppip1le  25652  efexple  25771  zabsle1  25786  lgsdir2lem4  25818  lgsne0  25825  gausslemma2dlem1a  25855  gausslemma2dlem3  25858  gausslemma2dlem4  25859  lgsquadlem1  25870  lgsquadlem2  25871  2lgslem1a1  25879  2lgslem1a2  25880  2sqlem2  25908  rplogsumlem2  25975  pntrsumbnd  26056  axlowdim  26661  crctcshwlkn0lem3  27504  crctcshwlkn0lem5  27506  crctcshwlkn0  27513  crctcsh  27516  clwlkclwwlklem2fv2  27688  clwlkclwwlklem2a  27690  clwwisshclwwslemlem  27705  clwwlkinwwlk  27732  clwwlkext2edg  27749  wwlksubclwwlk  27751  numclwwlk5  28081  topnfbey  28162  uzssico  30420  rezh  31098  zrhre  31146  hashf2  31229  ballotlemfc0  31636  ballotlemfcc  31637  chpvalz  31785  chtvalz  31786  zltp1ne  32232  0nn0m1nnn0  32235  elfzm12  32802  nn0prpwlem  33554  poimirlem24  34783  mblfinlem1  34796  mblfinlem2  34797  itg2addnclem2  34811  fzmul  34884  incsequz2  34892  ellz1  39229  lzunuz  39230  lzenom  39232  nerabdioph  39271  pell14qrgt0  39321  rmxycomplete  39379  monotuz  39403  monotoddzzfi  39404  oddcomabszz  39406  zindbi  39408  jm2.24  39425  congrep  39435  fzneg  39444  jm2.19  39455  oddfl  41408  fzdifsuc2  41442  climsuse  41754  stoweidlem26  42177  stoweidlem34  42185  fourierdlem20  42278  fourierdlem42  42300  fourierdlem51  42308  fourierdlem64  42321  fourierdlem76  42333  fourierdlem94  42351  fourierdlem97  42354  fourierdlem113  42370  zm1nn  43368  zgeltp1eq  43375  eluzge0nn0  43378  elfz2z  43381  2elfz2melfz  43384  elfzlble  43386  elfzelfzlble  43387  fzopredsuc  43389  smonoord  43397  fsummmodsndifre  43400  iccpartipre  43413  iccpartiltu  43414  iccpartigtl  43415  icceuelpartlem  43427  fmtno4prmfac  43566  lighneallem4b  43606  dfeven3  43655  dfodd4  43656  nn0o1gt2ALTV  43691  nnoALTV  43692  fpprel2  43738  gbegt5  43758  gbowgt5  43759  sbgoldbwt  43774  nnsum3primesle9  43791  nnsum4primesodd  43793  nnsum4primesoddALTV  43794  evengpop3  43795  evengpoap3  43796  nnsum4primesevenALTV  43798  bgoldbtbndlem1  43802  bgoldbtbndlem2  43803  bgoldbtbndlem3  43804  bgoldbtbndlem4  43805  cznnring  44059  elfzolborelfzop1  44406  zgtp1leeq  44408  mod0mul  44411  modn0mul  44412  m1modmmod  44413  difmodm1lt  44414  rege1logbzge0  44451  fllog2  44460  dignn0ldlem  44494  dignn0flhalflem1  44507  dignn0flhalflem2  44508
  Copyright terms: Public domain W3C validator