Metamath Proof Explorer

Theorem mulexp

Description: Positive integer exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 13-Feb-2005)

Ref Expression
Assertion mulexp 
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = 0 -> ( ( A x. B ) ^ j ) = ( ( A x. B ) ^ 0 ) )
2 oveq2 
 |-  ( j = 0 -> ( A ^ j ) = ( A ^ 0 ) )
3 oveq2 
 |-  ( j = 0 -> ( B ^ j ) = ( B ^ 0 ) )
4 2 3 oveq12d 
 |-  ( j = 0 -> ( ( A ^ j ) x. ( B ^ j ) ) = ( ( A ^ 0 ) x. ( B ^ 0 ) ) )
5 1 4 eqeq12d 
 |-  ( j = 0 -> ( ( ( A x. B ) ^ j ) = ( ( A ^ j ) x. ( B ^ j ) ) <-> ( ( A x. B ) ^ 0 ) = ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) )
6 5 imbi2d 
 |-  ( j = 0 -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ j ) = ( ( A ^ j ) x. ( B ^ j ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ 0 ) = ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) ) )
7 oveq2 
 |-  ( j = k -> ( ( A x. B ) ^ j ) = ( ( A x. B ) ^ k ) )
8 oveq2 
 |-  ( j = k -> ( A ^ j ) = ( A ^ k ) )
9 oveq2 
 |-  ( j = k -> ( B ^ j ) = ( B ^ k ) )
10 8 9 oveq12d 
 |-  ( j = k -> ( ( A ^ j ) x. ( B ^ j ) ) = ( ( A ^ k ) x. ( B ^ k ) ) )
11 7 10 eqeq12d 
 |-  ( j = k -> ( ( ( A x. B ) ^ j ) = ( ( A ^ j ) x. ( B ^ j ) ) <-> ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) ) )
12 11 imbi2d 
 |-  ( j = k -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ j ) = ( ( A ^ j ) x. ( B ^ j ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) ) ) )
13 oveq2 
 |-  ( j = ( k + 1 ) -> ( ( A x. B ) ^ j ) = ( ( A x. B ) ^ ( k + 1 ) ) )
14 oveq2 
 |-  ( j = ( k + 1 ) -> ( A ^ j ) = ( A ^ ( k + 1 ) ) )
15 oveq2 
 |-  ( j = ( k + 1 ) -> ( B ^ j ) = ( B ^ ( k + 1 ) ) )
16 14 15 oveq12d 
 |-  ( j = ( k + 1 ) -> ( ( A ^ j ) x. ( B ^ j ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) )
17 13 16 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( ( ( A x. B ) ^ j ) = ( ( A ^ j ) x. ( B ^ j ) ) <-> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) ) )
18 17 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ j ) = ( ( A ^ j ) x. ( B ^ j ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) ) ) )
19 oveq2 
 |-  ( j = N -> ( ( A x. B ) ^ j ) = ( ( A x. B ) ^ N ) )
20 oveq2 
 |-  ( j = N -> ( A ^ j ) = ( A ^ N ) )
21 oveq2 
 |-  ( j = N -> ( B ^ j ) = ( B ^ N ) )
22 20 21 oveq12d 
 |-  ( j = N -> ( ( A ^ j ) x. ( B ^ j ) ) = ( ( A ^ N ) x. ( B ^ N ) ) )
23 19 22 eqeq12d 
 |-  ( j = N -> ( ( ( A x. B ) ^ j ) = ( ( A ^ j ) x. ( B ^ j ) ) <-> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) ) )
24 23 imbi2d 
 |-  ( j = N -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ j ) = ( ( A ^ j ) x. ( B ^ j ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) ) ) )
25 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
26 exp0 
 |-  ( ( A x. B ) e. CC -> ( ( A x. B ) ^ 0 ) = 1 )
27 25 26 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ 0 ) = 1 )
28 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
29 exp0 
 |-  ( B e. CC -> ( B ^ 0 ) = 1 )
30 28 29 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 0 ) x. ( B ^ 0 ) ) = ( 1 x. 1 ) )
31 1t1e1 
 |-  ( 1 x. 1 ) = 1
32 30 31 syl6eq 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 0 ) x. ( B ^ 0 ) ) = 1 )
33 27 32 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ 0 ) = ( ( A ^ 0 ) x. ( B ^ 0 ) ) )
34 expp1 
 |-  ( ( ( A x. B ) e. CC /\ k e. NN0 ) -> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( ( A x. B ) ^ k ) x. ( A x. B ) ) )
35 25 34 sylan 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( ( A x. B ) ^ k ) x. ( A x. B ) ) )
36 35 adantr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) ) -> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( ( A x. B ) ^ k ) x. ( A x. B ) ) )
37 oveq1 
 |-  ( ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) -> ( ( ( A x. B ) ^ k ) x. ( A x. B ) ) = ( ( ( A ^ k ) x. ( B ^ k ) ) x. ( A x. B ) ) )
38 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
39 expcl 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( B ^ k ) e. CC )
40 38 39 anim12i 
 |-  ( ( ( A e. CC /\ k e. NN0 ) /\ ( B e. CC /\ k e. NN0 ) ) -> ( ( A ^ k ) e. CC /\ ( B ^ k ) e. CC ) )
41 40 anandirs 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( ( A ^ k ) e. CC /\ ( B ^ k ) e. CC ) )
42 simpl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( A e. CC /\ B e. CC ) )
43 mul4 
 |-  ( ( ( ( A ^ k ) e. CC /\ ( B ^ k ) e. CC ) /\ ( A e. CC /\ B e. CC ) ) -> ( ( ( A ^ k ) x. ( B ^ k ) ) x. ( A x. B ) ) = ( ( ( A ^ k ) x. A ) x. ( ( B ^ k ) x. B ) ) )
44 41 42 43 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( ( ( A ^ k ) x. ( B ^ k ) ) x. ( A x. B ) ) = ( ( ( A ^ k ) x. A ) x. ( ( B ^ k ) x. B ) ) )
45 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
46 45 adantlr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
47 expp1 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( B ^ ( k + 1 ) ) = ( ( B ^ k ) x. B ) )
48 47 adantll 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( B ^ ( k + 1 ) ) = ( ( B ^ k ) x. B ) )
49 46 48 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) = ( ( ( A ^ k ) x. A ) x. ( ( B ^ k ) x. B ) ) )
50 44 49 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) -> ( ( ( A ^ k ) x. ( B ^ k ) ) x. ( A x. B ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) )
51 37 50 sylan9eqr 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) ) -> ( ( ( A x. B ) ^ k ) x. ( A x. B ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) )
52 36 51 eqtrd 
 |-  ( ( ( ( A e. CC /\ B e. CC ) /\ k e. NN0 ) /\ ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) ) -> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) )
53 52 exp31 
 |-  ( ( A e. CC /\ B e. CC ) -> ( k e. NN0 -> ( ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) -> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) ) ) )
54 53 com12 
 |-  ( k e. NN0 -> ( ( A e. CC /\ B e. CC ) -> ( ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) -> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) ) ) )
55 54 a2d 
 |-  ( k e. NN0 -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ k ) = ( ( A ^ k ) x. ( B ^ k ) ) ) -> ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ ( k + 1 ) ) = ( ( A ^ ( k + 1 ) ) x. ( B ^ ( k + 1 ) ) ) ) ) )
56 6 12 18 24 33 55 nn0ind 
 |-  ( N e. NN0 -> ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) ) )
57 56 expdcom 
 |-  ( A e. CC -> ( B e. CC -> ( N e. NN0 -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) ) ) )
58 57 3imp 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )