Theorem nnred 9320

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

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

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 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277

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 9308

This theorem is used by:  exbtwnzlemstep  10693  qbtwnrelemcalc  10701  qbtwnre  10702  flqdiv  10772  modqmulnn  10793  modifeq2int  10837  modaddmodup  10838  modaddmodlo  10839  modsumfzodifsn  10847  addmodlteq  10849  bernneq3  11114  expnbnd  11115  facwordi  11193  faclbnd  11194  faclbnd2  11195  faclbnd3  11196  faclbnd6  11197  facubnd  11198  facavg  11199  bcp1nk  11215  bcval5  11216  hashf1  11302  caucvgrelemcau  11761  caucvgre  11762  cvg1nlemcxze  11763  cvg1nlemcau  11765  cvg1nlemres  11766  resqrexlemdecn  11793  resqrexlemga  11804  fsum3cvg3  12181  divcnv  12282  cvgratnnlembern  12308  cvgratnnlemseq  12311  cvgratnnlemabsle  12312  cvgratnnlemsumlt  12313  cvgratnnlemrate  12315  cvgratz  12317  eftabs  12441  efcllemp  12443  ege2le3  12456  efcj  12458  eftlub  12475  eflegeo  12486  eirraplem  12562  dvdslelemd  12628  nno  12691  nnoddm1d2  12695  divalglemnqt  12705  divalglemeunn  12706  bitsfzolem  12739  bitsfzo  12740  bitsinv1lem  12746  dvdsbnd  12751  sqgcd  12824  uzwodc  12832  lcmgcdlem  12873  ncoprmgcdne1b  12885  prmind2  12916  isprm5lem  12938  coprm  12941  prmfac1  12949  sqrt2irraplemnn  12977  divdenle  12995  qnumgt0  12996  nn0sqrtelqelz  13004  hashdvds  13021  eulerthlemrprm  13029  eulerthlema  13030  odzdvds  13046  pythagtriplem11  13075  pythagtriplem12  13076  pythagtriplem13  13077  pythagtriplem14  13078  pythagtriplem19  13083  pclemub  13088  pcpre1  13093  pcidlem  13124  dvdsprmpweqle  13138  pcadd  13141  pcmpt  13144  pcmpt2  13145  pcfaclem  13150  pcfac  13151  qexpz  13153  pockthlem  13157  pockthg  13158  1arith  13168  4sqlem5  13183  4sqlem6  13184  4sqlem10  13188  mul4sqlem  13194  4sqlem11  13202  4sqlem12  13203  4sqlem13m  13204  4sqlem14  13205  4sqlem15  13206  4sqlem16  13207  4sqlem17  13208  2expltfac  13241  ballotfilemonn  13272  ballotfilemimin  13300  znnen  13340  exmidunben  13368  nninfdclemp1  13392  nninfdclemlt  13393  nninfdclemf1  13394  strleund  13508  strext  13510  psrbaglesuppg  15108  logfac  16051  logbgcd1irraplemexp  16126  logbgcd1irraplemap  16127  zprmlogbaplem1  16137  zprmlogbaplem2  16138  log2tlbndlog2  16142  birthdaylem3  16149  pellexlem2  16152  wilthlem1  16154  chtqge0  16169  chtqwordi  16185  ppiqltx  16203  chtublem  16217  mersenne  16219  perfectlem2  16222  prmefexple  16230  bposlem1  16233  bposlem2  16234  bposlem3  16235  bposlem4  16236  bposlem5  16237  lgslem1  16241  lgsval2lem  16251  lgsdirprm  16275  lgsdir  16276  gausslemma2dlem0h  16297  gausslemma2dlem1a  16299  gausslemma2dlem2  16303  lgseisenlem1  16311  lgseisenlem2  16312  lgseisenlem3  16313  lgseisen  16315  lgsquadlem1  16318  lgsquadlem2  16319  lgsquadlem3  16320  2sqlem3  16358  2sqlem8  16364  cvgcmp2nlemabs  17203