Theorem msq11

Description: The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	msq11	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 · 𝐴 ) = ( 𝐵 · 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		le2msq	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) ) )
2		le2msq	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) → ( 𝐵 ≤ 𝐴 ↔ ( 𝐵 · 𝐵 ) ≤ ( 𝐴 · 𝐴 ) ) )
3	2	ancoms	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐵 ≤ 𝐴 ↔ ( 𝐵 · 𝐵 ) ≤ ( 𝐴 · 𝐴 ) ) )
4	1 3	anbi12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ↔ ( ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) ∧ ( 𝐵 · 𝐵 ) ≤ ( 𝐴 · 𝐴 ) ) ) )
5		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ )
6		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ )
7	5 6	letri3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) )
8	5 5	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 · 𝐴 ) ∈ ℝ )
9	6 6	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐵 · 𝐵 ) ∈ ℝ )
10	8 9	letri3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 · 𝐴 ) = ( 𝐵 · 𝐵 ) ↔ ( ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) ∧ ( 𝐵 · 𝐵 ) ≤ ( 𝐴 · 𝐴 ) ) ) )
11	4 7 10	3bitr4rd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 · 𝐴 ) = ( 𝐵 · 𝐵 ) ↔ 𝐴 = 𝐵 ) )