Theorem nnred 8946

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

Syntax hints:   → wi 4   ∈ wcel 2158  ℝcr 7824  ℕcn 8933

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-sep 4133  ax-cnex 7916  ax-resscn 7917  ax-1re 7919  ax-addrcl 7922

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-v 2751  df-in 3147  df-ss 3154  df-int 3857  df-inn 8934

This theorem is referenced by:  exbtwnzlemstep  10262  qbtwnrelemcalc  10270  qbtwnre  10271  flqdiv  10335  modqmulnn  10356  modifeq2int  10400  modaddmodup  10401  modaddmodlo  10402  modsumfzodifsn  10410  addmodlteq  10412  bernneq3  10657  expnbnd  10658  facwordi  10734  faclbnd  10735  faclbnd2  10736  faclbnd3  10737  faclbnd6  10738  facubnd  10739  facavg  10740  bcp1nk  10756  bcval5  10757  caucvgrelemcau  11003  caucvgre  11004  cvg1nlemcxze  11005  cvg1nlemcau  11007  cvg1nlemres  11008  resqrexlemdecn  11035  resqrexlemga  11046  fsum3cvg3  11418  divcnv  11519  cvgratnnlembern  11545  cvgratnnlemseq  11548  cvgratnnlemabsle  11549  cvgratnnlemsumlt  11550  cvgratnnlemrate  11552  cvgratz  11554  eftabs  11678  efcllemp  11680  ege2le3  11693  efcj  11695  eftlub  11712  eflegeo  11723  eirraplem  11798  dvdslelemd  11863  nno  11925  nnoddm1d2  11929  divalglemnqt  11939  divalglemeunn  11940  dvdsbnd  11971  sqgcd  12044  uzwodc  12052  lcmgcdlem  12091  ncoprmgcdne1b  12103  prmind2  12134  isprm5lem  12155  coprm  12158  prmfac1  12166  sqrt2irraplemnn  12193  divdenle  12211  qnumgt0  12212  nn0sqrtelqelz  12220  hashdvds  12235  eulerthlemrprm  12243  eulerthlema  12244  odzdvds  12259  pythagtriplem11  12288  pythagtriplem12  12289  pythagtriplem13  12290  pythagtriplem14  12291  pythagtriplem19  12296  pclemub  12301  pcpre1  12306  pcidlem  12336  dvdsprmpweqle  12350  pcadd  12353  pcmpt  12355  pcmpt2  12356  pcfaclem  12361  pcfac  12362  qexpz  12364  pockthlem  12368  pockthg  12369  1arith  12379  4sqlem5  12394  4sqlem6  12395  4sqlem10  12399  mul4sqlem  12405  znnen  12413  exmidunben  12441  nninfdclemp1  12465  nninfdclemlt  12466  nninfdclemf1  12467  strleund  12577  strext  12579  logbgcd1irraplemexp  14682  logbgcd1irraplemap  14683  lgslem1  14697  lgsval2lem  14707  lgsdirprm  14731  lgsdir  14732  lgseisenlem1  14746  lgseisenlem2  14747  2sqlem3  14760  2sqlem8  14766  cvgcmp2nlemabs  15077