Metamath Proof Explorer


Theorem expneg

Description: Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expneg A N 0 A N = 1 A N

Proof

Step Hyp Ref Expression
1 elnn0 N 0 N N = 0
2 nnne0 N N 0
3 2 adantl A N N 0
4 nncn N N
5 4 adantl A N N
6 5 negeq0d A N N = 0 N = 0
7 6 necon3abid A N N 0 ¬ N = 0
8 3 7 mpbid A N ¬ N = 0
9 8 iffalsed A N if N = 0 1 if 0 < N seq 1 × × A N 1 seq 1 × × A -N = if 0 < N seq 1 × × A N 1 seq 1 × × A -N
10 nnnn0 N N 0
11 10 adantl A N N 0
12 nn0nlt0 N 0 ¬ N < 0
13 11 12 syl A N ¬ N < 0
14 11 nn0red A N N
15 14 lt0neg1d A N N < 0 0 < N
16 13 15 mtbid A N ¬ 0 < N
17 16 iffalsed A N if 0 < N seq 1 × × A N 1 seq 1 × × A -N = 1 seq 1 × × A -N
18 5 negnegd A N -N = N
19 18 fveq2d A N seq 1 × × A -N = seq 1 × × A N
20 19 oveq2d A N 1 seq 1 × × A -N = 1 seq 1 × × A N
21 9 17 20 3eqtrd A N if N = 0 1 if 0 < N seq 1 × × A N 1 seq 1 × × A -N = 1 seq 1 × × A N
22 nnnegz N N
23 expval A N A N = if N = 0 1 if 0 < N seq 1 × × A N 1 seq 1 × × A -N
24 22 23 sylan2 A N A N = if N = 0 1 if 0 < N seq 1 × × A N 1 seq 1 × × A -N
25 expnnval A N A N = seq 1 × × A N
26 25 oveq2d A N 1 A N = 1 seq 1 × × A N
27 21 24 26 3eqtr4d A N A N = 1 A N
28 1div1e1 1 1 = 1
29 28 eqcomi 1 = 1 1
30 negeq N = 0 N = 0
31 neg0 0 = 0
32 30 31 eqtrdi N = 0 N = 0
33 32 oveq2d N = 0 A N = A 0
34 exp0 A A 0 = 1
35 33 34 sylan9eqr A N = 0 A N = 1
36 oveq2 N = 0 A N = A 0
37 36 34 sylan9eqr A N = 0 A N = 1
38 37 oveq2d A N = 0 1 A N = 1 1
39 29 35 38 3eqtr4a A N = 0 A N = 1 A N
40 27 39 jaodan A N N = 0 A N = 1 A N
41 1 40 sylan2b A N 0 A N = 1 A N