Theorem nnred 8995

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℝcr 7871  ℕcn 8982

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-in 3159  df-ss 3166  df-int 3871  df-inn 8983

This theorem is referenced by:  exbtwnzlemstep  10316  qbtwnrelemcalc  10324  qbtwnre  10325  flqdiv  10392  modqmulnn  10413  modifeq2int  10457  modaddmodup  10458  modaddmodlo  10459  modsumfzodifsn  10467  addmodlteq  10469  bernneq3  10733  expnbnd  10734  facwordi  10811  faclbnd  10812  faclbnd2  10813  faclbnd3  10814  faclbnd6  10815  facubnd  10816  facavg  10817  bcp1nk  10833  bcval5  10834  caucvgrelemcau  11124  caucvgre  11125  cvg1nlemcxze  11126  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemdecn  11156  resqrexlemga  11167  fsum3cvg3  11539  divcnv  11640  cvgratnnlembern  11666  cvgratnnlemseq  11669  cvgratnnlemabsle  11670  cvgratnnlemsumlt  11671  cvgratnnlemrate  11673  cvgratz  11675  eftabs  11799  efcllemp  11801  ege2le3  11814  efcj  11816  eftlub  11833  eflegeo  11844  eirraplem  11920  dvdslelemd  11985  nno  12047  nnoddm1d2  12051  divalglemnqt  12061  divalglemeunn  12062  dvdsbnd  12093  sqgcd  12166  uzwodc  12174  lcmgcdlem  12215  ncoprmgcdne1b  12227  prmind2  12258  isprm5lem  12279  coprm  12282  prmfac1  12290  sqrt2irraplemnn  12317  divdenle  12335  qnumgt0  12336  nn0sqrtelqelz  12344  hashdvds  12359  eulerthlemrprm  12367  eulerthlema  12368  odzdvds  12383  pythagtriplem11  12412  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem14  12415  pythagtriplem19  12420  pclemub  12425  pcpre1  12430  pcidlem  12461  dvdsprmpweqle  12475  pcadd  12478  pcmpt  12481  pcmpt2  12482  pcfaclem  12487  pcfac  12488  qexpz  12490  pockthlem  12494  pockthg  12495  1arith  12505  4sqlem5  12520  4sqlem6  12521  4sqlem10  12525  mul4sqlem  12531  4sqlem11  12539  4sqlem12  12540  4sqlem13m  12541  4sqlem14  12542  4sqlem15  12543  4sqlem16  12544  4sqlem17  12545  znnen  12555  exmidunben  12583  nninfdclemp1  12607  nninfdclemlt  12608  nninfdclemf1  12609  strleund  12721  strext  12723  psrbaglesuppg  14158  logbgcd1irraplemexp  15100  logbgcd1irraplemap  15101  wilthlem1  15112  lgslem1  15116  lgsval2lem  15126  lgsdirprm  15150  lgsdir  15151  gausslemma2dlem0h  15172  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisen  15190  lgsquadlem1  15191  2sqlem3  15204  2sqlem8  15210  cvgcmp2nlemabs  15522