Theorem zre 12533

Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
zre	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre

Step	Hyp	Ref	Expression
1		elz 12531	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 497	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11067  0cc0 11068  -cneg 11406  ℕcn 12186  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  zcn  12534  zrei  12535  zssre  12536  elnn0z  12542  elnnz1  12559  znnnlt1  12560  zletr  12577  znnsub  12579  znn0sub  12580  nzadd  12581  zltp1le  12583  zleltp1  12584  nn0ge0div  12603  zextle  12607  btwnnz  12610  suprzcl  12614  msqznn  12616  peano2uz2  12622  uzind  12626  fzind  12632  fnn0ind  12633  eluzuzle  12802  uzid  12808  uzneg  12813  uztric  12817  uz11  12818  eluzp1m1  12819  eluzp1p1  12821  eluzadd  12822  eluzsub  12823  eluzaddiOLD  12825  eluzsubiOLD  12827  subeluzsub  12830  uzin  12833  uz3m2nn  12853  peano2uz  12860  nn0pzuz  12864  uzwo  12870  eluz2b2  12880  uz2mulcl  12885  uzinfi  12887  eqreznegel  12893  lbzbi  12895  uzsupss  12899  nn01to3  12900  zmin  12903  zmax  12904  zbtwnre  12905  rebtwnz  12906  qre  12912  elpq  12934  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  z2ge  13158  qbtwnre  13159  zltaddlt1le  13466  elfz1eq  13496  fzn  13501  fzen  13502  uzsubsubfz  13507  fzaddel  13519  fzadd2  13520  ssfzunsnext  13530  ssfzunsn  13531  fzsuc2  13543  fzrev  13548  elfz1b  13554  fznuz  13570  uznfz  13571  fzp1nel  13572  elfz0fzfz0  13594  fz0fzelfz0  13595  fznn0sub2  13596  fz0fzdiffz0  13598  elfzmlbp  13600  difelfznle  13603  nelfzo  13625  elfzouz2  13635  fzo0n  13642  fzonlt0  13643  fzossrbm1  13649  fzospliti  13652  elfzo0z  13662  fzofzim  13670  fzo1fzo0n0  13676  eluzgtdifelfzo  13688  fzossfzop1  13704  ssfzoulel  13721  ssfzo12bi  13722  elfzonelfzo  13730  elfzomelpfzo  13732  elfznelfzob  13734  fzostep1  13744  fllt  13768  flid  13770  flbi2  13779  2tnp1ge0ge0  13791  flhalf  13792  fldiv4p1lem1div2  13797  fldiv4lem1div2uz2  13798  dfceil2  13801  ceile  13811  ceilid  13813  quoremz  13817  intfracq  13821  uzsup  13825  mulmod0  13839  zmod10  13849  zmodcl  13853  zmodfz  13855  zmodid2  13861  modcyc  13868  modaddid  13872  mulp1mod1  13876  muladdmod  13877  modmuladd  13878  modmuladdim  13879  modmul1  13889  modaddmodup  13899  modaddmodlo  13900  modaddmulmod  13903  zsqcl2  14103  leexp2  14136  iexpcyc  14172  fi1uzind  14472  ccatsymb  14547  ccatval21sw  14550  lswccatn0lsw  14556  swrdnd  14619  swrdnnn0nd  14621  swrd0  14623  swrdswrdlem  14669  swrdswrd  14670  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12lem3  14697  repswswrd  14749  cshwmodn  14760  cshwsublen  14761  cshwidxmod  14768  cshwidxmodr  14769  cshwidxm1  14772  repswcshw  14777  2cshw  14778  cshweqrep  14786  cshw1  14787  swrd2lsw  14918  nn0abscl  15278  rexuzre  15319  dvdsval3  16226  p1modz1  16229  moddvds  16233  absdvdsb  16244  dvdsabsb  16245  dvdsle  16280  alzdvds  16290  mod2eq1n2dvds  16317  evennn02n  16320  evennn2n  16321  ltoddhalfle  16331  divalgmod  16376  fldivndvdslt  16386  flodddiv4t2lthalf  16388  bitsp1o  16403  gcdabs1  16499  modgcd  16502  bezoutlem1  16509  dfgcd2  16516  algcvga  16549  lcmabs  16575  isprm3  16653  dvdsnprmd  16660  2mulprm  16663  oddprmgt2  16669  sqnprm  16672  zgcdsq  16723  hashdvds  16745  vfermltlALT  16773  powm2modprm  16774  modprm0  16776  modprmn0modprm0  16778  fldivp1  16868  zgz  16904  4sqlem4  16923  prmgaplem5  17026  prmgaplem7  17028  cshwshashlem2  17067  setsstruct  17146  mulgmodid  19045  gexdvds  19514  zringunit  21376  prmirred  21384  znf1o  21461  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  dyadf  25492  dyadovol  25494  degltlem1  25977  coskpi  26432  cosne0  26438  relogexp  26505  cxpeq  26667  relogbzexp  26686  ppival2  27038  ppival2g  27039  ppiprm  27061  chtprm  27063  chtnprm  27064  ppip1le  27071  efexple  27192  zabsle1  27207  lgsdir2lem4  27239  lgsne0  27246  gausslemma2dlem1a  27276  gausslemma2dlem3  27279  gausslemma2dlem4  27280  lgsquadlem1  27291  lgsquadlem2  27292  2lgslem1a1  27300  2lgslem1a2  27301  2sqlem2  27329  rplogsumlem2  27396  pntrsumbnd  27477  axlowdim  28888  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  crctcshwlkn0  29751  crctcsh  29754  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a  29927  clwwisshclwwslemlem  29942  clwwlkinwwlk  29969  clwwlkext2edg  29985  wwlksubclwwlk  29987  numclwwlk5  30317  topnfbey  30398  uzssico  32707  1fldgenq  33272  znfermltl  33337  rezh  33959  zrhre  34009  hashf2  34074  ballotlemfc0  34484  ballotlemfcc  34485  chpvalz  34619  chtvalz  34620  zltp1ne  35097  0nn0m1nnn0  35100  elfzm12  35662  nn0prpwlem  36310  poimirlem24  37638  mblfinlem1  37651  mblfinlem2  37652  itg2addnclem2  37666  fzmul  37735  incsequz2  37743  fimgmcyc  42522  ellz1  42755  lzunuz  42756  lzenom  42758  nerabdioph  42797  pell14qrgt0  42847  rmxycomplete  42906  monotuz  42930  monotoddzzfi  42931  oddcomabszz  42933  zindbi  42935  jm2.24  42952  congrep  42962  fzneg  42971  jm2.19  42982  fzunt  43444  fzunt1d  43446  fzuntgd  43447  oddfl  45276  fzdifsuc2  45308  climsuse  45606  stoweidlem26  46024  stoweidlem34  46032  fourierdlem20  46125  fourierdlem42  46147  fourierdlem51  46155  fourierdlem64  46168  fourierdlem76  46180  fourierdlem94  46198  fourierdlem97  46201  fourierdlem113  46217  natlocalincr  46874  natglobalincr  46875  zm1nn  47303  zgeltp1eq  47310  eluzge0nn0  47313  elfz2z  47316  2elfz2melfz  47319  elfzlble  47321  elfzelfzlble  47322  fzopredsuc  47324  ceilbi  47334  mod0mul  47357  modn0mul  47358  m1modmmod  47359  difmodm1lt  47360  mod2addne  47365  modm2nep1  47367  modp2nep1  47368  modm1nep2  47369  modm1nem2  47370  modm1p1ne  47371  smonoord  47372  fsummmodsndifre  47375  iccpartipre  47422  iccpartiltu  47423  iccpartigtl  47424  icceuelpartlem  47436  fmtno4prmfac  47573  lighneallem4b  47610  dfeven3  47659  dfodd4  47660  nn0o1gt2ALTV  47695  nnoALTV  47696  fpprel2  47742  gbegt5  47762  gbowgt5  47763  sbgoldbwt  47778  nnsum3primesle9  47795  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  evengpop3  47799  evengpoap3  47800  nnsum4primesevenALTV  47802  bgoldbtbndlem1  47806  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  gpgprismgriedgdmss  48043  gpgusgralem  48047  gpgedgvtx1  48053  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  gpg3nbgrvtx0  48067  cznnring  48250  elfzolborelfzop1  48508  zgtp1leeq  48510  rege1logbzge0  48548  fllog2  48557  dignn0ldlem  48591  dignn0flhalflem1  48604  dignn0flhalflem2  48605