Theorem nnred 8757

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 8748	. 2 ⊢ ℕ ⊆ ℝ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sseldi 3100	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1481  ℝcr 7643  ℕcn 8744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-cnex 7735  ax-resscn 7736  ax-1re 7738  ax-addrcl 7741

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691  df-in 3082  df-ss 3089  df-int 3780  df-inn 8745

This theorem is referenced by:  exbtwnzlemstep  10056  qbtwnrelemcalc  10064  qbtwnre  10065  flqdiv  10125  modqmulnn  10146  modifeq2int  10190  modaddmodup  10191  modaddmodlo  10192  modsumfzodifsn  10200  addmodlteq  10202  bernneq3  10445  expnbnd  10446  facwordi  10518  faclbnd  10519  faclbnd2  10520  faclbnd3  10521  faclbnd6  10522  facubnd  10523  facavg  10524  bcp1nk  10540  bcval5  10541  caucvgrelemcau  10784  caucvgre  10785  cvg1nlemcxze  10786  cvg1nlemcau  10788  cvg1nlemres  10789  resqrexlemdecn  10816  resqrexlemga  10827  fsum3cvg3  11197  divcnv  11298  cvgratnnlembern  11324  cvgratnnlemseq  11327  cvgratnnlemabsle  11328  cvgratnnlemsumlt  11329  cvgratnnlemrate  11331  cvgratz  11333  eftabs  11399  efcllemp  11401  ege2le3  11414  efcj  11416  eftlub  11433  eflegeo  11444  eirraplem  11519  dvdslelemd  11577  nno  11639  nnoddm1d2  11643  divalglemnqt  11653  divalglemeunn  11654  dvdsbnd  11681  sqgcd  11753  lcmgcdlem  11794  ncoprmgcdne1b  11806  prmind2  11837  coprm  11858  prmfac1  11866  sqrt2irraplemnn  11893  divdenle  11911  qnumgt0  11912  nn0sqrtelqelz  11920  hashdvds  11933  znnen  11947  exmidunben  11975  strleund  12086  logbgcd1irraplemexp  13093  logbgcd1irraplemap  13094  cvgcmp2nlemabs  13402