Metamath Proof Explorer

Theorem cxpcom

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

Ref Expression
Assertion cxpcom ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → A B C = A C B

Proof

Step Hyp Ref Expression
1 recn ⊢ B ∈ ℝ → B ∈ ℂ
2 recn ⊢ C ∈ ℝ → C ∈ ℂ
3 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
4 1 2 3 syl2an ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ⁢ C = C ⁢ B
5 4 3adant1 ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → B ⁢ C = C ⁢ B
6 5 oveq2d ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → A B ⁢ C = A C ⁢ B
7 cxpmul ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℂ → A B ⁢ C = A B C
8 2 7 syl3an3 ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → A B ⁢ C = A B C
9 simp1 ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ +
10 simp3 ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
11 1 3ad2ant2 ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℂ
12 9 10 11 cxpmuld ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → A C ⁢ B = A C B
13 6 8 12 3eqtr3d ⊢ A ∈ ℝ + ∧ B ∈ ℝ ∧ C ∈ ℝ → A B C = A C B