Theorem reexpcld 14179

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403  ℝcr 11126  ℕ₀cn0 12499  ↑cexp 14077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-n0 12500  df-z 12587  df-uz 12851  df-seq 14018  df-exp 14078

This theorem is referenced by:  expmordi  14183  exp11nnd  14277  faclbnd  14306  facubnd  14316  explecnv  15879  geomulcvg  15890  cvgrat  15897  efcllem  16091  eftlub  16125  bitsfzolem  16451  bitsfzo  16452  vfermltlALT  16820  pclem  16856  dvdsprmpweqle  16904  taylthlem2  26332  taylthlem2OLD  26333  radcnvlem1  26372  abelthlem7  26398  advlogexp  26614  leibpi  26902  ftalem1  27033  ftalem2  27034  ftalem5  27037  vma1  27126  logexprlim  27186  bposlem6  27250  gausslemma2dlem6  27333  rplogsumlem2  27446  rpvmasumlem  27448  dchrisum0flblem1  27469  pntlem3  27570  ostth2lem1  27579  ostth2lem2  27595  ostth2lem3  27596  ostth3  27599  numclwwlk5  30315  expgt0b  32741  nexple  32769  2exple2exp  32770  oexpled  32772  fldext2chn  33708  eulerpartlemgc  34340  signsply0  34529  knoppcnlem2  36458  knoppcnlem4  36460  knoppcnlem6  36462  knoppcnlem10  36466  knoppndvlem11  36486  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem18  36493  knoppndvlem21  36496  geomcau  37729  bfplem1  37792  lcmineqlem21  42008  lcmineqlem22  42009  3lexlogpow5ineq4  42015  3lexlogpow5ineq3  42016  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1lem1  42021  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p6  42032  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p2  42036  aks4d1p3  42037  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8d2  42044  aks4d1p8  42046  aks6d1c2lem4  42086  2ap1caineq  42104  aks6d1c7lem1  42139  oexpreposd  42318  dffltz  42604  fltltc  42631  fltnltalem  42632  fltnlta  42633  negexpidd  42652  3cubeslem3r  42657  3cubeslem4  42659  jm2.17a  42931  jm2.17b  42932  jm2.17c  42933  jm3.1lem1  42988  jm3.1lem2  42989  xralrple4  45348  stoweidlem1  45978  stoweidlem3  45980  stoweidlem7  45984  stoweidlem12  45989  stoweidlem19  45996  stoweidlem24  46001  stoweidlem25  46002  stoweidlem40  46017  stoweidlem42  46019  stoweidlem45  46022  wallispilem1  46042  stirlinglem10  46060  stirlinglem11  46061  stirlingr  46067  etransclem23  46234  etransclem48  46259  sge0ad2en  46408  ovnsubaddlem1  46547  hoiqssbllem2  46600  lighneallem2  47568  fllog2  48496  nnolog2flm1  48518  dig2nn1st  48533  dignn0flhalflem2  48544  nn0sumshdiglemA  48547