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	$⊢ φ \to A \in ℝ$
	expeq1d.n	$⊢ φ \to N \in ℕ$
	expeq1d.0	$⊢ φ \to 0 \leq A$
Assertion	expeq1d	$⊢ φ \to (A^{N} = 1 \leftrightarrow A = 1)$

Proof

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

Metamath Proof Explorer

Theorem expeq1d

Proof