Metamath Proof Explorer


Theorem lt2msqi

Description: The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 3-Aug-1999)

Ref Expression
Hypotheses ltplus1.1 𝐴 ∈ ℝ
prodgt0.2 𝐵 ∈ ℝ
Assertion lt2msqi ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ltplus1.1 𝐴 ∈ ℝ
2 prodgt0.2 𝐵 ∈ ℝ
3 lt2msq ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) )
4 2 3 mpanr1 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 0 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) )
5 1 4 mpanl1 ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) )