Theorem nnred 8496

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

Syntax hints:   → wi 4   ∈ wcel 1439  ℝcr 7410  ℕcn 8483

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-cnex 7497  ax-resscn 7498  ax-1re 7500  ax-addrcl 7503

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-v 2622  df-in 3006  df-ss 3013  df-int 3695  df-inn 8484

This theorem is referenced by:  exbtwnzlemstep  9720  qbtwnrelemcalc  9728  qbtwnre  9729  flqdiv  9789  modqmulnn  9810  modifeq2int  9854  modaddmodup  9855  modaddmodlo  9856  modsumfzodifsn  9864  addmodlteq  9866  bernneq3  10137  expnbnd  10138  facwordi  10209  faclbnd  10210  faclbnd2  10211  faclbnd3  10212  faclbnd6  10213  facubnd  10214  facavg  10215  bcp1nk  10231  ibcval5  10232  caucvgrelemcau  10474  caucvgre  10475  cvg1nlemcxze  10476  cvg1nlemcau  10478  cvg1nlemres  10479  resqrexlemdecn  10506  resqrexlemga  10517  fsum3cvg3  10850  divcnv  10952  cvgratnnlembern  10978  cvgratnnlemseq  10981  cvgratnnlemabsle  10982  cvgratnnlemsumlt  10983  cvgratnnlemrate  10985  cvgratz  10987  eftabs  11007  efcllemp  11009  ege2le3  11022  efcj  11024  eftlub  11041  eflegeo  11053  eirraplem  11125  dvdslelemd  11183  nno  11245  nnoddm1d2  11249  divalglemnqt  11259  divalglemeunn  11260  dvdsbnd  11287  sqgcd  11357  lcmgcdlem  11398  ncoprmgcdne1b  11410  prmind2  11441  coprm  11462  prmfac1  11470  sqrt2irraplemnn  11496  divdenle  11514  qnumgt0  11515  nn0sqrtelqelz  11523  hashdvds  11536  znnen  11550  strleund  11643