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 syl5bi ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( 𝐶 ∈ ℤ → ( 𝐴𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴𝑐 𝐵 ) ↑ 𝐶 ) ) )
34 33 impr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ ) ) → ( 𝐴𝑐 ( 𝐵 · 𝐶 ) ) = ( ( 𝐴𝑐 𝐵 ) ↑ 𝐶 ) )