Theorem nnred 12180

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11028  ℕcn 12165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166

This theorem is referenced by:  nnne0  12202  nnadddir  12224  uzwo3  12884  modmulnn  13839  bernneq3  14184  expmulnbnd  14188  expnngt1b  14195  facwordi  14242  faclbnd  14243  faclbnd2  14244  faclbnd3  14245  faclbnd5  14251  faclbnd6  14252  facubnd  14253  facavg  14254  bcp1nk  14270  hashf1  14410  swrds2  14893  isercolllem1  15618  isercoll  15621  o1fsum  15767  climcndslem1  15805  climcndslem2  15806  climcnds  15807  eftabs  16031  efcllem  16033  ege2le3  16046  efcj  16048  eftlub  16067  eflegeo  16079  eirrlem  16162  fzm1ndvds  16282  nno  16342  nnoddm1d2  16346  bitsfzolem  16394  bitsfzo  16395  bitsinv1lem  16401  sadcaddlem  16417  smueqlem  16450  bezoutlem3  16501  bezoutlem4  16502  sqgcd  16522  nn0expgcd  16524  lcmgcdlem  16566  lcmf  16593  prmind2  16645  coprm  16672  prmfac1  16681  prmndvdsfaclt  16686  divdenle  16710  qnumgt0  16711  zsqrtelqelz  16719  hashdvds  16736  eulerthlem2  16743  odzdvds  16757  vfermltl  16763  modprm0  16767  pythagtriplem11  16787  pythagtriplem13  16789  pythagtriplem19  16795  pclem  16800  pcpre1  16804  pcidlem  16834  dvdsprmpweqle  16848  pcadd  16851  pcmpt  16854  pcmpt2  16855  pcfaclem  16860  pcfac  16861  qexpz  16863  pockthlem  16867  pockthg  16868  prmreclem1  16878  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  1arithlem4  16888  1arith  16889  4sqlem5  16904  4sqlem6  16905  4sqlem10  16909  mul4sqlem  16915  4sqlem11  16917  4sqlem12  16918  4sqlem13  16919  4sqlem14  16920  4sqlem15  16921  4sqlem16  16922  4sqlem17  16923  vdwlem1  16943  vdwlem3  16945  vdwlem6  16948  vdwlem9  16951  vdwlem10  16952  vdwlem12  16954  vdwnnlem3  16959  ramub1lem1  16988  prmolefac  17008  prmgaplem4  17016  prmgaplem5  17017  prmgaplem6  17018  prmgaplem8  17020  2expltfac  17054  cshwshashnsame  17065  setsstruct2  17135  chnub  18579  psgnunilem4  19463  mndodconglem  19507  oddvds  19513  sylow1lem1  19564  sylow1lem5  19568  fislw  19591  efgredlem  19713  gexexlem  19818  zringlpirlem3  21454  prmirredlem  21462  fvmptnn04if  22824  fvmptnn04ifb  22826  fvmptnn04ifc  22827  fvmptnn04ifd  22828  chfacfisf  22829  chfacfisfcpmat  22830  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  lebnumii  24943  lmnn  25240  ovolunlem1a  25473  ovoliunlem1  25479  ovolicc2lem3  25496  ovolicc2lem4  25497  iundisj  25525  voliunlem1  25527  uniioombllem3  25562  dyadf  25568  dyadovol  25570  dyaddisjlem  25572  dyadmaxlem  25574  opnmbllem  25578  vitalilem4  25588  mbfi1fseqlem1  25692  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  itg2gt0  25737  itg2cnlem2  25739  dgreq0  26240  dgrco  26250  elqaalem2  26297  aaliou3lem2  26320  aaliou3lem8  26322  aaliou3lem9  26327  rtprmirr  26737  leibpi  26919  log2tlbnd  26922  birthdaylem3  26930  amgm  26968  emcllem2  26974  harmonicbnd4  26988  lgamgulmlem1  27006  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem4  27009  lgamgulmlem5  27010  lgamgulmlem6  27011  lgamucov  27015  lgamcvg2  27032  wilthlem1  27045  ftalem5  27054  basellem1  27058  basellem2  27059  basellem3  27060  basellem4  27061  basellem5  27062  basellem6  27063  basellem8  27065  chtge0  27089  chtwordi  27133  vma1  27143  dvdsflf1o  27164  dvdsflsumcom  27165  fsumfldivdiaglem  27166  sgmmul  27178  chtublem  27188  fsumvma2  27191  logfac2  27194  chpchtsum  27196  chpub  27197  logfaclbnd  27199  logexprlim  27202  mersenne  27204  perfectlem2  27207  dchrelbas4  27220  bposlem1  27261  bposlem2  27262  bposlem3  27263  bposlem4  27264  bposlem5  27265  bposlem6  27266  bposlem7  27267  bposlem9  27269  lgslem1  27274  lgsval2lem  27284  lgsdirprm  27308  lgsdir  27309  lgsne0  27312  lgsqrlem2  27324  gausslemma2dlem0h  27340  gausslemma2dlem0i  27341  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  gausslemma2dlem7  27350  gausslemma2d  27351  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgseisen  27356  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  2sqlem3  27397  2sqlem8  27403  2sqblem  27408  2sqmod  27413  chebbnd1lem1  27446  chebbnd1lem3  27448  chtppilimlem1  27450  rplogsumlem1  27461  rplogsumlem2  27462  dchrisum0lem1a  27463  rpvmasumlem  27464  dchrisumlema  27465  dchrisumlem1  27466  dchrisumlem2  27467  dchrisumlem3  27468  dchrvmasumiflem1  27478  dchrisum0flblem2  27486  dchrisum0re  27490  dchrisum0lem1b  27492  dchrisum0lem1  27493  dirith2  27505  selbergb  27526  selberg2lem  27527  logdivbnd  27533  selberg3lem2  27535  selberg4lem1  27537  pntrsumo1  27542  pntrsumbnd2  27544  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntpbnd1a  27562  pntpbnd1  27563  pntibndlem2a  27567  pntibndlem2  27568  pntlemg  27575  pntlemh  27576  pntlemj  27580  pntlemf  27582  ostth2lem1  27595  padicabvf  27608  padicabvcxp  27609  ostth2lem2  27611  ostth2lem3  27612  ostth2lem4  27613  ostth2  27614  ostth3  27615  numclwwlk5  30473  numclwwlk7  30476  nrt2irr  30558  ubthlem2  30957  minvecolem4  30966  iundisjf  32674  ssnnssfz  32875  iundisjfi  32884  nexple  32932  2exple2exp  32933  pfxlsw2ccat  33025  pmtrto1cl  33175  psgnfzto1stlem  33176  fzto1st1  33178  fzto1st  33179  psgnfzto1st  33181  cycpmco2lem6  33207  cycpmco2lem7  33208  fldextrspundgdvdslem  33840  fldextrspundgdvds  33841  fldext2rspun  33842  smatrcl  33956  smattr  33959  smatbl  33960  smatbr  33961  1smat1  33964  submateqlem1  33967  submateqlem2  33968  submateq  33969  esumcst  34223  fiunelros  34334  oddpwdc  34514  eulerpartlems  34520  eulerpartlemgc  34522  fiblem  34558  dstfrvunirn  34635  dstfrvclim1  34638  ballotlemimin  34666  fsum2dsub  34767  reprinfz1  34782  hgt750lemd  34808  hgt750lemb  34816  hgt750leme  34818  tgoldbachgtde  34820  tgoldbachgt  34823  subfaclim  35386  subfacval3  35387  erdszelem7  35395  erdszelem8  35396  erdsze2lem2  35402  cvmliftlem2  35484  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem8  35490  cvmliftlem9  35491  cvmliftlem10  35492  cvmliftlem13  35494  bcprod  35936  bccolsum  35937  faclimlem2  35942  faclim2  35946  nn0prpwlem  36520  knoppcnlem10  36778  knoppndvlem15  36802  knoppndvlem17  36804  knoppndvlem18  36805  knoppndvlem19  36806  knoppndvlem20  36807  knoppndvlem21  36808  poimirlem3  37958  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem9  37964  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem13  37968  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem26  37981  poimirlem28  37983  opnmbllem0  37991  mblfinlem2  37993  incsequz  38083  nninfnub  38086  lcmineqlem4  42485  lcmineqlem10  42491  lcmineqlem11  42492  lcmineqlem15  42496  lcmineqlem18  42499  lcmineqlem19  42500  lcmineqlem20  42501  lcmineqlem21  42502  lcmineqlem22  42503  lcmineqlem23  42504  lcmineqlem  42505  3lexlogpow5ineq2  42508  3lexlogpow5ineq4  42509  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p3  42531  aks4d1p4  42532  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7  42536  aks4d1p8d2  42538  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  primrootlekpowne0  42558  primrootspoweq0  42559  aks6d1c1  42569  hashscontpow1  42574  aks6d1c3  42576  aks6d1c4  42577  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c5lem1  42589  2ap1caineq  42598  sticksstones1  42599  sticksstones2  42600  sticksstones3  42601  sticksstones6  42604  sticksstones7  42605  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  aks6d1c6lem4  42626  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  aks6d1c7lem2  42634  unitscyglem1  42648  unitscyglem2  42649  unitscyglem4  42651  unitscyglem5  42652  aks5lem8  42654  oexpreposd  42768  fimgmcyclem  42992  fimgmcyc  42993  flt4lem5e  43103  flt4lem6  43105  flt4lem7  43106  fltltc  43108  fltnltalem  43109  fltnlta  43110  3cubeslem3r  43133  irrapxlem3  43270  irrapxlem4  43271  irrapxlem5  43272  pellexlem2  43276  pellexlem6  43280  pell14qrgt0  43305  pell14qrgapw  43322  pellfundgt1  43329  rmspecsqrtnq  43352  ltrmxnn0  43395  jm3.1lem1  43463  jm3.1lem3  43465  dgraa0p  43595  hashnzfz2  44766  rfcnnnub  45485  nnxrd  45725  fzisoeu  45751  fsumnncl  46020  sumnnodd  46078  limsup10exlem  46218  stoweidlem1  46447  stoweidlem3  46449  stoweidlem11  46457  stoweidlem17  46463  stoweidlem20  46466  stoweidlem25  46471  stoweidlem26  46472  stoweidlem34  46480  stoweidlem38  46484  stoweidlem42  46488  stoweidlem44  46490  stoweidlem51  46497  stoweidlem59  46505  stoweidlem60  46506  wallispi  46516  wallispi2  46519  stirlinglem3  46522  stirlinglem4  46523  stirlinglem8  46527  stirlinglem10  46529  stirlinglem12  46531  stirlinglem15  46534  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  dirkercncflem2  46550  fourierdlem11  46564  fourierdlem14  46567  fourierdlem15  46568  fourierdlem20  46573  fourierdlem31  46584  fourierdlem64  46616  fourierdlem93  46645  fourierdlem95  46647  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  sqwvfourb  46675  etransclem3  46683  etransclem19  46699  etransclem23  46703  etransclem24  46704  etransclem25  46705  etransclem32  46712  etransclem35  46715  etransclem41  46721  etransclem48  46728  qndenserrnbllem  46740  hoiqssbllem1  47068  hoiqssbllem2  47069  ovolval5lem1  47098  ovolval5lem2  47099  iccpartlt  47896  iccpartgt  47899  odz2prm2pw  48038  fmtnoprmfac1lem  48039  2pwp1prm  48064  sfprmdvdsmersenne  48078  lighneallem2  48081  proththdlem  48088  perfectALTVlem2  48210  gbowge7  48251  ztprmneprm  48835  pgrple2abl  48853  logbpw2m1  49055  nnpw2pmod  49071  nnolog2flm1  49078  blennngt2o2  49080  itcovalt2lem2lem1  49161