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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	expeq1d.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	expeq1d.0	⊢ ( 𝜑 → 0 ≤ 𝐴 )
Assertion	expeq1d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = 1 ↔ 𝐴 = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		expeq1d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		expeq1d.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		expeq1d.0	⊢ ( 𝜑 → 0 ≤ 𝐴 )
4	2	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5		1exp	⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
6	4 5	syl	⊢ ( 𝜑 → ( 1 ↑ 𝑁 ) = 1 )
7	6	eqeq2d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ↔ ( 𝐴 ↑ 𝑁 ) = 1 ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → 𝐴 ∈ ℝ )
9	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → 0 ≤ 𝐴 )
10		0ne1	⊢ 0 ≠ 1
11	10	a1i	⊢ ( 𝜑 → 0 ≠ 1 )
12	2	0expd	⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) = 0 )
13	11 12 6	3netr4d	⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) ≠ ( 1 ↑ 𝑁 ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → ( 0 ↑ 𝑁 ) ≠ ( 1 ↑ 𝑁 ) )
15		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
16	15	eqeq1d	⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ↔ ( 0 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) )
17	16	biimpac	⊢ ( ( ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ∧ 𝐴 = 0 ) → ( 0 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
18	17	adantll	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) ∧ 𝐴 = 0 ) → ( 0 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
19	14 18	mteqand	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → 𝐴 ≠ 0 )
20	8 9 19	ne0gt0d	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → 0 < 𝐴 )
21	8 20	elrpd	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → 𝐴 ∈ ℝ⁺ )
22		1rp	⊢ 1 ∈ ℝ⁺
23	22	a1i	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → 1 ∈ ℝ⁺ )
24	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → 𝑁 ∈ ℕ )
25		simpr	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
26	21 23 24 25	exp11nnd	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) ) → 𝐴 = 1 )
27	26	ex	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) → 𝐴 = 1 ) )
28	7 27	sylbird	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = 1 → 𝐴 = 1 ) )
29		oveq1	⊢ ( 𝐴 = 1 → ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
30	29	eqeq1d	⊢ ( 𝐴 = 1 → ( ( 𝐴 ↑ 𝑁 ) = 1 ↔ ( 1 ↑ 𝑁 ) = 1 ) )
31	6 30	syl5ibrcom	⊢ ( 𝜑 → ( 𝐴 = 1 → ( 𝐴 ↑ 𝑁 ) = 1 ) )
32	28 31	impbid	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = 1 ↔ 𝐴 = 1 ) )

Metamath Proof Explorer

Theorem expeq1d

Proof