Theorem nnred 9327

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

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

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 4251  ax-cnex 8277  ax-resscn 8278  ax-1re 8280  ax-addrcl 8283

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 9315

This theorem is used by:  exbtwnzlemstep  10700  qbtwnrelemcalc  10708  qbtwnre  10709  flqdiv  10780  modqmulnn  10801  modifeq2int  10845  modaddmodup  10846  modaddmodlo  10847  modsumfzodifsn  10855  addmodlteq  10857  bernneq3  11122  expnbnd  11123  facwordi  11201  faclbnd  11202  faclbnd2  11203  faclbnd3  11204  faclbnd6  11205  facubnd  11206  facavg  11207  bcp1nk  11223  bcval5  11224  hashf1  11310  caucvgrelemcau  11769  caucvgre  11770  cvg1nlemcxze  11771  cvg1nlemcau  11773  cvg1nlemres  11774  resqrexlemdecn  11801  resqrexlemga  11812  fsum3cvg3  12189  divcnv  12290  cvgratnnlembern  12316  cvgratnnlemseq  12319  cvgratnnlemabsle  12320  cvgratnnlemsumlt  12321  cvgratnnlemrate  12323  cvgratz  12325  eftabs  12449  efcllemp  12451  ege2le3  12464  efcj  12466  eftlub  12483  eflegeo  12494  eirraplem  12570  dvdslelemd  12636  nno  12699  nnoddm1d2  12703  divalglemnqt  12713  divalglemeunn  12714  bitsfzolem  12747  bitsfzo  12748  bitsinv1lem  12754  dvdsbnd  12759  sqgcd  12832  uzwodc  12840  lcmgcdlem  12881  ncoprmgcdne1b  12893  prmind2  12924  isprm5lem  12946  coprm  12949  prmfac1  12957  sqrt2irraplemnn  12985  divdenle  13003  qnumgt0  13004  nn0sqrtelqelz  13012  hashdvds  13029  eulerthlemrprm  13037  eulerthlema  13038  odzdvds  13054  pythagtriplem11  13083  pythagtriplem12  13084  pythagtriplem13  13085  pythagtriplem14  13086  pythagtriplem19  13091  pclemub  13096  pcpre1  13101  pcidlem  13132  dvdsprmpweqle  13146  pcadd  13149  pcmpt  13152  pcmpt2  13153  pcfaclem  13158  pcfac  13159  qexpz  13161  pockthlem  13165  pockthg  13166  1arith  13176  4sqlem5  13191  4sqlem6  13192  4sqlem10  13196  mul4sqlem  13202  4sqlem11  13210  4sqlem12  13211  4sqlem13m  13212  4sqlem14  13213  4sqlem15  13214  4sqlem16  13215  4sqlem17  13216  2expltfac  13249  ballotfilemonn  13280  ballotfilemimin  13308  znnen  13348  exmidunben  13376  nninfdclemp1  13400  nninfdclemlt  13401  nninfdclemf1  13402  strleund  13517  strext  13519  psrbaglesuppg  15172  logfac  16138  logbgcd1irraplemexp  16216  logbgcd1irraplemap  16217  zprmlogbaplem1  16227  zprmlogbaplem2  16228  log2tlbndlog2  16232  birthdaylem3  16239  pellexlem2  16242  wilthlem1  16244  chtqge0  16259  chtqwordi  16275  ppiqltx  16293  chtublem  16307  mersenne  16309  perfectlem2  16312  prmefexple  16320  bposlem1  16323  bposlem2  16324  bposlem3  16325  bposlem4  16326  bposlem5  16327  bposlem6  16328  bposlem7  16329  bposlem9  16331  lgslem1  16336  lgsval2lem  16346  lgsdirprm  16370  lgsdir  16371  gausslemma2dlem0h  16392  gausslemma2dlem1a  16394  gausslemma2dlem2  16398  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem3  16408  lgseisen  16410  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  2sqlem3  16453  2sqlem8  16459  cvgcmp2nlemabs  17299