Step | Hyp | Ref
| Expression |
1 | | lt2msq1 8841 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ โง ๐ด < ๐ต) โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต)) |
2 | 1 | 3expia 1205 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) |
3 | 2 | adantrr 479 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) |
4 | | simpr 110 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต โ โ โง 0 โค ๐ต)) |
5 | | simpll 527 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
6 | | lt2msq1 8841 |
. . . . . . . 8
โข (((๐ต โ โ โง 0 โค
๐ต) โง ๐ด โ โ โง ๐ต < ๐ด) โ (๐ต ยท ๐ต) < (๐ด ยท ๐ด)) |
7 | 6 | 3expia 1205 |
. . . . . . 7
โข (((๐ต โ โ โง 0 โค
๐ต) โง ๐ด โ โ) โ (๐ต < ๐ด โ (๐ต ยท ๐ต) < (๐ด ยท ๐ด))) |
8 | 4, 5, 7 | syl2anc 411 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต < ๐ด โ (๐ต ยท ๐ต) < (๐ด ยท ๐ด))) |
9 | 8 | con3d 631 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (ยฌ (๐ต ยท ๐ต) < (๐ด ยท ๐ด) โ ยฌ ๐ต < ๐ด)) |
10 | 5, 5 | remulcld 7987 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด ยท ๐ด) โ โ) |
11 | | simprl 529 |
. . . . . . 7
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
12 | 11, 11 | remulcld 7987 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ต ยท ๐ต) โ โ) |
13 | 10, 12 | lenltd 8074 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) โค (๐ต ยท ๐ต) โ ยฌ (๐ต ยท ๐ต) < (๐ด ยท ๐ด))) |
14 | 5, 11 | lenltd 8074 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด โค ๐ต โ ยฌ ๐ต < ๐ด)) |
15 | 9, 13, 14 | 3imtr4d 203 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) โค (๐ต ยท ๐ต) โ ๐ด โค ๐ต)) |
16 | 5 | recnd 7985 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โ โ) |
17 | 11 | recnd 7985 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ต โ โ) |
18 | | mulext 8570 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ โ) โง (๐ต โ โ โง ๐ต โ โ)) โ ((๐ด ยท ๐ด) # (๐ต ยท ๐ต) โ (๐ด # ๐ต โจ ๐ด # ๐ต))) |
19 | 16, 16, 17, 17, 18 | syl22anc 1239 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) # (๐ต ยท ๐ต) โ (๐ด # ๐ต โจ ๐ด # ๐ต))) |
20 | | oridm 757 |
. . . . 5
โข ((๐ด # ๐ต โจ ๐ด # ๐ต) โ ๐ด # ๐ต) |
21 | 19, 20 | imbitrdi 161 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) # (๐ต ยท ๐ต) โ ๐ด # ๐ต)) |
22 | 15, 21 | anim12d 335 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (((๐ด ยท ๐ด) โค (๐ต ยท ๐ต) โง (๐ด ยท ๐ด) # (๐ต ยท ๐ต)) โ (๐ด โค ๐ต โง ๐ด # ๐ต))) |
23 | | ltleap 8588 |
. . . 4
โข (((๐ด ยท ๐ด) โ โ โง (๐ต ยท ๐ต) โ โ) โ ((๐ด ยท ๐ด) < (๐ต ยท ๐ต) โ ((๐ด ยท ๐ด) โค (๐ต ยท ๐ต) โง (๐ด ยท ๐ด) # (๐ต ยท ๐ต)))) |
24 | 10, 12, 23 | syl2anc 411 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) < (๐ต ยท ๐ต) โ ((๐ด ยท ๐ด) โค (๐ต ยท ๐ต) โง (๐ด ยท ๐ด) # (๐ต ยท ๐ต)))) |
25 | | ltleap 8588 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ (๐ด โค ๐ต โง ๐ด # ๐ต))) |
26 | 5, 11, 25 | syl2anc 411 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (๐ด โค ๐ต โง ๐ด # ๐ต))) |
27 | 22, 24, 26 | 3imtr4d 203 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ด ยท ๐ด) < (๐ต ยท ๐ต) โ ๐ด < ๐ต)) |
28 | 3, 27 | impbid 129 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ด < ๐ต โ (๐ด ยท ๐ด) < (๐ต ยท ๐ต))) |