Theorem reexpcl 13702

Description: Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.)

Assertion

Ref	Expression
reexpcl	⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ)

Proof of Theorem reexpcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-resscn 10834	. 2 ⊢ ℝ ⊆ ℂ
2		remulcl 10862	. 2 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
3		1re 10881	. 2 ⊢ 1 ∈ ℝ
4	1, 2, 3	expcllem 13696	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  (class class class)co 7252  ℝcr 10776  ℕ₀cn0 12138  ↑cexp 13685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563  ax-cnex 10833  ax-resscn 10834  ax-1cn 10835  ax-icn 10836  ax-addcl 10837  ax-addrcl 10838  ax-mulcl 10839  ax-mulrcl 10840  ax-mulcom 10841  ax-addass 10842  ax-mulass 10843  ax-distr 10844  ax-i2m1 10845  ax-1ne0 10846  ax-1rid 10847  ax-rnegex 10848  ax-rrecex 10849  ax-cnre 10850  ax-pre-lttri 10851  ax-pre-lttrn 10852  ax-pre-ltadd 10853  ax-pre-mulgt0 10854

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  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 5153  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-pred 6189  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-riota 7209  df-ov 7255  df-oprab 7256  df-mpo 7257  df-om 7685  df-2nd 7802  df-wrecs 8089  df-recs 8150  df-rdg 8188  df-er 8433  df-en 8669  df-dom 8670  df-sdom 8671  df-pnf 10917  df-mnf 10918  df-xr 10919  df-ltxr 10920  df-le 10921  df-sub 11112  df-neg 11113  df-nn 11879  df-n0 12139  df-z 12225  df-uz 12487  df-seq 13625  df-exp 13686

This theorem is referenced by:  expgt1  13724  resqcl  13747  reexpcld  13784  rpexpmord  13789  leexp2r  13795  leexp1a  13796  bernneq  13847  bernneq3  13849  expnbnd  13850  expnlbnd  13851  expmulnbnd  13853  digit2  13854  digit1  13855  expnngt1  13859  faclbnd  13907  faclbnd2  13908  faclbnd3  13909  faclbnd4lem1  13910  faclbnd5  13915  faclbnd6  13916  geomulcvg  15491  reeftcl  15687  ege2le3  15702  eftlub  15721  eflegeo  15733  resin4p  15750  recos4p  15751  ef01bndlem  15796  sin01bnd  15797  cos01bnd  15798  sin01gt0  15802  rpnnen2lem2  15827  rpnnen2lem4  15829  rpnnen2lem11  15836  powm2modprm  16407  prmreclem6  16525  mbfi1fseqlem6  24765  aaliou3lem8  25385  radcnvlem1  25452  abelthlem5  25474  abelthlem7  25477  tangtx  25542  advlogexp  25690  logtayllem  25694  leibpilem2  25971  leibpi  25972  leibpisum  25973  basellem3  26112  chtublem  26239  logexprlim  26253  dchrisum0flblem1  26536  pntlem3  26637  ostth2lem1  26646  ostth2lem3  26663  ostth3  26666  hgt750lem  32506  tgoldbachgnn  32514  subfacval2  33024  nn0prpw  34414  mblfinlem1  35720  mblfinlem2  35721  bfplem1  35886  lcmineqlem20  39963  3lexlogpow5ineq1  39969  tgoldbach  45130  dignn0fr  45808  digexp  45814  dig2bits  45821