Metamath Proof Explorer

Theorem expneg

Description: Value of a complex number raised to a nonpositive integer power. When A = 0 and N is nonzero, both sides have the "value" ( 1 / 0 ) ; relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expneg ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
3 2 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
4 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
5 4 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
6 5 negeq0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 = 0 ↔ - 𝑁 = 0 ) )
7 6 necon3abid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ≠ 0 ↔ ¬ - 𝑁 = 0 ) )
8 3 7 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ¬ - 𝑁 = 0 )
9 8 iffalsed ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → if ( - 𝑁 = 0 , 1 , if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) ) = if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) )
10 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
11 10 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
12 nn0nlt0 ⊢ ( 𝑁 ∈ ℕ0 → ¬ 𝑁 < 0 )
13 11 12 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ¬ 𝑁 < 0 )
14 11 nn0red ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
15 14 lt0neg1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 < 0 ↔ 0 < - 𝑁 ) )
16 13 15 mtbid ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ¬ 0 < - 𝑁 )
17 16 iffalsed ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) )
18 5 negnegd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → - - 𝑁 = 𝑁 )
19 18 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
20 19 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) ) )
21 9 17 20 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → if ( - 𝑁 = 0 , 1 , if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) ) )
22 nnnegz ⊢ ( 𝑁 ∈ ℕ → - 𝑁 ∈ ℤ )
23 expval ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝑁 ∈ ℤ ) → ( 𝐴 ↑ - 𝑁 ) = if ( - 𝑁 = 0 , 1 , if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) ) )
24 22 23 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ - 𝑁 ) = if ( - 𝑁 = 0 , 1 , if ( 0 < - 𝑁 , ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - 𝑁 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ - - 𝑁 ) ) ) ) )
25 expnnval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
26 25 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 1 / ( 𝐴 ↑ 𝑁 ) ) = ( 1 / ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) ) )
27 21 24 26 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
28 1div1e1 ⊢ ( 1 / 1 ) = 1
29 28 eqcomi ⊢ 1 = ( 1 / 1 )
30 negeq ⊢ ( 𝑁 = 0 → - 𝑁 = - 0 )
31 neg0 ⊢ - 0 = 0
32 30 31 eqtrdi ⊢ ( 𝑁 = 0 → - 𝑁 = 0 )
33 32 oveq2d ⊢ ( 𝑁 = 0 → ( 𝐴 ↑ - 𝑁 ) = ( 𝐴 ↑ 0 ) )
34 exp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
35 33 34 sylan9eqr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ - 𝑁 ) = 1 )
36 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
37 36 34 sylan9eqr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = 1 )
38 37 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 1 / ( 𝐴 ↑ 𝑁 ) ) = ( 1 / 1 ) )
39 29 35 38 3eqtr4a ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
40 27 39 jaodan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )
41 1 40 sylan2b ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝑁 ) = ( 1 / ( 𝐴 ↑ 𝑁 ) ) )