Theorem nnred 9139

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8014  ℕcn 9126

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8106  ax-resscn 8107  ax-1re 8109  ax-addrcl 8112

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-in 3203  df-ss 3210  df-int 3924  df-inn 9127

This theorem is referenced by:  exbtwnzlemstep  10484  qbtwnrelemcalc  10492  qbtwnre  10493  flqdiv  10560  modqmulnn  10581  modifeq2int  10625  modaddmodup  10626  modaddmodlo  10627  modsumfzodifsn  10635  addmodlteq  10637  bernneq3  10901  expnbnd  10902  facwordi  10979  faclbnd  10980  faclbnd2  10981  faclbnd3  10982  faclbnd6  10983  facubnd  10984  facavg  10985  bcp1nk  11001  bcval5  11002  caucvgrelemcau  11512  caucvgre  11513  cvg1nlemcxze  11514  cvg1nlemcau  11516  cvg1nlemres  11517  resqrexlemdecn  11544  resqrexlemga  11555  fsum3cvg3  11928  divcnv  12029  cvgratnnlembern  12055  cvgratnnlemseq  12058  cvgratnnlemabsle  12059  cvgratnnlemsumlt  12060  cvgratnnlemrate  12062  cvgratz  12064  eftabs  12188  efcllemp  12190  ege2le3  12203  efcj  12205  eftlub  12222  eflegeo  12233  eirraplem  12309  dvdslelemd  12375  nno  12438  nnoddm1d2  12442  divalglemnqt  12452  divalglemeunn  12453  bitsfzolem  12486  bitsfzo  12487  bitsinv1lem  12493  dvdsbnd  12498  sqgcd  12571  uzwodc  12579  lcmgcdlem  12620  ncoprmgcdne1b  12632  prmind2  12663  isprm5lem  12684  coprm  12687  prmfac1  12695  sqrt2irraplemnn  12722  divdenle  12740  qnumgt0  12741  nn0sqrtelqelz  12749  hashdvds  12764  eulerthlemrprm  12772  eulerthlema  12773  odzdvds  12789  pythagtriplem11  12818  pythagtriplem12  12819  pythagtriplem13  12820  pythagtriplem14  12821  pythagtriplem19  12826  pclemub  12831  pcpre1  12836  pcidlem  12867  dvdsprmpweqle  12881  pcadd  12884  pcmpt  12887  pcmpt2  12888  pcfaclem  12893  pcfac  12894  qexpz  12896  pockthlem  12900  pockthg  12901  1arith  12911  4sqlem5  12926  4sqlem6  12927  4sqlem10  12931  mul4sqlem  12937  4sqlem11  12945  4sqlem12  12946  4sqlem13m  12947  4sqlem14  12948  4sqlem15  12949  4sqlem16  12950  4sqlem17  12951  2expltfac  12983  znnen  12990  exmidunben  13018  nninfdclemp1  13042  nninfdclemlt  13043  nninfdclemf1  13044  strleund  13157  strext  13159  psrbaglesuppg  14657  logbgcd1irraplemexp  15663  logbgcd1irraplemap  15664  wilthlem1  15675  mersenne  15692  perfectlem2  15695  lgslem1  15700  lgsval2lem  15710  lgsdirprm  15734  lgsdir  15735  gausslemma2dlem0h  15756  gausslemma2dlem1a  15758  gausslemma2dlem2  15762  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem3  15772  lgseisen  15774  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  2sqlem3  15817  2sqlem8  15823  cvgcmp2nlemabs  16514