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 N0N2=1N=1

Proof

Step Hyp Ref Expression
1 simpr N0N2=1N2=1
2 1 fveq2d N0N2=1N2=1
3 nn0re N0N
4 nn0ge0 N00N
5 sqrtsq N0NN2=N
6 3 4 5 syl2anc N0N2=N
7 6 adantr N0N2=1N2=N
8 sqrt1 1=1
9 8 a1i N0N2=11=1
10 2 7 9 3eqtr3d N0N2=1N=1