Theorem nnred 9300

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℝcr 8172  ℕcn 9287

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4247  ax-cnex 8264  ax-resscn 8265  ax-1re 8267  ax-addrcl 8270

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3969  df-inn 9288

This theorem is referenced by:  exbtwnzlemstep  10665  qbtwnrelemcalc  10673  qbtwnre  10674  flqdiv  10741  modqmulnn  10762  modifeq2int  10806  modaddmodup  10807  modaddmodlo  10808  modsumfzodifsn  10816  addmodlteq  10818  bernneq3  11083  expnbnd  11084  facwordi  11161  faclbnd  11162  faclbnd2  11163  faclbnd3  11164  faclbnd6  11165  facubnd  11166  facavg  11167  bcp1nk  11183  bcval5  11184  hashf1  11270  caucvgrelemcau  11729  caucvgre  11730  cvg1nlemcxze  11731  cvg1nlemcau  11733  cvg1nlemres  11734  resqrexlemdecn  11761  resqrexlemga  11772  fsum3cvg3  12146  divcnv  12247  cvgratnnlembern  12273  cvgratnnlemseq  12276  cvgratnnlemabsle  12277  cvgratnnlemsumlt  12278  cvgratnnlemrate  12280  cvgratz  12282  eftabs  12406  efcllemp  12408  ege2le3  12421  efcj  12423  eftlub  12440  eflegeo  12451  eirraplem  12527  dvdslelemd  12593  nno  12656  nnoddm1d2  12660  divalglemnqt  12670  divalglemeunn  12671  bitsfzolem  12704  bitsfzo  12705  bitsinv1lem  12711  dvdsbnd  12716  sqgcd  12789  uzwodc  12797  lcmgcdlem  12838  ncoprmgcdne1b  12850  prmind2  12881  isprm5lem  12902  coprm  12905  prmfac1  12913  sqrt2irraplemnn  12940  divdenle  12958  qnumgt0  12959  nn0sqrtelqelz  12967  hashdvds  12982  eulerthlemrprm  12990  eulerthlema  12991  odzdvds  13007  pythagtriplem11  13036  pythagtriplem12  13037  pythagtriplem13  13038  pythagtriplem14  13039  pythagtriplem19  13044  pclemub  13049  pcpre1  13054  pcidlem  13085  dvdsprmpweqle  13099  pcadd  13102  pcmpt  13105  pcmpt2  13106  pcfaclem  13111  pcfac  13112  qexpz  13114  pockthlem  13118  pockthg  13119  1arith  13129  4sqlem5  13144  4sqlem6  13145  4sqlem10  13149  mul4sqlem  13155  4sqlem11  13163  4sqlem12  13164  4sqlem13m  13165  4sqlem14  13166  4sqlem15  13167  4sqlem16  13168  4sqlem17  13169  2expltfac  13201  ballotfilemonn  13204  ballotfilemimin  13232  znnen  13272  exmidunben  13300  nninfdclemp1  13324  nninfdclemlt  13325  nninfdclemf1  13326  strleund  13440  strext  13442  psrbaglesuppg  15040  logfac  15978  logbgcd1irraplemexp  16053  logbgcd1irraplemap  16054  log2tlbndlog2  16065  birthdaylem3  16072  pellexlem2  16075  wilthlem1  16077  mersenne  16094  perfectlem2  16097  lgslem1  16102  lgsval2lem  16112  lgsdirprm  16136  lgsdir  16137  gausslemma2dlem0h  16158  gausslemma2dlem1a  16160  gausslemma2dlem2  16164  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgseisen  16176  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  2sqlem3  16219  2sqlem8  16225  cvgcmp2nlemabs  17055