Theorem zre 9483

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

Syntax hints:   → wi 4   ∨ w3o 1003   = wceq 1397   ∈ wcel 2202  ℝcr 8031  0cc0 8032  -cneg 8351  ℕcn 9143  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  zcn  9484  zrei  9485  zssre  9486  elnn0z  9492  elnnz1  9502  peano2z  9515  zaddcl  9519  ztri3or0  9521  ztri3or  9522  zletric  9523  zlelttric  9524  zltnle  9525  zleloe  9526  zletr  9529  znnsub  9531  nzadd  9532  zltp1le  9534  zleltp1  9535  znn0sub  9545  zapne  9554  zdceq  9555  zdcle  9556  zdclt  9557  zltlen  9558  nn0ge0div  9567  zextle  9571  btwnnz  9574  suprzclex  9578  msqznn  9580  peano2uz2  9587  uzind  9591  fzind  9595  fnn0ind  9596  eluzuzle  9764  uzid  9770  uzneg  9775  uz11  9779  eluzp1m1  9780  eluzp1p1  9782  eluzaddi  9783  eluzsubi  9784  uzin  9789  uz3m2nn  9807  peano2uz  9817  nn0pzuz  9821  eluz2b2  9837  uz2mulcl  9842  eqreznegel  9848  lbzbi  9850  qre  9859  elpq  9883  zltaddlt1le  10242  elfz1eq  10270  fznlem  10276  fzen  10278  uzsubsubfz  10282  fzaddel  10294  fzsuc2  10314  fzp1disj  10315  fzrev  10319  elfz1b  10325  fzneuz  10336  fzp1nel  10339  elfz0fzfz0  10361  fz0fzelfz0  10362  fznn0sub2  10363  fz0fzdiffz0  10365  elfzmlbp  10367  difelfznle  10370  nelfzo  10387  elfzouz2  10397  fzo0n  10403  fzonlt0  10404  fzossrbm1  10410  fzo1fzo0n0  10423  elfzo0z  10424  fzofzim  10428  eluzgtdifelfzo  10443  fzossfzop1  10458  ssfzo12bi  10471  elfzomelpfzo  10477  fzosplitprm1  10481  fzostep1  10484  infssuzex  10494  flid  10545  flqbi2  10552  2tnp1ge0ge0  10562  flhalf  10563  fldiv4p1lem1div2  10566  fldiv4lem1div2uz2  10567  ceiqle  10576  uzsinds  10707  zsqcl2  10880  ccatsymb  11183  ccatval21sw  11186  lswccatn0lsw  11192  swrd0g  11245  swrdswrdlem  11289  swrdswrd  11290  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  nn0abscl  11663  zmaxcl  11802  2zsupmax  11804  2zinfmin  11821  p1modz1  12373  evennn02n  12461  evennn2n  12462  ltoddhalfle  12472  bitsp1o  12532  dfgcd2  12603  algcvga  12641  isprm3  12708  dvdsnprmd  12715  sqnprm  12726  zgcdsq  12791  hashdvds  12811  fldivp1  12939  zgz  12964  4sqlem4  12983  4sqexercise1  12989  mulgval  13727  coskpi  15591  relogexp  15615  rplogbzexp  15697  zabsle1  15747  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem3  15811  gausslemma2dlem4  15812  lgsquadlem1  15825  lgsquadlem2  15826  2lgslem1a1  15834  2lgslem1a2  15835  2sqlem2  15863  clwwlkext2edg  16292