Theorem nnred 8119

Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem nnred

Step	Hyp	Ref	Expression
1		nnssre 8110	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 2998	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1434  ℝcr 7042  ℕcn 8106

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-cnex 7129  ax-resscn 7130  ax-1re 7132  ax-addrcl 7135

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-v 2604  df-in 2980  df-ss 2987  df-int 3645  df-inn 8107

This theorem is referenced by:  exbtwnzlemstep  9334  qbtwnrelemcalc  9342  qbtwnre  9343  flqdiv  9403  modqmulnn  9424  modifeq2int  9468  modaddmodup  9469  modaddmodlo  9470  modsumfzodifsn  9478  addmodlteq  9480  bernneq3  9692  expnbnd  9693  facwordi  9764  faclbnd  9765  faclbnd2  9766  faclbnd3  9767  faclbnd6  9768  facubnd  9769  facavg  9770  bcp1nk  9786  ibcval5  9787  caucvgrelemcau  10004  caucvgre  10005  cvg1nlemcxze  10006  cvg1nlemcau  10008  cvg1nlemres  10009  resqrexlemdecn  10036  resqrexlemga  10047  dvdslelemd  10388  nno  10450  nnoddm1d2  10454  divalglemnqt  10464  divalglemeunn  10465  dvdsbnd  10492  sqgcd  10562  lcmgcdlem  10603  ncoprmgcdne1b  10615  prmind2  10646  coprm  10667  prmfac1  10675  sqrt2irraplemnn  10701  znnen  10709