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

Theorem zrei 12560
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 12558 . 2 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
31, 2ax-mp 5 1 𝐴 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  cr 11105  cz 12554
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-neg 11443  df-z 12555
This theorem is referenced by:  dfuzi  12649  eluzaddiOLD  12850  eluzsubiOLD  12852  dvdslelem  16248  divalglem1  16333  divalglem6  16337  divalglem9  16340  gcdaddmlem  16461  basellem9  26582  axlowdimlem16  28204  poimirlem17  36493  poimirlem19  36495  poimirlem20  36496  fdc  36601  jm2.27dlem2  41734
  Copyright terms: Public domain W3C validator