Metamath Proof Explorer


Theorem mulexpz

Description: Integer exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion mulexpz ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elznn0nn ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
2 simpl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
3 simpl ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
4 2 3 anim12i ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
5 mulexp ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) )
6 5 3expa ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) )
7 4 6 sylan ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) )
8 simplll ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ∈ ℂ )
9 simplrl ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐵 ∈ ℂ )
10 8 9 mulcld ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
11 recn ( 𝑁 ∈ ℝ → 𝑁 ∈ ℂ )
12 11 ad2antrl ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
13 nnnn0 ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℕ0 )
14 13 ad2antll ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ0 )
15 expneg2 ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) )
16 10 12 14 15 syl3anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) )
17 expneg2 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
18 8 12 14 17 syl3anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
19 expneg2 ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐵𝑁 ) = ( 1 / ( 𝐵 ↑ - 𝑁 ) ) )
20 9 12 14 19 syl3anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐵𝑁 ) = ( 1 / ( 𝐵 ↑ - 𝑁 ) ) )
21 18 20 oveq12d ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) = ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) )
22 mulexp ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) = ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) )
23 8 9 14 22 syl3anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) = ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) )
24 23 oveq2d ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) = ( 1 / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
25 1t1e1 ( 1 · 1 ) = 1
26 25 oveq1i ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) = ( 1 / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) )
27 24 26 eqtr4di ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) = ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
28 expcl ( ( 𝐴 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) ∈ ℂ )
29 8 14 28 syl2anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝑁 ) ∈ ℂ )
30 simpllr ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ≠ 0 )
31 nnz ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℤ )
32 31 ad2antll ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℤ )
33 expne0i ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) ≠ 0 )
34 8 30 32 33 syl3anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝑁 ) ≠ 0 )
35 expcl ( ( 𝐵 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝑁 ) ∈ ℂ )
36 9 14 35 syl2anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐵 ↑ - 𝑁 ) ∈ ℂ )
37 simplrr ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐵 ≠ 0 )
38 expne0i ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ - 𝑁 ∈ ℤ ) → ( 𝐵 ↑ - 𝑁 ) ≠ 0 )
39 9 37 32 38 syl3anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐵 ↑ - 𝑁 ) ≠ 0 )
40 ax-1cn 1 ∈ ℂ
41 divmuldiv ( ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) ∧ ( ( ( 𝐴 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐴 ↑ - 𝑁 ) ≠ 0 ) ∧ ( ( 𝐵 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐵 ↑ - 𝑁 ) ≠ 0 ) ) ) → ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) = ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
42 40 40 41 mpanl12 ( ( ( ( 𝐴 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐴 ↑ - 𝑁 ) ≠ 0 ) ∧ ( ( 𝐵 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐵 ↑ - 𝑁 ) ≠ 0 ) ) → ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) = ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
43 29 34 36 39 42 syl22anc ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) = ( ( 1 · 1 ) / ( ( 𝐴 ↑ - 𝑁 ) · ( 𝐵 ↑ - 𝑁 ) ) ) )
44 27 43 eqtr4d ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) = ( ( 1 / ( 𝐴 ↑ - 𝑁 ) ) · ( 1 / ( 𝐵 ↑ - 𝑁 ) ) ) )
45 21 44 eqtr4d ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) = ( 1 / ( ( 𝐴 · 𝐵 ) ↑ - 𝑁 ) ) )
46 16 45 eqtr4d ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) )
47 7 46 jaodan ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) )
48 1 47 sylan2b ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) )
49 48 3impa ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴𝑁 ) · ( 𝐵𝑁 ) ) )