Theorem nnred 12201

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℕcn 12186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187

This theorem is referenced by:  nnne0  12220  uzwo3  12902  modmulnn  13851  bernneq3  14196  expmulnbnd  14200  expnngt1b  14207  facwordi  14254  faclbnd  14255  faclbnd2  14256  faclbnd3  14257  faclbnd5  14263  faclbnd6  14264  facubnd  14265  facavg  14266  bcp1nk  14282  hashf1  14422  swrds2  14906  isercolllem1  15631  isercoll  15634  o1fsum  15779  climcndslem1  15815  climcndslem2  15816  climcnds  15817  eftabs  16041  efcllem  16043  ege2le3  16056  efcj  16058  eftlub  16077  eflegeo  16089  eirrlem  16172  fzm1ndvds  16292  nno  16352  nnoddm1d2  16356  bitsfzolem  16404  bitsfzo  16405  bitsinv1lem  16411  sadcaddlem  16427  smueqlem  16460  bezoutlem3  16511  bezoutlem4  16512  sqgcd  16532  nn0expgcd  16534  lcmgcdlem  16576  lcmf  16603  prmind2  16655  coprm  16681  prmfac1  16690  prmndvdsfaclt  16695  divdenle  16719  qnumgt0  16720  zsqrtelqelz  16728  hashdvds  16745  eulerthlem2  16752  odzdvds  16766  vfermltl  16772  modprm0  16776  pythagtriplem11  16796  pythagtriplem13  16798  pythagtriplem19  16804  pclem  16809  pcpre1  16813  pcidlem  16843  dvdsprmpweqle  16857  pcadd  16860  pcmpt  16863  pcmpt2  16864  pcfaclem  16869  pcfac  16870  qexpz  16872  pockthlem  16876  pockthg  16877  prmreclem1  16887  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  1arithlem4  16897  1arith  16898  4sqlem5  16913  4sqlem6  16914  4sqlem10  16918  mul4sqlem  16924  4sqlem11  16926  4sqlem12  16927  4sqlem13  16928  4sqlem14  16929  4sqlem15  16930  4sqlem16  16931  4sqlem17  16932  vdwlem1  16952  vdwlem3  16954  vdwlem6  16957  vdwlem9  16960  vdwlem10  16961  vdwlem12  16963  vdwnnlem3  16968  ramub1lem1  16997  prmolefac  17017  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  prmgaplem8  17029  2expltfac  17063  cshwshashnsame  17074  setsstruct2  17144  psgnunilem4  19427  mndodconglem  19471  oddvds  19477  sylow1lem1  19528  sylow1lem5  19532  fislw  19555  efgredlem  19677  gexexlem  19782  zringlpirlem3  21374  prmirredlem  21382  fvmptnn04if  22736  fvmptnn04ifb  22738  fvmptnn04ifc  22739  fvmptnn04ifd  22740  chfacfisf  22741  chfacfisfcpmat  22742  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  lebnumii  24865  lmnn  25163  ovolunlem1a  25397  ovoliunlem1  25403  ovolicc2lem3  25420  ovolicc2lem4  25421  iundisj  25449  voliunlem1  25451  uniioombllem3  25486  dyadf  25492  dyadovol  25494  dyaddisjlem  25496  dyadmaxlem  25498  opnmbllem  25502  vitalilem4  25512  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  itg2gt0  25661  itg2cnlem2  25663  dgreq0  26171  dgrco  26181  elqaalem2  26228  aaliou3lem2  26251  aaliou3lem8  26253  aaliou3lem9  26258  rtprmirr  26670  leibpi  26852  log2tlbnd  26855  birthdaylem3  26863  amgm  26901  emcllem2  26907  harmonicbnd4  26921  lgamgulmlem1  26939  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamucov  26948  lgamcvg2  26965  wilthlem1  26978  ftalem5  26987  basellem1  26991  basellem2  26992  basellem3  26993  basellem4  26994  basellem5  26995  basellem6  26996  basellem8  26998  chtge0  27022  chtwordi  27066  vma1  27076  dvdsflf1o  27097  dvdsflsumcom  27098  fsumfldivdiaglem  27099  sgmmul  27112  chtublem  27122  fsumvma2  27125  logfac2  27128  chpchtsum  27130  chpub  27131  logfaclbnd  27133  logexprlim  27136  mersenne  27138  perfectlem2  27141  dchrelbas4  27154  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem7  27201  bposlem9  27203  lgslem1  27208  lgsval2lem  27218  lgsdirprm  27242  lgsdir  27243  lgsne0  27246  lgsqrlem2  27258  gausslemma2dlem0h  27274  gausslemma2dlem0i  27275  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  2sqlem3  27331  2sqlem8  27337  2sqblem  27342  2sqmod  27347  chebbnd1lem1  27380  chebbnd1lem3  27382  chtppilimlem1  27384  rplogsumlem1  27395  rplogsumlem2  27396  dchrisum0lem1a  27397  rpvmasumlem  27398  dchrisumlema  27399  dchrisumlem1  27400  dchrisumlem2  27401  dchrisumlem3  27402  dchrvmasumiflem1  27412  dchrisum0flblem2  27420  dchrisum0re  27424  dchrisum0lem1b  27426  dchrisum0lem1  27427  dirith2  27439  selbergb  27460  selberg2lem  27461  logdivbnd  27467  selberg3lem2  27469  selberg4lem1  27471  pntrsumo1  27476  pntrsumbnd2  27478  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntpbnd1a  27496  pntpbnd1  27497  pntibndlem2a  27501  pntibndlem2  27502  pntlemg  27509  pntlemh  27510  pntlemj  27514  pntlemf  27516  ostth2lem1  27529  padicabvf  27542  padicabvcxp  27543  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ostth2  27548  ostth3  27549  numclwwlk5  30317  numclwwlk7  30320  nrt2irr  30402  ubthlem2  30800  minvecolem4  30809  iundisjf  32518  ssnnssfz  32710  iundisjfi  32719  nexple  32769  2exple2exp  32770  pfxlsw2ccat  32872  chnub  32938  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st1  33059  fzto1st  33060  psgnfzto1st  33062  cycpmco2lem6  33088  cycpmco2lem7  33089  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  fldext2rspun  33677  smatrcl  33786  smattr  33789  smatbl  33790  smatbr  33791  1smat1  33794  submateqlem1  33797  submateqlem2  33798  submateq  33799  esumcst  34053  fiunelros  34164  oddpwdc  34345  eulerpartlems  34351  eulerpartlemgc  34353  fiblem  34389  dstfrvunirn  34466  dstfrvclim1  34469  ballotlemimin  34497  fsum2dsub  34598  reprinfz1  34613  hgt750lemd  34639  hgt750lemb  34647  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgt  34654  subfaclim  35175  subfacval3  35176  erdszelem7  35184  erdszelem8  35185  erdsze2lem2  35191  cvmliftlem2  35273  cvmliftlem6  35277  cvmliftlem7  35278  cvmliftlem8  35279  cvmliftlem9  35280  cvmliftlem10  35281  cvmliftlem13  35283  bcprod  35725  bccolsum  35726  faclimlem2  35731  faclim2  35735  nn0prpwlem  36310  knoppcnlem10  36490  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem18  36517  knoppndvlem19  36518  knoppndvlem20  36519  knoppndvlem21  36520  poimirlem3  37617  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem26  37640  poimirlem28  37642  opnmbllem0  37650  mblfinlem2  37652  incsequz  37742  nninfnub  37745  lcmineqlem4  42020  lcmineqlem10  42026  lcmineqlem11  42027  lcmineqlem15  42031  lcmineqlem18  42034  lcmineqlem19  42035  lcmineqlem20  42036  lcmineqlem21  42037  lcmineqlem22  42038  lcmineqlem23  42039  lcmineqlem  42040  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p3  42066  aks4d1p4  42067  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7  42071  aks4d1p8d2  42073  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  primrootlekpowne0  42093  primrootspoweq0  42094  aks6d1c1  42104  hashscontpow1  42109  aks6d1c3  42111  aks6d1c4  42112  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5lem1  42124  2ap1caineq  42133  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem4  42161  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  unitscyglem1  42183  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  aks5lem8  42189  nnadddir  42258  oexpreposd  42310  fimgmcyclem  42521  fimgmcyc  42522  flt4lem5e  42644  flt4lem6  42646  flt4lem7  42647  fltltc  42649  fltnltalem  42650  fltnlta  42651  3cubeslem3r  42675  irrapxlem3  42812  irrapxlem4  42813  irrapxlem5  42814  pellexlem2  42818  pellexlem6  42822  pell14qrgt0  42847  pell14qrgapw  42864  pellfundgt1  42871  rmspecsqrtnq  42894  ltrmxnn0  42938  jm3.1lem1  43006  jm3.1lem3  43008  dgraa0p  43138  hashnzfz2  44310  rfcnnnub  45030  nnxrd  45272  fzisoeu  45298  fsumnncl  45570  sumnnodd  45628  limsup10exlem  45770  stoweidlem1  45999  stoweidlem3  46001  stoweidlem11  46009  stoweidlem17  46015  stoweidlem20  46018  stoweidlem25  46023  stoweidlem26  46024  stoweidlem34  46032  stoweidlem38  46036  stoweidlem42  46040  stoweidlem44  46042  stoweidlem51  46049  stoweidlem59  46057  stoweidlem60  46058  wallispi  46068  wallispi2  46071  stirlinglem3  46074  stirlinglem4  46075  stirlinglem8  46079  stirlinglem10  46081  stirlinglem12  46083  stirlinglem15  46086  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkercncflem2  46102  fourierdlem11  46116  fourierdlem14  46119  fourierdlem15  46120  fourierdlem20  46125  fourierdlem31  46136  fourierdlem64  46168  fourierdlem93  46197  fourierdlem95  46199  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  sqwvfourb  46227  etransclem3  46235  etransclem19  46251  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem32  46264  etransclem35  46267  etransclem41  46273  etransclem48  46280  qndenserrnbllem  46292  hoiqssbllem1  46620  hoiqssbllem2  46621  ovolval5lem1  46650  ovolval5lem2  46651  iccpartlt  47425  iccpartgt  47428  odz2prm2pw  47564  fmtnoprmfac1lem  47565  2pwp1prm  47590  sfprmdvdsmersenne  47604  lighneallem2  47607  proththdlem  47614  perfectALTVlem2  47723  gbowge7  47764  ztprmneprm  48335  pgrple2abl  48353  logbpw2m1  48556  nnpw2pmod  48572  nnolog2flm1  48579  blennngt2o2  48581  itcovalt2lem2lem1  48662