Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  zrei Structured version   Visualization version   GIF version

Theorem zrei 12039
 Description: An integer is a real number. (Contributed by NM, 14-Jul-2005.)
Hypothesis
Ref Expression
zrei.1 𝐴 ∈ ℤ
Assertion
Ref Expression
zrei 𝐴 ∈ ℝ

Proof of Theorem zrei
StepHypRef Expression
1 zrei.1 . 2 𝐴 ∈ ℤ
2 zre 12037 . 2 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
31, 2ax-mp 5 1 𝐴 ∈ ℝ
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2111  ℝcr 10587  ℤcz 12033 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-iota 6299  df-fv 6348  df-ov 7159  df-neg 10924  df-z 12034 This theorem is referenced by:  dfuzi  12125  eluzaddi  12324  eluzsubi  12325  dvdslelem  15723  divalglem1  15808  divalglem6  15812  divalglem9  15815  gcdaddmlem  15936  basellem9  25787  axlowdimlem16  26864  poimirlem17  35389  poimirlem19  35391  poimirlem20  35392  fdc  35498  jm2.27dlem2  40369
 Copyright terms: Public domain W3C validator