Metamath Proof Explorer

Theorem le2sq2

Description: The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008)

Ref Expression
Assertion le2sq2 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ A ≤ B → A 2 ≤ B 2

Proof

Step Hyp Ref Expression
1 simprr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B
2 simprl ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℝ
3 0re ⊢ 0 ∈ ℝ
4 letr ⊢ 0 ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ∧ A ≤ B → 0 ≤ B
5 3 4 mp3an1 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ∧ A ≤ B → 0 ≤ B
6 5 exp4b ⊢ A ∈ ℝ → B ∈ ℝ → 0 ≤ A → A ≤ B → 0 ≤ B
7 6 com23 ⊢ A ∈ ℝ → 0 ≤ A → B ∈ ℝ → A ≤ B → 0 ≤ B
8 7 imp43 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ A ≤ B → 0 ≤ B
9 2 8 jca ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℝ ∧ 0 ≤ B
10 le2sq ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ A 2 ≤ B 2
11 9 10 syldan ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B ↔ A 2 ≤ B 2
12 1 11 mpbid ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ A ≤ B → A 2 ≤ B 2