Theorem nnred 9062

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℝcr 7937  ℕcn 9049

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4167  ax-cnex 8029  ax-resscn 8030  ax-1re 8032  ax-addrcl 8035

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775  df-in 3174  df-ss 3181  df-int 3889  df-inn 9050

This theorem is referenced by:  exbtwnzlemstep  10403  qbtwnrelemcalc  10411  qbtwnre  10412  flqdiv  10479  modqmulnn  10500  modifeq2int  10544  modaddmodup  10545  modaddmodlo  10546  modsumfzodifsn  10554  addmodlteq  10556  bernneq3  10820  expnbnd  10821  facwordi  10898  faclbnd  10899  faclbnd2  10900  faclbnd3  10901  faclbnd6  10902  facubnd  10903  facavg  10904  bcp1nk  10920  bcval5  10921  caucvgrelemcau  11341  caucvgre  11342  cvg1nlemcxze  11343  cvg1nlemcau  11345  cvg1nlemres  11346  resqrexlemdecn  11373  resqrexlemga  11384  fsum3cvg3  11757  divcnv  11858  cvgratnnlembern  11884  cvgratnnlemseq  11887  cvgratnnlemabsle  11888  cvgratnnlemsumlt  11889  cvgratnnlemrate  11891  cvgratz  11893  eftabs  12017  efcllemp  12019  ege2le3  12032  efcj  12034  eftlub  12051  eflegeo  12062  eirraplem  12138  dvdslelemd  12204  nno  12267  nnoddm1d2  12271  divalglemnqt  12281  divalglemeunn  12282  bitsfzolem  12315  bitsfzo  12316  bitsinv1lem  12322  dvdsbnd  12327  sqgcd  12400  uzwodc  12408  lcmgcdlem  12449  ncoprmgcdne1b  12461  prmind2  12492  isprm5lem  12513  coprm  12516  prmfac1  12524  sqrt2irraplemnn  12551  divdenle  12569  qnumgt0  12570  nn0sqrtelqelz  12578  hashdvds  12593  eulerthlemrprm  12601  eulerthlema  12602  odzdvds  12618  pythagtriplem11  12647  pythagtriplem12  12648  pythagtriplem13  12649  pythagtriplem14  12650  pythagtriplem19  12655  pclemub  12660  pcpre1  12665  pcidlem  12696  dvdsprmpweqle  12710  pcadd  12713  pcmpt  12716  pcmpt2  12717  pcfaclem  12722  pcfac  12723  qexpz  12725  pockthlem  12729  pockthg  12730  1arith  12740  4sqlem5  12755  4sqlem6  12756  4sqlem10  12760  mul4sqlem  12766  4sqlem11  12774  4sqlem12  12775  4sqlem13m  12776  4sqlem14  12777  4sqlem15  12778  4sqlem16  12779  4sqlem17  12780  2expltfac  12812  znnen  12819  exmidunben  12847  nninfdclemp1  12871  nninfdclemlt  12872  nninfdclemf1  12873  strleund  12985  strext  12987  psrbaglesuppg  14484  logbgcd1irraplemexp  15490  logbgcd1irraplemap  15491  wilthlem1  15502  mersenne  15519  perfectlem2  15522  lgslem1  15527  lgsval2lem  15537  lgsdirprm  15561  lgsdir  15562  gausslemma2dlem0h  15583  gausslemma2dlem1a  15585  gausslemma2dlem2  15589  lgseisenlem1  15597  lgseisenlem2  15598  lgseisenlem3  15599  lgseisen  15601  lgsquadlem1  15604  lgsquadlem2  15605  lgsquadlem3  15606  2sqlem3  15644  2sqlem8  15650  cvgcmp2nlemabs  16086