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

Theorem nnrei 10321
Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)
Hypothesis
Ref Expression
nnre.1  |-  A  e.  NN
Assertion
Ref Expression
nnrei  |-  A  e.  RR

Proof of Theorem nnrei
StepHypRef Expression
1 nnre.1 . 2  |-  A  e.  NN
2 nnre 10319 . 2  |-  ( A  e.  NN  ->  A  e.  RR )
31, 2ax-mp 5 1  |-  A  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1757   RRcr 9271   NNcn 10312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-i2m1 9340  ax-1ne0 9341  ax-rrecex 9344  ax-cnre 9345
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6085  df-om 6468  df-recs 6820  df-rdg 6854  df-nn 10313
This theorem is referenced by:  nncni  10322  nnne0i  10346  numlt  10764  numltc  10765  faclbnd4lem1  12055  ef01bndlem  13453  dvdslelem  13562  divalglem6  13587  pockthi  13953  modsubi  14086  prmlem1  14120  prmlem2  14132  strlemor1  14250  strleun  14253  strle1  14254  oppchomfval  14638  oppcbas  14642  rescco  14730  opprlem  16656  sralem  17182  opsrbaslem  17493  zlmlem  17792  znbaslem  17815  tnglem  20070  log2ublem1  22228  log2ublem2  22229  log2ub  22231  bpos1lem  22508  bposlem8  22517  bposlem9  22518  ttgval  22946  ttglem  22947  cchhllem  22958  ballotlem2  26721  ballotlem5  26732  ballotth  26770  jm2.27dlem2  29206  hlhilslem  35199
  Copyright terms: Public domain W3C validator