Metamath Proof Explorer


Theorem lt2sqi

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

Ref Expression
Hypotheses resqcl.1 A
lt2sq.2 B
Assertion lt2sqi 0 A 0 B A < B A 2 < B 2

Proof

Step Hyp Ref Expression
1 resqcl.1 A
2 lt2sq.2 B
3 1 2 lt2msqi 0 A 0 B A < B A A < B B
4 1 recni A
5 4 sqvali A 2 = A A
6 2 recni B
7 6 sqvali B 2 = B B
8 5 7 breq12i A 2 < B 2 A A < B B
9 3 8 bitr4di 0 A 0 B A < B A 2 < B 2