Metamath Proof Explorer

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 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ A = B ⁢ B ↔ A = B

Proof

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