Metamath Proof Explorer

Theorem nn0sq11

Description: The square function is one-to-one for nonnegative integers. (Contributed by AV, 25-Jun-2023)

Ref Expression
Assertion nn0sq11 
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( A e. NN0 -> A e. RR )
2 nn0ge0 
 |-  ( A e. NN0 -> 0 <_ A )
3 1 2 jca 
 |-  ( A e. NN0 -> ( A e. RR /\ 0 <_ A ) )
4 nn0re 
 |-  ( B e. NN0 -> B e. RR )
5 nn0ge0 
 |-  ( B e. NN0 -> 0 <_ B )
6 4 5 jca 
 |-  ( B e. NN0 -> ( B e. RR /\ 0 <_ B ) )
7 sq11 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> A = B ) )
8 3 6 7 syl2an 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> A = B ) )