Theorem zre 12522

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 12520	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 496	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11031  0cc0 11032  -cneg 11372  ℕcn 12168  ℤcz 12518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-neg 11374  df-z 12519

This theorem is referenced by:  zcn  12523  zrei  12524  zssre  12525  elnn0z  12531  elnnz1  12547  znnnlt1  12548  zletr  12565  znnsub  12567  znn0sub  12568  nzadd  12569  zltp1le  12571  zleltp1  12572  nn0ge0div  12592  zextle  12596  btwnnz  12599  suprzcl  12603  msqznn  12605  peano2uz2  12611  uzind  12615  fzind  12621  fnn0ind  12622  eluzuzle  12791  uzid  12797  uzneg  12802  uztric  12806  uz11  12807  eluzp1m1  12808  eluzp1p1  12810  eluzadd  12811  eluzsub  12812  subeluzsub  12815  uzin  12818  uz3m2nn  12838  peano2uz  12845  nn0pzuz  12849  uzwo  12855  eluz2b2  12865  uz2mulcl  12870  uzinfi  12872  eqreznegel  12878  lbzbi  12880  uzsupss  12884  nn01to3  12885  zmin  12888  zmax  12889  zbtwnre  12890  rebtwnz  12891  qre  12897  elpq  12919  rpnnen1lem2  12921  rpnnen1lem1  12922  rpnnen1lem3  12923  rpnnen1lem5  12925  z2ge  13144  qbtwnre  13145  zltaddlt1le  13452  elfz1eq  13483  fzn  13488  fzen  13489  uzsubsubfz  13494  fzaddel  13506  fzadd2  13507  ssfzunsnext  13517  ssfzunsn  13518  fzsuc2  13530  fzrev  13535  elfz1b  13541  fznuz  13557  uznfz  13558  fzp1nel  13559  elfz0fzfz0  13581  fz0fzelfz0  13582  fznn0sub2  13583  fz0fzdiffz0  13585  elfzmlbp  13587  difelfznle  13590  nelfzo  13613  elfzouz2  13623  fzo0n  13630  fzonlt0  13631  fzossrbm1  13637  fzospliti  13640  elfzo0z  13650  fzofzim  13658  fzo1fzo0n0  13664  eluzgtdifelfzo  13676  fzossfzop1  13692  ssfzoulel  13709  ssfzo12bi  13710  elfzonelfzo  13718  elfzomelpfzo  13721  elfznelfzob  13723  fzostep1  13735  fllt  13759  flid  13761  flbi2  13770  2tnp1ge0ge0  13782  flhalf  13783  fldiv4p1lem1div2  13788  fldiv4lem1div2uz2  13789  dfceil2  13792  ceile  13802  ceilid  13804  quoremz  13808  intfracq  13812  uzsup  13816  mulmod0  13830  zmod10  13840  zmodcl  13844  zmodfz  13846  zmodid2  13852  modcyc  13859  modaddid  13863  mulp1mod1  13867  muladdmod  13868  modmuladd  13869  modmuladdim  13870  modmul1  13880  modaddmodup  13890  modaddmodlo  13891  modaddmulmod  13894  zsqcl2  14094  leexp2  14127  iexpcyc  14163  fi1uzind  14463  ccatsymb  14539  ccatval21sw  14542  lswccatn0lsw  14548  swrdnd  14611  swrdnnn0nd  14613  swrd0  14615  swrdswrdlem  14660  swrdswrd  14661  swrdccatin2  14685  pfxccatin12lem2  14687  pfxccatin12lem3  14688  repswswrd  14740  cshwmodn  14751  cshwsublen  14752  cshwidxmod  14759  cshwidxmodr  14760  cshwidxm1  14763  repswcshw  14768  2cshw  14769  cshweqrep  14777  cshw1  14778  swrd2lsw  14908  nn0abscl  15268  rexuzre  15309  dvdsval3  16219  p1modz1  16222  moddvds  16226  absdvdsb  16237  dvdsabsb  16238  dvdsle  16273  alzdvds  16283  mod2eq1n2dvds  16310  evennn02n  16313  evennn2n  16314  ltoddhalfle  16324  divalgmod  16369  fldivndvdslt  16379  flodddiv4t2lthalf  16381  bitsp1o  16396  gcdabs1  16492  modgcd  16495  bezoutlem1  16502  dfgcd2  16509  algcvga  16542  lcmabs  16568  isprm3  16646  dvdsnprmd  16653  2mulprm  16656  oddprmgt2  16663  sqnprm  16666  zgcdsq  16717  hashdvds  16739  vfermltlALT  16767  powm2modprm  16768  modprm0  16770  modprmn0modprm0  16772  fldivp1  16862  zgz  16898  4sqlem4  16917  prmgaplem5  17020  prmgaplem7  17022  cshwshashlem2  17061  setsstruct  17140  mulgmodid  19083  gexdvds  19553  zringunit  21459  prmirred  21467  znf1o  21544  chfacfscmul0  22836  chfacfscmulgsum  22838  chfacfpmmul0  22840  chfacfpmmulgsum  22842  dyadf  25571  dyadovol  25573  degltlem1  26050  coskpi  26503  cosne0  26509  relogexp  26576  cxpeq  26737  relogbzexp  26756  ppival2  27108  ppival2g  27109  ppiprm  27131  chtprm  27133  chtnprm  27134  ppip1le  27141  efexple  27261  zabsle1  27276  lgsdir2lem4  27308  lgsne0  27315  gausslemma2dlem1a  27345  gausslemma2dlem3  27348  gausslemma2dlem4  27349  lgsquadlem1  27360  lgsquadlem2  27361  2lgslem1a1  27369  2lgslem1a2  27370  2sqlem2  27398  rplogsumlem2  27465  pntrsumbnd  27546  axlowdim  29047  crctcshwlkn0lem3  29898  crctcshwlkn0lem5  29900  crctcshwlkn0  29907  crctcsh  29910  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a  30086  clwwisshclwwslemlem  30101  clwwlkinwwlk  30128  clwwlkext2edg  30144  wwlksubclwwlk  30146  numclwwlk5  30476  topnfbey  30557  uzssico  32875  1fldgenq  33401  znfermltl  33444  ply1coedeg  33667  rezh  34132  zrhre  34182  hashf2  34247  ballotlemfc0  34656  ballotlemfcc  34657  chpvalz  34791  chtvalz  34792  zltp1ne  35311  0nn0m1nnn0  35314  elfzm12  35876  nn0prpwlem  36523  poimirlem24  37982  mblfinlem1  37995  mblfinlem2  37996  itg2addnclem2  38010  fzmul  38079  incsequz2  38087  fimgmcyc  42996  ellz1  43216  lzunuz  43217  lzenom  43219  nerabdioph  43258  pell14qrgt0  43308  rmxycomplete  43366  monotuz  43390  monotoddzzfi  43391  oddcomabszz  43393  zindbi  43395  jm2.24  43412  congrep  43422  fzneg  43431  jm2.19  43442  fzunt  43903  fzunt1d  43905  fzuntgd  43906  oddfl  45732  fzdifsuc2  45764  climsuse  46059  stoweidlem26  46475  stoweidlem34  46483  fourierdlem20  46576  fourierdlem42  46598  fourierdlem51  46606  fourierdlem64  46619  fourierdlem76  46631  fourierdlem94  46649  fourierdlem97  46652  fourierdlem113  46668  natlocalincr  47325  natglobalincr  47326  zm1nn  47765  zgeltp1eq  47772  eluzge0nn0  47775  elfz2z  47778  2elfz2melfz  47781  elfzlble  47783  elfzelfzlble  47784  fzopredsuc  47787  ceilbi  47800  mod0mul  47825  modn0mul  47826  m1modmmod  47827  difmodm1lt  47828  mod2addne  47833  modm2nep1  47835  modp2nep1  47836  modm1nep2  47837  modm1nem2  47838  modm1p1ne  47839  smonoord  47840  2timesltsqm1  47842  fsummmodsndifre  47845  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartipre  47896  iccpartiltu  47897  iccpartigtl  47898  icceuelpartlem  47910  fmtno4prmfac  48050  lighneallem4b  48087  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem4  48101  dfeven3  48149  dfodd4  48150  nn0o1gt2ALTV  48185  nnoALTV  48186  fpprel2  48232  gbegt5  48252  gbowgt5  48253  sbgoldbwt  48268  nnsum3primesle9  48285  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  evengpop3  48289  evengpoap3  48290  nnsum4primesevenALTV  48292  bgoldbtbndlem1  48296  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  gpgprismgriedgdmss  48543  gpgusgralem  48547  gpgedgvtx1  48553  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  cznnring  48753  elfzolborelfzop1  49010  zgtp1leeq  49012  rege1logbzge0  49050  fllog2  49059  dignn0ldlem  49093  dignn0flhalflem1  49106  dignn0flhalflem2  49107