This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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