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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 ↑𝑐 𝐵 ) ↑𝑐 𝐶 ) = ( ( 𝐴 ↑𝑐 𝐶 ) ↑𝑐 𝐵 ) )