Description: The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | lt2sq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lt2msq | |
|
2 | recn | |
|
3 | recn | |
|
4 | sqval | |
|
5 | sqval | |
|
6 | 4 5 | breqan12d | |
7 | 2 3 6 | syl2an | |
8 | 7 | ad2ant2r | |
9 | 1 8 | bitr4d | |