cxpcom

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

		Ref	Expression
	Assertion	cxpcom	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to {(A^{B})}^{C} = {(A^{C})}^{B}$

Step	Hyp	Ref	Expression
1		recn	$⊢ B \in ℝ \to B \in ℂ$
2		recn	$⊢ C \in ℝ \to C \in ℂ$
3		mulcom	$⊢ (B \in ℂ \land C \in ℂ) \to B C = C B$
4	1 2 3	syl2an	$⊢ (B \in ℝ \land C \in ℝ) \to B C = C B$
5	4	3adant1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to B C = C B$
6	5	oveq2d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to A^{B C} = A^{C B}$
7		cxpmul	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℂ) \to A^{B C} = {(A^{B})}^{C}$
8	2 7	syl3an3	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to A^{B C} = {(A^{B})}^{C}$
9		simp1	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to A \in ℝ^{+}$
10		simp3	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to C \in ℝ$
11	1	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to B \in ℂ$
12	9 10 11	cxpmuld	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to A^{C B} = {(A^{C})}^{B}$
13	6 8 12	3eqtr3d	$⊢ (A \in ℝ^{+} \land B \in ℝ \land C \in ℝ) \to {(A^{B})}^{C} = {(A^{C})}^{B}$

Metamath Proof Explorer