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	$⊢ (A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \to {(- A)}^{N} = - A^{N}$

Proof

Step	Hyp	Ref	Expression
1		nnz	$⊢ N \in ℕ \to N \in ℤ$
2		odd2np1	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
3	1 2	syl	$⊢ N \in ℕ \to (\neg 2 ∥ N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
4	3	biimpa	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to \exists n \in ℤ 2 n + 1 = N$
5	4	3adant1	$⊢ (A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \to \exists n \in ℤ 2 n + 1 = N$
6		simpl1	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to A \in ℂ$
7		simprr	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 2 n + 1 = N$
8		simpl2	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to N \in ℕ$
9	8	nncnd	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to N \in ℂ$
10		1cnd	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 1 \in ℂ$
11		2z	$⊢ 2 \in ℤ$
12		simprl	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to n \in ℤ$
13		zmulcl	$⊢ (2 \in ℤ \land n \in ℤ) \to 2 n \in ℤ$
14	11 12 13	sylancr	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 2 n \in ℤ$
15	14	zcnd	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 2 n \in ℂ$
16	9 10 15	subadd2d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to (N - 1 = 2 n \leftrightarrow 2 n + 1 = N)$
17	7 16	mpbird	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to N - 1 = 2 n$
18		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
19	8 18	syl	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to N - 1 \in ℕ_{0}$
20	17 19	eqeltrrd	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 2 n \in ℕ_{0}$
21	6 20	expcld	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} \in ℂ$
22	21 6	mulneg2d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} (- A) = - A^{2 n} A$
23		sqneg	$⊢ A \in ℂ \to {(- A)}^{2} = A^{2}$
24	6 23	syl	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2} = A^{2}$
25	24	oveq1d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {({(- A)}^{2})}^{n} = {(A^{2})}^{n}$
26	6	negcld	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to - A \in ℂ$
27		2rp	$⊢ 2 \in ℝ^{+}$
28	27	a1i	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 2 \in ℝ^{+}$
29	12	zred	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to n \in ℝ$
30	20	nn0ge0d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 0 \leq 2 n$
31	28 29 30	prodge0rd	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 0 \leq n$
32		elnn0z	$⊢ n \in ℕ_{0} \leftrightarrow (n \in ℤ \land 0 \leq n)$
33	12 31 32	sylanbrc	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to n \in ℕ_{0}$
34		2nn0	$⊢ 2 \in ℕ_{0}$
35	34	a1i	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to 2 \in ℕ_{0}$
36	26 33 35	expmuld	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n} = {({(- A)}^{2})}^{n}$
37	6 33 35	expmuld	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} = {(A^{2})}^{n}$
38	25 36 37	3eqtr4d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n} = A^{2 n}$
39	38	oveq1d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n} (- A) = A^{2 n} (- A)$
40	26 20	expp1d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n + 1} = {(- A)}^{2 n} (- A)$
41	7	oveq2d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n + 1} = {(- A)}^{N}$
42	40 41	eqtr3d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{2 n} (- A) = {(- A)}^{N}$
43	39 42	eqtr3d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} (- A) = {(- A)}^{N}$
44	22 43	eqtr3d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to - A^{2 n} A = {(- A)}^{N}$
45	6 20	expp1d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n + 1} = A^{2 n} A$
46	7	oveq2d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n + 1} = A^{N}$
47	45 46	eqtr3d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to A^{2 n} A = A^{N}$
48	47	negeqd	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to - A^{2 n} A = - A^{N}$
49	44 48	eqtr3d	$⊢ ((A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \land (n \in ℤ \land 2 n + 1 = N)) \to {(- A)}^{N} = - A^{N}$
50	5 49	rexlimddv	$⊢ (A \in ℂ \land N \in ℕ \land \neg 2 ∥ N) \to {(- A)}^{N} = - A^{N}$

Metamath Proof Explorer

Theorem oexpneg

Proof