Metamath Proof Explorer

Theorem absexp

Description: Absolute value of positive integer exponentiation. (Contributed by NM, 5-Jan-2006)

Ref Expression
Assertion absexp ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑗 = 0 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 0 ) )
2 1 fveq2d ⊢ ( 𝑗 = 0 → ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( abs ‘ ( 𝐴 ↑ 0 ) ) )
3 oveq2 ⊢ ( 𝑗 = 0 → ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) = ( ( abs ‘ 𝐴 ) ↑ 0 ) )
4 2 3 eqeq12d ⊢ ( 𝑗 = 0 → ( ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( abs ‘ ( 𝐴 ↑ 0 ) ) = ( ( abs ‘ 𝐴 ) ↑ 0 ) ) )
5 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑘 ) )
6 5 fveq2d ⊢ ( 𝑗 = 𝑘 → ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) )
7 oveq2 ⊢ ( 𝑗 = 𝑘 → ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) )
8 6 7 eqeq12d ⊢ ( 𝑗 = 𝑘 → ( ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) )
9 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( 𝑘 + 1 ) ) )
10 9 fveq2d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( abs ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) )
11 oveq2 ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) = ( ( abs ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) )
12 10 11 eqeq12d ⊢ ( 𝑗 = ( 𝑘 + 1 ) → ( ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( abs ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( abs ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) ) )
13 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ 𝑁 ) )
14 13 fveq2d ⊢ ( 𝑗 = 𝑁 → ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( abs ‘ ( 𝐴 ↑ 𝑁 ) ) )
15 oveq2 ⊢ ( 𝑗 = 𝑁 → ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )
16 14 15 eqeq12d ⊢ ( 𝑗 = 𝑁 → ( ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) ↔ ( abs ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) ) )
17 abs1 ⊢ ( abs ‘ 1 ) = 1
18 exp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
19 18 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( 𝐴 ↑ 0 ) ) = ( abs ‘ 1 ) )
20 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
21 20 recnd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℂ )
22 21 exp0d ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 0 ) = 1 )
23 17 19 22 3eqtr4a ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( 𝐴 ↑ 0 ) ) = ( ( abs ‘ 𝐴 ) ↑ 0 ) )
24 oveq1 ⊢ ( ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) → ( ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) · ( abs ‘ 𝐴 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) · ( abs ‘ 𝐴 ) ) )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ∧ ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) → ( ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) · ( abs ‘ 𝐴 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) · ( abs ‘ 𝐴 ) ) )
26 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑘 + 1 ) ) = ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) )
27 26 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( abs ‘ ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) )
28 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
29 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
30 absmul ⊢ ( ( ( 𝐴 ↑ 𝑘 ) ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) = ( ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) · ( abs ‘ 𝐴 ) ) )
31 28 29 30 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝑘 ) · 𝐴 ) ) = ( ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) · ( abs ‘ 𝐴 ) ) )
32 27 31 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) · ( abs ‘ 𝐴 ) ) )
33 32 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ∧ ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) → ( abs ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) · ( abs ‘ 𝐴 ) ) )
34 expp1 ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) · ( abs ‘ 𝐴 ) ) )
35 21 34 sylan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) · ( abs ‘ 𝐴 ) ) )
36 35 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ∧ ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) → ( ( abs ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) · ( abs ‘ 𝐴 ) ) )
37 25 33 36 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) ∧ ( abs ‘ ( 𝐴 ↑ 𝑘 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑘 ) ) → ( abs ‘ ( 𝐴 ↑ ( 𝑘 + 1 ) ) ) = ( ( abs ‘ 𝐴 ) ↑ ( 𝑘 + 1 ) ) )
38 4 8 12 16 23 37 nn0indd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 𝑁 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑁 ) )