Metamath Proof Explorer


Theorem lt2msqi

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

Ref Expression
Hypotheses ltplus1.1 A
prodgt0.2 B
Assertion lt2msqi 0 A 0 B A < B A A < B B

Proof

Step Hyp Ref Expression
1 ltplus1.1 A
2 prodgt0.2 B
3 lt2msq A 0 A B 0 B A < B A A < B B
4 2 3 mpanr1 A 0 A 0 B A < B A A < B B
5 1 4 mpanl1 0 A 0 B A < B A A < B B