Theorem rpexpcld 14294

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

Hypotheses

Ref	Expression
rpexpcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)
rpexpcld.2	⊢ (𝜑 → 𝑁 ∈ ℤ)

Assertion

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

Proof of Theorem rpexpcld

Step	Hyp	Ref	Expression
1		rpexpcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpexpcld.2	. 2 ⊢ (𝜑 → 𝑁 ∈ ℤ)
3		rpexpcl 14127	. 2 ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ+)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7416  ℤcz 12601  ℝ⁺crp 13026  ↑cexp 14108

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-nul 5272  ax-pow 5339  ax-pr 5407  ax-un 7738  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-tr 5222  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11453  df-neg 11454  df-div 11882  df-nn 12244  df-n0 12515  df-z 12602  df-uz 12873  df-rp 13027  df-seq 14049  df-exp 14109

This theorem is used by:  bitsfzolem  16502  bitsfzo  16503  bitsmod  16504  bitsinv1  16510  sadasslem  16538  sadeq  16540  plyeq0lem  26382  aalioulem4  26513  aalioulem5  26514  aalioulem6  26515  aaliou  26516  aaliou3lem8  26523  nnlogbexp  26961  lgamgulmlem3  27210  ftalem5  27256  basellem3  27262  2sqmod  27615  rplogsumlem2  27664  rpvmasumlem  27666  pntlemh  27778  pntlemq  27780  pntlemr  27781  pntlemj  27782  pntlemf  27784  padicabv  27809  ostth2lem3  27814  dya2ub  34673  dya2iocress  34677  dya2iocbrsiga  34678  dya2icobrsiga  34679  sxbrsigalem2  34689  omssubadd  34703  signsply0  34951  hgt750leme  35058  tgoldbachgtde  35060  faclim  36250  iprodfac  36251  knoppndvlem17  37149  knoppndvlem18  37150  geomcau  38442  lcmineqlem21  42848  3lexlogpow5ineq5  42859  aks4d1p1p7  42873  aks4d1p1  42875  aks4d1p8d2  42884  aks4d1p8  42886  fltltc  43425  fltnlta  43427  pellfund14  43657  dvdivbd  46669  stirlinglem1  46820  stirlinglem2  46821  stirlinglem4  46823  stirlinglem8  46827  stirlinglem10  46829  stirlinglem11  46830  stirlinglem13  46832  stirlinglem15  46834  stirlingr  46836  sge0ad2en  47177  ovnsubaddlem1  47316  fllog2  49380  dignn0flhalflem1  49427  dignn0flhalflem2  49428