Theorem nnred 12266

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  ℕcn 12251

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-i2m1 11186  ax-1ne0 11187  ax-rrecex 11190  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-nn 12252

This theorem is used by:  nnne0  12288  nnadddir  12310  uzwo3  12985  modmulnn  13942  bernneq3  14287  expmulnbnd  14291  expnngt1b  14298  facwordi  14345  faclbnd  14346  faclbnd2  14347  faclbnd3  14348  faclbnd5  14354  faclbnd6  14355  facubnd  14356  facavg  14357  bcp1nk  14373  hashf1  14514  swrds2  15003  isercolllem1  15742  isercoll  15745  o1fsum  15891  climcndslem1  15929  climcndslem2  15930  climcnds  15931  eftabs  16154  efcllem  16156  ege2le3  16169  efcj  16171  eftlub  16190  eflegeo  16202  eirrlem  16285  fzm1ndvds  16405  nno  16465  nnoddm1d2  16469  bitsfzolem  16517  bitsfzo  16518  bitsinv1lem  16524  sadcaddlem  16540  smueqlem  16573  bezoutlem3  16624  bezoutlem4  16625  sqgcd  16645  nn0expgcd  16647  lcmgcdlem  16689  lcmf  16716  prmind2  16768  coprm  16795  prmfac1  16804  prmndvdsfaclt  16809  divdenle  16833  qnumgt0  16834  zsqrtelqelz  16842  hashdvds  16859  eulerthlem2  16866  odzdvds  16880  vfermltl  16886  modprm0  16890  pythagtriplem11  16910  pythagtriplem13  16912  pythagtriplem19  16918  pclem  16923  pcpre1  16927  pcidlem  16957  dvdsprmpweqle  16971  pcadd  16974  pcmpt  16977  pcmpt2  16978  pcfaclem  16983  pcfac  16984  qexpz  16986  pockthlem  16990  pockthg  16991  prmreclem1  17001  prmreclem3  17003  prmreclem4  17004  prmreclem5  17005  1arithlem4  17011  1arith  17012  4sqlem5  17027  4sqlem6  17028  4sqlem10  17032  mul4sqlem  17038  4sqlem11  17040  4sqlem12  17041  4sqlem13  17042  4sqlem14  17043  4sqlem15  17044  4sqlem16  17045  4sqlem17  17046  vdwlem1  17066  vdwlem3  17068  vdwlem6  17071  vdwlem9  17074  vdwlem10  17075  vdwlem12  17077  vdwnnlem3  17082  ramub1lem1  17111  prmolefac  17131  prmgaplem4  17139  prmgaplem5  17140  prmgaplem6  17141  prmgaplem8  17143  2expltfac  17177  cshwshashnsame  17188  setsstruct2  17259  chnub  18703  psgnunilem4  19598  mndodconglem  19642  oddvds  19648  sylow1lem1  19699  sylow1lem5  19703  fislw  19726  efgredlem  19848  gexexlem  19953  zringlpirlem3  21651  prmirredlem  21659  fvmptnn04if  23043  fvmptnn04ifb  23045  fvmptnn04ifc  23046  fvmptnn04ifd  23047  chfacfisf  23048  chfacfisfcpmat  23049  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  lebnumii  25162  lmnn  25459  ovolunlem1a  25692  ovoliunlem1  25698  ovolicc2lem3  25715  ovolicc2lem4  25716  iundisj  25744  voliunlem1  25746  uniioombllem3  25781  dyadf  25787  dyadovol  25789  dyaddisjlem  25791  dyadmaxlem  25793  opnmbllem  25797  vitalilem4  25807  mbfi1fseqlem1  25911  mbfi1fseqlem3  25913  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  mbfi1fseqlem6  25916  itg2gt0  25956  itg2cnlem2  25958  dgreq0  26459  dgrco  26469  elqaalem2  26518  aaliou3lem2  26543  aaliou3lem8  26545  aaliou3lem9  26550  rtprmirr  26962  leibpi  27144  log2tlbnd  27147  birthdaylem3  27155  amgm  27192  emcllem2  27198  harmonicbnd4  27212  lgamgulmlem1  27230  lgamgulmlem2  27231  lgamgulmlem3  27232  lgamgulmlem4  27233  lgamgulmlem5  27234  lgamgulmlem6  27235  lgamucov  27239  lgamcvg2  27256  wilthlem1  27269  ftalem5  27278  basellem1  27282  basellem2  27283  basellem3  27284  basellem4  27285  basellem5  27286  basellem6  27287  basellem8  27289  chtge0  27313  chtwordi  27357  vma1  27367  dvdsflf1o  27388  dvdsflsumcom  27389  fsumfldivdiaglem  27390  sgmmul  27402  chtublem  27412  fsumvma2  27415  logfac2  27418  chpchtsum  27420  chpub  27421  logfaclbnd  27423  logexprlim  27426  mersenne  27428  perfectlem2  27431  dchrelbas4  27444  bposlem1  27485  bposlem2  27486  bposlem3  27487  bposlem4  27488  bposlem5  27489  bposlem6  27490  bposlem7  27491  bposlem9  27493  lgslem1  27498  lgsval2lem  27508  lgsdirprm  27532  lgsdir  27533  lgsne0  27536  lgsqrlem2  27548  gausslemma2dlem0h  27564  gausslemma2dlem0i  27565  gausslemma2dlem1a  27566  gausslemma2dlem2  27568  gausslemma2dlem7  27574  gausslemma2d  27575  lgseisenlem1  27576  lgseisenlem2  27577  lgseisenlem3  27578  lgseisenlem4  27579  lgseisen  27580  lgsquadlem1  27581  lgsquadlem2  27582  lgsquadlem3  27583  2sqlem3  27621  2sqlem8  27627  2sqblem  27632  2sqmod  27637  chebbnd1lem1  27670  chebbnd1lem3  27672  chtppilimlem1  27674  rplogsumlem1  27685  rplogsumlem2  27686  dchrisum0lem1a  27687  rpvmasumlem  27688  dchrisumlema  27689  dchrisumlem1  27690  dchrisumlem2  27691  dchrisumlem3  27692  dchrvmasumiflem1  27702  dchrisum0flblem2  27710  dchrisum0re  27714  dchrisum0lem1b  27716  dchrisum0lem1  27717  dirith2  27729  selbergb  27750  selberg2lem  27751  logdivbnd  27757  selberg3lem2  27759  selberg4lem1  27761  pntrsumo1  27766  pntrsumbnd2  27768  pntrlog2bndlem1  27778  pntrlog2bndlem2  27779  pntrlog2bndlem3  27780  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  pntpbnd1a  27786  pntpbnd1  27787  pntibndlem2a  27791  pntibndlem2  27792  pntlemg  27799  pntlemh  27800  pntlemj  27804  pntlemf  27806  ostth2lem1  27819  padicabvf  27832  padicabvcxp  27833  ostth2lem2  27835  ostth2lem3  27836  ostth2lem4  27837  ostth2  27838  ostth3  27839  numclwwlk5  30776  numclwwlk7  30779  nrt2irr  30861  ubthlem2  31260  minvecolem4  31269  iundisjf  32971  ssnnssfz  33169  iundisjfi  33178  nexple  33214  2exple2exp  33215  pfxlsw2ccat  33303  pmtrto1cl  33450  psgnfzto1stlem  33451  fzto1st1  33453  fzto1st  33454  psgnfzto1st  33456  cycpmco2lem6  33482  cycpmco2lem7  33483  fldextrspundgdvdslem  34101  fldextrspundgdvds  34102  fldext2rspun  34103  smatrcl  34217  smattr  34220  smatbl  34221  smatbr  34222  1smat1  34225  submateqlem1  34228  submateqlem2  34229  submateq  34230  esumcst  34484  fiunelros  34596  oddpwdc  34776  eulerpartlems  34782  eulerpartlemgc  34784  fiblem  34820  dstfrvunirn  34897  dstfrvclim1  34900  ballotlemimin  34928  fsum2dsub  35026  reprinfz1  35041  hgt750lemd  35067  hgt750lemb  35075  hgt750leme  35077  tgoldbachgtde  35079  tgoldbachgt  35082  subfaclim  35701  subfacval3  35702  erdszelem7  35710  erdszelem8  35711  erdsze2lem2  35717  cvmliftlem2  35799  cvmliftlem6  35803  cvmliftlem7  35804  cvmliftlem8  35805  cvmliftlem9  35806  cvmliftlem10  35807  cvmliftlem13  35809  bcprod  36251  bccolsum  36252  faclimlem2  36257  faclim2  36261  nn0prpwlem  36874  knoppcnlem10  37132  knoppndvlem15  37156  knoppndvlem17  37158  knoppndvlem18  37159  knoppndvlem19  37160  knoppndvlem20  37161  knoppndvlem21  37162  poimirlem3  38315  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem9  38321  poimirlem10  38322  poimirlem11  38323  poimirlem12  38324  poimirlem13  38325  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem21  38333  poimirlem22  38334  poimirlem23  38335  poimirlem26  38338  poimirlem28  38340  opnmbllem0  38348  mblfinlem2  38350  incsequz  38440  nninfnub  38443  lcmineqlem4  42840  lcmineqlem10  42846  lcmineqlem11  42847  lcmineqlem15  42851  lcmineqlem18  42854  lcmineqlem19  42855  lcmineqlem20  42856  lcmineqlem21  42857  lcmineqlem22  42858  lcmineqlem23  42859  lcmineqlem  42860  3lexlogpow5ineq2  42863  3lexlogpow5ineq4  42864  3lexlogpow2ineq2  42867  3lexlogpow5ineq5  42868  aks4d1p1p3  42877  aks4d1p1p2  42878  aks4d1p1p4  42879  aks4d1p1p5  42883  aks4d1p1  42884  aks4d1p3  42886  aks4d1p4  42887  aks4d1p5  42888  aks4d1p6  42889  aks4d1p7  42891  aks4d1p8d2  42893  aks4d1p8  42895  aks4d1p9  42896  posbezout  42908  primrootlekpowne0  42913  primrootspoweq0  42914  aks6d1c1  42924  hashscontpow1  42929  aks6d1c3  42931  aks6d1c4  42932  aks6d1c2lem4  42935  aks6d1c2  42938  aks6d1c5lem1  42944  2ap1caineq  42953  sticksstones1  42954  sticksstones2  42955  sticksstones3  42956  sticksstones6  42959  sticksstones7  42960  sticksstones10  42963  sticksstones12a  42965  sticksstones12  42966  aks6d1c6lem4  42981  bcled  42986  bcle2d  42987  aks6d1c7lem1  42988  aks6d1c7lem2  42989  unitscyglem1  43003  unitscyglem2  43004  unitscyglem4  43006  unitscyglem5  43007  aks5lem8  43009  oexpreposd  43124  fimgmcyclem  43342  fimgmcyc  43343  flt4lem5e  43429  flt4lem6  43431  flt4lem7  43432  fltltc  43434  fltnltalem  43435  fltnlta  43436  3cubeslem3r  43459  irrapxlem3  43592  irrapxlem4  43593  irrapxlem5  43594  pellexlem2  43598  pellexlem6  43602  pell14qrgt0  43627  pell14qrgapw  43644  pellfundgt1  43651  rmspecsqrtnq  43674  ltrmxnn0  43717  jm3.1lem1  43785  jm3.1lem3  43787  dgraa0p  43917  hashnzfz2  45072  rfcnnnub  45797  nnxrd  46034  fzisoeu  46060  fsumnncl  46329  sumnnodd  46387  limsup10exlem  46527  stoweidlem1  46756  stoweidlem3  46758  stoweidlem11  46766  stoweidlem17  46772  stoweidlem20  46775  stoweidlem25  46780  stoweidlem26  46781  stoweidlem34  46789  stoweidlem38  46793  stoweidlem42  46797  stoweidlem44  46799  stoweidlem51  46806  stoweidlem59  46814  stoweidlem60  46815  wallispi  46825  wallispi2  46828  stirlinglem3  46831  stirlinglem4  46832  stirlinglem8  46836  stirlinglem10  46838  stirlinglem12  46840  stirlinglem15  46843  dirkertrigeqlem2  46854  dirkertrigeqlem3  46855  dirkercncflem2  46859  fourierdlem11  46873  fourierdlem14  46876  fourierdlem15  46877  fourierdlem20  46882  fourierdlem31  46893  fourierdlem64  46925  fourierdlem93  46954  fourierdlem95  46956  fourierdlem103  46964  fourierdlem104  46965  fourierdlem112  46973  sqwvfourb  46984  etransclem3  46992  etransclem19  47008  etransclem23  47012  etransclem24  47013  etransclem25  47014  etransclem32  47021  etransclem35  47024  etransclem41  47030  etransclem48  47037  qndenserrnbllem  47049  hoiqssbllem1  47377  hoiqssbllem2  47378  ovolval5lem1  47407  ovolval5lem2  47408  iccpartlt  48214  iccpartgt  48217  odz2prm2pw  48356  fmtnoprmfac1lem  48357  2pwp1prm  48382  sfprmdvdsmersenne  48396  lighneallem2  48399  proththdlem  48406  perfectALTVlem2  48528  gbowge7  48569  ztprmneprm  49168  pgrple2abl  49186  logbpw2m1  49388  nnpw2pmod  49404  nnolog2flm1  49411  blennngt2o2  49413  itcovalt2lem2lem1  49494