Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โ
โ) |
2 | | simp3 999 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ถ โ
โ) |
3 | 1, 2 | remulcld 7987 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
4 | | simp2 998 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
5 | 4, 2 | remulcld 7987 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
6 | | reaplt 8544 |
. . 3
โข (((๐ด ยท ๐ถ) โ โ โง (๐ต ยท ๐ถ) โ โ) โ ((๐ด ยท ๐ถ) # (๐ต ยท ๐ถ) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โจ (๐ต ยท ๐ถ) < (๐ด ยท ๐ถ)))) |
7 | 3, 5, 6 | syl2anc 411 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ถ) # (๐ต ยท ๐ถ) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โจ (๐ต ยท ๐ถ) < (๐ด ยท ๐ถ)))) |
8 | | ax-pre-mulext 7928 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ถ) <โ (๐ต ยท ๐ถ) โ (๐ด <โ ๐ต โจ ๐ต <โ ๐ด))) |
9 | | ltxrlt 8022 |
. . . . 5
โข (((๐ด ยท ๐ถ) โ โ โง (๐ต ยท ๐ถ) โ โ) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ) <โ (๐ต ยท ๐ถ))) |
10 | 3, 5, 9 | syl2anc 411 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ) <โ (๐ต ยท ๐ถ))) |
11 | | reaplt 8544 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด # ๐ต โ (๐ด < ๐ต โจ ๐ต < ๐ด))) |
12 | 1, 4, 11 | syl2anc 411 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด # ๐ต โ (๐ด < ๐ต โจ ๐ต < ๐ด))) |
13 | | ltxrlt 8022 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ ๐ด <โ ๐ต)) |
14 | 1, 4, 13 | syl2anc 411 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด < ๐ต โ ๐ด <โ ๐ต)) |
15 | | ltxrlt 8022 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต < ๐ด โ ๐ต <โ ๐ด)) |
16 | 4, 1, 15 | syl2anc 411 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต < ๐ด โ ๐ต <โ ๐ด)) |
17 | 14, 16 | orbi12d 793 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ต โจ ๐ต < ๐ด) โ (๐ด <โ ๐ต โจ ๐ต <โ ๐ด))) |
18 | 12, 17 | bitrd 188 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด # ๐ต โ (๐ด <โ ๐ต โจ ๐ต <โ ๐ด))) |
19 | 8, 10, 18 | 3imtr4d 203 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โ ๐ด # ๐ต)) |
20 | | ax-pre-mulext 7928 |
. . . . 5
โข ((๐ต โ โ โง ๐ด โ โ โง ๐ถ โ โ) โ ((๐ต ยท ๐ถ) <โ (๐ด ยท ๐ถ) โ (๐ต <โ ๐ด โจ ๐ด <โ ๐ต))) |
21 | 20 | 3com12 1207 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต ยท ๐ถ) <โ (๐ด ยท ๐ถ) โ (๐ต <โ ๐ด โจ ๐ด <โ ๐ต))) |
22 | | ltxrlt 8022 |
. . . . 5
โข (((๐ต ยท ๐ถ) โ โ โง (๐ด ยท ๐ถ) โ โ) โ ((๐ต ยท ๐ถ) < (๐ด ยท ๐ถ) โ (๐ต ยท ๐ถ) <โ (๐ด ยท ๐ถ))) |
23 | 5, 3, 22 | syl2anc 411 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต ยท ๐ถ) < (๐ด ยท ๐ถ) โ (๐ต ยท ๐ถ) <โ (๐ด ยท ๐ถ))) |
24 | | orcom 728 |
. . . . 5
โข ((๐ด <โ ๐ต โจ ๐ต <โ ๐ด) โ (๐ต <โ ๐ด โจ ๐ด <โ ๐ต)) |
25 | 18, 24 | bitrdi 196 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด # ๐ต โ (๐ต <โ ๐ด โจ ๐ด <โ ๐ต))) |
26 | 21, 23, 25 | 3imtr4d 203 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ต ยท ๐ถ) < (๐ด ยท ๐ถ) โ ๐ด # ๐ต)) |
27 | 19, 26 | jaod 717 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โจ (๐ต ยท ๐ถ) < (๐ด ยท ๐ถ)) โ ๐ด # ๐ต)) |
28 | 7, 27 | sylbid 150 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ถ) # (๐ต ยท ๐ถ) โ ๐ด # ๐ต)) |