Description: The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015) (Proof shortened by AV, 10-Jul-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | oexpneg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnz | |
|
2 | odd2np1 | |
|
3 | 1 2 | syl | |
4 | 3 | biimpa | |
5 | 4 | 3adant1 | |
6 | simpl1 | |
|
7 | simprr | |
|
8 | simpl2 | |
|
9 | 8 | nncnd | |
10 | 1cnd | |
|
11 | 2z | |
|
12 | simprl | |
|
13 | zmulcl | |
|
14 | 11 12 13 | sylancr | |
15 | 14 | zcnd | |
16 | 9 10 15 | subadd2d | |
17 | 7 16 | mpbird | |
18 | nnm1nn0 | |
|
19 | 8 18 | syl | |
20 | 17 19 | eqeltrrd | |
21 | 6 20 | expcld | |
22 | 21 6 | mulneg2d | |
23 | sqneg | |
|
24 | 6 23 | syl | |
25 | 24 | oveq1d | |
26 | 6 | negcld | |
27 | 2rp | |
|
28 | 27 | a1i | |
29 | 12 | zred | |
30 | 20 | nn0ge0d | |
31 | 28 29 30 | prodge0rd | |
32 | elnn0z | |
|
33 | 12 31 32 | sylanbrc | |
34 | 2nn0 | |
|
35 | 34 | a1i | |
36 | 26 33 35 | expmuld | |
37 | 6 33 35 | expmuld | |
38 | 25 36 37 | 3eqtr4d | |
39 | 38 | oveq1d | |
40 | 26 20 | expp1d | |
41 | 7 | oveq2d | |
42 | 40 41 | eqtr3d | |
43 | 39 42 | eqtr3d | |
44 | 22 43 | eqtr3d | |
45 | 6 20 | expp1d | |
46 | 7 | oveq2d | |
47 | 45 46 | eqtr3d | |
48 | 47 | negeqd | |
49 | 44 48 | eqtr3d | |
50 | 5 49 | rexlimddv | |