Theorem nnrei 12217

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 12215	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ ℝ

Syntax hints:   ∈ wcel 2106  ℝcr 11105  ℕcn 12208

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-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

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-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-nn 12209

This theorem is referenced by:  nnne0i  12248  numlt  12698  numltc  12699  faclbnd4lem1  14249  ef01bndlem  16123  dvdslelem  16248  divalglem6  16337  pockthi  16836  modsubi  17001  prmlem1  17037  prmlem2  17049  strleun  17086  strle1  17087  basendxnplusgndx  17223  tsetndxnbasendx  17297  plendxnbasendx  17311  dsndxnbasendx  17330  unifndxnbasendx  17340  slotsdifunifndx  17342  slotsdifocndx  17359  oppchomfvalOLD  17655  oppcbasOLD  17660  resccoOLD  17777  opprlemOLD  20148  sralemOLD  20783  zlmlemOLD  21058  znbaslemOLD  21082  opsrbaslemOLD  21596  tnglemOLD  24141  log2ublem1  26440  log2ublem2  26441  log2ub  26443  bpos1lem  26774  bposlem8  26783  bposlem9  26784  slotsinbpsd  27681  slotslnbpsd  27682  lngndxnitvndx  27683  ttgvalOLD  28116  ttglemOLD  28118  cchhllemOLD  28134  basendxnedgfndx  28244  structvtxvallem  28269  lmat22e12  32787  lmat22e21  32788  lmat22e22  32789  ballotlem2  33475  ballotlem5  33486  ballotth  33524  chtvalz  33629  hgt750lem  33651  tgoldbachgt  33663  cnndvlem1  35401  hlhilslemOLD  40798  lcmineqlem  40905  3lexlogpow5ineq1  40907  jm2.27dlem2  41734  bgoldbtbndlem1  46459  tgblthelfgott  46469  tgoldbachlt  46470