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 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )

Proof

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