Metamath Proof Explorer


Theorem oexpnegnz

Description: The exponential of the negative of a number not being 0, when the exponent is odd. (Contributed by AV, 19-Jun-2020)

Ref Expression
Assertion oexpnegnz A A 0 N Odd A N = A N

Proof

Step Hyp Ref Expression
1 oddz N Odd N
2 odd2np1ALTV N N Odd n 2 n + 1 = N
3 1 2 syl N Odd N Odd n 2 n + 1 = N
4 3 biimpd N Odd N Odd n 2 n + 1 = N
5 4 pm2.43i N Odd n 2 n + 1 = N
6 5 3ad2ant3 A A 0 N Odd n 2 n + 1 = N
7 simpl1 A A 0 N Odd n 2 n + 1 = N A
8 simpl2 A A 0 N Odd n 2 n + 1 = N A 0
9 2z 2
10 simprl A A 0 N Odd n 2 n + 1 = N n
11 zmulcl 2 n 2 n
12 9 10 11 sylancr A A 0 N Odd n 2 n + 1 = N 2 n
13 7 8 12 expclzd A A 0 N Odd n 2 n + 1 = N A 2 n
14 13 7 mulneg2d A A 0 N Odd n 2 n + 1 = N A 2 n A = A 2 n A
15 sqneg A A 2 = A 2
16 7 15 syl A A 0 N Odd n 2 n + 1 = N A 2 = A 2
17 16 oveq1d A A 0 N Odd n 2 n + 1 = N A 2 n = A 2 n
18 7 negcld A A 0 N Odd n 2 n + 1 = N A
19 7 8 negne0d A A 0 N Odd n 2 n + 1 = N A 0
20 9 a1i n 2 n + 1 = N 2
21 simpl n 2 n + 1 = N n
22 20 21 jca n 2 n + 1 = N 2 n
23 22 adantl A A 0 N Odd n 2 n + 1 = N 2 n
24 18 19 23 jca31 A A 0 N Odd n 2 n + 1 = N A A 0 2 n
25 expmulz A A 0 2 n A 2 n = A 2 n
26 24 25 syl A A 0 N Odd n 2 n + 1 = N A 2 n = A 2 n
27 7 8 23 jca31 A A 0 N Odd n 2 n + 1 = N A A 0 2 n
28 expmulz A A 0 2 n A 2 n = A 2 n
29 27 28 syl A A 0 N Odd n 2 n + 1 = N A 2 n = A 2 n
30 17 26 29 3eqtr4d A A 0 N Odd n 2 n + 1 = N A 2 n = A 2 n
31 30 oveq1d A A 0 N Odd n 2 n + 1 = N A 2 n A = A 2 n A
32 18 19 12 expp1zd A A 0 N Odd n 2 n + 1 = N A 2 n + 1 = A 2 n A
33 simprr A A 0 N Odd n 2 n + 1 = N 2 n + 1 = N
34 33 oveq2d A A 0 N Odd n 2 n + 1 = N A 2 n + 1 = A N
35 32 34 eqtr3d A A 0 N Odd n 2 n + 1 = N A 2 n A = A N
36 31 35 eqtr3d A A 0 N Odd n 2 n + 1 = N A 2 n A = A N
37 14 36 eqtr3d A A 0 N Odd n 2 n + 1 = N A 2 n A = A N
38 7 8 12 expp1zd A A 0 N Odd n 2 n + 1 = N A 2 n + 1 = A 2 n A
39 33 oveq2d A A 0 N Odd n 2 n + 1 = N A 2 n + 1 = A N
40 38 39 eqtr3d A A 0 N Odd n 2 n + 1 = N A 2 n A = A N
41 40 negeqd A A 0 N Odd n 2 n + 1 = N A 2 n A = A N
42 37 41 eqtr3d A A 0 N Odd n 2 n + 1 = N A N = A N
43 6 42 rexlimddv A A 0 N Odd A N = A N