Theorem nnred 9267

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  ℕcn 9254

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3220  df-ss 3227  df-int 3955  df-inn 9255

This theorem is referenced by:  exbtwnzlemstep  10631  qbtwnrelemcalc  10639  qbtwnre  10640  flqdiv  10707  modqmulnn  10728  modifeq2int  10772  modaddmodup  10773  modaddmodlo  10774  modsumfzodifsn  10782  addmodlteq  10784  bernneq3  11049  expnbnd  11050  facwordi  11127  faclbnd  11128  faclbnd2  11129  faclbnd3  11130  faclbnd6  11131  facubnd  11132  facavg  11133  bcp1nk  11149  bcval5  11150  caucvgrelemcau  11690  caucvgre  11691  cvg1nlemcxze  11692  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemdecn  11722  resqrexlemga  11733  fsum3cvg3  12107  divcnv  12208  cvgratnnlembern  12234  cvgratnnlemseq  12237  cvgratnnlemabsle  12238  cvgratnnlemsumlt  12239  cvgratnnlemrate  12241  cvgratz  12243  eftabs  12367  efcllemp  12369  ege2le3  12382  efcj  12384  eftlub  12401  eflegeo  12412  eirraplem  12488  dvdslelemd  12554  nno  12617  nnoddm1d2  12621  divalglemnqt  12631  divalglemeunn  12632  bitsfzolem  12665  bitsfzo  12666  bitsinv1lem  12672  dvdsbnd  12677  sqgcd  12750  uzwodc  12758  lcmgcdlem  12799  ncoprmgcdne1b  12811  prmind2  12842  isprm5lem  12863  coprm  12866  prmfac1  12874  sqrt2irraplemnn  12901  divdenle  12919  qnumgt0  12920  nn0sqrtelqelz  12928  hashdvds  12943  eulerthlemrprm  12951  eulerthlema  12952  odzdvds  12968  pythagtriplem11  12997  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem14  13000  pythagtriplem19  13005  pclemub  13010  pcpre1  13015  pcidlem  13046  dvdsprmpweqle  13060  pcadd  13063  pcmpt  13066  pcmpt2  13067  pcfaclem  13072  pcfac  13073  qexpz  13075  pockthlem  13079  pockthg  13080  1arith  13090  4sqlem5  13105  4sqlem6  13106  4sqlem10  13110  mul4sqlem  13116  4sqlem11  13124  4sqlem12  13125  4sqlem13m  13126  4sqlem14  13127  4sqlem15  13128  4sqlem16  13129  4sqlem17  13130  2expltfac  13162  ballotfilemonn  13165  ballotfilemimin  13193  znnen  13233  exmidunben  13261  nninfdclemp1  13285  nninfdclemlt  13286  nninfdclemf1  13287  strleund  13400  strext  13402  psrbaglesuppg  14933  logbgcd1irraplemexp  15945  logbgcd1irraplemap  15946  pellexlem2  15958  wilthlem1  15960  mersenne  15977  perfectlem2  15980  lgslem1  15985  lgsval2lem  15995  lgsdirprm  16019  lgsdir  16020  gausslemma2dlem0h  16041  gausslemma2dlem1a  16043  gausslemma2dlem2  16047  lgseisenlem1  16055  lgseisenlem2  16056  lgseisenlem3  16057  lgseisen  16059  lgsquadlem1  16062  lgsquadlem2  16063  lgsquadlem3  16064  2sqlem3  16102  2sqlem8  16108  cvgcmp2nlemabs  16928