Step |
Hyp |
Ref |
Expression |
1 |
|
resqcl.1 |
โข ๐ด โ โ |
2 |
|
lt2sq.2 |
โข ๐ต โ โ |
3 |
1 2
|
le2msqi |
โข ( ( 0 โค ๐ด โง 0 โค ๐ต ) โ ( ๐ด โค ๐ต โ ( ๐ด ยท ๐ด ) โค ( ๐ต ยท ๐ต ) ) ) |
4 |
1
|
recni |
โข ๐ด โ โ |
5 |
4
|
sqvali |
โข ( ๐ด โ 2 ) = ( ๐ด ยท ๐ด ) |
6 |
2
|
recni |
โข ๐ต โ โ |
7 |
6
|
sqvali |
โข ( ๐ต โ 2 ) = ( ๐ต ยท ๐ต ) |
8 |
5 7
|
breq12i |
โข ( ( ๐ด โ 2 ) โค ( ๐ต โ 2 ) โ ( ๐ด ยท ๐ด ) โค ( ๐ต ยท ๐ต ) ) |
9 |
3 8
|
bitr4di |
โข ( ( 0 โค ๐ด โง 0 โค ๐ต ) โ ( ๐ด โค ๐ต โ ( ๐ด โ 2 ) โค ( ๐ต โ 2 ) ) ) |