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 syl5eq ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 ‘ 𝐴 ) ↑ 𝑁 ) )