Theorem sq11i

Description: The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999)

	Ref	Expression
Hypotheses	resqcl.1	|- A e. RR
	lt2sq.2	|- B e. RR
Assertion	sq11i	|- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		resqcl.1	|- A e. RR
2		lt2sq.2	|- B e. RR
3	1	recni	|- A e. CC
4	3	sqvali	|- ( A ^ 2 ) = ( A x. A )
5	2	recni	|- B e. CC
6	5	sqvali	|- ( B ^ 2 ) = ( B x. B )
7	4 6	eqeq12i	|- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A x. A ) = ( B x. B ) )
8	1 2	msq11i	|- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( A x. A ) = ( B x. B ) <-> A = B ) )
9	7 8	bitrid	|- ( ( 0 <_ A /\ 0 <_ B ) -> ( ( A ^ 2 ) = ( B ^ 2 ) <-> A = B ) )