Theorem nnred 12377

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11226  ℕcn 12362

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-i2m1 11295  ax-1ne0 11296  ax-rrecex 11299  ax-cnre 11300

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-nn 12363

This theorem is used by:  nnne0  12399  nnadddir  12421  uzwo3  13097  modmulnn  14056  bernneq3  14402  expmulnbnd  14406  expnngt1b  14413  facwordi  14460  faclbnd  14461  faclbnd2  14462  faclbnd3  14463  faclbnd5  14469  faclbnd6  14470  facubnd  14471  facavg  14472  bcp1nk  14488  hashf1  14629  swrds2  15120  isercolllem1  15861  isercoll  15864  o1fsum  16009  climcndslem1  16047  climcndslem2  16048  climcnds  16049  eftabs  16270  efcllem  16272  ege2le3  16285  efcj  16287  eftlub  16306  eflegeo  16318  eirrlem  16401  fzm1ndvds  16521  nno  16581  nnoddm1d2  16585  bitsfzolem  16633  bitsfzo  16634  bitsinv1lem  16640  sadcaddlem  16656  smueqlem  16689  bezoutlem3  16743  bezoutlem4  16744  sqgcd  16765  nn0expgcd  16767  lcmgcdlem  16810  lcmf  16837  prmind2  16889  coprm  16916  prmfac1  16925  prmndvdsfaclt  16930  divdenle  16954  qnumgt0  16955  zsqrtelqelz  16963  hashdvds  16981  eulerthlem2  16988  odzdvds  17002  vfermltl  17008  modprm0  17012  pythagtriplem11  17032  pythagtriplem13  17034  pythagtriplem19  17040  pclem  17045  pcpre1  17049  pcidlem  17079  dvdsprmpweqle  17093  pcadd  17096  pcmpt  17099  pcmpt2  17100  pcfaclem  17105  pcfac  17106  qexpz  17108  pockthlem  17112  pockthg  17113  prmreclem1  17123  prmreclem3  17125  prmreclem4  17126  prmreclem5  17127  1arithlem4  17133  1arith  17134  4sqlem5  17149  4sqlem6  17150  4sqlem10  17154  mul4sqlem  17160  4sqlem11  17162  4sqlem12  17163  4sqlem13  17164  4sqlem14  17165  4sqlem15  17166  4sqlem16  17167  4sqlem17  17168  vdwlem1  17188  vdwlem3  17190  vdwlem6  17193  vdwlem9  17196  vdwlem10  17197  vdwlem12  17199  vdwnnlem3  17204  ramub1lem1  17233  prmolefac  17253  prmgaplem4  17261  prmgaplem5  17262  prmgaplem6  17263  prmgaplem8  17265  2expltfac  17299  cshwshashnsame  17310  setsstruct2  17381  chnub  18825  psgnunilem4  19741  mndodconglem  19785  oddvds  19791  sylow1lem1  19842  sylow1lem5  19846  fislw  19869  efgredlem  19991  gexexlem  20096  zringlpirlem3  21800  prmirredlem  21808  fvmptnn04if  23197  fvmptnn04ifb  23199  fvmptnn04ifc  23200  fvmptnn04ifd  23201  chfacfisf  23202  chfacfisfcpmat  23203  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  lebnumii  25317  lmnn  25614  ovolunlem1a  25847  ovoliunlem1  25853  ovolicc2lem3  25870  ovolicc2lem4  25871  iundisj  25899  voliunlem1  25901  uniioombllem3  25936  dyadf  25942  dyadovol  25944  dyaddisjlem  25946  dyadmaxlem  25948  opnmbllem  25952  vitalilem4  25962  mbfi1fseqlem1  26066  mbfi1fseqlem3  26068  mbfi1fseqlem4  26069  mbfi1fseqlem5  26070  mbfi1fseqlem6  26071  itg2gt0  26111  itg2cnlem2  26113  dgreq0  26614  dgrco  26624  elqaalem2  26673  aaliou3lem2  26700  aaliou3lem8  26702  aaliou3lem9  26707  rtprmirr  27118  leibpi  27300  log2tlbnd  27303  birthdaylem3  27311  amgm  27348  emcllem2  27354  harmonicbnd4  27368  lgamgulmlem1  27386  lgamgulmlem2  27387  lgamgulmlem3  27388  lgamgulmlem4  27389  lgamgulmlem5  27390  lgamgulmlem6  27391  lgamucov  27395  lgamcvg2  27412  wilthlem1  27425  ftalem5  27434  basellem1  27438  basellem2  27439  basellem3  27440  basellem4  27441  basellem5  27442  basellem6  27443  basellem8  27445  chtge0  27469  chtwordi  27513  vma1  27523  dvdsflf1o  27544  dvdsflsumcom  27545  fsumfldivdiaglem  27546  sgmmul  27558  chtublem  27568  fsumvma2  27571  logfac2  27574  chpchtsum  27576  chpub  27577  logfaclbnd  27579  logexprlim  27582  mersenne  27584  perfectlem2  27587  dchrelbas4  27600  bposlem1  27641  bposlem2  27642  bposlem3  27643  bposlem4  27644  bposlem5  27645  bposlem6  27646  bposlem7  27647  bposlem9  27649  lgslem1  27654  lgsval2lem  27664  lgsdirprm  27688  lgsdir  27689  lgsne0  27692  lgsqrlem2  27704  gausslemma2dlem0h  27720  gausslemma2dlem0i  27721  gausslemma2dlem1a  27722  gausslemma2dlem2  27724  gausslemma2dlem7  27730  gausslemma2d  27731  lgseisenlem1  27732  lgseisenlem2  27733  lgseisenlem3  27734  lgseisenlem4  27735  lgseisen  27736  lgsquadlem1  27737  lgsquadlem2  27738  lgsquadlem3  27739  2sqlem3  27777  2sqlem8  27783  2sqblem  27788  2sqmod  27793  chebbnd1lem1  27826  chebbnd1lem3  27828  chtppilimlem1  27830  rplogsumlem1  27841  rplogsumlem2  27842  dchrisum0lem1a  27843  rpvmasumlem  27844  dchrisumlema  27845  dchrisumlem1  27846  dchrisumlem2  27847  dchrisumlem3  27848  dchrvmasumiflem1  27858  dchrisum0flblem2  27866  dchrisum0re  27870  dchrisum0lem1b  27872  dchrisum0lem1  27873  dirith2  27885  selbergb  27906  selberg2lem  27907  logdivbnd  27913  selberg3lem2  27915  selberg4lem1  27917  pntrsumo1  27922  pntrsumbnd2  27924  pntrlog2bndlem1  27934  pntrlog2bndlem2  27935  pntrlog2bndlem3  27936  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  pntpbnd1a  27942  pntpbnd1  27943  pntibndlem2a  27947  pntibndlem2  27948  pntlemg  27955  pntlemh  27956  pntlemj  27960  pntlemf  27962  ostth2lem1  27975  padicabvf  27988  padicabvcxp  27989  ostth2lem2  27991  ostth2lem3  27992  ostth2lem4  27993  ostth2  27994  ostth3  27995  flt4lem5e  28016  flt4lem6  28018  flt4lem7  28019  numclwwlk5  31019  numclwwlk7  31022  nrt2irr  31104  ubthlem2  31503  minvecolem4  31512  iundisjf  33255  ssnnssfz  33449  iundisjfi  33458  nexple  33494  2exple2exp  33495  pfxlsw2ccat  33583  pmtrto1cl  33730  psgnfzto1stlem  33731  fzto1st1  33733  fzto1st  33734  psgnfzto1st  33736  cycpmco2lem6  33762  cycpmco2lem7  33763  fldextrspundgdvdslem  34382  fldextrspundgdvds  34383  fldext2rspun  34384  smatrcl  34498  smattr  34501  smatbl  34502  smatbr  34503  1smat1  34506  submateqlem1  34509  submateqlem2  34510  submateq  34511  esumcst  34765  fiunelros  34877  oddpwdc  35056  eulerpartlems  35062  eulerpartlemgc  35064  fiblem  35100  dstfrvunirn  35177  dstfrvclim1  35180  ballotlemimin  35208  fsum2dsub  35306  reprinfz1  35321  hgt750lemd  35347  hgt750lemb  35355  hgt750leme  35357  tgoldbachgtde  35359  tgoldbachgt  35362  subfaclim  36120  subfacval3  36121  erdszelem7  36129  erdszelem8  36130  erdsze2lem2  36136  cvmliftlem2  36218  cvmliftlem6  36222  cvmliftlem7  36223  cvmliftlem8  36224  cvmliftlem9  36225  cvmliftlem10  36226  cvmliftlem13  36228  bcprod  36681  bccolsum  36682  faclimlem2  36687  faclim2  36691  nn0prpwlem  37288  knoppcnlem10  37546  knoppndvlem15  37570  knoppndvlem17  37572  knoppndvlem18  37573  knoppndvlem19  37574  knoppndvlem20  37575  knoppndvlem21  37576  poimirlem3  38733  poimirlem6  38736  poimirlem7  38737  poimirlem8  38738  poimirlem9  38739  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem13  38743  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem21  38751  poimirlem22  38752  poimirlem23  38753  poimirlem26  38756  poimirlem28  38758  opnmbllem0  38766  mblfinlem2  38768  incsequz  38874  nninfnub  38877  lcmineqlem4  43274  lcmineqlem10  43280  lcmineqlem11  43281  lcmineqlem15  43285  lcmineqlem18  43288  lcmineqlem19  43289  lcmineqlem20  43290  lcmineqlem21  43291  lcmineqlem22  43292  lcmineqlem23  43293  lcmineqlem  43294  3lexlogpow5ineq2  43297  3lexlogpow5ineq4  43298  3lexlogpow2ineq2  43301  3lexlogpow5ineq5  43302  aks4d1p1p3  43311  aks4d1p1p2  43312  aks4d1p1p4  43313  aks4d1p1p5  43317  aks4d1p1  43318  aks4d1p3  43320  aks4d1p4  43321  aks4d1p5  43322  aks4d1p6  43323  aks4d1p7  43325  aks4d1p8d2  43327  aks4d1p8  43329  aks4d1p9  43330  posbezout  43342  primrootlekpowne0  43347  primrootspoweq0  43348  aks6d1c1  43358  hashscontpow1  43363  aks6d1c3  43365  aks6d1c4  43366  aks6d1c2lem4  43369  aks6d1c2  43372  aks6d1c5lem1  43378  2ap1caineq  43387  sticksstones1  43388  sticksstones2  43389  sticksstones3  43390  sticksstones6  43393  sticksstones7  43394  sticksstones10  43397  sticksstones12a  43399  sticksstones12  43400  aks6d1c6lem4  43415  bcled  43420  bcle2d  43421  aks6d1c7lem1  43422  aks6d1c7lem2  43423  unitscyglem1  43437  unitscyglem2  43438  unitscyglem4  43440  unitscyglem5  43441  aks5lem8  43443  oexpreposd  43572  fimgmcyclem  43790  fimgmcyc  43791  fltltc  43865  fltnltalem  43866  fltnlta  43867  3cubeslem3r  43890  irrapxlem3  44024  irrapxlem4  44025  irrapxlem5  44026  pellexlem2  44030  pellexlem6  44034  pell14qrgt0  44059  pell14qrgapw  44076  pellfundgt1  44083  rmspecsqrtnq  44106  ltrmxnn0  44149  jm3.1lem1  44217  jm3.1lem3  44219  dgraa0p  44343  hashnzfz2  45497  rfcnnnub  46258  nnxrd  46495  fzisoeu  46521  fsumnncl  46789  sumnnodd  46847  limsup10exlem  46987  stoweidlem1  47216  stoweidlem3  47218  stoweidlem11  47226  stoweidlem17  47232  stoweidlem20  47235  stoweidlem25  47240  stoweidlem26  47241  stoweidlem34  47249  stoweidlem38  47253  stoweidlem42  47257  stoweidlem44  47259  stoweidlem51  47266  stoweidlem59  47274  stoweidlem60  47275  wallispi  47285  wallispi2  47288  stirlinglem3  47291  stirlinglem4  47292  stirlinglem8  47296  stirlinglem10  47298  stirlinglem12  47300  stirlinglem15  47303  dirkertrigeqlem2  47314  dirkertrigeqlem3  47315  dirkercncflem2  47319  fourierdlem11  47333  fourierdlem14  47336  fourierdlem15  47337  fourierdlem20  47342  fourierdlem31  47353  fourierdlem64  47385  fourierdlem93  47414  fourierdlem95  47416  fourierdlem103  47424  fourierdlem104  47425  fourierdlem112  47433  sqwvfourb  47444  etransclem3  47452  etransclem19  47468  etransclem23  47472  etransclem24  47473  etransclem25  47474  etransclem32  47481  etransclem35  47484  etransclem41  47490  etransclem48  47497  qndenserrnbllem  47509  hoiqssbllem1  47837  hoiqssbllem2  47838  ovolval5lem1  47867  ovolval5lem2  47868  iccpartlt  48711  iccpartgt  48714  odz2prm2pw  48853  fmtnoprmfac1lem  48854  2pwp1prm  48879  sfprmdvdsmersenne  48893  lighneallem2  48896  proththdlem  48903  perfectALTVlem2  49025  gbowge7  49066  ztprmneprm  49664  pgrple2abl  49682  logbpw2m1  49884  nnpw2pmod  49900  nnolog2flm1  49907  blennngt2o2  49909  itcovalt2lem2lem1  49990