Theorem nnred 9199

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8074  ℕcn 9186

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 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-in 3207  df-ss 3214  df-int 3934  df-inn 9187

This theorem is referenced by:  exbtwnzlemstep  10551  qbtwnrelemcalc  10559  qbtwnre  10560  flqdiv  10627  modqmulnn  10648  modifeq2int  10692  modaddmodup  10693  modaddmodlo  10694  modsumfzodifsn  10702  addmodlteq  10704  bernneq3  10968  expnbnd  10969  facwordi  11046  faclbnd  11047  faclbnd2  11048  faclbnd3  11049  faclbnd6  11050  facubnd  11051  facavg  11052  bcp1nk  11068  bcval5  11069  caucvgrelemcau  11601  caucvgre  11602  cvg1nlemcxze  11603  cvg1nlemcau  11605  cvg1nlemres  11606  resqrexlemdecn  11633  resqrexlemga  11644  fsum3cvg3  12018  divcnv  12119  cvgratnnlembern  12145  cvgratnnlemseq  12148  cvgratnnlemabsle  12149  cvgratnnlemsumlt  12150  cvgratnnlemrate  12152  cvgratz  12154  eftabs  12278  efcllemp  12280  ege2le3  12293  efcj  12295  eftlub  12312  eflegeo  12323  eirraplem  12399  dvdslelemd  12465  nno  12528  nnoddm1d2  12532  divalglemnqt  12542  divalglemeunn  12543  bitsfzolem  12576  bitsfzo  12577  bitsinv1lem  12583  dvdsbnd  12588  sqgcd  12661  uzwodc  12669  lcmgcdlem  12710  ncoprmgcdne1b  12722  prmind2  12753  isprm5lem  12774  coprm  12777  prmfac1  12785  sqrt2irraplemnn  12812  divdenle  12830  qnumgt0  12831  nn0sqrtelqelz  12839  hashdvds  12854  eulerthlemrprm  12862  eulerthlema  12863  odzdvds  12879  pythagtriplem11  12908  pythagtriplem12  12909  pythagtriplem13  12910  pythagtriplem14  12911  pythagtriplem19  12916  pclemub  12921  pcpre1  12926  pcidlem  12957  dvdsprmpweqle  12971  pcadd  12974  pcmpt  12977  pcmpt2  12978  pcfaclem  12983  pcfac  12984  qexpz  12986  pockthlem  12990  pockthg  12991  1arith  13001  4sqlem5  13016  4sqlem6  13017  4sqlem10  13021  mul4sqlem  13027  4sqlem11  13035  4sqlem12  13036  4sqlem13m  13037  4sqlem14  13038  4sqlem15  13039  4sqlem16  13040  4sqlem17  13041  2expltfac  13073  znnen  13080  exmidunben  13108  nninfdclemp1  13132  nninfdclemlt  13133  nninfdclemf1  13134  strleund  13247  strext  13249  psrbaglesuppg  14748  logbgcd1irraplemexp  15759  logbgcd1irraplemap  15760  pellexlem2  15772  wilthlem1  15774  mersenne  15791  perfectlem2  15794  lgslem1  15799  lgsval2lem  15809  lgsdirprm  15833  lgsdir  15834  gausslemma2dlem0h  15855  gausslemma2dlem1a  15857  gausslemma2dlem2  15861  lgseisenlem1  15869  lgseisenlem2  15870  lgseisenlem3  15871  lgseisen  15873  lgsquadlem1  15876  lgsquadlem2  15877  lgsquadlem3  15878  2sqlem3  15916  2sqlem8  15922  cvgcmp2nlemabs  16744