Metamath Proof Explorer

Theorem le2msq

Description: The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion le2msq ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A≤B↔A⁢A≤B⁢B

Proof

Step Hyp Ref Expression
1 lt2msq ⊢B∈ℝ∧0≤B∧A∈ℝ∧0≤A→B<A↔B⁢B<A⁢A
2 1 ancoms ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→B<A↔B⁢B<A⁢A
3 2 notbid ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→¬B<A↔¬B⁢B<A⁢A
4 simpll ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A∈ℝ
5 simprl ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→B∈ℝ
6 4 5 lenltd ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A≤B↔¬B<A
7 4 4 remulcld ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A⁢A∈ℝ
8 5 5 remulcld ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→B⁢B∈ℝ
9 7 8 lenltd ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A⁢A≤B⁢B↔¬B⁢B<A⁢A
10 3 6 9 3bitr4d ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A≤B↔A⁢A≤B⁢B