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

Theorem nnrei 11192
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
Hypothesis
Ref Expression
nnre.1 𝐴 ∈ ℕ
Assertion
Ref Expression
nnrei 𝐴 ∈ ℝ

Proof of Theorem nnrei
StepHypRef Expression
1 nnre.1 . 2 𝐴 ∈ ℕ
2 nnre 11190 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
31, 2ax-mp 5 1 𝐴 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2127  cr 10098  cn 11183
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-i2m1 10167  ax-1ne0 10168  ax-rrecex 10171  ax-cnre 10172
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-reu 3045  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-ov 6804  df-om 7219  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-nn 11184
This theorem is referenced by:  nncni  11193  nnne0i  11218  10re  11680  numlt  11690  numltc  11691  faclbnd4lem1  13245  ef01bndlem  15084  dvdslelem  15204  divalglem6  15294  pockthi  15784  modsubi  15949  prmlem1  15987  prmlem2  16000  strlemor1OLD  16142  strleun  16145  strle1  16146  oppchomfval  16546  oppcbas  16550  rescco  16664  opprlem  18799  sralem  19350  opsrbaslem  19650  opsrbaslemOLD  19651  zlmlem  20038  znbaslem  20059  znbaslemOLD  20060  tnglem  22616  log2ublem1  24843  log2ublem2  24844  log2ub  24846  bpos1lem  25177  bposlem8  25186  bposlem9  25187  ttgval  25925  ttglem  25926  cchhllem  25937  slotsbaseefdif  26043  structvtxvallem  26079  lmat22e12  30165  lmat22e21  30166  lmat22e22  30167  ballotlem2  30830  ballotlem5  30841  ballotth  30879  chtvalz  30987  hgt750lem  31009  tgoldbachgt  31021  cnndvlem1  32805  hlhilslem  37701  jm2.27dlem2  38048  bgoldbtbndlem1  42172  tgblthelfgott  42182  tgoldbachlt  42183  tgblthelfgottOLD  42188  tgoldbachltOLD  42189
  Copyright terms: Public domain W3C validator