Metamath Proof Explorer


Theorem oexpnegALTV

Description: The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015) (Revised by AV, 19-Jun-2020) (Proof shortened by AV, 10-Jul-2022)

Ref Expression
Assertion oexpnegALTV A N 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 ibi N Odd n 2 n + 1 = N
5 4 3ad2ant3 A N N Odd n 2 n + 1 = N
6 simpl1 A N N Odd n 2 n + 1 = N A
7 simprr A N N Odd n 2 n + 1 = N 2 n + 1 = N
8 simpl2 A N N Odd n 2 n + 1 = N N
9 8 nncnd A N N Odd n 2 n + 1 = N N
10 1cnd A N N Odd n 2 n + 1 = N 1
11 2z 2
12 simprl A N N Odd n 2 n + 1 = N n
13 zmulcl 2 n 2 n
14 11 12 13 sylancr A N N Odd n 2 n + 1 = N 2 n
15 14 zcnd A N N Odd n 2 n + 1 = N 2 n
16 9 10 15 subadd2d A N N Odd n 2 n + 1 = N N 1 = 2 n 2 n + 1 = N
17 7 16 mpbird A N N Odd n 2 n + 1 = N N 1 = 2 n
18 nnm1nn0 N N 1 0
19 8 18 syl A N N Odd n 2 n + 1 = N N 1 0
20 17 19 eqeltrrd A N N Odd n 2 n + 1 = N 2 n 0
21 6 20 expcld A N N Odd n 2 n + 1 = N A 2 n
22 21 6 mulneg2d A N N Odd n 2 n + 1 = N A 2 n A = A 2 n A
23 sqneg A A 2 = A 2
24 6 23 syl A N N Odd n 2 n + 1 = N A 2 = A 2
25 24 oveq1d A N N Odd n 2 n + 1 = N A 2 n = A 2 n
26 6 negcld A N N Odd n 2 n + 1 = N A
27 2rp 2 +
28 27 a1i A N N Odd n 2 n + 1 = N 2 +
29 12 zred A N N Odd n 2 n + 1 = N n
30 20 nn0ge0d A N N Odd n 2 n + 1 = N 0 2 n
31 28 29 30 prodge0rd A N N Odd n 2 n + 1 = N 0 n
32 elnn0z n 0 n 0 n
33 12 31 32 sylanbrc A N N Odd n 2 n + 1 = N n 0
34 2nn0 2 0
35 34 a1i A N N Odd n 2 n + 1 = N 2 0
36 26 33 35 expmuld A N N Odd n 2 n + 1 = N A 2 n = A 2 n
37 6 33 35 expmuld A N N Odd n 2 n + 1 = N A 2 n = A 2 n
38 25 36 37 3eqtr4d A N N Odd n 2 n + 1 = N A 2 n = A 2 n
39 38 oveq1d A N N Odd n 2 n + 1 = N A 2 n A = A 2 n A
40 26 20 expp1d A N N Odd n 2 n + 1 = N A 2 n + 1 = A 2 n A
41 7 oveq2d A N N Odd n 2 n + 1 = N A 2 n + 1 = A N
42 40 41 eqtr3d A N N Odd n 2 n + 1 = N A 2 n A = A N
43 39 42 eqtr3d A N N Odd n 2 n + 1 = N A 2 n A = A N
44 22 43 eqtr3d A N N Odd n 2 n + 1 = N A 2 n A = A N
45 6 20 expp1d A N N Odd n 2 n + 1 = N A 2 n + 1 = A 2 n A
46 7 oveq2d A N N Odd n 2 n + 1 = N A 2 n + 1 = A N
47 45 46 eqtr3d A N N Odd n 2 n + 1 = N A 2 n A = A N
48 47 negeqd A N N Odd n 2 n + 1 = N A 2 n A = A N
49 44 48 eqtr3d A N N Odd n 2 n + 1 = N A N = A N
50 5 49 rexlimddv A N N Odd A N = A N