Theorem nnre 9078

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

Syntax hints:   → wi 4   ∈ wcel 2178  ℝcr 7959  ℕcn 9071

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-cnex 8051  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778  df-in 3180  df-ss 3187  df-int 3900  df-inn 9072

This theorem is referenced by:  nnrei  9080  peano2nn  9083  nn1suc  9090  nnge1  9094  nnle1eq1  9095  nngt0  9096  nnnlt1  9097  nnap0  9100  nn2ge  9104  nn1gt1  9105  nndivre  9107  nnrecgt0  9109  nnsub  9110  arch  9327  nnrecl  9328  bndndx  9329  nn0ge0  9355  0mnnnnn0  9362  nnnegz  9410  elnnz  9417  elz2  9479  gtndiv  9503  prime  9507  btwnz  9527  qre  9781  elpq  9805  elpqb  9806  nnrp  9820  nnledivrp  9923  fzo1fzo0n0  10344  elfzo0le  10346  fzonmapblen  10348  ubmelfzo  10366  fzonn0p1p1  10379  elfzom1p1elfzo  10380  ubmelm1fzo  10392  subfzo0  10408  adddivflid  10472  flltdivnn0lt  10484  intfracq  10502  flqdiv  10503  m1modnnsub1  10552  addmodid  10554  modfzo0difsn  10577  nnlesq  10825  facndiv  10921  faclbnd  10923  faclbnd3  10925  bcval5  10945  seq3coll  11024  ccatval21sw  11099  caucvgre  11407  efaddlem  12100  nndivdvds  12222  nno  12332  nnoddm1d2  12336  divalglemnn  12344  divalg2  12352  ndvdsadd  12357  gcdmultiple  12456  gcdmultiplez  12457  gcdzeq  12458  sqgcd  12465  dvdssqlem  12466  lcmgcdlem  12514  coprmgcdb  12525  qredeq  12533  qredeu  12534  prmdvdsfz  12576  sqrt2irr  12599  divdenle  12634  phibndlem  12653  hashgcdlem  12675  oddprm  12697  pythagtriplem10  12707  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem16  12717  pythagtriplem19  12720  pclemub  12725  pc2dvds  12768  pcmpt  12781  fldivp1  12786  pcbc  12789  infpnlem1  12797  oddennn  12878  exmidunben  12912  mulgnegnn  13583  znidomb  14535  lgsval4a  15614  gausslemma2dlem0c  15643  gausslemma2dlem0d  15644  gausslemma2dlem1a  15650  gausslemma2dlem2  15654  gausslemma2dlem3  15655  lgsquadlem1  15669  lgsquadlem2  15670  2lgslem1a1  15678