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 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) ) |
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 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐴 ) < ( 𝐵 · 𝐵 ) ) ) |