Theorem nnred 9131

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8006  ℕcn 9118

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 4202  ax-cnex 8098  ax-resscn 8099  ax-1re 8101  ax-addrcl 8104

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 3924  df-inn 9119

This theorem is referenced by:  exbtwnzlemstep  10475  qbtwnrelemcalc  10483  qbtwnre  10484  flqdiv  10551  modqmulnn  10572  modifeq2int  10616  modaddmodup  10617  modaddmodlo  10618  modsumfzodifsn  10626  addmodlteq  10628  bernneq3  10892  expnbnd  10893  facwordi  10970  faclbnd  10971  faclbnd2  10972  faclbnd3  10973  faclbnd6  10974  facubnd  10975  facavg  10976  bcp1nk  10992  bcval5  10993  caucvgrelemcau  11499  caucvgre  11500  cvg1nlemcxze  11501  cvg1nlemcau  11503  cvg1nlemres  11504  resqrexlemdecn  11531  resqrexlemga  11542  fsum3cvg3  11915  divcnv  12016  cvgratnnlembern  12042  cvgratnnlemseq  12045  cvgratnnlemabsle  12046  cvgratnnlemsumlt  12047  cvgratnnlemrate  12049  cvgratz  12051  eftabs  12175  efcllemp  12177  ege2le3  12190  efcj  12192  eftlub  12209  eflegeo  12220  eirraplem  12296  dvdslelemd  12362  nno  12425  nnoddm1d2  12429  divalglemnqt  12439  divalglemeunn  12440  bitsfzolem  12473  bitsfzo  12474  bitsinv1lem  12480  dvdsbnd  12485  sqgcd  12558  uzwodc  12566  lcmgcdlem  12607  ncoprmgcdne1b  12619  prmind2  12650  isprm5lem  12671  coprm  12674  prmfac1  12682  sqrt2irraplemnn  12709  divdenle  12727  qnumgt0  12728  nn0sqrtelqelz  12736  hashdvds  12751  eulerthlemrprm  12759  eulerthlema  12760  odzdvds  12776  pythagtriplem11  12805  pythagtriplem12  12806  pythagtriplem13  12807  pythagtriplem14  12808  pythagtriplem19  12813  pclemub  12818  pcpre1  12823  pcidlem  12854  dvdsprmpweqle  12868  pcadd  12871  pcmpt  12874  pcmpt2  12875  pcfaclem  12880  pcfac  12881  qexpz  12883  pockthlem  12887  pockthg  12888  1arith  12898  4sqlem5  12913  4sqlem6  12914  4sqlem10  12918  mul4sqlem  12924  4sqlem11  12932  4sqlem12  12933  4sqlem13m  12934  4sqlem14  12935  4sqlem15  12936  4sqlem16  12937  4sqlem17  12938  2expltfac  12970  znnen  12977  exmidunben  13005  nninfdclemp1  13029  nninfdclemlt  13030  nninfdclemf1  13031  strleund  13144  strext  13146  psrbaglesuppg  14644  logbgcd1irraplemexp  15650  logbgcd1irraplemap  15651  wilthlem1  15662  mersenne  15679  perfectlem2  15682  lgslem1  15687  lgsval2lem  15697  lgsdirprm  15721  lgsdir  15722  gausslemma2dlem0h  15743  gausslemma2dlem1a  15745  gausslemma2dlem2  15749  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgseisen  15761  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  2sqlem3  15804  2sqlem8  15810  cvgcmp2nlemabs  16430