negexpidd

Description: The sum of a real number to the power of N and the negative of the number to the power of N equals zero if N is a nonnegative odd integer. (Contributed by Igor Ieskov, 21-Jan-2024)

	Ref	Expression
Hypotheses	negexpidd.1	$⊢ φ \to A \in ℝ$
	negexpidd.2	$⊢ φ \to N \in ℕ_{0}$
	negexpidd.3	$⊢ φ \to \neg 2 ∥ N$
Assertion	negexpidd	$⊢ φ \to A^{N} + {(- A)}^{N} = 0$

Proof

Step	Hyp	Ref	Expression
1		negexpidd.1	$⊢ φ \to A \in ℝ$
2		negexpidd.2	$⊢ φ \to N \in ℕ_{0}$
3		negexpidd.3	$⊢ φ \to \neg 2 ∥ N$
4	1 2	reexpcld	$⊢ φ \to A^{N} \in ℝ$
5	4	recnd	$⊢ φ \to A^{N} \in ℂ$
6	5	negidd	$⊢ φ \to A^{N} + (- A^{N}) = 0$
7	1	recnd	$⊢ φ \to A \in ℂ$
8	7	mulm1d	$⊢ φ \to -1 A = - A$
9	8	eqcomd	$⊢ φ \to - A = -1 A$
10	9	oveq1d	$⊢ φ \to {(- A)}^{N} = {-1 A}^{N}$
11		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
12	11	a1i	$⊢ φ \to (N \in ℕ_{0} \to N \in ℤ)$
13	12 3	jctird	$⊢ φ \to (N \in ℕ_{0} \to (N \in ℤ \land \neg 2 ∥ N))$
14	2 13	mpd	$⊢ φ \to (N \in ℤ \land \neg 2 ∥ N)$
15		m1expo	$⊢ (N \in ℤ \land \neg 2 ∥ N) \to {(- 1)}^{N} = - 1$
16	15	a1i	$⊢ φ \to ((N \in ℤ \land \neg 2 ∥ N) \to {(- 1)}^{N} = - 1)$
17	14 16	mpd	$⊢ φ \to {(- 1)}^{N} = - 1$
18	17	oveq1d	$⊢ φ \to {(- 1)}^{N} A^{N} = -1 A^{N}$
19	5	mulm1d	$⊢ φ \to -1 A^{N} = - A^{N}$
20	18 19	eqtr2d	$⊢ φ \to - A^{N} = {(- 1)}^{N} A^{N}$
21		neg1cn	$⊢ - 1 \in ℂ$
22	21	a1i	$⊢ φ \to - 1 \in ℂ$
23	22 7 2	mulexpd	$⊢ φ \to {-1 A}^{N} = {(- 1)}^{N} A^{N}$
24	20 23	eqtr4d	$⊢ φ \to - A^{N} = {-1 A}^{N}$
25	10 24	eqtr4d	$⊢ φ \to {(- A)}^{N} = - A^{N}$
26	25	oveq2d	$⊢ φ \to A^{N} + {(- A)}^{N} = A^{N} + (- A^{N})$
27	26	eqeq1d	$⊢ φ \to (A^{N} + {(- A)}^{N} = 0 \leftrightarrow A^{N} + (- A^{N}) = 0)$
28	6 27	mpbird	$⊢ φ \to A^{N} + {(- A)}^{N} = 0$

Metamath Proof Explorer

Theorem negexpidd

Proof