cxpmul2

Description: Product of exponents law for complex exponentiation. Variation on cxpmul with more general conditions on A and B when C is an integer. (Contributed by Mario Carneiro, 9-Aug-2014)

		Ref	Expression
	Assertion	cxpmul2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℕ_{0}) \to A^{B C} = {(A^{B})}^{C}$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 0 \to B x = B \cdot 0$
2	1	oveq2d	$⊢ x = 0 \to A^{B x} = A^{B \cdot 0}$
3		oveq2	$⊢ x = 0 \to {(A^{B})}^{x} = {(A^{B})}^{0}$
4	2 3	eqeq12d	$⊢ x = 0 \to (A^{B x} = {(A^{B})}^{x} \leftrightarrow A^{B \cdot 0} = {(A^{B})}^{0})$
5	4	imbi2d	$⊢ x = 0 \to (((A \in ℂ \land B \in ℂ) \to A^{B x} = {(A^{B})}^{x}) \leftrightarrow ((A \in ℂ \land B \in ℂ) \to A^{B \cdot 0} = {(A^{B})}^{0}))$
6		oveq2	$⊢ x = k \to B x = B k$
7	6	oveq2d	$⊢ x = k \to A^{B x} = A^{B k}$
8		oveq2	$⊢ x = k \to {(A^{B})}^{x} = {(A^{B})}^{k}$
9	7 8	eqeq12d	$⊢ x = k \to (A^{B x} = {(A^{B})}^{x} \leftrightarrow A^{B k} = {(A^{B})}^{k})$
10	9	imbi2d	$⊢ x = k \to (((A \in ℂ \land B \in ℂ) \to A^{B x} = {(A^{B})}^{x}) \leftrightarrow ((A \in ℂ \land B \in ℂ) \to A^{B k} = {(A^{B})}^{k}))$
11		oveq2	$⊢ x = k + 1 \to B x = B (k + 1)$
12	11	oveq2d	$⊢ x = k + 1 \to A^{B x} = A^{B (k + 1)}$
13		oveq2	$⊢ x = k + 1 \to {(A^{B})}^{x} = {(A^{B})}^{k + 1}$
14	12 13	eqeq12d	$⊢ x = k + 1 \to (A^{B x} = {(A^{B})}^{x} \leftrightarrow A^{B (k + 1)} = {(A^{B})}^{k + 1})$
15	14	imbi2d	$⊢ x = k + 1 \to (((A \in ℂ \land B \in ℂ) \to A^{B x} = {(A^{B})}^{x}) \leftrightarrow ((A \in ℂ \land B \in ℂ) \to A^{B (k + 1)} = {(A^{B})}^{k + 1}))$
16		oveq2	$⊢ x = C \to B x = B C$
17	16	oveq2d	$⊢ x = C \to A^{B x} = A^{B C}$
18		oveq2	$⊢ x = C \to {(A^{B})}^{x} = {(A^{B})}^{C}$
19	17 18	eqeq12d	$⊢ x = C \to (A^{B x} = {(A^{B})}^{x} \leftrightarrow A^{B C} = {(A^{B})}^{C})$
20	19	imbi2d	$⊢ x = C \to (((A \in ℂ \land B \in ℂ) \to A^{B x} = {(A^{B})}^{x}) \leftrightarrow ((A \in ℂ \land B \in ℂ) \to A^{B C} = {(A^{B})}^{C}))$
21		cxp0	$⊢ A \in ℂ \to A^{0} = 1$
22	21	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to A^{0} = 1$
23		mul01	$⊢ B \in ℂ \to B \cdot 0 = 0$
24	23	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to B \cdot 0 = 0$
25	24	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{B \cdot 0} = A^{0}$
26		cxpcl	$⊢ (A \in ℂ \land B \in ℂ) \to A^{B} \in ℂ$
27	26	exp0d	$⊢ (A \in ℂ \land B \in ℂ) \to {(A^{B})}^{0} = 1$
28	22 25 27	3eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to A^{B \cdot 0} = {(A^{B})}^{0}$
29		oveq1	$⊢ A^{B k} = {(A^{B})}^{k} \to A^{B k} A^{B} = {(A^{B})}^{k} A^{B}$
30		0cn	$⊢ 0 \in ℂ$
31		cxp0	$⊢ 0 \in ℂ \to 0^{0} = 1$
32	30 31	ax-mp	$⊢ 0^{0} = 1$
33		1t1e1	$⊢ 1 \cdot 1 = 1$
34	32 33	eqtr4i	$⊢ 0^{0} = 1 \cdot 1$
35		simplr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to A = 0$
36		simpr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to B = 0$
37	36	oveq1d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to B (k + 1) = 0 \cdot (k + 1)$
38		nn0p1nn	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ$
39	38	adantl	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to k + 1 \in ℕ$
40	39	nncnd	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to k + 1 \in ℂ$
41	40	ad2antrr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to k + 1 \in ℂ$
42	41	mul02d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to 0 \cdot (k + 1) = 0$
43	37 42	eqtrd	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to B (k + 1) = 0$
44	35 43	oveq12d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to A^{B (k + 1)} = 0^{0}$
45	36	oveq1d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to B k = 0 \cdot k$
46		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
47	46	adantl	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to k \in ℂ$
48	47	ad2antrr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to k \in ℂ$
49	48	mul02d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to 0 \cdot k = 0$
50	45 49	eqtrd	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to B k = 0$
51	35 50	oveq12d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to A^{B k} = 0^{0}$
52	51 32	eqtrdi	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to A^{B k} = 1$
53	35 36	oveq12d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to A^{B} = 0^{0}$
54	53 32	eqtrdi	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to A^{B} = 1$
55	52 54	oveq12d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to A^{B k} A^{B} = 1 \cdot 1$
56	34 44 55	3eqtr4a	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B = 0) \to A^{B (k + 1)} = A^{B k} A^{B}$
57		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to A \in ℂ$
58	57	ad2antrr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A \in ℂ$
59		simplr	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to B \in ℂ$
60	59 47	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to B k \in ℂ$
61	60	ad2antrr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to B k \in ℂ$
62		cxpcl	$⊢ (A \in ℂ \land B k \in ℂ) \to A^{B k} \in ℂ$
63	58 61 62	syl2anc	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A^{B k} \in ℂ$
64	63	mul01d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A^{B k} \cdot 0 = 0$
65		simplr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A = 0$
66	65	oveq1d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A^{B} = 0^{B}$
67	59	ad2antrr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to B \in ℂ$
68		simpr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to B \neq 0$
69		0cxp	$⊢ (B \in ℂ \land B \neq 0) \to 0^{B} = 0$
70	67 68 69	syl2anc	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to 0^{B} = 0$
71	66 70	eqtrd	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A^{B} = 0$
72	71	oveq2d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A^{B k} A^{B} = A^{B k} \cdot 0$
73	65	oveq1d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A^{B (k + 1)} = 0^{B (k + 1)}$
74	40	ad2antrr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to k + 1 \in ℂ$
75	67 74	mulcld	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to B (k + 1) \in ℂ$
76	39	nnne0d	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to k + 1 \neq 0$
77	76	ad2antrr	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to k + 1 \neq 0$
78	67 74 68 77	mulne0d	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to B (k + 1) \neq 0$
79		0cxp	$⊢ (B (k + 1) \in ℂ \land B (k + 1) \neq 0) \to 0^{B (k + 1)} = 0$
80	75 78 79	syl2anc	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to 0^{B (k + 1)} = 0$
81	73 80	eqtrd	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A^{B (k + 1)} = 0$
82	64 72 81	3eqtr4rd	$⊢ ((((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \land B \neq 0) \to A^{B (k + 1)} = A^{B k} A^{B}$
83	56 82	pm2.61dane	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A = 0) \to A^{B (k + 1)} = A^{B k} A^{B}$
84	59	adantr	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to B \in ℂ$
85	47	adantr	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to k \in ℂ$
86		1cnd	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to 1 \in ℂ$
87	84 85 86	adddid	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to B (k + 1) = B k + B \cdot 1$
88	84	mulid1d	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to B \cdot 1 = B$
89	88	oveq2d	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to B k + B \cdot 1 = B k + B$
90	87 89	eqtrd	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to B (k + 1) = B k + B$
91	90	oveq2d	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to A^{B (k + 1)} = A^{B k + B}$
92	57	adantr	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to A \in ℂ$
93		simpr	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to A \neq 0$
94	60	adantr	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to B k \in ℂ$
95		cxpadd	$⊢ ((A \in ℂ \land A \neq 0) \land B k \in ℂ \land B \in ℂ) \to A^{B k + B} = A^{B k} A^{B}$
96	92 93 94 84 95	syl211anc	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to A^{B k + B} = A^{B k} A^{B}$
97	91 96	eqtrd	$⊢ (((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \land A \neq 0) \to A^{B (k + 1)} = A^{B k} A^{B}$
98	83 97	pm2.61dane	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to A^{B (k + 1)} = A^{B k} A^{B}$
99		expp1	$⊢ (A^{B} \in ℂ \land k \in ℕ_{0}) \to {(A^{B})}^{k + 1} = {(A^{B})}^{k} A^{B}$
100	26 99	sylan	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to {(A^{B})}^{k + 1} = {(A^{B})}^{k} A^{B}$
101	98 100	eqeq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to (A^{B (k + 1)} = {(A^{B})}^{k + 1} \leftrightarrow A^{B k} A^{B} = {(A^{B})}^{k} A^{B})$
102	29 101	syl5ibr	$⊢ ((A \in ℂ \land B \in ℂ) \land k \in ℕ_{0}) \to (A^{B k} = {(A^{B})}^{k} \to A^{B (k + 1)} = {(A^{B})}^{k + 1})$
103	102	expcom	$⊢ k \in ℕ_{0} \to ((A \in ℂ \land B \in ℂ) \to (A^{B k} = {(A^{B})}^{k} \to A^{B (k + 1)} = {(A^{B})}^{k + 1}))$
104	103	a2d	$⊢ k \in ℕ_{0} \to (((A \in ℂ \land B \in ℂ) \to A^{B k} = {(A^{B})}^{k}) \to ((A \in ℂ \land B \in ℂ) \to A^{B (k + 1)} = {(A^{B})}^{k + 1}))$
105	5 10 15 20 28 104	nn0ind	$⊢ C \in ℕ_{0} \to ((A \in ℂ \land B \in ℂ) \to A^{B C} = {(A^{B})}^{C})$
106	105	com12	$⊢ (A \in ℂ \land B \in ℂ) \to (C \in ℕ_{0} \to A^{B C} = {(A^{B})}^{C})$
107	106	3impia	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℕ_{0}) \to A^{B C} = {(A^{B})}^{C}$

Metamath Proof Explorer

Theorem cxpmul2

Proof