Theorem nnred 9156

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8031  ℕcn 9143

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-inn 9144

This theorem is referenced by:  exbtwnzlemstep  10508  qbtwnrelemcalc  10516  qbtwnre  10517  flqdiv  10584  modqmulnn  10605  modifeq2int  10649  modaddmodup  10650  modaddmodlo  10651  modsumfzodifsn  10659  addmodlteq  10661  bernneq3  10925  expnbnd  10926  facwordi  11003  faclbnd  11004  faclbnd2  11005  faclbnd3  11006  faclbnd6  11007  facubnd  11008  facavg  11009  bcp1nk  11025  bcval5  11026  caucvgrelemcau  11545  caucvgre  11546  cvg1nlemcxze  11547  cvg1nlemcau  11549  cvg1nlemres  11550  resqrexlemdecn  11577  resqrexlemga  11588  fsum3cvg3  11962  divcnv  12063  cvgratnnlembern  12089  cvgratnnlemseq  12092  cvgratnnlemabsle  12093  cvgratnnlemsumlt  12094  cvgratnnlemrate  12096  cvgratz  12098  eftabs  12222  efcllemp  12224  ege2le3  12237  efcj  12239  eftlub  12256  eflegeo  12267  eirraplem  12343  dvdslelemd  12409  nno  12472  nnoddm1d2  12476  divalglemnqt  12486  divalglemeunn  12487  bitsfzolem  12520  bitsfzo  12521  bitsinv1lem  12527  dvdsbnd  12532  sqgcd  12605  uzwodc  12613  lcmgcdlem  12654  ncoprmgcdne1b  12666  prmind2  12697  isprm5lem  12718  coprm  12721  prmfac1  12729  sqrt2irraplemnn  12756  divdenle  12774  qnumgt0  12775  nn0sqrtelqelz  12783  hashdvds  12798  eulerthlemrprm  12806  eulerthlema  12807  odzdvds  12823  pythagtriplem11  12852  pythagtriplem12  12853  pythagtriplem13  12854  pythagtriplem14  12855  pythagtriplem19  12860  pclemub  12865  pcpre1  12870  pcidlem  12901  dvdsprmpweqle  12915  pcadd  12918  pcmpt  12921  pcmpt2  12922  pcfaclem  12927  pcfac  12928  qexpz  12930  pockthlem  12934  pockthg  12935  1arith  12945  4sqlem5  12960  4sqlem6  12961  4sqlem10  12965  mul4sqlem  12971  4sqlem11  12979  4sqlem12  12980  4sqlem13m  12981  4sqlem14  12982  4sqlem15  12983  4sqlem16  12984  4sqlem17  12985  2expltfac  13017  znnen  13024  exmidunben  13052  nninfdclemp1  13076  nninfdclemlt  13077  nninfdclemf1  13078  strleund  13191  strext  13193  psrbaglesuppg  14692  logbgcd1irraplemexp  15698  logbgcd1irraplemap  15699  wilthlem1  15710  mersenne  15727  perfectlem2  15730  lgslem1  15735  lgsval2lem  15745  lgsdirprm  15769  lgsdir  15770  gausslemma2dlem0h  15791  gausslemma2dlem1a  15793  gausslemma2dlem2  15797  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisen  15809  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  2sqlem3  15852  2sqlem8  15858  cvgcmp2nlemabs  16662