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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	expeqidd.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
	expeqidd.0	⊢ ( 𝜑 → 0 ≤ 𝐴 )
Assertion	expeqidd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = 𝐴 ↔ ( 𝐴 = 0 ∨ 𝐴 = 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		expeqidd.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		expeqidd.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
3		expeqidd.0	⊢ ( 𝜑 → 0 ≤ 𝐴 )
4		df-ne	⊢ ( 𝐴 ≠ 0 ↔ ¬ 𝐴 = 0 )
5	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
6	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → 𝐴 ∈ ℂ )
7		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → 𝐴 ≠ 0 )
8		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
9	2 8	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10	9	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
11	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → 𝑁 ∈ ℤ )
12	6 7 11	expm1d	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → ( 𝐴 ↑ ( 𝑁 − 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) / 𝐴 ) )
13		simpr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → ( 𝐴 ↑ 𝑁 ) = 𝐴 )
14	13	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → ( ( 𝐴 ↑ 𝑁 ) / 𝐴 ) = ( 𝐴 / 𝐴 ) )
15	6 7	dividd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → ( 𝐴 / 𝐴 ) = 1 )
16	12 14 15	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → ( 𝐴 ↑ ( 𝑁 − 1 ) ) = 1 )
17	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
18		uz2m1nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ )
19	2 18	syl	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( 𝑁 − 1 ) ∈ ℕ )
21	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → 0 ≤ 𝐴 )
22	17 20 21	expeq1d	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 ↑ ( 𝑁 − 1 ) ) = 1 ↔ 𝐴 = 1 ) )
23	22	biimpa	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ ( 𝑁 − 1 ) ) = 1 ) → 𝐴 = 1 )
24	16 23	syldan	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → 𝐴 = 1 )
25	24	an32s	⊢ ( ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) ∧ 𝐴 ≠ 0 ) → 𝐴 = 1 )
26	25	ex	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → ( 𝐴 ≠ 0 → 𝐴 = 1 ) )
27	4 26	biimtrrid	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → ( ¬ 𝐴 = 0 → 𝐴 = 1 ) )
28	27	orrd	⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 𝑁 ) = 𝐴 ) → ( 𝐴 = 0 ∨ 𝐴 = 1 ) )
29	28	ex	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = 𝐴 → ( 𝐴 = 0 ∨ 𝐴 = 1 ) ) )
30	9	0expd	⊢ ( 𝜑 → ( 0 ↑ 𝑁 ) = 0 )
31		oveq1	⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
32		id	⊢ ( 𝐴 = 0 → 𝐴 = 0 )
33	31 32	eqeq12d	⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 𝑁 ) = 𝐴 ↔ ( 0 ↑ 𝑁 ) = 0 ) )
34	30 33	syl5ibrcom	⊢ ( 𝜑 → ( 𝐴 = 0 → ( 𝐴 ↑ 𝑁 ) = 𝐴 ) )
35		1exp	⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
36	10 35	syl	⊢ ( 𝜑 → ( 1 ↑ 𝑁 ) = 1 )
37		oveq1	⊢ ( 𝐴 = 1 → ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
38		id	⊢ ( 𝐴 = 1 → 𝐴 = 1 )
39	37 38	eqeq12d	⊢ ( 𝐴 = 1 → ( ( 𝐴 ↑ 𝑁 ) = 𝐴 ↔ ( 1 ↑ 𝑁 ) = 1 ) )
40	36 39	syl5ibrcom	⊢ ( 𝜑 → ( 𝐴 = 1 → ( 𝐴 ↑ 𝑁 ) = 𝐴 ) )
41	34 40	jaod	⊢ ( 𝜑 → ( ( 𝐴 = 0 ∨ 𝐴 = 1 ) → ( 𝐴 ↑ 𝑁 ) = 𝐴 ) )
42	29 41	impbid	⊢ ( 𝜑 → ( ( 𝐴 ↑ 𝑁 ) = 𝐴 ↔ ( 𝐴 = 0 ∨ 𝐴 = 1 ) ) )