Theorem nnred 9249

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8125  ℕcn 9236

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 2214  ax-sep 4227  ax-cnex 8217  ax-resscn 8218  ax-1re 8220  ax-addrcl 8223

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2814  df-in 3216  df-ss 3223  df-int 3949  df-inn 9237

This theorem is referenced by:  exbtwnzlemstep  10606  qbtwnrelemcalc  10614  qbtwnre  10615  flqdiv  10682  modqmulnn  10703  modifeq2int  10747  modaddmodup  10748  modaddmodlo  10749  modsumfzodifsn  10757  addmodlteq  10759  bernneq3  11023  expnbnd  11024  facwordi  11101  faclbnd  11102  faclbnd2  11103  faclbnd3  11104  faclbnd6  11105  facubnd  11106  facavg  11107  bcp1nk  11123  bcval5  11124  caucvgrelemcau  11661  caucvgre  11662  cvg1nlemcxze  11663  cvg1nlemcau  11665  cvg1nlemres  11666  resqrexlemdecn  11693  resqrexlemga  11704  fsum3cvg3  12078  divcnv  12179  cvgratnnlembern  12205  cvgratnnlemseq  12208  cvgratnnlemabsle  12209  cvgratnnlemsumlt  12210  cvgratnnlemrate  12212  cvgratz  12214  eftabs  12338  efcllemp  12340  ege2le3  12353  efcj  12355  eftlub  12372  eflegeo  12383  eirraplem  12459  dvdslelemd  12525  nno  12588  nnoddm1d2  12592  divalglemnqt  12602  divalglemeunn  12603  bitsfzolem  12636  bitsfzo  12637  bitsinv1lem  12643  dvdsbnd  12648  sqgcd  12721  uzwodc  12729  lcmgcdlem  12770  ncoprmgcdne1b  12782  prmind2  12813  isprm5lem  12834  coprm  12837  prmfac1  12845  sqrt2irraplemnn  12872  divdenle  12890  qnumgt0  12891  nn0sqrtelqelz  12899  hashdvds  12914  eulerthlemrprm  12922  eulerthlema  12923  odzdvds  12939  pythagtriplem11  12968  pythagtriplem12  12969  pythagtriplem13  12970  pythagtriplem14  12971  pythagtriplem19  12976  pclemub  12981  pcpre1  12986  pcidlem  13017  dvdsprmpweqle  13031  pcadd  13034  pcmpt  13037  pcmpt2  13038  pcfaclem  13043  pcfac  13044  qexpz  13046  pockthlem  13050  pockthg  13051  1arith  13061  4sqlem5  13076  4sqlem6  13077  4sqlem10  13081  mul4sqlem  13087  4sqlem11  13095  4sqlem12  13096  4sqlem13m  13097  4sqlem14  13098  4sqlem15  13099  4sqlem16  13100  4sqlem17  13101  2expltfac  13133  znnen  13141  exmidunben  13169  nninfdclemp1  13193  nninfdclemlt  13194  nninfdclemf1  13195  strleund  13308  strext  13310  psrbaglesuppg  14813  logbgcd1irraplemexp  15825  logbgcd1irraplemap  15826  pellexlem2  15838  wilthlem1  15840  mersenne  15857  perfectlem2  15860  lgslem1  15865  lgsval2lem  15875  lgsdirprm  15899  lgsdir  15900  gausslemma2dlem0h  15921  gausslemma2dlem1a  15923  gausslemma2dlem2  15927  lgseisenlem1  15935  lgseisenlem2  15936  lgseisenlem3  15937  lgseisen  15939  lgsquadlem1  15942  lgsquadlem2  15943  lgsquadlem3  15944  2sqlem3  15982  2sqlem8  15988  cvgcmp2nlemabs  16808