Theorem zre 11973

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

Syntax hints:   → wi 4   ∨ w3o 1083   = wceq 1538   ∈ wcel 2111  ℝcr 10525  0cc0 10526  -cneg 10860  ℕcn 11625  ℤcz 11969

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862  df-z 11970

This theorem is referenced by:  zcn  11974  zrei  11975  zssre  11976  elnn0z  11982  elnnz1  11996  znnnlt1  11997  zletr  12014  znnsub  12016  znn0sub  12017  nzadd  12018  zltp1le  12020  zleltp1  12021  nn0ge0div  12039  zextle  12043  btwnnz  12046  suprzcl  12050  msqznn  12052  peano2uz2  12058  uzind  12062  fzind  12068  fnn0ind  12069  eluzuzle  12240  uzid  12246  uzneg  12251  uztric  12254  uz11  12255  eluzp1m1  12256  eluzp1p1  12258  eluzaddi  12259  eluzsubi  12260  subeluzsub  12263  uzin  12266  uz3m2nn  12279  peano2uz  12289  nn0pzuz  12293  uzwo  12299  eluz2b2  12309  uz2mulcl  12314  uzinfi  12316  eqreznegel  12322  lbzbi  12324  uzsupss  12328  nn01to3  12329  zmin  12332  zmax  12333  zbtwnre  12334  rebtwnz  12335  qre  12341  elpq  12362  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  z2ge  12579  qbtwnre  12580  zltaddlt1le  12883  elfz1eq  12913  fzn  12918  fzen  12919  uzsubsubfz  12924  fzaddel  12936  fzadd2  12937  ssfzunsnext  12947  ssfzunsn  12948  fzsuc2  12960  fzrev  12965  elfz1b  12971  fznuz  12984  uznfz  12985  fzp1nel  12986  elfz0fzfz0  13007  fz0fzelfz0  13008  fznn0sub2  13009  fz0fzdiffz0  13011  elfzmlbp  13013  difelfznle  13016  nelfzo  13038  elfzouz2  13047  fzo0n  13054  fzonlt0  13055  fzossrbm1  13061  fzospliti  13064  elfzo0z  13074  fzofzim  13079  fzo1fzo0n0  13083  eluzgtdifelfzo  13094  fzossfzop1  13110  ssfzoulel  13126  ssfzo12bi  13127  elfzonelfzo  13134  elfzomelpfzo  13136  elfznelfzob  13138  fzostep1  13148  fllt  13171  flid  13173  flbi2  13182  2tnp1ge0ge0  13194  flhalf  13195  fldiv4p1lem1div2  13200  fldiv4lem1div2uz2  13201  dfceil2  13204  ceile  13212  ceilid  13214  quoremz  13218  intfracq  13222  uzsup  13226  mulmod0  13240  zmod10  13250  zmodcl  13254  zmodfz  13256  zmodid2  13262  modcyc  13269  mulp1mod1  13275  modmuladd  13276  modmuladdim  13277  modmul1  13287  modaddmodup  13297  modaddmodlo  13298  modaddmulmod  13301  zsqcl2  13498  leexp2  13531  iexpcyc  13565  fi1uzind  13851  ccatsymb  13927  ccatval21sw  13930  lswccatn0lsw  13936  swrdnd  14007  swrdnnn0nd  14009  swrd0  14011  swrdswrdlem  14057  swrdswrd  14058  swrdccatin2  14082  pfxccatin12lem2  14084  pfxccatin12lem3  14085  repswswrd  14137  cshwmodn  14148  cshwsublen  14149  cshwidxmod  14156  cshwidxmodr  14157  cshwidxm1  14160  repswcshw  14165  2cshw  14166  cshweqrep  14174  cshw1  14175  swrd2lsw  14305  nn0abscl  14664  rexuzre  14704  dvdsval3  15603  p1modz1  15606  moddvds  15610  absdvdsb  15620  dvdsabsb  15621  dvdsle  15652  alzdvds  15662  mod2eq1n2dvds  15688  evennn02n  15691  evennn2n  15692  ltoddhalfle  15702  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  16422  setsstruct  16515  mulgmodid  18258  gexdvds  18701  zringunit  20181  prmirred  20188  znf1o  20243  chfacfscmul0  21463  chfacfscmulgsum  21465  chfacfpmmul0  21467  chfacfpmmulgsum  21469  dyadf  24195  dyadovol  24197  degltlem1  24673  coskpi  25115  cosne0  25121  relogexp  25187  cxpeq  25346  relogbzexp  25362  ppival2  25713  ppival2g  25714  ppiprm  25736  chtprm  25738  chtnprm  25739  ppip1le  25746  efexple  25865  zabsle1  25880  lgsdir2lem4  25912  lgsne0  25919  gausslemma2dlem1a  25949  gausslemma2dlem3  25952  gausslemma2dlem4  25953  lgsquadlem1  25964  lgsquadlem2  25965  2lgslem1a1  25973  2lgslem1a2  25974  2sqlem2  26002  rplogsumlem2  26069  pntrsumbnd  26150  axlowdim  26755  crctcshwlkn0lem3  27598  crctcshwlkn0lem5  27600  crctcshwlkn0  27607  crctcsh  27610  clwlkclwwlklem2fv2  27781  clwlkclwwlklem2a  27783  clwwisshclwwslemlem  27798  clwwlkinwwlk  27825  clwwlkext2edg  27841  wwlksubclwwlk  27843  numclwwlk5  28173  topnfbey  28254  uzssico  30533  rezh  31322  zrhre  31370  hashf2  31453  ballotlemfc0  31860  ballotlemfcc  31861  chpvalz  32009  chtvalz  32010  zltp1ne  32458  0nn0m1nnn0  32461  elfzm12  33031  nn0prpwlem  33783  poimirlem24  35081  mblfinlem1  35094  mblfinlem2  35095  itg2addnclem2  35109  fzmul  35179  incsequz2  35187  ellz1  39708  lzunuz  39709  lzenom  39711  nerabdioph  39750  pell14qrgt0  39800  rmxycomplete  39858  monotuz  39882  monotoddzzfi  39883  oddcomabszz  39885  zindbi  39887  jm2.24  39904  congrep  39914  fzneg  39923  jm2.19  39934  oddfl  41908  fzdifsuc2  41942  climsuse  42250  stoweidlem26  42668  stoweidlem34  42676  fourierdlem20  42769  fourierdlem42  42791  fourierdlem51  42799  fourierdlem64  42812  fourierdlem76  42824  fourierdlem94  42842  fourierdlem97  42845  fourierdlem113  42861  zm1nn  43859  zgeltp1eq  43866  eluzge0nn0  43869  elfz2z  43872  2elfz2melfz  43875  elfzlble  43877  elfzelfzlble  43878  fzopredsuc  43880  smonoord  43888  fsummmodsndifre  43891  iccpartipre  43938  iccpartiltu  43939  iccpartigtl  43940  icceuelpartlem  43952  fmtno4prmfac  44089  lighneallem4b  44127  dfeven3  44176  dfodd4  44177  nn0o1gt2ALTV  44212  nnoALTV  44213  fpprel2  44259  gbegt5  44279  gbowgt5  44280  sbgoldbwt  44295  nnsum3primesle9  44312  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  evengpop3  44316  evengpoap3  44317  nnsum4primesevenALTV  44319  bgoldbtbndlem1  44323  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbndlem4  44326  cznnring  44580  elfzolborelfzop1  44928  zgtp1leeq  44930  mod0mul  44933  modn0mul  44934  m1modmmod  44935  difmodm1lt  44936  rege1logbzge0  44973  fllog2  44982  dignn0ldlem  45016  dignn0flhalflem1  45029  dignn0flhalflem2  45030