Metamath Proof Explorer

Theorem le2sq2

Description: The square function is nondecreasing on the nonnegative reals. (Contributed by NM, 21-Mar-2008)

Ref Expression
Assertion le2sq2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) )

Proof

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