Theorem nnred 8931

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7809  ℕcn 8918

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4121  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2739  df-in 3135  df-ss 3142  df-int 3845  df-inn 8919

This theorem is referenced by:  exbtwnzlemstep  10247  qbtwnrelemcalc  10255  qbtwnre  10256  flqdiv  10320  modqmulnn  10341  modifeq2int  10385  modaddmodup  10386  modaddmodlo  10387  modsumfzodifsn  10395  addmodlteq  10397  bernneq3  10642  expnbnd  10643  facwordi  10719  faclbnd  10720  faclbnd2  10721  faclbnd3  10722  faclbnd6  10723  facubnd  10724  facavg  10725  bcp1nk  10741  bcval5  10742  caucvgrelemcau  10988  caucvgre  10989  cvg1nlemcxze  10990  cvg1nlemcau  10992  cvg1nlemres  10993  resqrexlemdecn  11020  resqrexlemga  11031  fsum3cvg3  11403  divcnv  11504  cvgratnnlembern  11530  cvgratnnlemseq  11533  cvgratnnlemabsle  11534  cvgratnnlemsumlt  11535  cvgratnnlemrate  11537  cvgratz  11539  eftabs  11663  efcllemp  11665  ege2le3  11678  efcj  11680  eftlub  11697  eflegeo  11708  eirraplem  11783  dvdslelemd  11848  nno  11910  nnoddm1d2  11914  divalglemnqt  11924  divalglemeunn  11925  dvdsbnd  11956  sqgcd  12029  uzwodc  12037  lcmgcdlem  12076  ncoprmgcdne1b  12088  prmind2  12119  isprm5lem  12140  coprm  12143  prmfac1  12151  sqrt2irraplemnn  12178  divdenle  12196  qnumgt0  12197  nn0sqrtelqelz  12205  hashdvds  12220  eulerthlemrprm  12228  eulerthlema  12229  odzdvds  12244  pythagtriplem11  12273  pythagtriplem12  12274  pythagtriplem13  12275  pythagtriplem14  12276  pythagtriplem19  12281  pclemub  12286  pcpre1  12291  pcidlem  12321  dvdsprmpweqle  12335  pcadd  12338  pcmpt  12340  pcmpt2  12341  pcfaclem  12346  pcfac  12347  qexpz  12349  pockthlem  12353  pockthg  12354  1arith  12364  4sqlem5  12379  4sqlem6  12380  4sqlem10  12384  mul4sqlem  12390  znnen  12398  exmidunben  12426  nninfdclemp1  12450  nninfdclemlt  12451  nninfdclemf1  12452  strleund  12561  strext  12563  logbgcd1irraplemexp  14356  logbgcd1irraplemap  14357  lgslem1  14371  lgsval2lem  14381  lgsdirprm  14405  lgsdir  14406  lgseisenlem1  14420  lgseisenlem2  14421  2sqlem3  14434  2sqlem8  14440  cvgcmp2nlemabs  14750