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

Theorem zrei 11584
 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 11582 . 2 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
31, 2ax-mp 5 1 𝐴 ∈ ℝ
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2144  ℝcr 10136  ℤcz 11578 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-ov 6795  df-neg 10470  df-z 11579 This theorem is referenced by:  dfuzi  11669  eluzaddi  11914  eluzsubi  11915  dvdslelem  15239  divalglem1  15324  divalglem6  15328  divalglem9  15331  gcdaddmlem  15452  basellem9  25035  axlowdimlem16  26057  poimirlem17  33752  poimirlem19  33754  poimirlem20  33755  fdc  33866  jm2.27dlem2  38096
 Copyright terms: Public domain W3C validator