Theorem zre 9598

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

Syntax hints:   → wi 4   ∨ w3o 1004   = wceq 1398   ∈ wcel 2205  ℝcr 8142  0cc0 8143  -cneg 8461  ℕcn 9254  ℤcz 9594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-rab 2531  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-neg 8463  df-z 9595

This theorem is referenced by:  zcn  9599  zrei  9600  zssre  9601  elnn0z  9607  elnnz1  9617  peano2z  9630  zaddcl  9634  ztri3or0  9636  ztri3or  9637  zletric  9638  zlelttric  9639  zltnle  9640  zleloe  9641  zletr  9644  znnsub  9646  nzadd  9647  zltp1le  9649  zleltp1  9650  znn0sub  9660  zapne  9669  zdceq  9670  zdcle  9671  zdclt  9672  zltlen  9674  nn0ge0div  9683  zextle  9687  btwnnz  9690  suprzclex  9694  msqznn  9696  peano2uz2  9703  uzind  9707  fzind  9711  fnn0ind  9712  eluzuzle  9880  uzid  9886  uzneg  9891  uz11  9895  eluzp1m1  9896  eluzp1p1  9898  eluzaddi  9899  eluzsubi  9900  uzin  9905  uz3m2nn  9923  peano2uz  9933  nn0pzuz  9937  eluz2b2  9953  uz2mulcl  9958  eqreznegel  9964  lbzbi  9966  qre  9975  elpq  9999  zltaddlt1le  10360  elfz1eq  10389  fznlem  10395  fzen  10397  uzsubsubfz  10401  fzaddel  10414  fzsuc2  10435  fzp1disj  10436  fzrev  10440  elfz1b  10446  fzneuz  10457  fzp1nel  10460  elfz0fzfz0  10482  fz0fzelfz0  10483  fznn0sub2  10484  fz0fzdiffz0  10486  elfzmlbp  10488  difelfznle  10491  nelfzo  10508  elfzouz2  10518  fzo0n  10524  fzonlt0  10525  fzossrbm1  10531  fzo1fzo0n0  10544  elfzo0z  10545  fzofzim  10549  eluzgtdifelfzo  10564  fzossfzop1  10579  ssfzo12bi  10592  elfzomelpfzo  10598  fzosplitprm1  10602  fzostep1  10605  infssuzex  10615  flid  10668  flqbi2  10675  2tnp1ge0ge0  10685  flhalf  10686  fldiv4p1lem1div2  10689  fldiv4lem1div2uz2  10690  ceiqle  10699  uzsinds  10830  zsqcl2  11003  ssenneg  11229  ccatsymb  11315  ccatval21sw  11318  lswccatn0lsw  11324  swrd0g  11377  swrdswrdlem  11421  swrdswrd  11422  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  nn0abscl  11795  zmaxcl  11934  2zsupmax  11936  2zinfmin  11953  p1modz1  12505  evennn02n  12593  evennn2n  12594  ltoddhalfle  12604  bitsp1o  12664  dfgcd2  12735  algcvga  12773  isprm3  12840  dvdsnprmd  12847  sqnprm  12858  zgcdsq  12923  hashdvds  12943  fldivp1  13071  zgz  13096  4sqlem4  13115  4sqexercise1  13121  mulgval  13875  coskpi  15839  relogexp  15863  rplogbzexp  15945  zabsle1  15998  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem3  16062  gausslemma2dlem4  16063  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1a1  16085  2lgslem1a2  16086  2sqlem2  16114  clwwlkext2edg  16543