Description: Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005) (Revised by Mario Carneiro, 27-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | lt2msq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lt2msq1 | |
|
2 | 1 | 3expia | |
3 | 2 | adantrr | |
4 | id | |
|
5 | 4 4 | oveq12d | |
6 | 5 | a1i | |
7 | lt2msq1 | |
|
8 | 7 | 3expia | |
9 | 8 | adantrr | |
10 | 9 | ancoms | |
11 | 6 10 | orim12d | |
12 | 11 | con3d | |
13 | simpll | |
|
14 | 13 13 | remulcld | |
15 | simprl | |
|
16 | 15 15 | remulcld | |
17 | 14 16 | lttrid | |
18 | 13 15 | lttrid | |
19 | 12 17 18 | 3imtr4d | |
20 | 3 19 | impbid | |