Metamath Proof Explorer


Theorem cxpcom

Description: Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022)

Ref Expression
Assertion cxpcom ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴𝑐 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴𝑐 𝐶 ) ↑𝑐 𝐵 ) )

Proof

Step Hyp Ref Expression
1 recn ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
2 recn ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
3 mulcom ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
4 1 2 3 syl2an ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
5 4 3adant1 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
6 5 oveq2d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴𝑐 ( 𝐵 · 𝐶 ) ) = ( 𝐴𝑐 ( 𝐶 · 𝐵 ) ) )
7 cxpmul ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝐴𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴𝑐 𝐵 ) ↑𝑐 𝐶 ) )
8 2 7 syl3an3 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴𝑐 𝐵 ) ↑𝑐 𝐶 ) )
9 simp1 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ+ )
10 simp3 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
11 1 3ad2ant2 ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
12 9 10 11 cxpmuld ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴𝑐 ( 𝐶 · 𝐵 ) ) = ( ( 𝐴𝑐 𝐶 ) ↑𝑐 𝐵 ) )
13 6 8 12 3eqtr3d ( ( 𝐴 ∈ ℝ+𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴𝑐 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴𝑐 𝐶 ) ↑𝑐 𝐵 ) )