Theorem zre 12594

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

Syntax hints:   → wi 4   ∨ w3o 1100   = wceq 1567   ∈ wcel 2149  ℝcr 11098  0cc0 11099  -cneg 11441  ℕcn 12232  ℤcz 12590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-neg 11443  df-z 12591

This theorem is referenced by:  zcn  12595  zrei  12596  zssre  12597  elnn0z  12603  elnnz1  12619  znnnlt1  12620  zletr  12637  znnsub  12639  znn0sub  12640  nzadd  12641  zltp1le  12643  zleltp1  12644  nn0ge0div  12664  zextle  12668  btwnnz  12671  suprzcl  12675  msqznn  12677  peano2uz2  12683  uzind  12687  fzind  12693  fnn0ind  12694  eluzuzle  12870  uzid  12876  uzneg  12881  uztric  12885  uz11  12886  eluzp1m1  12887  eluzp1p1  12889  eluzadd  12890  eluzsub  12891  subeluzsub  12894  uzin  12897  uz3m2nn  12917  peano2uz  12924  nn0pzuz  12928  uzwo  12934  eluz2b2  12944  uz2mulcl  12949  uzinfi  12951  eqreznegel  12957  lbzbi  12959  uzsupss  12963  nn01to3  12964  zmin  12967  zmax  12968  zbtwnre  12969  rebtwnz  12970  qre  12976  elpq  12998  rpnnen1lem2  13000  rpnnen1lem1  13001  rpnnen1lem3  13002  rpnnen1lem5  13004  z2ge  13223  qbtwnre  13224  zltaddlt1le  13531  elfz1eq  13562  fzn  13567  fzen  13568  uzsubsubfz  13573  fzaddel  13585  fzadd2  13586  ssfzunsnext  13596  ssfzunsn  13597  fzsuc2  13609  fzrev  13614  elfz1b  13620  fznuz  13636  uznfz  13637  fzp1nel  13638  elfz0fzfz0  13660  fz0fzelfz0  13661  fznn0sub2  13662  fz0fzdiffz0  13664  elfzmlbp  13666  difelfznle  13669  nelfzo  13692  elfzouz2  13702  fzo0n  13709  fzonlt0  13710  fzossrbm1  13716  fzospliti  13719  elfzo0z  13729  fzofzim  13737  fzo1fzo0n0  13743  eluzgtdifelfzo  13755  fzossfzop1  13771  ssfzoulel  13788  ssfzo12bi  13789  elfzonelfzo  13797  elfzomelpfzo  13800  elfznelfzob  13802  fzostep1  13814  fllt  13838  flid  13840  flbi2  13849  2tnp1ge0ge0  13861  flhalf  13862  fldiv4p1lem1div2  13867  fldiv4lem1div2uz2  13868  dfceil2  13871  ceile  13881  ceilid  13883  quoremz  13887  intfracq  13891  uzsup  13895  mulmod0  13909  zmod10  13919  zmodcl  13923  zmodfz  13925  zmodid2  13931  modcyc  13938  modaddid  13942  mulp1mod1  13946  muladdmod  13947  modmuladd  13948  modmuladdim  13949  modmul1  13959  modaddmodup  13969  modaddmodlo  13970  modaddmulmod  13973  zsqcl2  14173  leexp2  14206  iexpcyc  14242  fi1uzind  14543  ccatsymb  14619  ccatval21sw  14622  lswccatn0lsw  14628  swrdnd  14691  swrdnnn0nd  14693  swrd0  14695  swrdswrdlem  14740  swrdswrd  14741  swrdccatin2  14765  pfxccatin12lem2  14767  pfxccatin12lem3  14768  repswswrd  14820  cshwmodn  14831  cshwsublen  14832  cshwidxmod  14839  cshwidxmodr  14840  cshwidxm1  14843  repswcshw  14848  2cshw  14849  cshweqrep  14857  cshw1  14858  swrd2lsw  14988  nn0abscl  15362  rexuzre  15403  dvdsval3  16313  p1modz1  16316  moddvds  16320  absdvdsb  16331  dvdsabsb  16332  dvdsle  16367  alzdvds  16377  mod2eq1n2dvds  16404  evennn02n  16407  evennn2n  16408  ltoddhalfle  16418  divalgmod  16463  fldivndvdslt  16473  flodddiv4t2lthalf  16475  bitsp1o  16490  gcdabs1  16586  modgcd  16589  bezoutlem1  16596  dfgcd2  16603  algcvga  16636  lcmabs  16662  isprm3  16740  dvdsnprmd  16747  2mulprm  16750  oddprmgt2  16757  sqnprm  16760  zgcdsq  16811  hashdvds  16833  vfermltlALT  16861  powm2modprm  16862  modprm0  16864  modprmn0modprm0  16866  fldivp1  16956  zgz  16992  4sqlem4  17011  prmgaplem5  17114  prmgaplem7  17116  cshwshashlem2  17155  setsstruct  17235  mulgmodid  19178  gexdvds  19653  zringunit  21584  prmirred  21592  znf1o  21669  chfacfscmul0  22983  chfacfscmulgsum  22985  chfacfpmmul0  22987  chfacfpmmulgsum  22989  dyadf  25718  dyadovol  25720  degltlem1  26197  coskpi  26653  cosne0  26659  relogexp  26726  cxpeq  26887  relogbzexp  26906  ppival2  27257  ppival2g  27258  ppiprm  27280  chtprm  27282  chtnprm  27283  ppip1le  27290  efexple  27410  zabsle1  27425  lgsdir2lem4  27457  lgsne0  27464  gausslemma2dlem1a  27494  gausslemma2dlem3  27497  gausslemma2dlem4  27498  lgsquadlem1  27509  lgsquadlem2  27510  2lgslem1a1  27518  2lgslem1a2  27519  2sqlem2  27547  rplogsumlem2  27614  pntrsumbnd  27695  axlowdim  29251  crctcshwlkn0lem3  30101  crctcshwlkn0lem5  30103  crctcshwlkn0  30110  crctcsh  30113  clwlkclwwlklem2fv2  30287  clwlkclwwlklem2a  30289  clwwisshclwwslemlem  30304  clwwlkinwwlk  30331  clwwlkext2edg  30347  wwlksubclwwlk  30349  numclwwlk5  30679  topnfbey  30760  uzssico  33069  1fldgenq  33585  znfermltl  33623  ply1coedeg  33823  rezh  34303  zrhre  34353  hashf2  34418  ballotlemfc0  34827  ballotlemfcc  34828  chpvalz  34959  chtvalz  34960  zltp1ne  35499  0nn0m1nnn0  35502  elfzm12  36065  nn0prpwlem  36721  poimirlem24  38182  mblfinlem1  38195  mblfinlem2  38196  itg2addnclem2  38210  fzmul  38279  incsequz2  38287  fimgmcyc  43193  ellz1  43389  lzunuz  43390  lzenom  43392  nerabdioph  43427  pell14qrgt0  43477  rmxycomplete  43535  monotuz  43559  monotoddzzfi  43560  oddcomabszz  43562  zindbi  43564  jm2.24  43581  congrep  43591  fzneg  43600  jm2.19  43611  fzunt  44072  fzunt1d  44074  fzuntgd  44075  oddfl  45888  fzdifsuc2  45920  climsuse  46215  stoweidlem26  46631  stoweidlem34  46639  fourierdlem20  46732  fourierdlem42  46754  fourierdlem51  46762  fourierdlem64  46775  fourierdlem76  46787  fourierdlem94  46805  fourierdlem97  46808  fourierdlem113  46824  natlocalincr  47483  natglobalincr  47484  zm1nn  47927  zgeltp1eq  47934  eluzge0nn0  47937  elfz2z  47940  2elfz2melfz  47943  elfzlble  47945  elfzelfzlble  47946  fzopredsuc  47949  ceilbi  47962  mod0mul  47987  modn0mul  47988  m1modmmod  47989  difmodm1lt  47990  mod2addne  47995  modm2nep1  47997  modp2nep1  47998  modm1nep2  47999  modm1nem2  48000  modm1p1ne  48001  smonoord  48002  2timesltsqm1  48004  fsummmodsndifre  48007  muldvdsfacgt  48011  muldvdsfacm1  48012  iccpartipre  48058  iccpartiltu  48059  iccpartigtl  48060  icceuelpartlem  48072  fmtno4prmfac  48212  lighneallem4b  48249  nprmdvdsfacm1lem2  48261  nprmdvdsfacm1lem4  48263  dfeven3  48311  dfodd4  48312  nn0o1gt2ALTV  48347  nnoALTV  48348  fpprel2  48394  gbegt5  48414  gbowgt5  48415  sbgoldbwt  48430  nnsum3primesle9  48447  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  evengpop3  48451  evengpoap3  48452  nnsum4primesevenALTV  48454  bgoldbtbndlem1  48458  bgoldbtbndlem2  48459  bgoldbtbndlem3  48460  bgoldbtbndlem4  48461  gpgprismgriedgdmss  48705  gpgusgralem  48709  gpgedgvtx1  48715  gpg5nbgrvtx03starlem2  48722  gpg5nbgrvtx13starlem2  48725  gpg3nbgrvtx0  48729  cznnring  48915  elfzolborelfzop1  49183  zgtp1leeq  49185  rege1logbzge0  49223  fllog2  49232  dignn0ldlem  49266  dignn0flhalflem1  49279  dignn0flhalflem2  49280