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	$$⊢\left(N\in {\mathbb{N}}_0\wedge N^2=1\right)\to N=1$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge N^2=1\right)\to N^2=1$$
2	1	fveq2d	$$⊢\left(N\in {\mathbb{N}}_0\wedge N^2=1\right)\to \sqrt{N^2}=\sqrt{1}$$
3		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
4		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
5		sqrtsq	$$⊢\left(N\in ℝ\wedge 0\le N\right)\to \sqrt{N^2}=N$$
6	3 4 5	syl2anc	$$⊢N\in {\mathbb{N}}_0\to \sqrt{N^2}=N$$
7	6	adantr	$$⊢\left(N\in {\mathbb{N}}_0\wedge N^2=1\right)\to \sqrt{N^2}=N$$
8		sqrt1	$$⊢\sqrt{1}=1$$
9	8	a1i	$$⊢\left(N\in {\mathbb{N}}_0\wedge N^2=1\right)\to \sqrt{1}=1$$
10	2 7 9	3eqtr3d	$$⊢\left(N\in {\mathbb{N}}_0\wedge N^2=1\right)\to N=1$$