Theorem nnred 8932

Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nnred	|- ( ph -> A e. RR )

Proof of Theorem nnred

Step	Hyp	Ref	Expression
1		nnssre 8923	. 2 |- NN C_ RR
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sselid 3154	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7810   NNcn 8919

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4122  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2740  df-in 3136  df-ss 3143  df-int 3846  df-inn 8920

This theorem is referenced by:  exbtwnzlemstep  10248  qbtwnrelemcalc  10256  qbtwnre  10257  flqdiv  10321  modqmulnn  10342  modifeq2int  10386  modaddmodup  10387  modaddmodlo  10388  modsumfzodifsn  10396  addmodlteq  10398  bernneq3  10643  expnbnd  10644  facwordi  10720  faclbnd  10721  faclbnd2  10722  faclbnd3  10723  faclbnd6  10724  facubnd  10725  facavg  10726  bcp1nk  10742  bcval5  10743  caucvgrelemcau  10989  caucvgre  10990  cvg1nlemcxze  10991  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemdecn  11021  resqrexlemga  11032  fsum3cvg3  11404  divcnv  11505  cvgratnnlembern  11531  cvgratnnlemseq  11534  cvgratnnlemabsle  11535  cvgratnnlemsumlt  11536  cvgratnnlemrate  11538  cvgratz  11540  eftabs  11664  efcllemp  11666  ege2le3  11679  efcj  11681  eftlub  11698  eflegeo  11709  eirraplem  11784  dvdslelemd  11849  nno  11911  nnoddm1d2  11915  divalglemnqt  11925  divalglemeunn  11926  dvdsbnd  11957  sqgcd  12030  uzwodc  12038  lcmgcdlem  12077  ncoprmgcdne1b  12089  prmind2  12120  isprm5lem  12141  coprm  12144  prmfac1  12152  sqrt2irraplemnn  12179  divdenle  12197  qnumgt0  12198  nn0sqrtelqelz  12206  hashdvds  12221  eulerthlemrprm  12229  eulerthlema  12230  odzdvds  12245  pythagtriplem11  12274  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem14  12277  pythagtriplem19  12282  pclemub  12287  pcpre1  12292  pcidlem  12322  dvdsprmpweqle  12336  pcadd  12339  pcmpt  12341  pcmpt2  12342  pcfaclem  12347  pcfac  12348  qexpz  12350  pockthlem  12354  pockthg  12355  1arith  12365  4sqlem5  12380  4sqlem6  12381  4sqlem10  12385  mul4sqlem  12391  znnen  12399  exmidunben  12427  nninfdclemp1  12451  nninfdclemlt  12452  nninfdclemf1  12453  strleund  12562  strext  12564  logbgcd1irraplemexp  14389  logbgcd1irraplemap  14390  lgslem1  14404  lgsval2lem  14414  lgsdirprm  14438  lgsdir  14439  lgseisenlem1  14453  lgseisenlem2  14454  2sqlem3  14467  2sqlem8  14473  cvgcmp2nlemabs  14783