Theorem expeq1d

Description: A nonnegative real number is one if and only if it is one when raised to a positive integer. (Contributed by SN, 3-Jul-2025)

	Ref	Expression
Hypotheses	expeq1d.a	$$⊢\phi \to A\in ℝ$$
	expeq1d.n	$$⊢\phi \to N\in \mathbb{N}$$
	expeq1d.0	$$⊢\phi \to 0\le A$$
Assertion	expeq1d	$$⊢\phi \to \left(A^N=1\leftrightarrow A=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		expeq1d.a	$$⊢\phi \to A\in ℝ$$
2		expeq1d.n	$$⊢\phi \to N\in \mathbb{N}$$
3		expeq1d.0	$$⊢\phi \to 0\le A$$
4	2	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
5		1exp	$$⊢N\in \mathbb{Z}\to 1^N=1$$
6	4 5	syl	$$⊢\phi \to 1^N=1$$
7	6	eqeq2d	$$⊢\phi \to \left(A^N=1^N\leftrightarrow A^N=1\right)$$
8	1	adantr	$$⊢\left(\phi \wedge A^N=1^N\right)\to A\in ℝ$$
9	3	adantr	$$⊢\left(\phi \wedge A^N=1^N\right)\to 0\le A$$
10		0ne1	$$⊢0\ne 1$$
11	10	a1i	$$⊢\phi \to 0\ne 1$$
12	2	0expd	$$⊢\phi \to 0^N=0$$
13	11 12 6	3netr4d	$$⊢\phi \to 0^N\ne 1^N$$
14	13	adantr	$$⊢\left(\phi \wedge A^N=1^N\right)\to 0^N\ne 1^N$$
15		oveq1	$$⊢A=0\to A^N=0^N$$
16	15	eqeq1d	$$⊢A=0\to \left(A^N=1^N\leftrightarrow 0^N=1^N\right)$$
17	16	biimpac	$$⊢\left(A^N=1^N\wedge A=0\right)\to 0^N=1^N$$
18	17	adantll	$$⊢\left(\left(\phi \wedge A^N=1^N\right)\wedge A=0\right)\to 0^N=1^N$$
19	14 18	mteqand	$$⊢\left(\phi \wedge A^N=1^N\right)\to A\ne 0$$
20	8 9 19	ne0gt0d	$$⊢\left(\phi \wedge A^N=1^N\right)\to 0<A$$
21	8 20	elrpd	$$⊢\left(\phi \wedge A^N=1^N\right)\to A\in {ℝ}^{+}$$
22		1rp	$$⊢1\in {ℝ}^{+}$$
23	22	a1i	$$⊢\left(\phi \wedge A^N=1^N\right)\to 1\in {ℝ}^{+}$$
24	2	adantr	$$⊢\left(\phi \wedge A^N=1^N\right)\to N\in \mathbb{N}$$
25		simpr	$$⊢\left(\phi \wedge A^N=1^N\right)\to A^N=1^N$$
26	21 23 24 25	exp11nnd	$$⊢\left(\phi \wedge A^N=1^N\right)\to A=1$$
27	26	ex	$$⊢\phi \to \left(A^N=1^N\to A=1\right)$$
28	7 27	sylbird	$$⊢\phi \to \left(A^N=1\to A=1\right)$$
29		oveq1	$$⊢A=1\to A^N=1^N$$
30	29	eqeq1d	$$⊢A=1\to \left(A^N=1\leftrightarrow 1^N=1\right)$$
31	6 30	syl5ibrcom	$$⊢\phi \to \left(A=1\to A^N=1\right)$$
32	28 31	impbid	$$⊢\phi \to \left(A^N=1\leftrightarrow A=1\right)$$