Theorem zre 11986

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

Syntax hints:   → wi 4   ∨ w3o 1082   = wceq 1537   ∈ wcel 2114  ℝcr 10536  0cc0 10537  -cneg 10871  ℕcn 11638  ℤcz 11982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-neg 10873  df-z 11983

This theorem is referenced by:  zcn  11987  zrei  11988  zssre  11989  elnn0z  11995  elnnz1  12009  znnnlt1  12010  zletr  12027  znnsub  12029  znn0sub  12030  nzadd  12031  zltp1le  12033  zleltp1  12034  nn0ge0div  12052  zextle  12056  btwnnz  12059  suprzcl  12063  msqznn  12065  peano2uz2  12071  uzind  12075  fzind  12081  fnn0ind  12082  eluzuzle  12253  uzid  12259  uzneg  12264  uztric  12267  uz11  12268  eluzp1m1  12269  eluzp1p1  12271  eluzaddi  12272  eluzsubi  12273  subeluzsub  12276  uzin  12279  uz3m2nn  12292  peano2uz  12302  nn0pzuz  12306  uzwo  12312  eluz2b2  12322  uz2mulcl  12327  uzinfi  12329  eqreznegel  12335  lbzbi  12337  uzsupss  12341  nn01to3  12342  zmin  12345  zmax  12346  zbtwnre  12347  rebtwnz  12348  qre  12354  elpq  12375  rpnnen1lem2  12377  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  z2ge  12592  qbtwnre  12593  zltaddlt1le  12891  elfz1eq  12919  fzn  12924  fzen  12925  uzsubsubfz  12930  fzaddel  12942  fzadd2  12943  ssfzunsnext  12953  ssfzunsn  12954  fzsuc2  12966  fzrev  12971  elfz1b  12977  fznuz  12990  uznfz  12991  fzp1nel  12992  elfz0fzfz0  13013  fz0fzelfz0  13014  fznn0sub2  13015  fz0fzdiffz0  13017  elfzmlbp  13019  difelfznle  13022  nelfzo  13044  elfzouz2  13053  fzo0n  13060  fzonlt0  13061  fzossrbm1  13067  fzospliti  13070  elfzo0z  13080  fzofzim  13085  fzo1fzo0n0  13089  eluzgtdifelfzo  13100  fzossfzop1  13116  ssfzoulel  13132  ssfzo12bi  13133  elfzonelfzo  13140  elfzomelpfzo  13142  elfznelfzob  13144  fzostep1  13154  fllt  13177  flid  13179  flbi2  13188  2tnp1ge0ge0  13200  flhalf  13201  fldiv4p1lem1div2  13206  fldiv4lem1div2uz2  13207  dfceil2  13210  ceile  13218  ceilid  13220  quoremz  13224  intfracq  13228  uzsup  13232  mulmod0  13246  zmod10  13256  zmodcl  13260  zmodfz  13262  zmodid2  13268  modcyc  13275  mulp1mod1  13281  modmuladd  13282  modmuladdim  13283  modmul1  13293  modaddmodup  13303  modaddmodlo  13304  modaddmulmod  13307  zsqcl2  13503  leexp2  13536  iexpcyc  13570  fi1uzind  13856  ccatsymb  13936  ccatval21sw  13939  lswccatn0lsw  13945  swrdnd  14016  swrdnnn0nd  14018  swrd0  14020  swrdswrdlem  14066  swrdswrd  14067  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12lem3  14094  repswswrd  14146  cshwmodn  14157  cshwsublen  14158  cshwidxmod  14165  cshwidxmodr  14166  cshwidxm1  14169  repswcshw  14174  2cshw  14175  cshweqrep  14183  cshw1  14184  swrd2lsw  14314  nn0abscl  14672  rexuzre  14712  dvdsval3  15611  p1modz1  15614  moddvds  15618  absdvdsb  15628  dvdsabsb  15629  dvdsle  15660  alzdvds  15670  mod2eq1n2dvds  15696  evennn02n  15699  evennn2n  15700  ltoddhalfle  15710  divalgmod  15757  fldivndvdslt  15765  flodddiv4t2lthalf  15767  bitsp1o  15782  gcdabs  15877  gcdabs1  15878  modgcd  15880  bezoutlem1  15887  dfgcd2  15894  algcvga  15923  lcmabs  15949  isprm3  16027  dvdsnprmd  16034  2mulprm  16037  oddprmgt2  16043  sqnprm  16046  zgcdsq  16093  hashdvds  16112  vfermltlALT  16139  powm2modprm  16140  modprm0  16142  modprmn0modprm0  16144  fldivp1  16233  zgz  16269  4sqlem4  16288  prmgaplem5  16391  prmgaplem7  16393  cshwshashlem2  16430  setsstruct  16523  mulgmodid  18266  gexdvds  18709  zringunit  20635  prmirred  20642  znf1o  20698  chfacfscmul0  21466  chfacfscmulgsum  21468  chfacfpmmul0  21470  chfacfpmmulgsum  21472  dyadf  24192  dyadovol  24194  degltlem1  24666  coskpi  25108  cosne0  25114  relogexp  25179  cxpeq  25338  relogbzexp  25354  ppival2  25705  ppival2g  25706  ppiprm  25728  chtprm  25730  chtnprm  25731  ppip1le  25738  efexple  25857  zabsle1  25872  lgsdir2lem4  25904  lgsne0  25911  gausslemma2dlem1a  25941  gausslemma2dlem3  25944  gausslemma2dlem4  25945  lgsquadlem1  25956  lgsquadlem2  25957  2lgslem1a1  25965  2lgslem1a2  25966  2sqlem2  25994  rplogsumlem2  26061  pntrsumbnd  26142  axlowdim  26747  crctcshwlkn0lem3  27590  crctcshwlkn0lem5  27592  crctcshwlkn0  27599  crctcsh  27602  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a  27776  clwwisshclwwslemlem  27791  clwwlkinwwlk  27818  clwwlkext2edg  27835  wwlksubclwwlk  27837  numclwwlk5  28167  topnfbey  28248  uzssico  30507  rezh  31212  zrhre  31260  hashf2  31343  ballotlemfc0  31750  ballotlemfcc  31751  chpvalz  31899  chtvalz  31900  zltp1ne  32348  0nn0m1nnn0  32351  elfzm12  32918  nn0prpwlem  33670  poimirlem24  34931  mblfinlem1  34944  mblfinlem2  34945  itg2addnclem2  34959  fzmul  35031  incsequz2  35039  ellz1  39413  lzunuz  39414  lzenom  39416  nerabdioph  39455  pell14qrgt0  39505  rmxycomplete  39563  monotuz  39587  monotoddzzfi  39588  oddcomabszz  39590  zindbi  39592  jm2.24  39609  congrep  39619  fzneg  39628  jm2.19  39639  oddfl  41592  fzdifsuc2  41626  climsuse  41938  stoweidlem26  42360  stoweidlem34  42368  fourierdlem20  42461  fourierdlem42  42483  fourierdlem51  42491  fourierdlem64  42504  fourierdlem76  42516  fourierdlem94  42534  fourierdlem97  42537  fourierdlem113  42553  zm1nn  43551  zgeltp1eq  43558  eluzge0nn0  43561  elfz2z  43564  2elfz2melfz  43567  elfzlble  43569  elfzelfzlble  43570  fzopredsuc  43572  smonoord  43580  fsummmodsndifre  43583  iccpartipre  43630  iccpartiltu  43631  iccpartigtl  43632  icceuelpartlem  43644  fmtno4prmfac  43783  lighneallem4b  43823  dfeven3  43872  dfodd4  43873  nn0o1gt2ALTV  43908  nnoALTV  43909  fpprel2  43955  gbegt5  43975  gbowgt5  43976  sbgoldbwt  43991  nnsum3primesle9  44008  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  evengpop3  44012  evengpoap3  44013  nnsum4primesevenALTV  44015  bgoldbtbndlem1  44019  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  cznnring  44276  elfzolborelfzop1  44623  zgtp1leeq  44625  mod0mul  44628  modn0mul  44629  m1modmmod  44630  difmodm1lt  44631  rege1logbzge0  44668  fllog2  44677  dignn0ldlem  44711  dignn0flhalflem1  44724  dignn0flhalflem2  44725