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

Metamath Proof Explorer

Theorem cxpmul2z

Description: Generalize cxpmul2 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion cxpmul2z ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elznn0 ⊢ ( 𝐶 ∈ ℤ ↔ ( 𝐶 ∈ ℝ ∧ ( 𝐶 ∈ ℕ0 ∨ - 𝐶 ∈ ℕ0 ) ) )
2 cxpmul2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )
3 2 3expia ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐶 ∈ ℕ0 → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
4 3 ad4ant13 ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ℕ0 → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
5 simplll ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐴 ∈ ℂ )
6 simplr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐵 ∈ ℂ )
7 simprr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - 𝐶 ∈ ℕ0 )
8 cxpmul2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ - 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) )
9 5 6 7 8 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) )
10 9 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 1 / ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) ) = ( 1 / ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) ) )
11 simprl ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐶 ∈ ℝ )
12 11 recnd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐶 ∈ ℂ )
13 6 12 mulneg2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐵 · - 𝐶 ) = - ( 𝐵 · 𝐶 ) )
14 13 negeqd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - ( 𝐵 · - 𝐶 ) = - - ( 𝐵 · 𝐶 ) )
15 6 12 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
16 15 negnegd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - - ( 𝐵 · 𝐶 ) = ( 𝐵 · 𝐶 ) )
17 14 16 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - ( 𝐵 · - 𝐶 ) = ( 𝐵 · 𝐶 ) )
18 17 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 - ( 𝐵 · - 𝐶 ) ) = ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) )
19 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → 𝐴 ≠ 0 )
20 12 negcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → - 𝐶 ∈ ℂ )
21 6 20 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐵 · - 𝐶 ) ∈ ℂ )
22 cxpneg ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( 𝐵 · - 𝐶 ) ∈ ℂ ) → ( 𝐴 ↑𝑐 - ( 𝐵 · - 𝐶 ) ) = ( 1 / ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) ) )
23 5 19 21 22 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 - ( 𝐵 · - 𝐶 ) ) = ( 1 / ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) ) )
24 18 23 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( 1 / ( 𝐴 ↑𝑐 ( 𝐵 · - 𝐶 ) ) ) )
25 cxpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )
26 25 ad4ant13 ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ )
27 expneg2 ⊢ ( ( ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ - 𝐶 ∈ ℕ0 ) → ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) = ( 1 / ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) ) )
28 26 12 7 27 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) = ( 1 / ( ( 𝐴 ↑𝑐 𝐵 ) ↑ - 𝐶 ) ) )
29 10 24 28 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℝ ∧ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )
30 29 expr ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℝ ) → ( - 𝐶 ∈ ℕ0 → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
31 4 30 jaod ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 ∈ ℕ0 ∨ - 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
32 31 expimpd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( ( 𝐶 ∈ ℝ ∧ ( 𝐶 ∈ ℕ0 ∨ - 𝐶 ∈ ℕ0 ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
33 1 32 biimtrid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( 𝐶 ∈ ℤ → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) ) )
34 33 impr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴 ↑𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 ↑𝑐 𝐵 ) ↑ 𝐶 ) )