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

Metamath Proof Explorer

Theorem nn0sqeq1

Description: A natural number with square one is equal to one. (Contributed by Thierry Arnoux, 2-Feb-2020) (Proof shortened by Thierry Arnoux, 6-Jun-2023)

Ref Expression
Assertion nn0sqeq1 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 ↑ 2 ) = 1 ) → 𝑁 = 1 )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 ↑ 2 ) = 1 ) → ( 𝑁 ↑ 2 ) = 1 )
2 1 fveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 ↑ 2 ) = 1 ) → ( √ ‘ ( 𝑁 ↑ 2 ) ) = ( √ ‘ 1 ) )
3 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
4 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
5 sqrtsq ⊢ ( ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) → ( √ ‘ ( 𝑁 ↑ 2 ) ) = 𝑁 )
6 3 4 5 syl2anc ⊢ ( 𝑁 ∈ ℕ0 → ( √ ‘ ( 𝑁 ↑ 2 ) ) = 𝑁 )
7 6 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 ↑ 2 ) = 1 ) → ( √ ‘ ( 𝑁 ↑ 2 ) ) = 𝑁 )
8 sqrt1 ⊢ ( √ ‘ 1 ) = 1
9 8 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 ↑ 2 ) = 1 ) → ( √ ‘ 1 ) = 1 )
10 2 7 9 3eqtr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 ↑ 2 ) = 1 ) → 𝑁 = 1 )