Metamath Proof Explorer


Theorem oexpneg

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 AN¬2NAN=AN

Proof

Step Hyp Ref Expression
1 nnz NN
2 odd2np1 N¬2Nn2n+1=N
3 1 2 syl N¬2Nn2n+1=N
4 3 biimpa N¬2Nn2n+1=N
5 4 3adant1 AN¬2Nn2n+1=N
6 simpl1 AN¬2Nn2n+1=NA
7 simprr AN¬2Nn2n+1=N2n+1=N
8 simpl2 AN¬2Nn2n+1=NN
9 8 nncnd AN¬2Nn2n+1=NN
10 1cnd AN¬2Nn2n+1=N1
11 2z 2
12 simprl AN¬2Nn2n+1=Nn
13 zmulcl 2n2n
14 11 12 13 sylancr AN¬2Nn2n+1=N2n
15 14 zcnd AN¬2Nn2n+1=N2n
16 9 10 15 subadd2d AN¬2Nn2n+1=NN1=2n2n+1=N
17 7 16 mpbird AN¬2Nn2n+1=NN1=2n
18 nnm1nn0 NN10
19 8 18 syl AN¬2Nn2n+1=NN10
20 17 19 eqeltrrd AN¬2Nn2n+1=N2n0
21 6 20 expcld AN¬2Nn2n+1=NA2n
22 21 6 mulneg2d AN¬2Nn2n+1=NA2nA=A2nA
23 sqneg AA2=A2
24 6 23 syl AN¬2Nn2n+1=NA2=A2
25 24 oveq1d AN¬2Nn2n+1=NA2n=A2n
26 6 negcld AN¬2Nn2n+1=NA
27 2rp 2+
28 27 a1i AN¬2Nn2n+1=N2+
29 12 zred AN¬2Nn2n+1=Nn
30 20 nn0ge0d AN¬2Nn2n+1=N02n
31 28 29 30 prodge0rd AN¬2Nn2n+1=N0n
32 elnn0z n0n0n
33 12 31 32 sylanbrc AN¬2Nn2n+1=Nn0
34 2nn0 20
35 34 a1i AN¬2Nn2n+1=N20
36 26 33 35 expmuld AN¬2Nn2n+1=NA2n=A2n
37 6 33 35 expmuld AN¬2Nn2n+1=NA2n=A2n
38 25 36 37 3eqtr4d AN¬2Nn2n+1=NA2n=A2n
39 38 oveq1d AN¬2Nn2n+1=NA2nA=A2nA
40 26 20 expp1d AN¬2Nn2n+1=NA2n+1=A2nA
41 7 oveq2d AN¬2Nn2n+1=NA2n+1=AN
42 40 41 eqtr3d AN¬2Nn2n+1=NA2nA=AN
43 39 42 eqtr3d AN¬2Nn2n+1=NA2nA=AN
44 22 43 eqtr3d AN¬2Nn2n+1=NA2nA=AN
45 6 20 expp1d AN¬2Nn2n+1=NA2n+1=A2nA
46 7 oveq2d AN¬2Nn2n+1=NA2n+1=AN
47 45 46 eqtr3d AN¬2Nn2n+1=NA2nA=AN
48 47 negeqd AN¬2Nn2n+1=NA2nA=AN
49 44 48 eqtr3d AN¬2Nn2n+1=NAN=AN
50 5 49 rexlimddv AN¬2NAN=AN