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 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) → ( - 𝐴𝑁 ) = - ( 𝐴𝑁 ) )

Proof

Step Hyp Ref Expression
1 oddz ( 𝑁 ∈ Odd → 𝑁 ∈ ℤ )
2 odd2np1ALTV ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
3 1 2 syl ( 𝑁 ∈ Odd → ( 𝑁 ∈ Odd ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
4 3 ibi ( 𝑁 ∈ Odd → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
5 4 3ad2ant3 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
6 simpl1 ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝐴 ∈ ℂ )
7 simprr ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
8 simpl2 ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝑁 ∈ ℕ )
9 8 nncnd ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝑁 ∈ ℂ )
10 1cnd ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 1 ∈ ℂ )
11 2z 2 ∈ ℤ
12 simprl ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝑛 ∈ ℤ )
13 zmulcl ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 · 𝑛 ) ∈ ℤ )
14 11 12 13 sylancr ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 2 · 𝑛 ) ∈ ℤ )
15 14 zcnd ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 2 · 𝑛 ) ∈ ℂ )
16 9 10 15 subadd2d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 𝑁 − 1 ) = ( 2 · 𝑛 ) ↔ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
17 7 16 mpbird ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝑁 − 1 ) = ( 2 · 𝑛 ) )
18 nnm1nn0 ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
19 8 18 syl ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝑁 − 1 ) ∈ ℕ0 )
20 17 19 eqeltrrd ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 2 · 𝑛 ) ∈ ℕ0 )
21 6 20 expcld ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝐴 ↑ ( 2 · 𝑛 ) ) ∈ ℂ )
22 21 6 mulneg2d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) = - ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) )
23 sqneg ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
24 6 23 syl ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
25 24 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( - 𝐴 ↑ 2 ) ↑ 𝑛 ) = ( ( 𝐴 ↑ 2 ) ↑ 𝑛 ) )
26 6 negcld ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → - 𝐴 ∈ ℂ )
27 2rp 2 ∈ ℝ+
28 27 a1i ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 2 ∈ ℝ+ )
29 12 zred ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝑛 ∈ ℝ )
30 20 nn0ge0d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 0 ≤ ( 2 · 𝑛 ) )
31 28 29 30 prodge0rd ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 0 ≤ 𝑛 )
32 elnn0z ( 𝑛 ∈ ℕ0 ↔ ( 𝑛 ∈ ℤ ∧ 0 ≤ 𝑛 ) )
33 12 31 32 sylanbrc ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝑛 ∈ ℕ0 )
34 2nn0 2 ∈ ℕ0
35 34 a1i ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 2 ∈ ℕ0 )
36 26 33 35 expmuld ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ ( 2 · 𝑛 ) ) = ( ( - 𝐴 ↑ 2 ) ↑ 𝑛 ) )
37 6 33 35 expmuld ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝐴 ↑ ( 2 · 𝑛 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 𝑛 ) )
38 25 36 37 3eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ ( 2 · 𝑛 ) ) = ( 𝐴 ↑ ( 2 · 𝑛 ) ) )
39 38 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( - 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) = ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) )
40 26 20 expp1d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( - 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) )
41 7 oveq2d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( - 𝐴𝑁 ) )
42 40 41 eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( - 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) = ( - 𝐴𝑁 ) )
43 39 42 eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) = ( - 𝐴𝑁 ) )
44 22 43 eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → - ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) = ( - 𝐴𝑁 ) )
45 6 20 expp1d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) )
46 7 oveq2d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( 𝐴𝑁 ) )
47 45 46 eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) = ( 𝐴𝑁 ) )
48 47 negeqd ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → - ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) = - ( 𝐴𝑁 ) )
49 44 48 eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴𝑁 ) = - ( 𝐴𝑁 ) )
50 5 49 rexlimddv ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) → ( - 𝐴𝑁 ) = - ( 𝐴𝑁 ) )