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 A
lt2sq.2 B
Assertion le2sqi 0A0BABA2B2

Proof

Step Hyp Ref Expression
1 resqcl.1 A
2 lt2sq.2 B
3 1 2 le2msqi 0A0BABAABB
4 1 recni A
5 4 sqvali A2=AA
6 2 recni B
7 6 sqvali B2=BB
8 5 7 breq12i A2B2AABB
9 3 8 bitr4di 0A0BABA2B2