Metamath Proof Explorer


Theorem absexpz

Description: Absolute value of integer exponentiation. (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Assertion absexpz ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elznn0nn ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
2 absexp ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )
3 2 ex ( 𝐴 ∈ ℂ → ( 𝑁 ∈ ℕ0 → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) ) )
4 3 adantr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑁 ∈ ℕ0 → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) ) )
5 1cnd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 1 ∈ ℂ )
6 simpll ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ∈ ℂ )
7 nnnn0 ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℕ0 )
8 7 ad2antll ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ0 )
9 6 8 expcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝑁 ) ∈ ℂ )
10 simplr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐴 ≠ 0 )
11 nnz ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℤ )
12 11 ad2antll ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℤ )
13 6 10 12 expne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝑁 ) ≠ 0 )
14 absdiv ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝐴 ↑ - 𝑁 ) ≠ 0 ) → ( abs ‘ ( 1 / ( 𝐴 ↑ - 𝑁 ) ) ) = ( ( abs ‘ 1 ) / ( abs ‘ ( 𝐴 ↑ - 𝑁 ) ) ) )
15 5 9 13 14 syl3anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( abs ‘ ( 1 / ( 𝐴 ↑ - 𝑁 ) ) ) = ( ( abs ‘ 1 ) / ( abs ‘ ( 𝐴 ↑ - 𝑁 ) ) ) )
16 abs1 ( abs ‘ 1 ) = 1
17 16 oveq1i ( ( abs ‘ 1 ) / ( abs ‘ ( 𝐴 ↑ - 𝑁 ) ) ) = ( 1 / ( abs ‘ ( 𝐴 ↑ - 𝑁 ) ) )
18 absexp ( ( 𝐴 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ - 𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ - 𝑁 ) )
19 6 8 18 syl2anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( abs ‘ ( 𝐴 ↑ - 𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ - 𝑁 ) )
20 19 oveq2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 1 / ( abs ‘ ( 𝐴 ↑ - 𝑁 ) ) ) = ( 1 / ( ( abs ‘ 𝐴 ) ↑ - 𝑁 ) ) )
21 17 20 eqtrid ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( abs ‘ 1 ) / ( abs ‘ ( 𝐴 ↑ - 𝑁 ) ) ) = ( 1 / ( ( abs ‘ 𝐴 ) ↑ - 𝑁 ) ) )
22 15 21 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( abs ‘ ( 1 / ( 𝐴 ↑ - 𝑁 ) ) ) = ( 1 / ( ( abs ‘ 𝐴 ) ↑ - 𝑁 ) ) )
23 simprl ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℝ )
24 23 recnd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
25 expneg2 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
26 6 24 8 25 syl3anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐴𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
27 26 fveq2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( abs ‘ ( 1 / ( 𝐴 ↑ - 𝑁 ) ) ) )
28 abscl ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
29 28 ad2antrr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
30 29 recnd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
31 expneg2 ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) = ( 1 / ( ( abs ‘ 𝐴 ) ↑ - 𝑁 ) ) )
32 30 24 8 31 syl3anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) = ( 1 / ( ( abs ‘ 𝐴 ) ↑ - 𝑁 ) ) )
33 22 27 32 3eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )
34 33 ex ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) ) )
35 4 34 jaod ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) ) )
36 35 3impia ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )
37 1 36 syl3an3b ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐴𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )