Theorem nnred 9318

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℝcr 8178  ℕcn 9305

This proof depends on 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 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof 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 3971  df-inn 9306

This theorem is used by:  exbtwnzlemstep  10684  qbtwnrelemcalc  10692  qbtwnre  10693  flqdiv  10760  modqmulnn  10781  modifeq2int  10825  modaddmodup  10826  modaddmodlo  10827  modsumfzodifsn  10835  addmodlteq  10837  bernneq3  11102  expnbnd  11103  facwordi  11180  faclbnd  11181  faclbnd2  11182  faclbnd3  11183  faclbnd6  11184  facubnd  11185  facavg  11186  bcp1nk  11202  bcval5  11203  hashf1  11289  caucvgrelemcau  11748  caucvgre  11749  cvg1nlemcxze  11750  cvg1nlemcau  11752  cvg1nlemres  11753  resqrexlemdecn  11780  resqrexlemga  11791  fsum3cvg3  12165  divcnv  12266  cvgratnnlembern  12292  cvgratnnlemseq  12295  cvgratnnlemabsle  12296  cvgratnnlemsumlt  12297  cvgratnnlemrate  12299  cvgratz  12301  eftabs  12425  efcllemp  12427  ege2le3  12440  efcj  12442  eftlub  12459  eflegeo  12470  eirraplem  12546  dvdslelemd  12612  nno  12675  nnoddm1d2  12679  divalglemnqt  12689  divalglemeunn  12690  bitsfzolem  12723  bitsfzo  12724  bitsinv1lem  12730  dvdsbnd  12735  sqgcd  12808  uzwodc  12816  lcmgcdlem  12857  ncoprmgcdne1b  12869  prmind2  12900  isprm5lem  12921  coprm  12924  prmfac1  12932  sqrt2irraplemnn  12959  divdenle  12977  qnumgt0  12978  nn0sqrtelqelz  12986  hashdvds  13001  eulerthlemrprm  13009  eulerthlema  13010  odzdvds  13026  pythagtriplem11  13055  pythagtriplem12  13056  pythagtriplem13  13057  pythagtriplem14  13058  pythagtriplem19  13063  pclemub  13068  pcpre1  13073  pcidlem  13104  dvdsprmpweqle  13118  pcadd  13121  pcmpt  13124  pcmpt2  13125  pcfaclem  13130  pcfac  13131  qexpz  13133  pockthlem  13137  pockthg  13138  1arith  13148  4sqlem5  13163  4sqlem6  13164  4sqlem10  13168  mul4sqlem  13174  4sqlem11  13182  4sqlem12  13183  4sqlem13m  13184  4sqlem14  13185  4sqlem15  13186  4sqlem16  13187  4sqlem17  13188  2expltfac  13220  ballotfilemonn  13223  ballotfilemimin  13251  znnen  13291  exmidunben  13319  nninfdclemp1  13343  nninfdclemlt  13344  nninfdclemf1  13345  strleund  13459  strext  13461  psrbaglesuppg  15059  logfac  16001  logbgcd1irraplemexp  16076  logbgcd1irraplemap  16077  log2tlbndlog2  16088  birthdaylem3  16095  pellexlem2  16098  wilthlem1  16100  mersenne  16117  perfectlem2  16120  lgslem1  16131  lgsval2lem  16141  lgsdirprm  16165  lgsdir  16166  gausslemma2dlem0h  16187  gausslemma2dlem1a  16189  gausslemma2dlem2  16193  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem3  16203  lgseisen  16205  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  2sqlem3  16248  2sqlem8  16254  cvgcmp2nlemabs  17093