Metamath Proof Explorer

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 ) → ( 𝐴 ↑ ( 𝑀 + 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) · ( 𝐴 ↑ 𝑁 ) ) )