Step | Hyp | Ref
| Expression |
1 | | lt2msq1 12047 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ โง ๐ด < ๐ต) โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต)) |
2 | 1 | 3expia 1122 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) |
3 | 2 | adantrr 716 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) |
4 | | id 22 |
. . . . . . 7
โข (๐ด = ๐ต โ ๐ด = ๐ต) |
5 | 4, 4 | oveq12d 7379 |
. . . . . 6
โข (๐ด = ๐ต โ (๐ด ยท ๐ด) = (๐ต ยท ๐ต)) |
6 | 5 | a1i 11 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด = ๐ต โ (๐ด ยท ๐ด) = (๐ต ยท ๐ต))) |
7 | | lt2msq1 12047 |
. . . . . . . 8
โข (((๐ต โ โ โง 0 โค
๐ต) โง ๐ด โ โ โง ๐ต < ๐ด) โ (๐ต ยท ๐ต) < (๐ด ยท ๐ด)) |
8 | 7 | 3expia 1122 |
. . . . . . 7
โข (((๐ต โ โ โง 0 โค
๐ต) โง ๐ด โ โ) โ (๐ต < ๐ด โ (๐ต ยท ๐ต) < (๐ด ยท ๐ด))) |
9 | 8 | adantrr 716 |
. . . . . 6
โข (((๐ต โ โ โง 0 โค
๐ต) โง (๐ด โ โ โง 0 โค ๐ด)) โ (๐ต < ๐ด โ (๐ต ยท ๐ต) < (๐ด ยท ๐ด))) |
10 | 9 | ancoms 460 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต < ๐ด โ (๐ต ยท ๐ต) < (๐ด ยท ๐ด))) |
11 | 6, 10 | orim12d 964 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด = ๐ต โจ ๐ต < ๐ด) โ ((๐ด ยท ๐ด) = (๐ต ยท ๐ต) โจ (๐ต ยท ๐ต) < (๐ด ยท ๐ด)))) |
12 | 11 | con3d 152 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (ยฌ ((๐ด ยท ๐ด) = (๐ต ยท ๐ต) โจ (๐ต ยท ๐ต) < (๐ด ยท ๐ด)) โ ยฌ (๐ด = ๐ต โจ ๐ต < ๐ด))) |
13 | | simpll 766 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
14 | 13, 13 | remulcld 11193 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด ยท ๐ด) โ โ) |
15 | | simprl 770 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
16 | 15, 15 | remulcld 11193 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต ยท ๐ต) โ โ) |
17 | 14, 16 | lttrid 11301 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) < (๐ต ยท ๐ต) โ ยฌ ((๐ด ยท ๐ด) = (๐ต ยท ๐ต) โจ (๐ต ยท ๐ต) < (๐ด ยท ๐ด)))) |
18 | 13, 15 | lttrid 11301 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต < ๐ด))) |
19 | 12, 17, 18 | 3imtr4d 294 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) < (๐ต ยท ๐ต) โ ๐ด < ๐ต)) |
20 | 3, 19 | impbid 211 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) |