Theorem sq11i

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

	Ref	Expression
Hypotheses	resqcl.1	⊢ 𝐴 ∈ ℝ
	lt2sq.2	⊢ 𝐵 ∈ ℝ
Assertion	sq11i	⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		resqcl.1	⊢ 𝐴 ∈ ℝ
2		lt2sq.2	⊢ 𝐵 ∈ ℝ
3	1	recni	⊢ 𝐴 ∈ ℂ
4	3	sqvali	⊢ ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 )
5	2	recni	⊢ 𝐵 ∈ ℂ
6	5	sqvali	⊢ ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 )
7	4 6	eqeq12i	⊢ ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( 𝐴 · 𝐴 ) = ( 𝐵 · 𝐵 ) )
8	1 2	msq11i	⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( ( 𝐴 · 𝐴 ) = ( 𝐵 · 𝐵 ) ↔ 𝐴 = 𝐵 ) )
9	7 8	bitrid	⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ 𝐴 = 𝐵 ) )