Theorem reexpcld 14116

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 14031	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7360  ℝcr 11028  ℕ₀cn0 12428  ↑cexp 14014

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-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

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-nel 3038  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-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780  df-seq 13955  df-exp 14015

This theorem is referenced by:  expmordi  14120  exp11nnd  14214  faclbnd  14243  facubnd  14253  explecnv  15821  geomulcvg  15832  cvgrat  15839  efcllem  16033  eftlub  16067  bitsfzolem  16394  bitsfzo  16395  vfermltlALT  16764  pclem  16800  dvdsprmpweqle  16848  taylthlem2  26351  taylthlem2OLD  26352  radcnvlem1  26391  abelthlem7  26416  advlogexp  26632  leibpi  26919  ftalem1  27050  ftalem2  27051  ftalem5  27054  vma1  27143  logexprlim  27202  bposlem6  27266  gausslemma2dlem6  27349  rplogsumlem2  27462  rpvmasumlem  27464  dchrisum0flblem1  27485  pntlem3  27586  ostth2lem1  27595  ostth2lem2  27611  ostth2lem3  27612  ostth3  27615  numclwwlk5  30473  expgt0b  32905  nexple  32932  2exple2exp  32933  oexpled  32935  fldext2chn  33888  eulerpartlemgc  34522  signsply0  34711  knoppcnlem2  36770  knoppcnlem4  36772  knoppcnlem6  36774  knoppcnlem10  36778  knoppndvlem11  36798  knoppndvlem14  36801  knoppndvlem15  36802  knoppndvlem17  36804  knoppndvlem18  36805  knoppndvlem21  36808  geomcau  38094  bfplem1  38157  lcmineqlem21  42502  lcmineqlem22  42503  3lexlogpow5ineq4  42509  3lexlogpow5ineq3  42510  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1lem1  42515  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8d2  42538  aks4d1p8  42540  aks6d1c2lem4  42580  2ap1caineq  42598  aks6d1c7lem1  42633  oexpreposd  42768  dffltz  43081  fltltc  43108  fltnltalem  43109  fltnlta  43110  negexpidd  43128  3cubeslem3r  43133  3cubeslem4  43135  jm2.17a  43406  jm2.17b  43407  jm2.17c  43408  jm3.1lem1  43463  jm3.1lem2  43464  xralrple4  45820  stoweidlem1  46447  stoweidlem3  46449  stoweidlem7  46453  stoweidlem12  46458  stoweidlem19  46465  stoweidlem24  46470  stoweidlem25  46471  stoweidlem40  46486  stoweidlem42  46488  stoweidlem45  46491  wallispilem1  46511  stirlinglem10  46529  stirlinglem11  46530  stirlingr  46536  etransclem23  46703  etransclem48  46728  sge0ad2en  46877  ovnsubaddlem1  47016  hoiqssbllem2  47069  lighneallem2  48081  fllog2  49056  nnolog2flm1  49078  dig2nn1st  49093  dignn0flhalflem2  49104  nn0sumshdiglemA  49107