Theorem zre 9581

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

Syntax hints:   → wi 4   ∨ w3o 1004   = wceq 1398   ∈ wcel 2203  ℝcr 8126  0cc0 8127  -cneg 8445  ℕcn 9237  ℤcz 9577

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 2214

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 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-rab 2529  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053  df-neg 8447  df-z 9578

This theorem is referenced by:  zcn  9582  zrei  9583  zssre  9584  elnn0z  9590  elnnz1  9600  peano2z  9613  zaddcl  9617  ztri3or0  9619  ztri3or  9620  zletric  9621  zlelttric  9622  zltnle  9623  zleloe  9624  zletr  9627  znnsub  9629  nzadd  9630  zltp1le  9632  zleltp1  9633  znn0sub  9643  zapne  9652  zdceq  9653  zdcle  9654  zdclt  9655  zltlen  9656  nn0ge0div  9665  zextle  9669  btwnnz  9672  suprzclex  9676  msqznn  9678  peano2uz2  9685  uzind  9689  fzind  9693  fnn0ind  9694  eluzuzle  9862  uzid  9868  uzneg  9873  uz11  9877  eluzp1m1  9878  eluzp1p1  9880  eluzaddi  9881  eluzsubi  9882  uzin  9887  uz3m2nn  9905  peano2uz  9915  nn0pzuz  9919  eluz2b2  9935  uz2mulcl  9940  eqreznegel  9946  lbzbi  9948  qre  9957  elpq  9981  zltaddlt1le  10341  elfz1eq  10369  fznlem  10375  fzen  10377  uzsubsubfz  10381  fzaddel  10393  fzsuc2  10413  fzp1disj  10414  fzrev  10418  elfz1b  10424  fzneuz  10435  fzp1nel  10438  elfz0fzfz0  10460  fz0fzelfz0  10461  fznn0sub2  10462  fz0fzdiffz0  10464  elfzmlbp  10466  difelfznle  10469  nelfzo  10486  elfzouz2  10496  fzo0n  10502  fzonlt0  10503  fzossrbm1  10509  fzo1fzo0n0  10522  elfzo0z  10523  fzofzim  10527  eluzgtdifelfzo  10542  fzossfzop1  10557  ssfzo12bi  10570  elfzomelpfzo  10576  fzosplitprm1  10580  fzostep1  10583  infssuzex  10593  flid  10644  flqbi2  10651  2tnp1ge0ge0  10661  flhalf  10662  fldiv4p1lem1div2  10665  fldiv4lem1div2uz2  10666  ceiqle  10675  uzsinds  10806  zsqcl2  10979  ssenneg  11204  ccatsymb  11290  ccatval21sw  11293  lswccatn0lsw  11299  swrd0g  11352  swrdswrdlem  11396  swrdswrd  11397  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12lem3  11424  nn0abscl  11770  zmaxcl  11909  2zsupmax  11911  2zinfmin  11928  p1modz1  12480  evennn02n  12568  evennn2n  12569  ltoddhalfle  12579  bitsp1o  12639  dfgcd2  12710  algcvga  12748  isprm3  12815  dvdsnprmd  12822  sqnprm  12833  zgcdsq  12898  hashdvds  12918  fldivp1  13046  zgz  13071  4sqlem4  13090  4sqexercise1  13096  mulgval  13839  coskpi  15713  relogexp  15737  rplogbzexp  15819  zabsle1  15872  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem3  15936  gausslemma2dlem4  15937  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem1a1  15959  2lgslem1a2  15960  2sqlem2  15988  clwwlkext2edg  16417