Theorem zre 12737

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2147  ℝcr 11238  0cc0 11239   -cneg 11581  ℕcn 12375  ℤcz 12733

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-neg 11583  df-z 12734

This theorem is used by:  zcn  12738  zrei  12739  zssre  12740  elnn0z  12746  elnnz1  12762  znnnlt1  12763  zletr  12780  znnsub  12782  znn0sub  12783  nzadd  12784  zltp1le  12786  zleltp1  12787  0nn0m1nnn0  12793  nn0ge0div  12808  zextle  12812  btwnnz  12815  suprzcl  12819  msqznn  12821  peano2uz2  12827  uzind  12831  fzind  12837  fnn0ind  12838  eluzuzle  13014  uzid  13020  uzneg  13025  uztric  13029  uz11  13030  eluzp1m1  13031  eluzp1p1  13033  eluzadd  13034  eluzsub  13035  subeluzsub  13038  uzin  13041  uz3m2nn  13061  peano2uz  13068  nn0pzuz  13072  uzwo  13078  eluz2b2  13088  uz2mulcl  13093  uzinfi  13095  eqreznegel  13101  lbzbi  13103  uzsupss  13107  nn01to3  13108  zmin  13111  zmax  13112  zbtwnre  13113  rebtwnz  13114  qre  13120  elpq  13143  rpnnen1lem2  13145  rpnnen1lem1  13146  rpnnen1lem3  13147  rpnnen1lem5  13149  z2ge  13368  qbtwnre  13369  zltaddlt1le  13676  elfz1eq  13708  fzn  13713  fzen  13714  uzsubsubfz  13720  fzaddel  13732  fzadd2  13733  ssfzunsnext  13743  ssfzunsn  13744  fzsuc2  13756  fzrev  13761  elfz1b  13767  fznuz  13783  uznfz  13784  fzp1nel  13785  elfz0fzfz0  13807  fz0fzelfz0  13808  fznn0sub2  13809  fz0fzdiffz0  13811  elfzmlbp  13813  difelfznle  13816  nelfzo  13839  elfzouz2  13849  fzo0n  13856  fzonlt0  13857  fzossrbm1  13863  fzospliti  13866  elfzo0z  13876  fzofzim  13884  fzo1fzo0n0  13890  eluzgtdifelfzo  13902  fzossfzop1  13918  ssfzoulel  13935  ssfzo12bi  13936  elfzonelfzo  13944  elfzomelpfzo  13947  elfznelfzob  13949  fzostep1  13961  fllt  13986  flid  13988  flbi2  13997  2tnp1ge0ge0  14009  flhalf  14010  fldiv4p1lem1div2  14015  fldiv4lem1div2uz2  14016  dfceil2  14019  ceile  14029  ceilid  14031  quoremz  14035  intfracq  14039  uzsup  14043  mulmod0  14057  zmod10  14067  zmodcl  14071  zmodfz  14073  zmodid2  14079  modcyc  14086  modaddid  14090  mulp1mod1  14094  muladdmod  14095  modmuladd  14096  modmuladdim  14097  modmul1  14107  modaddmodup  14117  modaddmodlo  14118  modaddmulmod  14121  zsqcl2  14321  leexp2  14354  iexpcyc  14391  fi1uzind  14693  ccatsymb  14769  ccatval21sw  14772  lswccatn0lsw  14779  swrdnd  14846  swrdnnn0nd  14848  swrd0  14850  swrdswrdlem  14895  swrdswrd  14896  swrdccatin2  14920  pfxccatin12lem2  14922  pfxccatin12lem3  14923  repswswrd  14977  cshwmodn  14988  cshwsublen  14989  cshwidxmod  14996  cshwidxmodr  14997  cshwidxm1  15000  repswcshw  15005  2cshw  15006  cshweqrep  15014  cshw1  15015  swrd2lsw  15148  nn0abscl  15522  rexuzre  15564  dvdsval3  16470  p1modz1  16473  moddvds  16477  absdvdsb  16488  dvdsabsb  16489  dvdsle  16524  alzdvds  16534  mod2eq1n2dvds  16561  evennn02n  16564  evennn2n  16565  ltoddhalfle  16575  divalgmod  16620  fldivndvdslt  16630  flodddiv4t2lthalf  16632  bitsp1o  16647  gcdabs1  16746  modgcd  16749  bezoutlem1  16756  dfgcd2  16763  algcvga  16798  lcmabs  16824  isprm3  16902  dvdsnprmd  16909  2mulprm  16912  oddprmgt2  16919  sqnprm  16922  zgcdsq  16973  hashdvds  16996  vfermltlALT  17024  powm2modprm  17025  modprm0  17027  modprmn0modprm0  17029  fldivp1  17119  zgz  17155  4sqlem4  17174  prmgaplem5  17277  prmgaplem7  17279  cshwshashlem2  17318  setsstruct  17398  mulgmodid  19373  gexdvds  19849  zringunit  21827  prmirred  21835  znf1o  21912  chfacfscmul0  23231  chfacfscmulgsum  23233  chfacfpmmul0  23235  chfacfpmmulgsum  23237  dyadf  25967  dyadovol  25969  degltlem1  26445  coskpi  26908  cosne0  26914  relogexp  26981  cxpeq  27142  relogbzexp  27161  ppival2  27512  ppival2g  27513  ppiprm  27535  chtprm  27537  chtnprm  27538  ppip1le  27545  efexple  27665  zabsle1  27680  lgsdir2lem4  27712  lgsne0  27719  gausslemma2dlem1a  27749  gausslemma2dlem3  27752  gausslemma2dlem4  27753  lgsquadlem1  27764  lgsquadlem2  27765  2lgslem1a1  27773  2lgslem1a2  27774  2sqlem2  27802  rplogsumlem2  27869  pntrsumbnd  27950  fltoprmgt3  28053  axlowdim  29596  crctcshwlkn0lem3  30458  crctcshwlkn0lem5  30460  crctcshwlkn0  30467  crctcsh  30470  clwlkclwwlklem2fv2  30644  clwlkclwwlklem2a  30646  clwwisshclwwslemlem  30661  clwwlkinwwlk  30688  clwwlkext2edg  30704  wwlksubclwwlk  30706  numclwwlk5  31046  topnfbey  31127  uzssico  33472  1fldgenq  33988  znfermltl  34026  ply1coedeg  34224  rezh  34712  zrhre  34762  hashf2  34827  ballotlemfc0  35236  ballotlemfcc  35237  chpvalz  35368  chtvalz  35369  zltp1ne  36098  elfzm12  36648  nn0prpwlem  37325  poimirlem24  38830  mblfinlem1  38843  mblfinlem2  38844  itg2addnclem2  38858  fzmul  38941  incsequz2  38949  fimgmcyc  43864  ellz1  44044  lzunuz  44045  lzenom  44047  nerabdioph  44082  pell14qrgt0  44132  rmxycomplete  44190  monotuz  44214  monotoddzzfi  44215  oddcomabszz  44217  zindbi  44219  jm2.24  44236  congrep  44246  fzneg  44255  jm2.19  44266  fzunt  44717  fzunt1d  44719  fzuntgd  44720  oddfl  46567  fzdifsuc2  46599  climsuse  46893  stoweidlem26  47309  stoweidlem34  47317  fourierdlem20  47410  fourierdlem42  47432  fourierdlem51  47440  fourierdlem64  47453  fourierdlem76  47465  fourierdlem94  47483  fourierdlem97  47486  fourierdlem113  47502  zm1nn  48645  zgeltp1eq  48652  eluzge0nn0  48655  elfz2z  48658  2elfz2melfz  48661  elfzlble  48663  elfzelfzlble  48664  fzopredsuc  48667  ceilbi  48680  mod0mul  48705  modn0mul  48706  m1modmmod  48707  difmodm1lt  48708  mod2addne  48713  modm2nep1  48715  modp2nep1  48716  modm1nep2  48717  modm1nem2  48718  modm1p1ne  48719  smonoord  48720  2timesltsqm1  48722  fsummmodsndifre  48725  muldvdsfacgt  48729  muldvdsfacm1  48730  iccpartipre  48776  iccpartiltu  48777  iccpartigtl  48778  icceuelpartlem  48790  fmtno4prmfac  48930  lighneallem4b  48967  nprmdvdsfacm1lem2  48979  nprmdvdsfacm1lem4  48981  dfeven3  49029  dfodd4  49030  nn0o1gt2ALTV  49065  nnoALTV  49066  fpprel2  49112  gbegt5  49132  gbowgt5  49133  sbgoldbwt  49148  nnsum3primesle9  49165  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  evengpop3  49169  evengpoap3  49170  nnsum4primesevenALTV  49172  bgoldbtbndlem1  49176  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  bgoldbtbndlem4  49179  gpgprismgriedgdmss  49423  gpgusgralem  49427  gpgedgvtx1  49433  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx13starlem2  49443  gpg3nbgrvtx0  49447  cznnring  49632  gzilaz  49735  lazcjcl  49741  elfzolborelfzop1  49962  zgtp1leeq  49964  rege1logbzge0  50002  fllog2  50011  dignn0ldlem  50045  dignn0flhalflem1  50058  dignn0flhalflem2  50059