ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zre GIF version

Theorem zre 9081
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre
StepHypRef Expression
1 elz 9079 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 272 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 962   = wceq 1332  wcel 1481  cr 7642  0cc0 7643  -cneg 7957  cn 8743  cz 9077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-rab 2426  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-iota 5095  df-fv 5138  df-ov 5784  df-neg 7959  df-z 9078
This theorem is referenced by:  zcn  9082  zrei  9083  zssre  9084  elnn0z  9090  elnnz1  9100  peano2z  9113  zaddcl  9117  ztri3or0  9119  ztri3or  9120  zletric  9121  zlelttric  9122  zltnle  9123  zleloe  9124  zletr  9126  znnsub  9128  nzadd  9129  zltp1le  9131  zleltp1  9132  znn0sub  9142  zapne  9148  zdceq  9149  zdcle  9150  zdclt  9151  zltlen  9152  nn0ge0div  9161  zextle  9165  btwnnz  9168  suprzclex  9172  msqznn  9174  peano2uz2  9181  uzind  9185  fzind  9189  fnn0ind  9190  eluzuzle  9357  uzid  9363  uzneg  9367  uz11  9371  eluzp1m1  9372  eluzp1p1  9374  eluzaddi  9375  eluzsubi  9376  uzin  9381  uz3m2nn  9394  peano2uz  9404  nn0pzuz  9408  eluz2b2  9423  uz2mulcl  9428  eqreznegel  9432  lbzbi  9434  qre  9443  elpq  9466  zltaddlt1le  9819  elfz1eq  9845  fznlem  9851  fzen  9853  uzsubsubfz  9857  fzaddel  9869  fzsuc2  9889  fzp1disj  9890  fzrev  9894  elfz1b  9900  fzneuz  9911  fzp1nel  9914  elfz0fzfz0  9933  fz0fzelfz0  9934  fznn0sub2  9935  fz0fzdiffz0  9937  elfzmlbp  9939  difelfznle  9942  elfzouz2  9968  fzonlt0  9974  fzossrbm1  9980  fzo1fzo0n0  9990  elfzo0z  9991  fzofzim  9995  eluzgtdifelfzo  10004  fzossfzop1  10019  ssfzo12bi  10032  elfzomelpfzo  10038  fzosplitprm1  10041  fzostep1  10044  flid  10087  flqbi2  10094  2tnp1ge0ge0  10104  flhalf  10105  fldiv4p1lem1div2  10108  ceiqle  10116  uzsinds  10245  zsqcl2  10400  nn0abscl  10888  zmaxcl  11027  2zsupmax  11028  evennn02n  11613  evennn2n  11614  ltoddhalfle  11624  infssuzex  11676  dfgcd2  11736  algcvga  11766  isprm3  11833  dvdsnprmd  11840  sqnprm  11850  zgcdsq  11913  hashdvds  11931  coskpi  12975  relogexp  12999  rplogbzexp  13077
  Copyright terms: Public domain W3C validator