Theorem nnred 12353

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11202  ℕcn 12338

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-i2m1 11271  ax-1ne0 11272  ax-rrecex 11275  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-nn 12339

This theorem is used by:  nnne0  12375  nnadddir  12397  uzwo3  13073  modmulnn  14032  bernneq3  14378  expmulnbnd  14382  expnngt1b  14389  facwordi  14436  faclbnd  14437  faclbnd2  14438  faclbnd3  14439  faclbnd5  14445  faclbnd6  14446  facubnd  14447  facavg  14448  bcp1nk  14464  hashf1  14605  swrds2  15096  isercolllem1  15837  isercoll  15840  o1fsum  15985  climcndslem1  16023  climcndslem2  16024  climcnds  16025  eftabs  16246  efcllem  16248  ege2le3  16261  efcj  16263  eftlub  16282  eflegeo  16294  eirrlem  16377  fzm1ndvds  16497  nno  16557  nnoddm1d2  16561  bitsfzolem  16609  bitsfzo  16610  bitsinv1lem  16616  sadcaddlem  16632  smueqlem  16665  bezoutlem3  16719  bezoutlem4  16720  sqgcd  16741  nn0expgcd  16743  lcmgcdlem  16786  lcmf  16813  prmind2  16865  coprm  16892  prmfac1  16901  prmndvdsfaclt  16906  divdenle  16930  qnumgt0  16931  zsqrtelqelz  16939  hashdvds  16957  eulerthlem2  16964  odzdvds  16978  vfermltl  16984  modprm0  16988  pythagtriplem11  17008  pythagtriplem13  17010  pythagtriplem19  17016  pclem  17021  pcpre1  17025  pcidlem  17055  dvdsprmpweqle  17069  pcadd  17072  pcmpt  17075  pcmpt2  17076  pcfaclem  17081  pcfac  17082  qexpz  17084  pockthlem  17088  pockthg  17089  prmreclem1  17099  prmreclem3  17101  prmreclem4  17102  prmreclem5  17103  1arithlem4  17109  1arith  17110  4sqlem5  17125  4sqlem6  17126  4sqlem10  17130  mul4sqlem  17136  4sqlem11  17138  4sqlem12  17139  4sqlem13  17140  4sqlem14  17141  4sqlem15  17142  4sqlem16  17143  4sqlem17  17144  vdwlem1  17164  vdwlem3  17166  vdwlem6  17169  vdwlem9  17172  vdwlem10  17173  vdwlem12  17175  vdwnnlem3  17180  ramub1lem1  17209  prmolefac  17229  prmgaplem4  17237  prmgaplem5  17238  prmgaplem6  17239  prmgaplem8  17241  2expltfac  17275  cshwshashnsame  17286  setsstruct2  17357  chnub  18801  psgnunilem4  19716  mndodconglem  19760  oddvds  19766  sylow1lem1  19817  sylow1lem5  19821  fislw  19844  efgredlem  19966  gexexlem  20071  zringlpirlem3  21775  prmirredlem  21783  fvmptnn04if  23172  fvmptnn04ifb  23174  fvmptnn04ifc  23175  fvmptnn04ifd  23176  chfacfisf  23177  chfacfisfcpmat  23178  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  lebnumii  25292  lmnn  25589  ovolunlem1a  25822  ovoliunlem1  25828  ovolicc2lem3  25845  ovolicc2lem4  25846  iundisj  25874  voliunlem1  25876  uniioombllem3  25911  dyadf  25917  dyadovol  25919  dyaddisjlem  25921  dyadmaxlem  25923  opnmbllem  25927  vitalilem4  25937  mbfi1fseqlem1  26041  mbfi1fseqlem3  26043  mbfi1fseqlem4  26044  mbfi1fseqlem5  26045  mbfi1fseqlem6  26046  itg2gt0  26086  itg2cnlem2  26088  dgreq0  26589  dgrco  26599  elqaalem2  26648  aaliou3lem2  26675  aaliou3lem8  26677  aaliou3lem9  26682  rtprmirr  27093  leibpi  27275  log2tlbnd  27278  birthdaylem3  27286  amgm  27323  emcllem2  27329  harmonicbnd4  27343  lgamgulmlem1  27361  lgamgulmlem2  27362  lgamgulmlem3  27363  lgamgulmlem4  27364  lgamgulmlem5  27365  lgamgulmlem6  27366  lgamucov  27370  lgamcvg2  27387  wilthlem1  27400  ftalem5  27409  basellem1  27413  basellem2  27414  basellem3  27415  basellem4  27416  basellem5  27417  basellem6  27418  basellem8  27420  chtge0  27444  chtwordi  27488  vma1  27498  dvdsflf1o  27519  dvdsflsumcom  27520  fsumfldivdiaglem  27521  sgmmul  27533  chtublem  27543  fsumvma2  27546  logfac2  27549  chpchtsum  27551  chpub  27552  logfaclbnd  27554  logexprlim  27557  mersenne  27559  perfectlem2  27562  dchrelbas4  27575  bposlem1  27616  bposlem2  27617  bposlem3  27618  bposlem4  27619  bposlem5  27620  bposlem6  27621  bposlem7  27622  bposlem9  27624  lgslem1  27629  lgsval2lem  27639  lgsdirprm  27663  lgsdir  27664  lgsne0  27667  lgsqrlem2  27679  gausslemma2dlem0h  27695  gausslemma2dlem0i  27696  gausslemma2dlem1a  27697  gausslemma2dlem2  27699  gausslemma2dlem7  27705  gausslemma2d  27706  lgseisenlem1  27707  lgseisenlem2  27708  lgseisenlem3  27709  lgseisenlem4  27710  lgseisen  27711  lgsquadlem1  27712  lgsquadlem2  27713  lgsquadlem3  27714  2sqlem3  27752  2sqlem8  27758  2sqblem  27763  2sqmod  27768  chebbnd1lem1  27801  chebbnd1lem3  27803  chtppilimlem1  27805  rplogsumlem1  27816  rplogsumlem2  27817  dchrisum0lem1a  27818  rpvmasumlem  27819  dchrisumlema  27820  dchrisumlem1  27821  dchrisumlem2  27822  dchrisumlem3  27823  dchrvmasumiflem1  27833  dchrisum0flblem2  27841  dchrisum0re  27845  dchrisum0lem1b  27847  dchrisum0lem1  27848  dirith2  27860  selbergb  27881  selberg2lem  27882  logdivbnd  27888  selberg3lem2  27890  selberg4lem1  27892  pntrsumo1  27897  pntrsumbnd2  27899  pntrlog2bndlem1  27909  pntrlog2bndlem2  27910  pntrlog2bndlem3  27911  pntrlog2bndlem4  27912  pntrlog2bndlem5  27913  pntpbnd1a  27917  pntpbnd1  27918  pntibndlem2a  27922  pntibndlem2  27923  pntlemg  27930  pntlemh  27931  pntlemj  27935  pntlemf  27937  ostth2lem1  27950  padicabvf  27963  padicabvcxp  27964  ostth2lem2  27966  ostth2lem3  27967  ostth2lem4  27968  ostth2  27969  ostth3  27970  flt4lem5e  27991  flt4lem6  27993  flt4lem7  27994  numclwwlk5  30994  numclwwlk7  30997  nrt2irr  31079  ubthlem2  31478  minvecolem4  31487  iundisjf  33230  ssnnssfz  33425  iundisjfi  33434  nexple  33470  2exple2exp  33471  pfxlsw2ccat  33559  pmtrto1cl  33706  psgnfzto1stlem  33707  fzto1st1  33709  fzto1st  33710  psgnfzto1st  33712  cycpmco2lem6  33738  cycpmco2lem7  33739  fldextrspundgdvdslem  34358  fldextrspundgdvds  34359  fldext2rspun  34360  smatrcl  34474  smattr  34477  smatbl  34478  smatbr  34479  1smat1  34482  submateqlem1  34485  submateqlem2  34486  submateq  34487  esumcst  34741  fiunelros  34853  oddpwdc  35032  eulerpartlems  35038  eulerpartlemgc  35040  fiblem  35076  dstfrvunirn  35153  dstfrvclim1  35156  ballotlemimin  35184  fsum2dsub  35282  reprinfz1  35297  hgt750lemd  35323  hgt750lemb  35331  hgt750leme  35333  tgoldbachgtde  35335  tgoldbachgt  35338  subfaclim  36039  subfacval3  36040  erdszelem7  36048  erdszelem8  36049  erdsze2lem2  36055  cvmliftlem2  36137  cvmliftlem6  36141  cvmliftlem7  36142  cvmliftlem8  36143  cvmliftlem9  36144  cvmliftlem10  36145  cvmliftlem13  36147  bcprod  36595  bccolsum  36596  faclimlem2  36601  faclim2  36605  nn0prpwlem  37202  knoppcnlem10  37460  knoppndvlem15  37484  knoppndvlem17  37486  knoppndvlem18  37487  knoppndvlem19  37488  knoppndvlem20  37489  knoppndvlem21  37490  poimirlem3  38634  poimirlem6  38637  poimirlem7  38638  poimirlem8  38639  poimirlem9  38640  poimirlem10  38641  poimirlem11  38642  poimirlem12  38643  poimirlem13  38644  poimirlem15  38646  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  poimirlem21  38652  poimirlem22  38653  poimirlem23  38654  poimirlem26  38657  poimirlem28  38659  opnmbllem0  38667  mblfinlem2  38669  incsequz  38775  nninfnub  38778  lcmineqlem4  43175  lcmineqlem10  43181  lcmineqlem11  43182  lcmineqlem15  43186  lcmineqlem18  43189  lcmineqlem19  43190  lcmineqlem20  43191  lcmineqlem21  43192  lcmineqlem22  43193  lcmineqlem23  43194  lcmineqlem  43195  3lexlogpow5ineq2  43198  3lexlogpow5ineq4  43199  3lexlogpow2ineq2  43202  3lexlogpow5ineq5  43203  aks4d1p1p3  43212  aks4d1p1p2  43213  aks4d1p1p4  43214  aks4d1p1p5  43218  aks4d1p1  43219  aks4d1p3  43221  aks4d1p4  43222  aks4d1p5  43223  aks4d1p6  43224  aks4d1p7  43226  aks4d1p8d2  43228  aks4d1p8  43230  aks4d1p9  43231  posbezout  43243  primrootlekpowne0  43248  primrootspoweq0  43249  aks6d1c1  43259  hashscontpow1  43264  aks6d1c3  43266  aks6d1c4  43267  aks6d1c2lem4  43270  aks6d1c2  43273  aks6d1c5lem1  43279  2ap1caineq  43288  sticksstones1  43289  sticksstones2  43290  sticksstones3  43291  sticksstones6  43294  sticksstones7  43295  sticksstones10  43298  sticksstones12a  43300  sticksstones12  43301  aks6d1c6lem4  43316  bcled  43321  bcle2d  43322  aks6d1c7lem1  43323  aks6d1c7lem2  43324  unitscyglem1  43338  unitscyglem2  43339  unitscyglem4  43341  unitscyglem5  43342  aks5lem8  43344  oexpreposd  43472  fimgmcyclem  43690  fimgmcyc  43691  fltltc  43765  fltnltalem  43766  fltnlta  43767  3cubeslem3r  43790  irrapxlem3  43924  irrapxlem4  43925  irrapxlem5  43926  pellexlem2  43930  pellexlem6  43934  pell14qrgt0  43959  pell14qrgapw  43976  pellfundgt1  43983  rmspecsqrtnq  44006  ltrmxnn0  44049  jm3.1lem1  44117  jm3.1lem3  44119  dgraa0p  44244  hashnzfz2  45398  rfcnnnub  46146  nnxrd  46383  fzisoeu  46409  fsumnncl  46677  sumnnodd  46735  limsup10exlem  46875  stoweidlem1  47104  stoweidlem3  47106  stoweidlem11  47114  stoweidlem17  47120  stoweidlem20  47123  stoweidlem25  47128  stoweidlem26  47129  stoweidlem34  47137  stoweidlem38  47141  stoweidlem42  47145  stoweidlem44  47147  stoweidlem51  47154  stoweidlem59  47162  stoweidlem60  47163  wallispi  47173  wallispi2  47176  stirlinglem3  47179  stirlinglem4  47180  stirlinglem8  47184  stirlinglem10  47186  stirlinglem12  47188  stirlinglem15  47191  dirkertrigeqlem2  47202  dirkertrigeqlem3  47203  dirkercncflem2  47207  fourierdlem11  47221  fourierdlem14  47224  fourierdlem15  47225  fourierdlem20  47230  fourierdlem31  47241  fourierdlem64  47273  fourierdlem93  47302  fourierdlem95  47304  fourierdlem103  47312  fourierdlem104  47313  fourierdlem112  47321  sqwvfourb  47332  etransclem3  47340  etransclem19  47356  etransclem23  47360  etransclem24  47361  etransclem25  47362  etransclem32  47369  etransclem35  47372  etransclem41  47378  etransclem48  47385  qndenserrnbllem  47397  hoiqssbllem1  47725  hoiqssbllem2  47726  ovolval5lem1  47755  ovolval5lem2  47756  iccpartlt  48599  iccpartgt  48602  odz2prm2pw  48741  fmtnoprmfac1lem  48742  2pwp1prm  48767  sfprmdvdsmersenne  48781  lighneallem2  48784  proththdlem  48791  perfectALTVlem2  48913  gbowge7  48954  ztprmneprm  49552  pgrple2abl  49570  logbpw2m1  49772  nnpw2pmod  49788  nnolog2flm1  49795  blennngt2o2  49797  itcovalt2lem2lem1  49878