Step | Hyp | Ref
| Expression |
1 | | 0re 7956 |
. . . . 5
โข 0 โ
โ |
2 | | reaplt 8544 |
. . . . 5
โข ((๐ถ โ โ โง 0 โ
โ) โ (๐ถ # 0
โ (๐ถ < 0 โจ 0
< ๐ถ))) |
3 | 1, 2 | mpan2 425 |
. . . 4
โข (๐ถ โ โ โ (๐ถ # 0 โ (๐ถ < 0 โจ 0 < ๐ถ))) |
4 | 3 | pm5.32i 454 |
. . 3
โข ((๐ถ โ โ โง ๐ถ # 0) โ (๐ถ โ โ โง (๐ถ < 0 โจ 0 < ๐ถ))) |
5 | | simp1 997 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ๐ด โ
โ) |
6 | 5 | recnd 7985 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ๐ด โ
โ) |
7 | | simp3l 1025 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ๐ถ โ
โ) |
8 | 7 | recnd 7985 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ๐ถ โ
โ) |
9 | 6, 8 | mulneg2d 8368 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (๐ด ยท -๐ถ) = -(๐ด ยท ๐ถ)) |
10 | | simp2 998 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ๐ต โ
โ) |
11 | 10 | recnd 7985 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ๐ต โ
โ) |
12 | 11, 8 | mulneg2d 8368 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (๐ต ยท -๐ถ) = -(๐ต ยท ๐ถ)) |
13 | 9, 12 | breq12d 4016 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ((๐ด ยท -๐ถ) # (๐ต ยท -๐ถ) โ -(๐ด ยท ๐ถ) # -(๐ต ยท ๐ถ))) |
14 | 7 | renegcld 8336 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ -๐ถ โ
โ) |
15 | | simp3r 1026 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ๐ถ < 0) |
16 | 7 | lt0neg1d 8471 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (๐ถ < 0 โ 0 < -๐ถ)) |
17 | 15, 16 | mpbid 147 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ 0 < -๐ถ) |
18 | | reapmul1lem 8550 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (-๐ถ โ โ โง 0 <
-๐ถ)) โ (๐ด # ๐ต โ (๐ด ยท -๐ถ) # (๐ต ยท -๐ถ))) |
19 | 5, 10, 14, 17, 18 | syl112anc 1242 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (๐ด # ๐ต โ (๐ด ยท -๐ถ) # (๐ต ยท -๐ถ))) |
20 | 5, 7 | remulcld 7987 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (๐ด ยท ๐ถ) โ โ) |
21 | 10, 7 | remulcld 7987 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (๐ต ยท ๐ถ) โ โ) |
22 | 20, 21 | ltnegd 8479 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โ -(๐ต ยท ๐ถ) < -(๐ด ยท ๐ถ))) |
23 | 21, 20 | ltnegd 8479 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ((๐ต ยท ๐ถ) < (๐ด ยท ๐ถ) โ -(๐ด ยท ๐ถ) < -(๐ต ยท ๐ถ))) |
24 | 22, 23 | orbi12d 793 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โจ (๐ต ยท ๐ถ) < (๐ด ยท ๐ถ)) โ (-(๐ต ยท ๐ถ) < -(๐ด ยท ๐ถ) โจ -(๐ด ยท ๐ถ) < -(๐ต ยท ๐ถ)))) |
25 | | reaplt 8544 |
. . . . . . . . . 10
โข (((๐ด ยท ๐ถ) โ โ โง (๐ต ยท ๐ถ) โ โ) โ ((๐ด ยท ๐ถ) # (๐ต ยท ๐ถ) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โจ (๐ต ยท ๐ถ) < (๐ด ยท ๐ถ)))) |
26 | 20, 21, 25 | syl2anc 411 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ((๐ด ยท ๐ถ) # (๐ต ยท ๐ถ) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โจ (๐ต ยท ๐ถ) < (๐ด ยท ๐ถ)))) |
27 | 20 | renegcld 8336 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ -(๐ด ยท ๐ถ) โ โ) |
28 | 21 | renegcld 8336 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ -(๐ต ยท ๐ถ) โ โ) |
29 | | reaplt 8544 |
. . . . . . . . . . 11
โข ((-(๐ด ยท ๐ถ) โ โ โง -(๐ต ยท ๐ถ) โ โ) โ (-(๐ด ยท ๐ถ) # -(๐ต ยท ๐ถ) โ (-(๐ด ยท ๐ถ) < -(๐ต ยท ๐ถ) โจ -(๐ต ยท ๐ถ) < -(๐ด ยท ๐ถ)))) |
30 | 27, 28, 29 | syl2anc 411 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (-(๐ด ยท ๐ถ) # -(๐ต ยท ๐ถ) โ (-(๐ด ยท ๐ถ) < -(๐ต ยท ๐ถ) โจ -(๐ต ยท ๐ถ) < -(๐ด ยท ๐ถ)))) |
31 | | orcom 728 |
. . . . . . . . . 10
โข ((-(๐ด ยท ๐ถ) < -(๐ต ยท ๐ถ) โจ -(๐ต ยท ๐ถ) < -(๐ด ยท ๐ถ)) โ (-(๐ต ยท ๐ถ) < -(๐ด ยท ๐ถ) โจ -(๐ด ยท ๐ถ) < -(๐ต ยท ๐ถ))) |
32 | 30, 31 | bitrdi 196 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (-(๐ด ยท ๐ถ) # -(๐ต ยท ๐ถ) โ (-(๐ต ยท ๐ถ) < -(๐ด ยท ๐ถ) โจ -(๐ด ยท ๐ถ) < -(๐ต ยท ๐ถ)))) |
33 | 24, 26, 32 | 3bitr4d 220 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ ((๐ด ยท ๐ถ) # (๐ต ยท ๐ถ) โ -(๐ด ยท ๐ถ) # -(๐ต ยท ๐ถ))) |
34 | 13, 19, 33 | 3bitr4d 220 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ < 0)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
35 | 34 | 3expa 1203 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ถ < 0)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
36 | 35 | anassrs 400 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โง ๐ถ < 0) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
37 | | reapmul1lem 8550 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
38 | 37 | 3expa 1203 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง 0 <
๐ถ)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
39 | 38 | anassrs 400 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โง 0 <
๐ถ) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
40 | 36, 39 | jaodan 797 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โง (๐ถ < 0 โจ 0 < ๐ถ)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
41 | 40 | anasss 399 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง (๐ถ < 0 โจ 0 < ๐ถ))) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
42 | 4, 41 | sylan2b 287 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |
43 | 42 | 3impa 1194 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ # 0)) โ (๐ด # ๐ต โ (๐ด ยท ๐ถ) # (๐ต ยท ๐ถ))) |