Theorem reexpcld 13809

Description: Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
reexpcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
reexpcld.2	⊢ (𝜑 → 𝑁 ∈ ℕ0)

Assertion

Ref	Expression
reexpcld	⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ)

Proof of Theorem reexpcld

Step	Hyp	Ref	Expression
1		reexpcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		reexpcld.2	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
3		reexpcl 13727	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ)
4	1, 2, 3	syl2anc 583	1 ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7255  ℝcr 10801  ℕ₀cn0 12163  ↑cexp 13710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250  df-uz 12512  df-seq 13650  df-exp 13711

This theorem is referenced by:  expmordi  13813  faclbnd  13932  facubnd  13942  explecnv  15505  geomulcvg  15516  cvgrat  15523  efcllem  15715  eftlub  15746  bitsfzolem  16069  bitsfzo  16070  vfermltlALT  16431  pclem  16467  dvdsprmpweqle  16515  taylthlem2  25438  radcnvlem1  25477  abelthlem7  25502  advlogexp  25715  leibpi  25997  ftalem1  26127  ftalem2  26128  ftalem5  26131  vma1  26220  logexprlim  26278  bposlem6  26342  gausslemma2dlem6  26425  rplogsumlem2  26538  rpvmasumlem  26540  dchrisum0flblem1  26561  pntlem3  26662  ostth2lem1  26671  ostth2lem2  26687  ostth2lem3  26688  ostth3  26691  numclwwlk5  28653  nexple  31877  eulerpartlemgc  32229  signsply0  32430  knoppcnlem2  34601  knoppcnlem4  34603  knoppcnlem6  34605  knoppcnlem10  34609  knoppndvlem11  34629  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem18  34636  knoppndvlem21  34639  geomcau  35844  bfplem1  35907  lcmineqlem21  39985  lcmineqlem22  39986  3lexlogpow5ineq4  39992  3lexlogpow5ineq3  39993  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1lem1  39998  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8  40023  2ap1caineq  40029  oexpreposd  40242  exp11nnd  40245  dffltz  40387  fltltc  40414  fltnltalem  40415  fltnlta  40416  negexpidd  40420  3cubeslem3r  40425  3cubeslem4  40427  jm2.17a  40698  jm2.17b  40699  jm2.17c  40700  jm3.1lem1  40755  jm3.1lem2  40756  xralrple4  42802  stoweidlem1  43432  stoweidlem3  43434  stoweidlem7  43438  stoweidlem12  43443  stoweidlem19  43450  stoweidlem24  43455  stoweidlem25  43456  stoweidlem40  43471  stoweidlem42  43473  stoweidlem45  43476  wallispilem1  43496  stirlinglem10  43514  stirlinglem11  43515  stirlingr  43521  etransclem23  43688  etransclem48  43713  sge0ad2en  43859  ovnsubaddlem1  43998  hoiqssbllem2  44051  lighneallem2  44946  fllog2  45802  nnolog2flm1  45824  dig2nn1st  45839  dignn0flhalflem2  45850  nn0sumshdiglemA  45853