Metamath Proof Explorer


Theorem lt2sq

Description: The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006)

Ref Expression
Assertion lt2sq A0AB0BA<BA2<B2

Proof

Step Hyp Ref Expression
1 lt2msq A0AB0BA<BAA<BB
2 recn AA
3 recn BB
4 sqval AA2=AA
5 sqval BB2=BB
6 4 5 breqan12d ABA2<B2AA<BB
7 2 3 6 syl2an ABA2<B2AA<BB
8 7 ad2ant2r A0AB0BA2<B2AA<BB
9 1 8 bitr4d A0AB0BA<BA2<B2