Theorem zre 9396

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

Syntax hints:   → wi 4   ∨ w3o 980   = wceq 1373   ∈ wcel 2177  ℝcr 7944  0cc0 7945  -cneg 8264  ℕcn 9056  ℤcz 9392

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-rab 2494  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-iota 5241  df-fv 5288  df-ov 5960  df-neg 8266  df-z 9393

This theorem is referenced by:  zcn  9397  zrei  9398  zssre  9399  elnn0z  9405  elnnz1  9415  peano2z  9428  zaddcl  9432  ztri3or0  9434  ztri3or  9435  zletric  9436  zlelttric  9437  zltnle  9438  zleloe  9439  zletr  9442  znnsub  9444  nzadd  9445  zltp1le  9447  zleltp1  9448  znn0sub  9458  zapne  9467  zdceq  9468  zdcle  9469  zdclt  9470  zltlen  9471  nn0ge0div  9480  zextle  9484  btwnnz  9487  suprzclex  9491  msqznn  9493  peano2uz2  9500  uzind  9504  fzind  9508  fnn0ind  9509  eluzuzle  9676  uzid  9682  uzneg  9687  uz11  9691  eluzp1m1  9692  eluzp1p1  9694  eluzaddi  9695  eluzsubi  9696  uzin  9701  uz3m2nn  9714  peano2uz  9724  nn0pzuz  9728  eluz2b2  9744  uz2mulcl  9749  eqreznegel  9755  lbzbi  9757  qre  9766  elpq  9790  zltaddlt1le  10149  elfz1eq  10177  fznlem  10183  fzen  10185  uzsubsubfz  10189  fzaddel  10201  fzsuc2  10221  fzp1disj  10222  fzrev  10226  elfz1b  10232  fzneuz  10243  fzp1nel  10246  elfz0fzfz0  10268  fz0fzelfz0  10269  fznn0sub2  10270  fz0fzdiffz0  10272  elfzmlbp  10274  difelfznle  10277  nelfzo  10294  elfzouz2  10304  fzo0n  10310  fzonlt0  10311  fzossrbm1  10317  fzo1fzo0n0  10329  elfzo0z  10330  fzofzim  10334  eluzgtdifelfzo  10348  fzossfzop1  10363  ssfzo12bi  10376  elfzomelpfzo  10382  fzosplitprm1  10385  fzostep1  10388  infssuzex  10398  flid  10449  flqbi2  10456  2tnp1ge0ge0  10466  flhalf  10467  fldiv4p1lem1div2  10470  fldiv4lem1div2uz2  10471  ceiqle  10480  uzsinds  10611  zsqcl2  10784  ccatsymb  11081  ccatval21sw  11084  lswccatn0lsw  11090  swrd0g  11136  swrdswrdlem  11180  swrdswrd  11181  nn0abscl  11471  zmaxcl  11610  2zsupmax  11612  2zinfmin  11629  p1modz1  12180  evennn02n  12268  evennn2n  12269  ltoddhalfle  12279  bitsp1o  12339  dfgcd2  12410  algcvga  12448  isprm3  12515  dvdsnprmd  12522  sqnprm  12533  zgcdsq  12598  hashdvds  12618  fldivp1  12746  zgz  12771  4sqlem4  12790  4sqexercise1  12796  mulgval  13533  coskpi  15395  relogexp  15419  rplogbzexp  15501  zabsle1  15551  lgsne0  15590  gausslemma2dlem1a  15610  gausslemma2dlem3  15615  gausslemma2dlem4  15616  lgsquadlem1  15629  lgsquadlem2  15630  2lgslem1a1  15638  2lgslem1a2  15639  2sqlem2  15667