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	$⊢ (A \in ℂ \land A \neq 0 \land N \in Odd) \to {(- A)}^{N} = - A^{N}$

Proof

Step	Hyp	Ref	Expression
1		oddz	$⊢ N \in Odd \to N \in ℤ$
2		odd2np1ALTV	$⊢ N \in ℤ \to (N \in Odd \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
3	1 2	syl	$⊢ N \in Odd \to (N \in Odd \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
4	3	biimpd	$⊢ N \in Odd \to (N \in Odd \to \exists n \in ℤ 2 n + 1 = N)$
5	4	pm2.43i	$⊢ N \in Odd \to \exists n \in ℤ 2 n + 1 = N$
6	5	3ad2ant3	$⊢ (A \in ℂ \land A \neq 0 \land N \in Odd) \to \exists n \in ℤ 2 n + 1 = N$
7		simpl1	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A \in ℂ$
8		simpl2	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A \neq 0$
9		2z	$⊢ 2 \in ℤ$
10		simprl	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to n \in ℤ$
11		zmulcl	$⊢ (2 \in ℤ \land n \in ℤ) \to 2 n \in ℤ$
12	9 10 11	sylancr	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to 2 n \in ℤ$
13	7 8 12	expclzd	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} \in ℂ$
14	13 7	mulneg2d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} (- A) = - A^{2 n} A$
15		sqneg	$⊢ A \in ℂ \to {(- A)}^{2} = A^{2}$
16	7 15	syl	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2} = A^{2}$
17	16	oveq1d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {({(- A)}^{2})}^{n} = {(A^{2})}^{n}$
18	7	negcld	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to - A \in ℂ$
19	7 8	negne0d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to - A \neq 0$
20	9	a1i	$⊢ (n \in ℤ \land 2 n + 1 = N) \to 2 \in ℤ$
21		simpl	$⊢ (n \in ℤ \land 2 n + 1 = N) \to n \in ℤ$
22	20 21	jca	$⊢ (n \in ℤ \land 2 n + 1 = N) \to (2 \in ℤ \land n \in ℤ)$
23	22	adantl	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to (2 \in ℤ \land n \in ℤ)$
24	18 19 23	jca31	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to ((- A \in ℂ \land - A \neq 0) \land (2 \in ℤ \land n \in ℤ))$
25		expmulz	$⊢ ((- A \in ℂ \land - A \neq 0) \land (2 \in ℤ \land n \in ℤ)) \to {(- A)}^{2 n} = {({(- A)}^{2})}^{n}$
26	24 25	syl	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n} = {({(- A)}^{2})}^{n}$
27	7 8 23	jca31	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to ((A \in ℂ \land A \neq 0) \land (2 \in ℤ \land n \in ℤ))$
28		expmulz	$⊢ ((A \in ℂ \land A \neq 0) \land (2 \in ℤ \land n \in ℤ)) \to A^{2 n} = {(A^{2})}^{n}$
29	27 28	syl	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} = {(A^{2})}^{n}$
30	17 26 29	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n} = A^{2 n}$
31	30	oveq1d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n} (- A) = A^{2 n} (- A)$
32	18 19 12	expp1zd	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n + 1} = {(- A)}^{2 n} (- A)$
33		simprr	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to 2 n + 1 = N$
34	33	oveq2d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n + 1} = {(- A)}^{N}$
35	32 34	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n} (- A) = {(- A)}^{N}$
36	31 35	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} (- A) = {(- A)}^{N}$
37	14 36	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to - A^{2 n} A = {(- A)}^{N}$
38	7 8 12	expp1zd	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n + 1} = A^{2 n} A$
39	33	oveq2d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n + 1} = A^{N}$
40	38 39	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} A = A^{N}$
41	40	negeqd	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to - A^{2 n} A = - A^{N}$
42	37 41	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0 \land N \in Odd) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{N} = - A^{N}$
43	6 42	rexlimddv	$⊢ (A \in ℂ \land A \neq 0 \land N \in Odd) \to {(- A)}^{N} = - A^{N}$

Metamath Proof Explorer

Theorem oexpnegnz

Proof