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 )