Theorem nnred 9111

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 7986  ℕcn 9098

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 4201  ax-cnex 8078  ax-resscn 8079  ax-1re 8081  ax-addrcl 8084

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 2801  df-in 3203  df-ss 3210  df-int 3923  df-inn 9099

This theorem is referenced by:  exbtwnzlemstep  10454  qbtwnrelemcalc  10462  qbtwnre  10463  flqdiv  10530  modqmulnn  10551  modifeq2int  10595  modaddmodup  10596  modaddmodlo  10597  modsumfzodifsn  10605  addmodlteq  10607  bernneq3  10871  expnbnd  10872  facwordi  10949  faclbnd  10950  faclbnd2  10951  faclbnd3  10952  faclbnd6  10953  facubnd  10954  facavg  10955  bcp1nk  10971  bcval5  10972  caucvgrelemcau  11477  caucvgre  11478  cvg1nlemcxze  11479  cvg1nlemcau  11481  cvg1nlemres  11482  resqrexlemdecn  11509  resqrexlemga  11520  fsum3cvg3  11893  divcnv  11994  cvgratnnlembern  12020  cvgratnnlemseq  12023  cvgratnnlemabsle  12024  cvgratnnlemsumlt  12025  cvgratnnlemrate  12027  cvgratz  12029  eftabs  12153  efcllemp  12155  ege2le3  12168  efcj  12170  eftlub  12187  eflegeo  12198  eirraplem  12274  dvdslelemd  12340  nno  12403  nnoddm1d2  12407  divalglemnqt  12417  divalglemeunn  12418  bitsfzolem  12451  bitsfzo  12452  bitsinv1lem  12458  dvdsbnd  12463  sqgcd  12536  uzwodc  12544  lcmgcdlem  12585  ncoprmgcdne1b  12597  prmind2  12628  isprm5lem  12649  coprm  12652  prmfac1  12660  sqrt2irraplemnn  12687  divdenle  12705  qnumgt0  12706  nn0sqrtelqelz  12714  hashdvds  12729  eulerthlemrprm  12737  eulerthlema  12738  odzdvds  12754  pythagtriplem11  12783  pythagtriplem12  12784  pythagtriplem13  12785  pythagtriplem14  12786  pythagtriplem19  12791  pclemub  12796  pcpre1  12801  pcidlem  12832  dvdsprmpweqle  12846  pcadd  12849  pcmpt  12852  pcmpt2  12853  pcfaclem  12858  pcfac  12859  qexpz  12861  pockthlem  12865  pockthg  12866  1arith  12876  4sqlem5  12891  4sqlem6  12892  4sqlem10  12896  mul4sqlem  12902  4sqlem11  12910  4sqlem12  12911  4sqlem13m  12912  4sqlem14  12913  4sqlem15  12914  4sqlem16  12915  4sqlem17  12916  2expltfac  12948  znnen  12955  exmidunben  12983  nninfdclemp1  13007  nninfdclemlt  13008  nninfdclemf1  13009  strleund  13122  strext  13124  psrbaglesuppg  14621  logbgcd1irraplemexp  15627  logbgcd1irraplemap  15628  wilthlem1  15639  mersenne  15656  perfectlem2  15659  lgslem1  15664  lgsval2lem  15674  lgsdirprm  15698  lgsdir  15699  gausslemma2dlem0h  15720  gausslemma2dlem1a  15722  gausslemma2dlem2  15726  lgseisenlem1  15734  lgseisenlem2  15735  lgseisenlem3  15736  lgseisen  15738  lgsquadlem1  15741  lgsquadlem2  15742  lgsquadlem3  15743  2sqlem3  15781  2sqlem8  15787  cvgcmp2nlemabs  16331