This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )