Theorem nnrei 11668

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

Syntax hints:   ∈ wcel 2112  ℝcr 10559  ℕcn 11659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pr 5291  ax-un 7452  ax-1cn 10618  ax-icn 10619  ax-addcl 10620  ax-addrcl 10621  ax-mulcl 10622  ax-mulrcl 10623  ax-i2m1 10628  ax-1ne0 10629  ax-rrecex 10632  ax-cnre 10633

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-ral 3073  df-rex 3074  df-reu 3075  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-iun 4878  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7146  df-om 7573  df-wrecs 7950  df-recs 8011  df-rdg 8049  df-nn 11660

This theorem is referenced by:  nnne0i  11699  numlt  12147  numltc  12148  faclbnd4lem1  13688  ef01bndlem  15570  dvdslelem  15695  divalglem6  15784  pockthi  16283  modsubi  16448  prmlem1  16484  prmlem2  16496  strleun  16634  strle1  16635  oppchomfval  17027  oppcbas  17031  rescco  17146  opprlem  19434  sralem  20002  zlmlem  20271  znbaslem  20291  opsrbaslem  20794  tnglem  23327  log2ublem1  25616  log2ublem2  25617  log2ub  25619  bpos1lem  25950  bposlem8  25959  bposlem9  25960  ttgval  26753  ttglem  26754  cchhllem  26765  slotsbaseefdif  26872  structvtxvallem  26897  lmat22e12  31275  lmat22e21  31276  lmat22e22  31277  ballotlem2  31959  ballotlem5  31970  ballotth  32008  chtvalz  32113  hgt750lem  32135  tgoldbachgt  32147  cnndvlem1  34251  hlhilslem  39499  lcmineqlem  39604  3lexlogpow5ineq1  39606  jm2.27dlem2  40309  bgoldbtbndlem1  44675  tgblthelfgott  44685  tgoldbachlt  44686