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	|- ( ph -> A e. RR )
	negexpidd.2	|- ( ph -> N e. NN0 )
	negexpidd.3	|- ( ph -> -. 2 || N )
Assertion	negexpidd	|- ( ph -> ( ( A ^ N ) + ( -u A ^ N ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		negexpidd.1	|- ( ph -> A e. RR )
2		negexpidd.2	|- ( ph -> N e. NN0 )
3		negexpidd.3	|- ( ph -> -. 2 || N )
4	1 2	reexpcld	|- ( ph -> ( A ^ N ) e. RR )
5	4	recnd	|- ( ph -> ( A ^ N ) e. CC )
6	5	negidd	|- ( ph -> ( ( A ^ N ) + -u ( A ^ N ) ) = 0 )
7	1	recnd	|- ( ph -> A e. CC )
8	7	mulm1d	|- ( ph -> ( -u 1 x. A ) = -u A )
9	8	eqcomd	|- ( ph -> -u A = ( -u 1 x. A ) )
10	9	oveq1d	|- ( ph -> ( -u A ^ N ) = ( ( -u 1 x. A ) ^ N ) )
11		nn0z	|- ( N e. NN0 -> N e. ZZ )
12	11	a1i	|- ( ph -> ( N e. NN0 -> N e. ZZ ) )
13	12 3	jctird	|- ( ph -> ( N e. NN0 -> ( N e. ZZ /\ -. 2 || N ) ) )
14	2 13	mpd	|- ( ph -> ( N e. ZZ /\ -. 2 || N ) )
15		m1expo	|- ( ( N e. ZZ /\ -. 2 || N ) -> ( -u 1 ^ N ) = -u 1 )
16	15	a1i	|- ( ph -> ( ( N e. ZZ /\ -. 2 || N ) -> ( -u 1 ^ N ) = -u 1 ) )
17	14 16	mpd	|- ( ph -> ( -u 1 ^ N ) = -u 1 )
18	17	oveq1d	|- ( ph -> ( ( -u 1 ^ N ) x. ( A ^ N ) ) = ( -u 1 x. ( A ^ N ) ) )
19	5	mulm1d	|- ( ph -> ( -u 1 x. ( A ^ N ) ) = -u ( A ^ N ) )
20	18 19	eqtr2d	|- ( ph -> -u ( A ^ N ) = ( ( -u 1 ^ N ) x. ( A ^ N ) ) )
21		neg1cn	|- -u 1 e. CC
22	21	a1i	|- ( ph -> -u 1 e. CC )
23	22 7 2	mulexpd	|- ( ph -> ( ( -u 1 x. A ) ^ N ) = ( ( -u 1 ^ N ) x. ( A ^ N ) ) )
24	20 23	eqtr4d	|- ( ph -> -u ( A ^ N ) = ( ( -u 1 x. A ) ^ N ) )
25	10 24	eqtr4d	|- ( ph -> ( -u A ^ N ) = -u ( A ^ N ) )
26	25	oveq2d	|- ( ph -> ( ( A ^ N ) + ( -u A ^ N ) ) = ( ( A ^ N ) + -u ( A ^ N ) ) )
27	26	eqeq1d	|- ( ph -> ( ( ( A ^ N ) + ( -u A ^ N ) ) = 0 <-> ( ( A ^ N ) + -u ( A ^ N ) ) = 0 ) )
28	6 27	mpbird	|- ( ph -> ( ( A ^ N ) + ( -u A ^ N ) ) = 0 )