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 ∥ 𝑁 ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )