Theorem nnrei 11887

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

Step	Hyp	Ref	Expression
1		nnre.1	. 2 ⊢ 𝐴 ∈ ℕ
2		nnre 11885	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℝ

Syntax hints:   ∈ wcel 2112  ℝcr 10776  ℕcn 11878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pr 5346  ax-un 7563  ax-1cn 10835  ax-icn 10836  ax-addcl 10837  ax-addrcl 10838  ax-mulcl 10839  ax-mulrcl 10840  ax-i2m1 10845  ax-1ne0 10846  ax-rrecex 10849  ax-cnre 10850

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-pred 6189  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-ov 7255  df-om 7685  df-wrecs 8089  df-recs 8150  df-rdg 8188  df-nn 11879

This theorem is referenced by:  nnne0i  11918  numlt  12366  numltc  12367  faclbnd4lem1  13910  ef01bndlem  15796  dvdslelem  15921  divalglem6  16010  pockthi  16511  modsubi  16676  prmlem1  16712  prmlem2  16724  strleun  16761  strle1  16762  basendxnplusgndx  16893  tsetndxnbasendx  16966  plendxnbasendx  16979  dsndxnbasendx  16995  unifndxnbasendx  17004  oppchomfvalOLD  17316  oppcbasOLD  17321  resccoOLD  17438  opprlemOLD  19758  sralemOLD  20330  zlmlemOLD  20606  znbaslemOLD  20630  opsrbaslemOLD  21136  tnglemOLD  23678  log2ublem1  25976  log2ublem2  25977  log2ub  25979  bpos1lem  26310  bposlem8  26319  bposlem9  26320  slotsinbpsd  26682  slotslnbpsd  26683  ttgval  27115  ttglemOLD  27117  cchhllemOLD  27133  basendxnedgfndx  27243  structvtxvallem  27268  lmat22e12  31646  lmat22e21  31647  lmat22e22  31648  ballotlem2  32330  ballotlem5  32341  ballotth  32379  chtvalz  32484  hgt750lem  32506  tgoldbachgt  32518  cnndvlem1  34619  hlhilslemOLD  39859  lcmineqlem  39967  3lexlogpow5ineq1  39969  jm2.27dlem2  40720  bgoldbtbndlem1  45118  tgblthelfgott  45128  tgoldbachlt  45129