Theorem nnred 9020

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7895  ℕcn 9007

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7987  ax-resscn 7988  ax-1re 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-in 3163  df-ss 3170  df-int 3876  df-inn 9008

This theorem is referenced by:  exbtwnzlemstep  10354  qbtwnrelemcalc  10362  qbtwnre  10363  flqdiv  10430  modqmulnn  10451  modifeq2int  10495  modaddmodup  10496  modaddmodlo  10497  modsumfzodifsn  10505  addmodlteq  10507  bernneq3  10771  expnbnd  10772  facwordi  10849  faclbnd  10850  faclbnd2  10851  faclbnd3  10852  faclbnd6  10853  facubnd  10854  facavg  10855  bcp1nk  10871  bcval5  10872  caucvgrelemcau  11162  caucvgre  11163  cvg1nlemcxze  11164  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemdecn  11194  resqrexlemga  11205  fsum3cvg3  11578  divcnv  11679  cvgratnnlembern  11705  cvgratnnlemseq  11708  cvgratnnlemabsle  11709  cvgratnnlemsumlt  11710  cvgratnnlemrate  11712  cvgratz  11714  eftabs  11838  efcllemp  11840  ege2le3  11853  efcj  11855  eftlub  11872  eflegeo  11883  eirraplem  11959  dvdslelemd  12025  nno  12088  nnoddm1d2  12092  divalglemnqt  12102  divalglemeunn  12103  bitsfzolem  12136  bitsfzo  12137  bitsinv1lem  12143  dvdsbnd  12148  sqgcd  12221  uzwodc  12229  lcmgcdlem  12270  ncoprmgcdne1b  12282  prmind2  12313  isprm5lem  12334  coprm  12337  prmfac1  12345  sqrt2irraplemnn  12372  divdenle  12390  qnumgt0  12391  nn0sqrtelqelz  12399  hashdvds  12414  eulerthlemrprm  12422  eulerthlema  12423  odzdvds  12439  pythagtriplem11  12468  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem14  12471  pythagtriplem19  12476  pclemub  12481  pcpre1  12486  pcidlem  12517  dvdsprmpweqle  12531  pcadd  12534  pcmpt  12537  pcmpt2  12538  pcfaclem  12543  pcfac  12544  qexpz  12546  pockthlem  12550  pockthg  12551  1arith  12561  4sqlem5  12576  4sqlem6  12577  4sqlem10  12581  mul4sqlem  12587  4sqlem11  12595  4sqlem12  12596  4sqlem13m  12597  4sqlem14  12598  4sqlem15  12599  4sqlem16  12600  4sqlem17  12601  2expltfac  12633  znnen  12640  exmidunben  12668  nninfdclemp1  12692  nninfdclemlt  12693  nninfdclemf1  12694  strleund  12806  strext  12808  psrbaglesuppg  14302  logbgcd1irraplemexp  15288  logbgcd1irraplemap  15289  wilthlem1  15300  mersenne  15317  perfectlem2  15320  lgslem1  15325  lgsval2lem  15335  lgsdirprm  15359  lgsdir  15360  gausslemma2dlem0h  15381  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  2sqlem3  15442  2sqlem8  15448  cvgcmp2nlemabs  15763