Theorem nnred 9270

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  ℕcn 9257

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3220  df-ss 3227  df-int 3955  df-inn 9258

This theorem is referenced by:  exbtwnzlemstep  10634  qbtwnrelemcalc  10642  qbtwnre  10643  flqdiv  10710  modqmulnn  10731  modifeq2int  10775  modaddmodup  10776  modaddmodlo  10777  modsumfzodifsn  10785  addmodlteq  10787  bernneq3  11052  expnbnd  11053  facwordi  11130  faclbnd  11131  faclbnd2  11132  faclbnd3  11133  faclbnd6  11134  facubnd  11135  facavg  11136  bcp1nk  11152  bcval5  11153  caucvgrelemcau  11694  caucvgre  11695  cvg1nlemcxze  11696  cvg1nlemcau  11698  cvg1nlemres  11699  resqrexlemdecn  11726  resqrexlemga  11737  fsum3cvg3  12111  divcnv  12212  cvgratnnlembern  12238  cvgratnnlemseq  12241  cvgratnnlemabsle  12242  cvgratnnlemsumlt  12243  cvgratnnlemrate  12245  cvgratz  12247  eftabs  12371  efcllemp  12373  ege2le3  12386  efcj  12388  eftlub  12405  eflegeo  12416  eirraplem  12492  dvdslelemd  12558  nno  12621  nnoddm1d2  12625  divalglemnqt  12635  divalglemeunn  12636  bitsfzolem  12669  bitsfzo  12670  bitsinv1lem  12676  dvdsbnd  12681  sqgcd  12754  uzwodc  12762  lcmgcdlem  12803  ncoprmgcdne1b  12815  prmind2  12846  isprm5lem  12867  coprm  12870  prmfac1  12878  sqrt2irraplemnn  12905  divdenle  12923  qnumgt0  12924  nn0sqrtelqelz  12932  hashdvds  12947  eulerthlemrprm  12955  eulerthlema  12956  odzdvds  12972  pythagtriplem11  13001  pythagtriplem12  13002  pythagtriplem13  13003  pythagtriplem14  13004  pythagtriplem19  13009  pclemub  13014  pcpre1  13019  pcidlem  13050  dvdsprmpweqle  13064  pcadd  13067  pcmpt  13070  pcmpt2  13071  pcfaclem  13076  pcfac  13077  qexpz  13079  pockthlem  13083  pockthg  13084  1arith  13094  4sqlem5  13109  4sqlem6  13110  4sqlem10  13114  mul4sqlem  13120  4sqlem11  13128  4sqlem12  13129  4sqlem13m  13130  4sqlem14  13131  4sqlem15  13132  4sqlem16  13133  4sqlem17  13134  2expltfac  13166  ballotfilemonn  13169  ballotfilemimin  13197  znnen  13237  exmidunben  13265  nninfdclemp1  13289  nninfdclemlt  13290  nninfdclemf1  13291  strleund  13404  strext  13406  psrbaglesuppg  14951  logbgcd1irraplemexp  15963  logbgcd1irraplemap  15964  pellexlem2  15976  wilthlem1  15978  mersenne  15995  perfectlem2  15998  lgslem1  16003  lgsval2lem  16013  lgsdirprm  16037  lgsdir  16038  gausslemma2dlem0h  16059  gausslemma2dlem1a  16061  gausslemma2dlem2  16065  lgseisenlem1  16073  lgseisenlem2  16074  lgseisenlem3  16075  lgseisen  16077  lgsquadlem1  16080  lgsquadlem2  16081  lgsquadlem3  16082  2sqlem3  16120  2sqlem8  16126  cvgcmp2nlemabs  16956