Theorem nnre 9320

Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nnre	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Proof of Theorem nnre

Step	Hyp	Ref	Expression
1		nnssre 9317	. 2 ⊢ ℕ ⊆ ℝ
2	1	sseli 3244	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℝcr 8184  ℕcn 9313

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3971  df-inn 9314

This theorem is used by:  nnrei  9322  peano2nn  9325  nn1suc  9332  nnge1  9336  nnle1eq1  9337  nngt0  9338  nnnlt1  9339  nnap0  9342  nn2ge  9346  nn1gt1  9347  nndivre  9349  nnrecgt0  9351  nnsub  9352  arch  9571  nnrecl  9572  bndndx  9573  nn0ge0  9599  0mnnnnn0  9606  nnnegz  9658  elnnz  9665  elz2  9727  gtndiv  9752  prime  9756  btwnz  9776  qre  10041  elpq  10066  elpqb  10067  nnrp  10081  nnledivrp  10184  fzo1fzo0n0  10612  elfzo0le  10614  fzonmapblen  10616  ubmelfzo  10635  fzonn0p1p1  10648  elfzom1p1elfzo  10649  ubmelm1fzo  10661  subfzo0  10678  adddivflid  10748  flltdivnn0lt  10760  intfracq  10778  flqdiv  10779  m1modnnsub1  10828  addmodid  10830  modfzo0difsn  10853  nnlesq  11101  facndiv  11199  faclbnd  11201  faclbnd3  11203  bcval5  11223  seq3coll  11316  ccatval21sw  11395  caucvgre  11769  efaddlem  12466  nndivdvds  12588  nno  12698  nnoddm1d2  12702  divalglemnn  12710  divalg2  12718  ndvdsadd  12723  gcdmultiple  12822  gcdmultiplez  12823  gcdzeq  12824  sqgcd  12831  dvdssqlem  12832  lcmgcdlem  12880  coprmgcdb  12891  qredeq  12899  qredeu  12900  prmdvdsfz  12943  sqrt2irr  12966  divdenle  13002  phibndlem  13023  hashgcdlem  13045  oddprm  13067  pythagtriplem10  13077  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  pythagtriplem19  13090  pclemub  13095  pc2dvds  13138  pcmpt  13151  fldivp1  13156  pcbc  13159  infpnlem1  13167  ballotfilemonn  13279  oddennn  13341  exmidunben  13375  mulgnegnn  13994  znidomb  15102  birthdaylem3  16227  pellexlem1  16229  ppiqltx  16281  chtublem  16295  bcmono  16304  bposlem1  16311  bposlem5  16315  bposlem6  16316  lgsval4a  16346  gausslemma2dlem0c  16375  gausslemma2dlem0d  16376  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem3  16387  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem1a1  16410