Theorem nnre 9192

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 9189	. 2 ⊢ ℕ ⊆ ℝ
2	1	sseli 3224	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8074  ℕcn 9185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-in 3207  df-ss 3214  df-int 3934  df-inn 9186

This theorem is referenced by:  nnrei  9194  peano2nn  9197  nn1suc  9204  nnge1  9208  nnle1eq1  9209  nngt0  9210  nnnlt1  9211  nnap0  9214  nn2ge  9218  nn1gt1  9219  nndivre  9221  nnrecgt0  9223  nnsub  9224  arch  9441  nnrecl  9442  bndndx  9443  nn0ge0  9469  0mnnnnn0  9476  nnnegz  9526  elnnz  9533  elz2  9595  gtndiv  9619  prime  9623  btwnz  9643  qre  9903  elpq  9927  elpqb  9928  nnrp  9942  nnledivrp  10045  fzo1fzo0n0  10468  elfzo0le  10470  fzonmapblen  10472  ubmelfzo  10491  fzonn0p1p1  10504  elfzom1p1elfzo  10505  ubmelm1fzo  10517  subfzo0  10534  adddivflid  10598  flltdivnn0lt  10610  intfracq  10628  flqdiv  10629  m1modnnsub1  10678  addmodid  10680  modfzo0difsn  10703  nnlesq  10951  facndiv  11047  faclbnd  11049  faclbnd3  11051  bcval5  11071  seq3coll  11152  ccatval21sw  11231  caucvgre  11604  efaddlem  12298  nndivdvds  12420  nno  12530  nnoddm1d2  12534  divalglemnn  12542  divalg2  12550  ndvdsadd  12555  gcdmultiple  12654  gcdmultiplez  12655  gcdzeq  12656  sqgcd  12663  dvdssqlem  12664  lcmgcdlem  12712  coprmgcdb  12723  qredeq  12731  qredeu  12732  prmdvdsfz  12774  sqrt2irr  12797  divdenle  12832  phibndlem  12851  hashgcdlem  12873  oddprm  12895  pythagtriplem10  12905  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem16  12915  pythagtriplem19  12918  pclemub  12923  pc2dvds  12966  pcmpt  12979  fldivp1  12984  pcbc  12987  infpnlem1  12995  oddennn  13076  exmidunben  13110  mulgnegnn  13782  znidomb  14737  pellexlem1  15774  lgsval4a  15824  gausslemma2dlem0c  15853  gausslemma2dlem0d  15854  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem3  15865  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem1a1  15888