Theorem zre 9461

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

Syntax hints:   → wi 4   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200  ℝcr 8009  0cc0 8010  -cneg 8329  ℕcn 9121  ℤcz 9457

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458

This theorem is referenced by:  zcn  9462  zrei  9463  zssre  9464  elnn0z  9470  elnnz1  9480  peano2z  9493  zaddcl  9497  ztri3or0  9499  ztri3or  9500  zletric  9501  zlelttric  9502  zltnle  9503  zleloe  9504  zletr  9507  znnsub  9509  nzadd  9510  zltp1le  9512  zleltp1  9513  znn0sub  9523  zapne  9532  zdceq  9533  zdcle  9534  zdclt  9535  zltlen  9536  nn0ge0div  9545  zextle  9549  btwnnz  9552  suprzclex  9556  msqznn  9558  peano2uz2  9565  uzind  9569  fzind  9573  fnn0ind  9574  eluzuzle  9742  uzid  9748  uzneg  9753  uz11  9757  eluzp1m1  9758  eluzp1p1  9760  eluzaddi  9761  eluzsubi  9762  uzin  9767  uz3m2nn  9780  peano2uz  9790  nn0pzuz  9794  eluz2b2  9810  uz2mulcl  9815  eqreznegel  9821  lbzbi  9823  qre  9832  elpq  9856  zltaddlt1le  10215  elfz1eq  10243  fznlem  10249  fzen  10251  uzsubsubfz  10255  fzaddel  10267  fzsuc2  10287  fzp1disj  10288  fzrev  10292  elfz1b  10298  fzneuz  10309  fzp1nel  10312  elfz0fzfz0  10334  fz0fzelfz0  10335  fznn0sub2  10336  fz0fzdiffz0  10338  elfzmlbp  10340  difelfznle  10343  nelfzo  10360  elfzouz2  10370  fzo0n  10376  fzonlt0  10377  fzossrbm1  10383  fzo1fzo0n0  10395  elfzo0z  10396  fzofzim  10400  eluzgtdifelfzo  10415  fzossfzop1  10430  ssfzo12bi  10443  elfzomelpfzo  10449  fzosplitprm1  10452  fzostep1  10455  infssuzex  10465  flid  10516  flqbi2  10523  2tnp1ge0ge0  10533  flhalf  10534  fldiv4p1lem1div2  10537  fldiv4lem1div2uz2  10538  ceiqle  10547  uzsinds  10678  zsqcl2  10851  ccatsymb  11150  ccatval21sw  11153  lswccatn0lsw  11159  swrd0g  11207  swrdswrdlem  11251  swrdswrd  11252  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12lem3  11279  nn0abscl  11611  zmaxcl  11750  2zsupmax  11752  2zinfmin  11769  p1modz1  12320  evennn02n  12408  evennn2n  12409  ltoddhalfle  12419  bitsp1o  12479  dfgcd2  12550  algcvga  12588  isprm3  12655  dvdsnprmd  12662  sqnprm  12673  zgcdsq  12738  hashdvds  12758  fldivp1  12886  zgz  12911  4sqlem4  12930  4sqexercise1  12936  mulgval  13674  coskpi  15537  relogexp  15561  rplogbzexp  15643  zabsle1  15693  lgsne0  15732  gausslemma2dlem1a  15752  gausslemma2dlem3  15757  gausslemma2dlem4  15758  lgsquadlem1  15771  lgsquadlem2  15772  2lgslem1a1  15780  2lgslem1a2  15781  2sqlem2  15809