Theorem nnred 11035

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 11024	. 2 |- NN C_ RR
2		nnred.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3601	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1990   RRcr 9935   NNcn 11020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-nn 11021

This theorem is referenced by:  uzwo3  11783  modmulnn  12688  bernneq3  12992  expmulnbnd  12996  facwordi  13076  faclbnd  13077  faclbnd2  13078  faclbnd3  13079  faclbnd5  13085  faclbnd6  13086  facubnd  13087  facavg  13088  bcp1nk  13104  hashf1  13241  swrds2  13685  isercolllem1  14395  isercoll  14398  o1fsum  14545  climcndslem1  14581  climcndslem2  14582  climcnds  14583  eftabs  14806  efcllem  14808  ege2le3  14820  efcj  14822  eftlub  14839  eflegeo  14851  eirrlem  14932  fzm1ndvds  15044  nno  15098  nnoddm1d2  15102  bitsfzolem  15156  bitsfzo  15157  bitsinv1lem  15163  sadcaddlem  15179  smueqlem  15212  bezoutlem3  15258  bezoutlem4  15259  sqgcd  15278  lcmgcdlem  15319  lcmf  15346  prmind2  15398  coprm  15423  prmfac1  15431  prmndvdsfaclt  15435  divdenle  15457  qnumgt0  15458  zsqrtelqelz  15466  hashdvds  15480  eulerthlem2  15487  odzdvds  15500  modprm1div  15502  vfermltl  15506  modprm0  15510  pythagtriplem11  15530  pythagtriplem13  15532  pythagtriplem19  15538  pclem  15543  pcpre1  15547  pcidlem  15576  dvdsprmpweqle  15590  pcadd  15593  pcmpt  15596  pcmpt2  15597  pcfaclem  15602  pcfac  15603  qexpz  15605  pockthlem  15609  pockthg  15610  prmreclem1  15620  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  1arithlem4  15630  1arith  15631  4sqlem5  15646  4sqlem6  15647  4sqlem10  15651  mul4sqlem  15657  4sqlem11  15659  4sqlem12  15660  4sqlem13  15661  4sqlem14  15662  4sqlem15  15663  4sqlem16  15664  4sqlem17  15665  vdwlem1  15685  vdwlem3  15687  vdwlem6  15690  vdwlem9  15693  vdwlem10  15694  vdwlem12  15696  vdwnnlem3  15701  ramub1lem1  15730  prmolefac  15750  prmgaplem4  15758  prmgaplem5  15759  prmgaplem6  15760  prmgaplem8  15762  2expltfac  15799  cshwshashnsame  15810  setsstruct2  15896  psgnunilem4  17917  mndodconglem  17960  oddvds  17966  sylow1lem1  18013  sylow1lem5  18017  fislw  18040  efgredlem  18160  gexexlem  18255  zringlpirlem3  19834  prmirredlem  19841  fvmptnn04if  20654  fvmptnn04ifb  20656  fvmptnn04ifc  20657  fvmptnn04ifd  20658  chfacfisf  20659  chfacfisfcpmat  20660  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  lebnumii  22765  lmnn  23061  ovolunlem1a  23264  ovoliunlem1  23270  ovolicc2lem3  23287  ovolicc2lem4  23288  iundisj  23316  voliunlem1  23318  uniioombllem3  23353  dyadf  23359  dyadovol  23361  dyaddisjlem  23363  dyadmaxlem  23365  opnmbllem  23369  vitalilem4  23380  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2gt0  23527  itg2cnlem2  23529  dgreq0  24021  dgrco  24031  elqaalem2  24075  aaliou3lem2  24098  aaliou3lem8  24100  aaliou3lem9  24105  leibpi  24669  log2tlbnd  24672  birthdaylem3  24680  amgm  24717  emcllem2  24723  harmonicbnd4  24737  lgamgulmlem1  24755  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamucov  24764  lgamcvg2  24781  wilthlem1  24794  ftalem5  24803  basellem1  24807  basellem2  24808  basellem3  24809  basellem4  24810  basellem5  24811  basellem6  24812  basellem8  24814  chtge0  24838  chtwordi  24882  vma1  24892  dvdsflf1o  24913  dvdsflsumcom  24914  fsumfldivdiaglem  24915  sgmmul  24926  chtublem  24936  fsumvma2  24939  logfac2  24942  chpchtsum  24944  chpub  24945  logfaclbnd  24947  logexprlim  24950  mersenne  24952  perfectlem2  24955  dchrelbas4  24968  bposlem1  25009  bposlem2  25010  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem7  25015  bposlem9  25017  lgslem1  25022  lgslem4  25025  lgsval2lem  25032  lgsdirprm  25056  lgsdir  25057  lgsne0  25060  lgsqrlem2  25072  gausslemma2dlem0h  25088  gausslemma2dlem0i  25089  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  gausslemma2dlem7  25098  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  m1lgs  25113  2sqlem3  25145  2sqlem8  25151  2sqblem  25156  chebbnd1lem1  25158  chebbnd1lem3  25160  chtppilimlem1  25162  rplogsumlem1  25173  rplogsumlem2  25174  dchrisum0lem1a  25175  rpvmasumlem  25176  dchrisumlema  25177  dchrisumlem1  25178  dchrisumlem2  25179  dchrisumlem3  25180  dchrvmasumiflem1  25190  dchrisum0flblem2  25198  dchrisum0re  25202  dchrisum0lem1b  25204  dchrisum0lem1  25205  dirith2  25217  selbergb  25238  selberg2lem  25239  logdivbnd  25245  selberg3lem2  25247  selberg4lem1  25249  pntrsumo1  25254  pntrsumbnd2  25256  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntpbnd1a  25274  pntpbnd1  25275  pntibndlem2a  25279  pntibndlem2  25280  pntlemg  25287  pntlemh  25288  pntlemj  25292  pntlemf  25294  ostth2lem1  25307  padicabvf  25320  padicabvcxp  25321  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  ostth2  25326  ostth3  25327  clwlksfclwwlk  26962  numclwwlk5  27246  numclwwlk7  27249  ubthlem2  27727  minvecolem4  27736  iundisjf  29402  ssnnssfz  29549  iundisjfi  29555  2sqmod  29648  pmtrto1cl  29849  psgnfzto1stlem  29850  fzto1st1  29852  fzto1st  29853  psgnfzto1st  29855  smatrcl  29862  smattr  29865  smatbl  29866  smatbr  29867  1smat1  29870  submateqlem1  29873  submateqlem2  29874  submateq  29875  esumcst  30125  fiunelros  30237  oddpwdc  30416  eulerpartlems  30422  eulerpartlemgc  30424  fiblem  30460  dstfrvunirn  30536  dstfrvclim1  30539  ballotlemimin  30567  fsum2dsub  30685  reprinfz1  30700  hgt750lemd  30726  hgt750lemb  30734  hgt750leme  30736  tgoldbachgtde  30738  tgoldbachgt  30741  subfaclim  31170  subfacval3  31171  erdszelem7  31179  erdszelem8  31180  erdsze2lem2  31186  cvmliftlem2  31268  cvmliftlem6  31272  cvmliftlem7  31273  cvmliftlem8  31274  cvmliftlem9  31275  cvmliftlem10  31276  cvmliftlem13  31278  bcprod  31624  bccolsum  31625  faclimlem2  31630  faclim2  31634  nn0prpwlem  32317  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem18  32520  knoppndvlem19  32521  knoppndvlem20  32522  knoppndvlem21  32523  poimirlem3  33412  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem26  33435  poimirlem28  33437  opnmbllem0  33445  mblfinlem2  33447  incsequz  33544  nninfnub  33547  irrapxlem3  37388  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  pell14qrgt0  37423  pell14qrgapw  37440  pellfundgt1  37447  rmspecsqrtnq  37470  rmspecsqrtnqOLD  37471  ltrmxnn0  37516  jm3.1lem1  37584  jm3.1lem3  37586  dgraa0p  37719  hashnzfz2  38520  rfcnnnub  39195  nnxrd  39201  fzisoeu  39514  fsumnncl  39803  sumnnodd  39862  limsup10exlem  40004  stoweidlem1  40218  stoweidlem3  40220  stoweidlem11  40228  stoweidlem17  40234  stoweidlem20  40237  stoweidlem25  40242  stoweidlem26  40243  stoweidlem34  40251  stoweidlem38  40255  stoweidlem42  40259  stoweidlem44  40261  stoweidlem51  40268  stoweidlem59  40276  stoweidlem60  40277  wallispi  40287  wallispi2  40290  stirlinglem3  40293  stirlinglem4  40294  stirlinglem8  40298  stirlinglem10  40300  stirlinglem12  40302  stirlinglem15  40305  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkercncflem2  40321  fourierdlem11  40335  fourierdlem14  40338  fourierdlem15  40339  fourierdlem20  40344  fourierdlem31  40355  fourierdlem64  40387  fourierdlem93  40416  fourierdlem95  40418  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  sqwvfourb  40446  etransclem3  40454  etransclem19  40470  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem32  40483  etransclem35  40486  etransclem41  40492  etransclem48  40499  qndenserrnbllem  40514  hoiqssbllem1  40836  hoiqssbllem2  40837  ovolval5lem1  40866  ovolval5lem2  40867  iccpartlt  41360  iccpartgt  41363  odz2prm2pw  41475  fmtnoprmfac1lem  41476  2pwp1prm  41503  sfprmdvdsmersenne  41520  lighneallem2  41523  proththdlem  41530  perfectALTVlem2  41631  gbowge7  41651  ztprmneprm  42125  pgrple2abl  42146  logbpw2m1  42361  nnpw2pmod  42377  nnolog2flm1  42384  blennngt2o2  42386