Theorem expeqidd

Description: A nonnegative real number is zero or one if and only if it is itself when raised to an integer greater than one. (Contributed by SN, 3-Jul-2025)

	Ref	Expression
Hypotheses	expeqidd.a	|- ( ph -> A e. RR )
	expeqidd.n	|- ( ph -> N e. ( ZZ>= ` 2 ) )
	expeqidd.0	|- ( ph -> 0 <_ A )
Assertion	expeqidd	|- ( ph -> ( ( A ^ N ) = A <-> ( A = 0 \/ A = 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		expeqidd.a	|- ( ph -> A e. RR )
2		expeqidd.n	|- ( ph -> N e. ( ZZ>= ` 2 ) )
3		expeqidd.0	|- ( ph -> 0 <_ A )
4		df-ne	|- ( A =/= 0 <-> -. A = 0 )
5	1	recnd	|- ( ph -> A e. CC )
6	5	ad2antrr	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> A e. CC )
7		simplr	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> A =/= 0 )
8		eluz2nn	|- ( N e. ( ZZ>= ` 2 ) -> N e. NN )
9	2 8	syl	|- ( ph -> N e. NN )
10	9	nnzd	|- ( ph -> N e. ZZ )
11	10	ad2antrr	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> N e. ZZ )
12	6 7 11	expm1d	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( A ^ ( N - 1 ) ) = ( ( A ^ N ) / A ) )
13		simpr	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( A ^ N ) = A )
14	13	oveq1d	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( ( A ^ N ) / A ) = ( A / A ) )
15	6 7	dividd	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( A / A ) = 1 )
16	12 14 15	3eqtrd	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> ( A ^ ( N - 1 ) ) = 1 )
17	1	adantr	|- ( ( ph /\ A =/= 0 ) -> A e. RR )
18		uz2m1nn	|- ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
19	2 18	syl	|- ( ph -> ( N - 1 ) e. NN )
20	19	adantr	|- ( ( ph /\ A =/= 0 ) -> ( N - 1 ) e. NN )
21	3	adantr	|- ( ( ph /\ A =/= 0 ) -> 0 <_ A )
22	17 20 21	expeq1d	|- ( ( ph /\ A =/= 0 ) -> ( ( A ^ ( N - 1 ) ) = 1 <-> A = 1 ) )
23	22	biimpa	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ ( N - 1 ) ) = 1 ) -> A = 1 )
24	16 23	syldan	|- ( ( ( ph /\ A =/= 0 ) /\ ( A ^ N ) = A ) -> A = 1 )
25	24	an32s	|- ( ( ( ph /\ ( A ^ N ) = A ) /\ A =/= 0 ) -> A = 1 )
26	25	ex	|- ( ( ph /\ ( A ^ N ) = A ) -> ( A =/= 0 -> A = 1 ) )
27	4 26	biimtrrid	|- ( ( ph /\ ( A ^ N ) = A ) -> ( -. A = 0 -> A = 1 ) )
28	27	orrd	|- ( ( ph /\ ( A ^ N ) = A ) -> ( A = 0 \/ A = 1 ) )
29	28	ex	|- ( ph -> ( ( A ^ N ) = A -> ( A = 0 \/ A = 1 ) ) )
30	9	0expd	|- ( ph -> ( 0 ^ N ) = 0 )
31		oveq1	|- ( A = 0 -> ( A ^ N ) = ( 0 ^ N ) )
32		id	|- ( A = 0 -> A = 0 )
33	31 32	eqeq12d	|- ( A = 0 -> ( ( A ^ N ) = A <-> ( 0 ^ N ) = 0 ) )
34	30 33	syl5ibrcom	|- ( ph -> ( A = 0 -> ( A ^ N ) = A ) )
35		1exp	|- ( N e. ZZ -> ( 1 ^ N ) = 1 )
36	10 35	syl	|- ( ph -> ( 1 ^ N ) = 1 )
37		oveq1	|- ( A = 1 -> ( A ^ N ) = ( 1 ^ N ) )
38		id	|- ( A = 1 -> A = 1 )
39	37 38	eqeq12d	|- ( A = 1 -> ( ( A ^ N ) = A <-> ( 1 ^ N ) = 1 ) )
40	36 39	syl5ibrcom	|- ( ph -> ( A = 1 -> ( A ^ N ) = A ) )
41	34 40	jaod	|- ( ph -> ( ( A = 0 \/ A = 1 ) -> ( A ^ N ) = A ) )
42	29 41	impbid	|- ( ph -> ( ( A ^ N ) = A <-> ( A = 0 \/ A = 1 ) ) )