Theorem oexpnegnz

Description: The exponential of the negative of a number not being 0, when the exponent is odd. (Contributed by AV, 19-Jun-2020)

	Ref	Expression
Assertion	oexpnegnz	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		oddz	⊢ ( 𝑁 ∈ Odd → 𝑁 ∈ ℤ )
2		odd2np1ALTV	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 ∈ Odd ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
3	1 2	syl	⊢ ( 𝑁 ∈ Odd → ( 𝑁 ∈ Odd ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
4	3	biimpd	⊢ ( 𝑁 ∈ Odd → ( 𝑁 ∈ Odd → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )
5	4	pm2.43i	⊢ ( 𝑁 ∈ Odd → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
6	5	3ad2ant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) → ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
7		simpl1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝐴 ∈ ℂ )
8		simpl2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝐴 ≠ 0 )
9		2z	⊢ 2 ∈ ℤ
10		simprl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → 𝑛 ∈ ℤ )
11		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 2 · 𝑛 ) ∈ ℤ )
12	9 10 11	sylancr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 2 · 𝑛 ) ∈ ℤ )
13	7 8 12	expclzd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝐴 ↑ ( 2 · 𝑛 ) ) ∈ ℂ )
14	13 7	mulneg2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) = - ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) )
15		sqneg	⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
16	7 15	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
17	16	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( - 𝐴 ↑ 2 ) ↑ 𝑛 ) = ( ( 𝐴 ↑ 2 ) ↑ 𝑛 ) )
18	7	negcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → - 𝐴 ∈ ℂ )
19	7 8	negne0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → - 𝐴 ≠ 0 )
20	9	a1i	⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) → 2 ∈ ℤ )
21		simpl	⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) → 𝑛 ∈ ℤ )
22	20 21	jca	⊢ ( ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) → ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
23	22	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
24	18 19 23	jca31	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( - 𝐴 ∈ ℂ ∧ - 𝐴 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) )
25		expmulz	⊢ ( ( ( - 𝐴 ∈ ℂ ∧ - 𝐴 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) → ( - 𝐴 ↑ ( 2 · 𝑛 ) ) = ( ( - 𝐴 ↑ 2 ) ↑ 𝑛 ) )
26	24 25	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ ( 2 · 𝑛 ) ) = ( ( - 𝐴 ↑ 2 ) ↑ 𝑛 ) )
27	7 8 23	jca31	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) )
28		expmulz	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) → ( 𝐴 ↑ ( 2 · 𝑛 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 𝑛 ) )
29	27 28	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝐴 ↑ ( 2 · 𝑛 ) ) = ( ( 𝐴 ↑ 2 ) ↑ 𝑛 ) )
30	17 26 29	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ ( 2 · 𝑛 ) ) = ( 𝐴 ↑ ( 2 · 𝑛 ) ) )
31	30	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( - 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) = ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) )
32	18 19 12	expp1zd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( - 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) )
33		simprr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 2 · 𝑛 ) + 1 ) = 𝑁 )
34	33	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( - 𝐴 ↑ 𝑁 ) )
35	32 34	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( - 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) = ( - 𝐴 ↑ 𝑁 ) )
36	31 35	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · - 𝐴 ) = ( - 𝐴 ↑ 𝑁 ) )
37	14 36	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → - ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) = ( - 𝐴 ↑ 𝑁 ) )
38	7 8 12	expp1zd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) )
39	33	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) = ( 𝐴 ↑ 𝑁 ) )
40	38 39	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) = ( 𝐴 ↑ 𝑁 ) )
41	40	negeqd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → - ( ( 𝐴 ↑ ( 2 · 𝑛 ) ) · 𝐴 ) = - ( 𝐴 ↑ 𝑁 ) )
42	37 41	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) ∧ ( 𝑛 ∈ ℤ ∧ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
43	6 42	rexlimddv	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )