Theorem nnred 8866

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℝcr 7748  ℕcn 8853

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4099  ax-cnex 7840  ax-resscn 7841  ax-1re 7843  ax-addrcl 7846

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-v 2727  df-in 3121  df-ss 3128  df-int 3824  df-inn 8854

This theorem is referenced by:  exbtwnzlemstep  10179  qbtwnrelemcalc  10187  qbtwnre  10188  flqdiv  10252  modqmulnn  10273  modifeq2int  10317  modaddmodup  10318  modaddmodlo  10319  modsumfzodifsn  10327  addmodlteq  10329  bernneq3  10573  expnbnd  10574  facwordi  10649  faclbnd  10650  faclbnd2  10651  faclbnd3  10652  faclbnd6  10653  facubnd  10654  facavg  10655  bcp1nk  10671  bcval5  10672  caucvgrelemcau  10918  caucvgre  10919  cvg1nlemcxze  10920  cvg1nlemcau  10922  cvg1nlemres  10923  resqrexlemdecn  10950  resqrexlemga  10961  fsum3cvg3  11333  divcnv  11434  cvgratnnlembern  11460  cvgratnnlemseq  11463  cvgratnnlemabsle  11464  cvgratnnlemsumlt  11465  cvgratnnlemrate  11467  cvgratz  11469  eftabs  11593  efcllemp  11595  ege2le3  11608  efcj  11610  eftlub  11627  eflegeo  11638  eirraplem  11713  dvdslelemd  11777  nno  11839  nnoddm1d2  11843  divalglemnqt  11853  divalglemeunn  11854  dvdsbnd  11885  sqgcd  11958  uzwodc  11966  lcmgcdlem  12005  ncoprmgcdne1b  12017  prmind2  12048  isprm5lem  12069  coprm  12072  prmfac1  12080  sqrt2irraplemnn  12107  divdenle  12125  qnumgt0  12126  nn0sqrtelqelz  12134  hashdvds  12149  eulerthlemrprm  12157  eulerthlema  12158  odzdvds  12173  pythagtriplem11  12202  pythagtriplem12  12203  pythagtriplem13  12204  pythagtriplem14  12205  pythagtriplem19  12210  pclemub  12215  pcpre1  12220  pcidlem  12250  dvdsprmpweqle  12264  pcadd  12267  pcmpt  12269  pcmpt2  12270  pcfaclem  12275  pcfac  12276  qexpz  12278  pockthlem  12282  pockthg  12283  1arith  12293  4sqlem5  12308  4sqlem6  12309  4sqlem10  12313  mul4sqlem  12319  znnen  12327  exmidunben  12355  nninfdclemp1  12379  nninfdclemlt  12380  nninfdclemf1  12381  strleund  12478  logbgcd1irraplemexp  13486  logbgcd1irraplemap  13487  lgslem1  13501  lgsval2lem  13511  lgsdirprm  13535  lgsdir  13536  2sqlem3  13553  2sqlem8  13559  cvgcmp2nlemabs  13871