cxpadd

Description: Sum of exponents law for complex exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

		Ref	Expression
	Assertion	cxpadd	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to A^{B + C} = A^{B} A^{C}$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to B \in ℂ$
2		simp3	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to C \in ℂ$
3		logcl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ℂ$
4	3	3ad2ant1	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to \log A \in ℂ$
5	1 2 4	adddird	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to (B + C) \log A = B \log A + C \log A$
6	5	fveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to e^{(B + C) \log A} = e^{B \log A + C \log A}$
7	1 4	mulcld	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to B \log A \in ℂ$
8	2 4	mulcld	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to C \log A \in ℂ$
9		efadd	$⊢ (B \log A \in ℂ \land C \log A \in ℂ) \to e^{B \log A + C \log A} = e^{B \log A} e^{C \log A}$
10	7 8 9	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to e^{B \log A + C \log A} = e^{B \log A} e^{C \log A}$
11	6 10	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to e^{(B + C) \log A} = e^{B \log A} e^{C \log A}$
12		simp1l	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to A \in ℂ$
13		simp1r	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to A \neq 0$
14		addcl	$⊢ (B \in ℂ \land C \in ℂ) \to B + C \in ℂ$
15	14	3adant1	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to B + C \in ℂ$
16		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land B + C \in ℂ) \to A^{B + C} = e^{(B + C) \log A}$
17	12 13 15 16	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to A^{B + C} = e^{(B + C) \log A}$
18		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land B \in ℂ) \to A^{B} = e^{B \log A}$
19	12 13 1 18	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to A^{B} = e^{B \log A}$
20		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land C \in ℂ) \to A^{C} = e^{C \log A}$
21	12 13 2 20	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to A^{C} = e^{C \log A}$
22	19 21	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to A^{B} A^{C} = e^{B \log A} e^{C \log A}$
23	11 17 22	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land B \in ℂ \land C \in ℂ) \to A^{B + C} = A^{B} A^{C}$

Metamath Proof Explorer

Theorem cxpadd

Proof