Theorem zre 11381

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

Syntax hints:   → wi 4   ∨ w3o 1036   = wceq 1483   ∈ wcel 1990  ℝcr 9935  0cc0 9936  -cneg 10267  ℕcn 11020  ℤcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378

This theorem is referenced by:  zcn  11382  zrei  11383  zssre  11384  elnn0z  11390  elnnz1  11403  znnnlt1  11404  zletr  11421  znnsub  11423  znn0sub  11424  nzadd  11425  zltp1le  11427  zleltp1  11428  nn0ge0div  11446  zextle  11450  btwnnz  11453  suprzcl  11457  msqznn  11459  peano2uz2  11465  uzind  11469  fzind  11475  fnn0ind  11476  eluzuzle  11696  uzid  11702  uzneg  11706  uztric  11709  uz11  11710  eluzp1m1  11711  eluzp1p1  11713  eluzaddi  11714  eluzsubi  11715  uzin  11720  uz3m2nn  11731  peano2uz  11741  nn0pzuz  11745  uzwo  11751  eluz2b2  11761  uz2mulcl  11766  uzinfi  11768  eqreznegel  11774  lbzbi  11776  uzsupss  11780  nn01to3  11781  zmin  11784  zmax  11785  zbtwnre  11786  rebtwnz  11787  qre  11793  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  z2ge  12029  qbtwnre  12030  zltaddlt1le  12324  elfz1eq  12352  fzn  12357  fzen  12358  uzsubsubfz  12363  fzaddel  12375  fzadd2  12376  ssfzunsnext  12386  ssfzunsn  12387  fzsuc2  12398  fzrev  12403  elfz1b  12409  fznuz  12422  uznfz  12423  fzp1nel  12424  elfz0fzfz0  12444  fz0fzelfz0  12445  fznn0sub2  12446  fz0fzdiffz0  12448  elfzmlbp  12450  difelfznle  12453  nelfzo  12475  elfzouz2  12484  fzo0n  12490  fzonlt0  12491  fzossrbm1  12497  fzospliti  12500  elfzo0z  12509  fzofzim  12514  fzo1fzo0n0  12518  eluzgtdifelfzo  12529  fzossfzop1  12545  ssfzoulel  12562  ssfzo12bi  12563  elfzonelfzo  12570  elfzomelpfzo  12572  elfznelfzob  12574  fzostep1  12584  fllt  12607  flid  12609  flbi2  12618  2tnp1ge0ge0  12630  flhalf  12631  fldiv4p1lem1div2  12636  fldiv4lem1div2uz2  12637  dfceil2  12640  ceile  12648  ceilid  12650  quoremz  12654  intfracq  12658  uzsup  12662  mulmod0  12676  zmod10  12686  zmodcl  12690  zmodfz  12692  zmodid2  12698  modcyc  12705  mulp1mod1  12711  modmuladd  12712  modmuladdim  12713  modmul1  12723  modaddmodup  12733  modaddmodlo  12734  modaddmulmod  12737  leexp2  12915  zsqcl2  12941  iexpcyc  12969  fi1uzind  13279  fi1uzindOLD  13285  ccatsymb  13366  lswccatn0lsw  13373  swrdnd  13432  swrd0  13434  swrdswrdlem  13459  swrdswrd  13460  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12lem3  13490  repswswrd  13531  cshwmodn  13541  cshwsublen  13542  cshwidxmod  13549  cshwidxmodr  13550  cshwidxm1  13553  repswcshw  13558  2cshw  13559  cshweqrep  13567  cshw1  13568  swrd2lsw  13695  nn0abscl  14052  rexuzre  14092  znnenlem  14940  dvdsval3  14987  moddvds  14991  absdvdsb  15000  dvdsabsb  15001  dvdsle  15032  alzdvds  15042  mulmoddvds  15051  mod2eq1n2dvds  15071  evennn02n  15074  evennn2n  15075  ltoddhalfle  15085  divalgmod  15129  divalgmodOLD  15130  fldivndvdslt  15138  flodddiv4t2lthalf  15140  bitsp1o  15155  gcdabs  15250  gcdabs1  15251  modgcd  15253  bezoutlem1  15256  dfgcd2  15263  algcvga  15292  lcmabs  15318  isprm3  15396  dvdsnprmd  15403  oddprmgt2  15411  sqnprm  15414  zgcdsq  15461  hashdvds  15480  vfermltlALT  15507  powm2modprm  15508  modprm0  15510  modprmn0modprm0  15512  fldivp1  15601  zgz  15637  4sqlem4  15656  prmgaplem5  15759  prmgaplem7  15761  cshwshashlem2  15803  setsstruct  15898  mulgmodid  17581  gexdvds  17999  zringunit  19836  prmirred  19843  znf1o  19900  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  dyadf  23359  dyadovol  23361  degltlem1  23832  coskpi  24272  cosne0  24276  relogexp  24342  cxpeq  24498  relogbzexp  24514  ppival2  24854  ppival2g  24855  ppiprm  24877  chtprm  24879  chtnprm  24880  ppip1le  24887  efexple  25006  zabsle1  25021  lgsdir2lem4  25053  lgsne0  25060  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  gausslemma2dlem4  25094  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1a1  25114  2lgslem1a2  25115  2sqlem2  25143  rplogsumlem2  25174  pntrsumbnd  25255  axlowdim  25841  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  crctcshwlkn0  26713  crctcsh  26716  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a  26899  clwwlkinwwlk  26905  clwwlksext2edg  26923  wwlksubclwwlks  26925  clwwisshclwwslemlem  26926  clwlksfclwwlk  26962  numclwlk1lem2f1  27227  numclwwlk5  27246  topnfbey  27325  uzssico  29546  rezh  30015  zrhre  30063  hashf2  30146  ballotlemfc0  30554  ballotlemfcc  30555  chpvalz  30706  chtvalz  30707  elfzm12  31569  nn0prpwlem  32317  poimirlem24  33433  mblfinlem1  33446  mblfinlem2  33447  itg2addnclem2  33462  fzmul  33537  incsequz2  33545  ellz1  37330  lzunuz  37331  lzenom  37333  nerabdioph  37373  pell14qrgt0  37423  rmxycomplete  37482  monotuz  37506  monotoddzzfi  37507  oddcomabszz  37509  zindbi  37511  jm2.24  37530  congrep  37540  fzneg  37549  jm2.19  37560  oddfl  39489  fzdifsuc2  39525  climsuse  39840  stoweidlem26  40243  stoweidlem34  40251  fourierdlem20  40344  fourierdlem42  40366  fourierdlem51  40374  fourierdlem64  40387  fourierdlem76  40399  fourierdlem94  40417  fourierdlem97  40420  fourierdlem113  40436  zm1nn  41316  zgeltp1eq  41318  eluzge0nn0  41322  elfz2z  41325  2elfz2melfz  41328  elfzlble  41330  elfzelfzlble  41331  fzopredsuc  41333  smonoord  41341  fsummmodsndifre  41344  iccpartipre  41357  iccpartiltu  41358  iccpartigtl  41359  icceuelpartlem  41371  pfxccatin12lem2  41424  fmtno4prmfac  41484  lighneallem4b  41526  dfeven3  41570  dfodd4  41571  nn0o1gt2ALTV  41605  nnoALTV  41606  gbegt5  41649  gbowgt5  41650  sbgoldbwt  41665  nnsum3primesle9  41682  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  evengpop3  41686  evengpoap3  41687  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  cznnring  41956  elfzolborelfzop1  42309  zgtp1leeq  42311  mod0mul  42314  modn0mul  42315  m1modmmod  42316  difmodm1lt  42317  rege1logbzge0  42353  fllog2  42362  dignn0ldlem  42396  dignn0flhalflem1  42409  dignn0flhalflem2  42410