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	|- ( ( N e. NN0 /\ ( N ^ 2 ) = 1 ) -> N = 1 )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( N e. NN0 /\ ( N ^ 2 ) = 1 ) -> ( N ^ 2 ) = 1 )
2	1	fveq2d	|- ( ( N e. NN0 /\ ( N ^ 2 ) = 1 ) -> ( sqrt ` ( N ^ 2 ) ) = ( sqrt ` 1 ) )
3		nn0re	|- ( N e. NN0 -> N e. RR )
4		nn0ge0	|- ( N e. NN0 -> 0 <_ N )
5		sqrtsq	|- ( ( N e. RR /\ 0 <_ N ) -> ( sqrt ` ( N ^ 2 ) ) = N )
6	3 4 5	syl2anc	|- ( N e. NN0 -> ( sqrt ` ( N ^ 2 ) ) = N )
7	6	adantr	|- ( ( N e. NN0 /\ ( N ^ 2 ) = 1 ) -> ( sqrt ` ( N ^ 2 ) ) = N )
8		sqrt1	|- ( sqrt ` 1 ) = 1
9	8	a1i	|- ( ( N e. NN0 /\ ( N ^ 2 ) = 1 ) -> ( sqrt ` 1 ) = 1 )
10	2 7 9	3eqtr3d	|- ( ( N e. NN0 /\ ( N ^ 2 ) = 1 ) -> N = 1 )