Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
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 ) )