Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	negexpidd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	negexpidd.3	⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
Assertion	negexpidd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( - 𝐴 ↑ 𝑁 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		negexpidd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		negexpidd.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3		negexpidd.3	⊢ ( 𝜑 → ¬ 2 ∥ 𝑁 )
4	1 2	reexpcld	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )
6	5	negidd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + - ( 𝐴 ↑ 𝑁 ) ) = 0 )
7	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
8	7	mulm1d	⊢ ( 𝜑 → ( - 1 · 𝐴 ) = - 𝐴 )
9	8	eqcomd	⊢ ( 𝜑 → - 𝐴 = ( - 1 · 𝐴 ) )
10	9	oveq1d	⊢ ( 𝜑 → ( - 𝐴 ↑ 𝑁 ) = ( ( - 1 · 𝐴 ) ↑ 𝑁 ) )
11		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
12	11	a1i	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ ) )
13	12 3	jctird	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) ) )
14	2 13	mpd	⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) )
15		m1expo	⊢ ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( - 1 ↑ 𝑁 ) = - 1 )
16	15	a1i	⊢ ( 𝜑 → ( ( 𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ) → ( - 1 ↑ 𝑁 ) = - 1 ) )
17	14 16	mpd	⊢ ( 𝜑 → ( - 1 ↑ 𝑁 ) = - 1 )
18	17	oveq1d	⊢ ( 𝜑 → ( ( - 1 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) = ( - 1 · ( 𝐴 ↑ 𝑁 ) ) )
19	5	mulm1d	⊢ ( 𝜑 → ( - 1 · ( 𝐴 ↑ 𝑁 ) ) = - ( 𝐴 ↑ 𝑁 ) )
20	18 19	eqtr2d	⊢ ( 𝜑 → - ( 𝐴 ↑ 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) )
21		neg1cn	⊢ - 1 ∈ ℂ
22	21	a1i	⊢ ( 𝜑 → - 1 ∈ ℂ )
23	22 7 2	mulexpd	⊢ ( 𝜑 → ( ( - 1 · 𝐴 ) ↑ 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( 𝐴 ↑ 𝑁 ) ) )
24	20 23	eqtr4d	⊢ ( 𝜑 → - ( 𝐴 ↑ 𝑁 ) = ( ( - 1 · 𝐴 ) ↑ 𝑁 ) )
25	10 24	eqtr4d	⊢ ( 𝜑 → ( - 𝐴 ↑ 𝑁 ) = - ( 𝐴 ↑ 𝑁 ) )
26	25	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( - 𝐴 ↑ 𝑁 ) ) = ( ( 𝐴 ↑ 𝑁 ) + - ( 𝐴 ↑ 𝑁 ) ) )
27	26	eqeq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 𝑁 ) + ( - 𝐴 ↑ 𝑁 ) ) = 0 ↔ ( ( 𝐴 ↑ 𝑁 ) + - ( 𝐴 ↑ 𝑁 ) ) = 0 ) )
28	6 27	mpbird	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) + ( - 𝐴 ↑ 𝑁 ) ) = 0 )