Metamath Proof Explorer


Theorem le2sqi

Description: The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999)

Ref Expression
Hypotheses resqcl.1 𝐴 ∈ ℝ
lt2sq.2 𝐵 ∈ ℝ
Assertion le2sqi ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴𝐵 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 resqcl.1 𝐴 ∈ ℝ
2 lt2sq.2 𝐵 ∈ ℝ
3 1 2 le2msqi ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴𝐵 ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) ) )
4 1 recni 𝐴 ∈ ℂ
5 4 sqvali ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 )
6 2 recni 𝐵 ∈ ℂ
7 6 sqvali ( 𝐵 ↑ 2 ) = ( 𝐵 · 𝐵 )
8 5 7 breq12i ( ( 𝐴 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) ↔ ( 𝐴 · 𝐴 ) ≤ ( 𝐵 · 𝐵 ) )
9 3 8 bitr4di ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( 𝐴𝐵 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐵 ↑ 2 ) ) )