Theorem expadd

Description: Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by NM, 30-Nov-2004)

	Ref	Expression
Assertion	expadd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑗 = 0 → ( 𝑀 + 𝑗 ) = ( 𝑀 + 0 ) )
2	1	oveq2d	⊢ ( 𝑗 = 0 → ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( 𝐴 ↑ ( 𝑀 + 0 ) ) )
3		oveq2	⊢ ( 𝑗 = 0 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 0 ) )
4	3	oveq2d	⊢ ( 𝑗 = 0 → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 0 ) ) )
5	2 4	eqeq12d	⊢ ( 𝑗 = 0 → ( ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) ↔ ( 𝐴 ↑ ( 𝑀 + 0 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 0 ) ) ) )
6	5	imbi2d	⊢ ( 𝑗 = 0 → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 0 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 0 ) ) ) ) )
7		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑀 + 𝑗 ) = ( 𝑀 + 𝑘 ) )
8	7	oveq2d	⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) )
9		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑘 ) )
10	9	oveq2d	⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) )
11	8 10	eqeq12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) ↔ ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
12	11	imbi2d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) ) ) )
13		oveq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑀 + 𝑗 ) = ( 𝑀 + ( 𝑘 + 1 ) ) )
14	13	oveq2d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) )
15		oveq2	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
16	15	oveq2d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
17	14 16	eqeq12d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) ↔ ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) ) )
18	17	imbi2d	⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) ) ) )
19		oveq2	⊢ ( 𝑗 = 𝑁 → ( 𝑀 + 𝑗 ) = ( 𝑀 + 𝑁 ) )
20	19	oveq2d	⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) )
21		oveq2	⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑁 ) )
22	21	oveq2d	⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) )
23	20 22	eqeq12d	⊢ ( 𝑗 = 𝑁 → ( ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) ↔ ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) ) )
24	23	imbi2d	⊢ ( 𝑗 = 𝑁 → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑗 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑗 ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) )
25		nn0cn	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
26	25	addridd	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 0 ) = 𝑀 )
27	26	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 0 ) = 𝑀 )
28	27	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 0 ) ) = ( 𝐴 ↑ 𝑀 ) )
29		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
30	29	mulridd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) · 1 ) = ( 𝐴 ↑ 𝑀 ) )
31	28 30	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 0 ) ) = ( ( 𝐴 ↑ 𝑀 ) · 1 ) )
32		exp0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
33	32	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ 0 ) = 1 )
34	33	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 0 ) ) = ( ( 𝐴 ↑ 𝑀 ) · 1 ) )
35	31 34	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 0 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 0 ) ) )
36		oveq1	⊢ ( ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) → ( ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) · 𝐴 ) = ( ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝐴 ) )
37		nn0cn	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
38		ax-1cn	⊢ 1 ∈ ℂ
39		addass	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 𝑘 ) + 1 ) = ( 𝑀 + ( 𝑘 + 1 ) ) )
40	38 39	mp3an3	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑀 + 𝑘 ) + 1 ) = ( 𝑀 + ( 𝑘 + 1 ) ) )
41	25 37 40	syl2an	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 + 𝑘 ) + 1 ) = ( 𝑀 + ( 𝑘 + 1 ) ) )
42	41	adantll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑀 + 𝑘 ) + 1 ) = ( 𝑀 + ( 𝑘 + 1 ) ) )
43	42	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) )
44		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
45		nn0addcl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 + 𝑘 ) ∈ ℕ0 )
46	45	adantll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 + 𝑘 ) ∈ ℕ0 )
47		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 + 𝑘 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) · 𝐴 ) )
48	44 46 47	syl2anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑀 + 𝑘 ) + 1 ) ) = ( ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) · 𝐴 ) )
49	43 48	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) · 𝐴 ) )
50		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
51	50	adantlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
52	51	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) )
53	29	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
54		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
55	54	adantlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
56	53 55 44	mulassd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝐴 ) = ( ( 𝐴 ↑ 𝑀 ) · ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) )
57	52 56	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝐴 ) )
58	49 57	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) · 𝐴 ) = ( ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝐴 ) ) )
59	36 58	imbitrrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) → ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) ) )
60	59	expcom	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) → ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) ) ) )
61	60	a2d	⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑘 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑘 ) ) ) → ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) ) ) )
62	6 12 18 24 35 61	nn0ind	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) ) )
63	62	expdcom	⊢ ( 𝐴 ∈ ℂ → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) ) ) )
64	63	3imp	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) )