This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )