Theorem nnred 9149

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8024  ℕcn 9136

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8116  ax-resscn 8117  ax-1re 8119  ax-addrcl 8122

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-in 3204  df-ss 3211  df-int 3927  df-inn 9137

This theorem is referenced by:  exbtwnzlemstep  10500  qbtwnrelemcalc  10508  qbtwnre  10509  flqdiv  10576  modqmulnn  10597  modifeq2int  10641  modaddmodup  10642  modaddmodlo  10643  modsumfzodifsn  10651  addmodlteq  10653  bernneq3  10917  expnbnd  10918  facwordi  10995  faclbnd  10996  faclbnd2  10997  faclbnd3  10998  faclbnd6  10999  facubnd  11000  facavg  11001  bcp1nk  11017  bcval5  11018  caucvgrelemcau  11534  caucvgre  11535  cvg1nlemcxze  11536  cvg1nlemcau  11538  cvg1nlemres  11539  resqrexlemdecn  11566  resqrexlemga  11577  fsum3cvg3  11950  divcnv  12051  cvgratnnlembern  12077  cvgratnnlemseq  12080  cvgratnnlemabsle  12081  cvgratnnlemsumlt  12082  cvgratnnlemrate  12084  cvgratz  12086  eftabs  12210  efcllemp  12212  ege2le3  12225  efcj  12227  eftlub  12244  eflegeo  12255  eirraplem  12331  dvdslelemd  12397  nno  12460  nnoddm1d2  12464  divalglemnqt  12474  divalglemeunn  12475  bitsfzolem  12508  bitsfzo  12509  bitsinv1lem  12515  dvdsbnd  12520  sqgcd  12593  uzwodc  12601  lcmgcdlem  12642  ncoprmgcdne1b  12654  prmind2  12685  isprm5lem  12706  coprm  12709  prmfac1  12717  sqrt2irraplemnn  12744  divdenle  12762  qnumgt0  12763  nn0sqrtelqelz  12771  hashdvds  12786  eulerthlemrprm  12794  eulerthlema  12795  odzdvds  12811  pythagtriplem11  12840  pythagtriplem12  12841  pythagtriplem13  12842  pythagtriplem14  12843  pythagtriplem19  12848  pclemub  12853  pcpre1  12858  pcidlem  12889  dvdsprmpweqle  12903  pcadd  12906  pcmpt  12909  pcmpt2  12910  pcfaclem  12915  pcfac  12916  qexpz  12918  pockthlem  12922  pockthg  12923  1arith  12933  4sqlem5  12948  4sqlem6  12949  4sqlem10  12953  mul4sqlem  12959  4sqlem11  12967  4sqlem12  12968  4sqlem13m  12969  4sqlem14  12970  4sqlem15  12971  4sqlem16  12972  4sqlem17  12973  2expltfac  13005  znnen  13012  exmidunben  13040  nninfdclemp1  13064  nninfdclemlt  13065  nninfdclemf1  13066  strleund  13179  strext  13181  psrbaglesuppg  14679  logbgcd1irraplemexp  15685  logbgcd1irraplemap  15686  wilthlem1  15697  mersenne  15714  perfectlem2  15717  lgslem1  15722  lgsval2lem  15732  lgsdirprm  15756  lgsdir  15757  gausslemma2dlem0h  15778  gausslemma2dlem1a  15780  gausslemma2dlem2  15784  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgseisen  15796  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  2sqlem3  15839  2sqlem8  15845  cvgcmp2nlemabs  16586