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	$$⊢\phi \to A\in ℝ$$
	expeqidd.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 2}$$
	expeqidd.0	$$⊢\phi \to 0\le A$$
Assertion	expeqidd	$$⊢\phi \to \left(A^N=A\leftrightarrow \left(A=0\vee A=1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		expeqidd.a	$$⊢\phi \to A\in ℝ$$
2		expeqidd.n	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 2}$$
3		expeqidd.0	$$⊢\phi \to 0\le A$$
4		df-ne	$$⊢A\ne 0\leftrightarrow \neg A=0$$
5	1	recnd	$$⊢\phi \to A\in ℂ$$
6	5	ad2antrr	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to A\in ℂ$$
7		simplr	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to A\ne 0$$
8		eluz2nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{N}$$
9	2 8	syl	$$⊢\phi \to N\in \mathbb{N}$$
10	9	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
11	10	ad2antrr	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to N\in \mathbb{Z}$$
12	6 7 11	expm1d	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to A^{N-1}=\frac{A^N}{A}$$
13		simpr	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to A^N=A$$
14	13	oveq1d	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to \frac{A^N}{A}=\frac{A}{A}$$
15	6 7	dividd	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to \frac{A}{A}=1$$
16	12 14 15	3eqtrd	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to A^{N-1}=1$$
17	1	adantr	$$⊢\left(\phi \wedge A\ne 0\right)\to A\in ℝ$$
18		uz2m1nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N-1\in \mathbb{N}$$
19	2 18	syl	$$⊢\phi \to N-1\in \mathbb{N}$$
20	19	adantr	$$⊢\left(\phi \wedge A\ne 0\right)\to N-1\in \mathbb{N}$$
21	3	adantr	$$⊢\left(\phi \wedge A\ne 0\right)\to 0\le A$$
22	17 20 21	expeq1d	$$⊢\left(\phi \wedge A\ne 0\right)\to \left(A^{N-1}=1\leftrightarrow A=1\right)$$
23	22	biimpa	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^{N-1}=1\right)\to A=1$$
24	16 23	syldan	$$⊢\left(\left(\phi \wedge A\ne 0\right)\wedge A^N=A\right)\to A=1$$
25	24	an32s	$$⊢\left(\left(\phi \wedge A^N=A\right)\wedge A\ne 0\right)\to A=1$$
26	25	ex	$$⊢\left(\phi \wedge A^N=A\right)\to \left(A\ne 0\to A=1\right)$$
27	4 26	biimtrrid	$$⊢\left(\phi \wedge A^N=A\right)\to \left(\neg A=0\to A=1\right)$$
28	27	orrd	$$⊢\left(\phi \wedge A^N=A\right)\to \left(A=0\vee A=1\right)$$
29	28	ex	$$⊢\phi \to \left(A^N=A\to \left(A=0\vee A=1\right)\right)$$
30	9	0expd	$$⊢\phi \to 0^N=0$$
31		oveq1	$$⊢A=0\to A^N=0^N$$
32		id	$$⊢A=0\to A=0$$
33	31 32	eqeq12d	$$⊢A=0\to \left(A^N=A\leftrightarrow 0^N=0\right)$$
34	30 33	syl5ibrcom	$$⊢\phi \to \left(A=0\to A^N=A\right)$$
35		1exp	$$⊢N\in \mathbb{Z}\to 1^N=1$$
36	10 35	syl	$$⊢\phi \to 1^N=1$$
37		oveq1	$$⊢A=1\to A^N=1^N$$
38		id	$$⊢A=1\to A=1$$
39	37 38	eqeq12d	$$⊢A=1\to \left(A^N=A\leftrightarrow 1^N=1\right)$$
40	36 39	syl5ibrcom	$$⊢\phi \to \left(A=1\to A^N=A\right)$$
41	34 40	jaod	$$⊢\phi \to \left(\left(A=0\vee A=1\right)\to A^N=A\right)$$
42	29 41	impbid	$$⊢\phi \to \left(A^N=A\leftrightarrow \left(A=0\vee A=1\right)\right)$$