mulcxp

Description: Complex exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

		Ref	Expression
	Assertion	mulcxp	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to {A B}^{C} = A^{C} B^{C}$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to A \in ℝ$
2	1	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to A \in ℂ$
3	2	mul01d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to A \cdot 0 = 0$
4	3	oveq1d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to {A \cdot 0}^{C} = 0^{C}$
5		simp3	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to C \in ℂ$
6	2 5	mulcxplem	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to 0^{C} = A^{C} 0^{C}$
7	4 6	eqtrd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to {A \cdot 0}^{C} = A^{C} 0^{C}$
8		oveq2	$⊢ B = 0 \to A B = A \cdot 0$
9	8	oveq1d	$⊢ B = 0 \to {A B}^{C} = {A \cdot 0}^{C}$
10		oveq1	$⊢ B = 0 \to B^{C} = 0^{C}$
11	10	oveq2d	$⊢ B = 0 \to A^{C} B^{C} = A^{C} 0^{C}$
12	9 11	eqeq12d	$⊢ B = 0 \to ({A B}^{C} = A^{C} B^{C} \leftrightarrow {A \cdot 0}^{C} = A^{C} 0^{C})$
13	7 12	syl5ibrcom	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to (B = 0 \to {A B}^{C} = A^{C} B^{C})$
14		simp2l	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to B \in ℝ$
15	14	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to B \in ℂ$
16	15	mul02d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to 0 \cdot B = 0$
17	16	oveq1d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to {0 \cdot B}^{C} = 0^{C}$
18	15 5	mulcxplem	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to 0^{C} = B^{C} 0^{C}$
19		cxpcl	$⊢ (B \in ℂ \land C \in ℂ) \to B^{C} \in ℂ$
20	15 5 19	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to B^{C} \in ℂ$
21		0cn	$⊢ 0 \in ℂ$
22		cxpcl	$⊢ (0 \in ℂ \land C \in ℂ) \to 0^{C} \in ℂ$
23	21 5 22	sylancr	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to 0^{C} \in ℂ$
24	20 23	mulcomd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to B^{C} 0^{C} = 0^{C} B^{C}$
25	18 24	eqtrd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to 0^{C} = 0^{C} B^{C}$
26	17 25	eqtrd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to {0 \cdot B}^{C} = 0^{C} B^{C}$
27		oveq1	$⊢ A = 0 \to A B = 0 \cdot B$
28	27	oveq1d	$⊢ A = 0 \to {A B}^{C} = {0 \cdot B}^{C}$
29		oveq1	$⊢ A = 0 \to A^{C} = 0^{C}$
30	29	oveq1d	$⊢ A = 0 \to A^{C} B^{C} = 0^{C} B^{C}$
31	28 30	eqeq12d	$⊢ A = 0 \to ({A B}^{C} = A^{C} B^{C} \leftrightarrow {0 \cdot B}^{C} = 0^{C} B^{C})$
32	26 31	syl5ibrcom	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to (A = 0 \to {A B}^{C} = A^{C} B^{C})$
33	32	a1dd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to (A = 0 \to (B \neq 0 \to {A B}^{C} = A^{C} B^{C}))$
34	1	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to A \in ℝ$
35		simpl1r	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to 0 \leq A$
36		simprl	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to A \neq 0$
37	34 35 36	ne0gt0d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to 0 < A$
38	34 37	elrpd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to A \in ℝ^{+}$
39	14	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to B \in ℝ$
40		simpl2r	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to 0 \leq B$
41		simprr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to B \neq 0$
42	39 40 41	ne0gt0d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to 0 < B$
43	39 42	elrpd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to B \in ℝ^{+}$
44	38 43	relogmuld	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to \log A B = \log A + \log B$
45	44	oveq2d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to C \log A B = C (\log A + \log B)$
46	5	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to C \in ℂ$
47	2	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to A \in ℂ$
48	47 36	logcld	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to \log A \in ℂ$
49	15	adantr	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to B \in ℂ$
50	49 41	logcld	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to \log B \in ℂ$
51	46 48 50	adddid	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to C (\log A + \log B) = C \log A + C \log B$
52	45 51	eqtrd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to C \log A B = C \log A + C \log B$
53	52	fveq2d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to e^{C \log A B} = e^{C \log A + C \log B}$
54	46 48	mulcld	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to C \log A \in ℂ$
55	46 50	mulcld	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to C \log B \in ℂ$
56		efadd	$⊢ (C \log A \in ℂ \land C \log B \in ℂ) \to e^{C \log A + C \log B} = e^{C \log A} e^{C \log B}$
57	54 55 56	syl2anc	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to e^{C \log A + C \log B} = e^{C \log A} e^{C \log B}$
58	53 57	eqtrd	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to e^{C \log A B} = e^{C \log A} e^{C \log B}$
59	47 49	mulcld	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to A B \in ℂ$
60	47 49 36 41	mulne0d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to A B \neq 0$
61		cxpef	$⊢ (A B \in ℂ \land A B \neq 0 \land C \in ℂ) \to {A B}^{C} = e^{C \log A B}$
62	59 60 46 61	syl3anc	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to {A B}^{C} = e^{C \log A B}$
63		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land C \in ℂ) \to A^{C} = e^{C \log A}$
64	47 36 46 63	syl3anc	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to A^{C} = e^{C \log A}$
65		cxpef	$⊢ (B \in ℂ \land B \neq 0 \land C \in ℂ) \to B^{C} = e^{C \log B}$
66	49 41 46 65	syl3anc	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to B^{C} = e^{C \log B}$
67	64 66	oveq12d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to A^{C} B^{C} = e^{C \log A} e^{C \log B}$
68	58 62 67	3eqtr4d	$⊢ (((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \land (A \neq 0 \land B \neq 0)) \to {A B}^{C} = A^{C} B^{C}$
69	68	exp32	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to (A \neq 0 \to (B \neq 0 \to {A B}^{C} = A^{C} B^{C}))$
70	33 69	pm2.61dne	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to (B \neq 0 \to {A B}^{C} = A^{C} B^{C})$
71	13 70	pm2.61dne	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B) \land C \in ℂ) \to {A B}^{C} = A^{C} B^{C}$

Metamath Proof Explorer

Theorem mulcxp

Proof