Step | Hyp | Ref
| Expression |
1 | | 0xr 11207 |
. . . . . 6
โข 0 โ
โ* |
2 | | simpr 486 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ ๐ถ โ
โ*) |
3 | | xrleloe 13069 |
. . . . . 6
โข ((0
โ โ* โง ๐ถ โ โ*) โ (0 โค
๐ถ โ (0 < ๐ถ โจ 0 = ๐ถ))) |
4 | 1, 2, 3 | sylancr 588 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (0 โค
๐ถ โ (0 < ๐ถ โจ 0 = ๐ถ))) |
5 | | simpllr 775 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ๐ถ โ
โ*) |
6 | | elxr 13042 |
. . . . . . . . . . . 12
โข (๐ถ โ โ*
โ (๐ถ โ โ
โจ ๐ถ = +โ โจ
๐ถ =
-โ)) |
7 | 5, 6 | sylib 217 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ถ โ โ โจ ๐ถ = +โ โจ ๐ถ = -โ)) |
8 | | simplrr 777 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ ๐ด โค ๐ต) |
9 | | simprll 778 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ ๐ด โ โ) |
10 | | simprlr 779 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ ๐ต โ โ) |
11 | | simprr 772 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ ๐ถ โ โ) |
12 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ 0 < ๐ถ) |
13 | | lemul1 12012 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) |
14 | 9, 10, 11, 12, 13 | syl112anc 1375 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ (๐ด โค ๐ต โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) |
15 | 8, 14 | mpbid 231 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) |
16 | | rexmul 13196 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ)) |
17 | 9, 11, 16 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ)) |
18 | | rexmul 13196 |
. . . . . . . . . . . . . . 15
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยทe ๐ถ) = (๐ต ยท ๐ถ)) |
19 | 10, 11, 18 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ (๐ต ยทe ๐ถ) = (๐ต ยท ๐ถ)) |
20 | 15, 17, 19 | 3brtr4d 5138 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ)) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
21 | 20 | expr 458 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ถ โ โ โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |
22 | | simprl 770 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ๐ด โ โ) |
23 | | 0re 11162 |
. . . . . . . . . . . . . . 15
โข 0 โ
โ |
24 | | lttri4 11244 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ โง 0 โ
โ) โ (๐ด < 0
โจ ๐ด = 0 โจ 0 <
๐ด)) |
25 | 22, 23, 24 | sylancl 587 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ด < 0 โจ ๐ด = 0 โจ 0 < ๐ด)) |
26 | | simplll 774 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โ ๐ด โ
โ*) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ๐ด โ
โ*) |
28 | | xmulpnf1n 13203 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ*
โง ๐ด < 0) โ
(๐ด ยทe
+โ) = -โ) |
29 | 27, 28 | sylan 581 |
. . . . . . . . . . . . . . . . 17
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด < 0) โ (๐ด ยทe +โ) =
-โ) |
30 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โ ๐ต โ
โ*) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ๐ต โ
โ*) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด < 0) โ ๐ต โ
โ*) |
33 | | pnfxr 11214 |
. . . . . . . . . . . . . . . . . . 19
โข +โ
โ โ* |
34 | | xmulcl 13198 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ต โ โ*
โง +โ โ โ*) โ (๐ต ยทe +โ) โ
โ*) |
35 | 32, 33, 34 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด < 0) โ (๐ต ยทe +โ) โ
โ*) |
36 | | mnfle 13060 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ต ยทe +โ)
โ โ* โ -โ โค (๐ต ยทe
+โ)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด < 0) โ -โ โค (๐ต ยทe
+โ)) |
38 | 29, 37 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด < 0) โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ)) |
39 | 38 | ex 414 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ด < 0 โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ))) |
40 | | oveq1 7365 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด = 0 โ (๐ด ยทe +โ) = (0
ยทe +โ)) |
41 | | xmul02 13193 |
. . . . . . . . . . . . . . . . . . . 20
โข (+โ
โ โ* โ (0 ยทe +โ) =
0) |
42 | 33, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
โข (0
ยทe +โ) = 0 |
43 | 40, 42 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด = 0 โ (๐ด ยทe +โ) =
0) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด = 0) โ (๐ด ยทe +โ) =
0) |
45 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ๐ด โค ๐ต) |
46 | | breq1 5109 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ด = 0 โ (๐ด โค ๐ต โ 0 โค ๐ต)) |
47 | 45, 46 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ด = 0 โ 0 โค ๐ต)) |
48 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ๐ต โ โ) |
49 | | leloe 11246 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((0
โ โ โง ๐ต
โ โ) โ (0 โค ๐ต โ (0 < ๐ต โจ 0 = ๐ต))) |
50 | 23, 48, 49 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (0 โค ๐ต โ (0 < ๐ต โจ 0 = ๐ต))) |
51 | 47, 50 | sylibd 238 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ด = 0 โ (0 < ๐ต โจ 0 = ๐ต))) |
52 | 51 | imp 408 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด = 0) โ (0 < ๐ต โจ 0 = ๐ต)) |
53 | | pnfge 13056 |
. . . . . . . . . . . . . . . . . . . . 21
โข (0 โ
โ* โ 0 โค +โ) |
54 | 1, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 โค
+โ |
55 | | xmulpnf1 13199 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต โ โ*
โง 0 < ๐ต) โ
(๐ต ยทe
+โ) = +โ) |
56 | 31, 55 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง 0 < ๐ต) โ (๐ต ยทe +โ) =
+โ) |
57 | 54, 56 | breqtrrid 5144 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง 0 < ๐ต) โ 0 โค (๐ต ยทe
+โ)) |
58 | | xrleid 13076 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (0 โ
โ* โ 0 โค 0) |
59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
โข 0 โค
0 |
60 | 59, 42 | breqtrri 5133 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 โค (0
ยทe +โ) |
61 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง 0 = ๐ต) โ 0 = ๐ต) |
62 | 61 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง 0 = ๐ต) โ (0 ยทe
+โ) = (๐ต
ยทe +โ)) |
63 | 60, 62 | breqtrid 5143 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง 0 = ๐ต) โ 0 โค (๐ต ยทe
+โ)) |
64 | 57, 63 | jaodan 957 |
. . . . . . . . . . . . . . . . . 18
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง (0 < ๐ต โจ 0 = ๐ต)) โ 0 โค (๐ต ยทe
+โ)) |
65 | 52, 64 | syldan 592 |
. . . . . . . . . . . . . . . . 17
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด = 0) โ 0 โค (๐ต ยทe
+โ)) |
66 | 44, 65 | eqbrtrd 5128 |
. . . . . . . . . . . . . . . 16
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ด = 0) โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ)) |
67 | 66 | ex 414 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ด = 0 โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ))) |
68 | | pnfge 13056 |
. . . . . . . . . . . . . . . . . 18
โข (+โ
โ โ* โ +โ โค +โ) |
69 | 33, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข +โ
โค +โ |
70 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง 0 < ๐ด)) โ ๐ด โ
โ*) |
71 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง 0 < ๐ด)) โ 0 < ๐ด) |
72 | | xmulpnf1 13199 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = +โ) |
73 | 70, 71, 72 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง 0 < ๐ด)) โ (๐ด ยทe +โ) =
+โ) |
74 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง 0 < ๐ด)) โ ๐ต โ
โ*) |
75 | | ltletr 11252 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((0
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ ((0 < ๐ด โง ๐ด โค ๐ต) โ 0 < ๐ต)) |
76 | 23, 75 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 <
๐ด โง ๐ด โค ๐ต) โ 0 < ๐ต)) |
77 | 76 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ((0 < ๐ด โง ๐ด โค ๐ต) โ 0 < ๐ต)) |
78 | 45, 77 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (0 < ๐ด โ 0 < ๐ต)) |
79 | 78 | impr 456 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง 0 < ๐ด)) โ 0 < ๐ต) |
80 | 74, 79, 55 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง 0 < ๐ด)) โ (๐ต ยทe +โ) =
+โ) |
81 | 73, 80 | breq12d 5119 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง 0 < ๐ด)) โ ((๐ด ยทe +โ) โค (๐ต ยทe +โ)
โ +โ โค +โ)) |
82 | 69, 81 | mpbiri 258 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ((๐ด โ โ โง ๐ต โ โ) โง 0 < ๐ด)) โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ)) |
83 | 82 | expr 458 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (0 < ๐ด โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ))) |
84 | 39, 67, 83 | 3jaod 1429 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ((๐ด < 0 โจ ๐ด = 0 โจ 0 < ๐ด) โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ))) |
85 | 25, 84 | mpd 15 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ)) |
86 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ถ = +โ โ (๐ด ยทe ๐ถ) = (๐ด ยทe
+โ)) |
87 | | oveq2 7366 |
. . . . . . . . . . . . . 14
โข (๐ถ = +โ โ (๐ต ยทe ๐ถ) = (๐ต ยทe
+โ)) |
88 | 86, 87 | breq12d 5119 |
. . . . . . . . . . . . 13
โข (๐ถ = +โ โ ((๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ) โ (๐ด ยทe +โ) โค (๐ต ยทe
+โ))) |
89 | 85, 88 | syl5ibrcom 247 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ถ = +โ โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |
90 | | nltmnf 13055 |
. . . . . . . . . . . . . . . . . 18
โข (0 โ
โ* โ ยฌ 0 < -โ) |
91 | 1, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข ยฌ 0
< -โ |
92 | | breq2 5110 |
. . . . . . . . . . . . . . . . 17
โข (๐ถ = -โ โ (0 < ๐ถ โ 0 <
-โ)) |
93 | 91, 92 | mtbiri 327 |
. . . . . . . . . . . . . . . 16
โข (๐ถ = -โ โ ยฌ 0 <
๐ถ) |
94 | 93 | con2i 139 |
. . . . . . . . . . . . . . 15
โข (0 <
๐ถ โ ยฌ ๐ถ = -โ) |
95 | 94 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โ ยฌ ๐ถ = -โ) |
96 | 95 | adantr 482 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ยฌ ๐ถ = -โ) |
97 | 96 | pm2.21d 121 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ถ = -โ โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |
98 | 21, 89, 97 | 3jaod 1429 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ ((๐ถ โ โ โจ ๐ถ = +โ โจ ๐ถ = -โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |
99 | 7, 98 | mpd 15 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
100 | 99 | anassrs 469 |
. . . . . . . . 9
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด โ โ) โง ๐ต โ โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
101 | | xmulcl 13198 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ*
โง ๐ถ โ
โ*) โ (๐ด ยทe ๐ถ) โ
โ*) |
102 | 101 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (๐ด ยทe ๐ถ) โ
โ*) |
103 | 102 | ad2antrr 725 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = +โ) โ (๐ด ยทe ๐ถ) โ
โ*) |
104 | | pnfge 13056 |
. . . . . . . . . . . 12
โข ((๐ด ยทe ๐ถ) โ โ*
โ (๐ด
ยทe ๐ถ)
โค +โ) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = +โ) โ (๐ด ยทe ๐ถ) โค +โ) |
106 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ต = +โ โ (๐ต ยทe ๐ถ) = (+โ
ยทe ๐ถ)) |
107 | | xmulpnf2 13200 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โ*
โง 0 < ๐ถ) โ
(+โ ยทe ๐ถ) = +โ) |
108 | 107 | ad2ant2lr 747 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โ (+โ ยทe
๐ถ) =
+โ) |
109 | 106, 108 | sylan9eqr 2795 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = +โ) โ (๐ต ยทe ๐ถ) = +โ) |
110 | 105, 109 | breqtrrd 5134 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = +โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
111 | 110 | adantlr 714 |
. . . . . . . . 9
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด โ โ) โง ๐ต = +โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
112 | | simplrr 777 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ ๐ด โค ๐ต) |
113 | | simpr 486 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ ๐ต = -โ) |
114 | 26 | adantr 482 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ ๐ด โ
โ*) |
115 | | mnfle 13060 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ*
โ -โ โค ๐ด) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ -โ โค ๐ด) |
117 | 113, 116 | eqbrtrd 5128 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ ๐ต โค ๐ด) |
118 | | xrletri3 13079 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ๐ต โค ๐ด))) |
119 | 118 | ad3antrrr 729 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ๐ต โค ๐ด))) |
120 | 112, 117,
119 | mpbir2and 712 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ ๐ด = ๐ต) |
121 | 120 | oveq1d 7373 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ (๐ด ยทe ๐ถ) = (๐ต ยทe ๐ถ)) |
122 | | xmulcl 13198 |
. . . . . . . . . . . . . 14
โข ((๐ต โ โ*
โง ๐ถ โ
โ*) โ (๐ต ยทe ๐ถ) โ
โ*) |
123 | 122 | adantll 713 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (๐ต ยทe ๐ถ) โ
โ*) |
124 | 123 | ad2antrr 725 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ (๐ต ยทe ๐ถ) โ
โ*) |
125 | | xrleid 13076 |
. . . . . . . . . . . 12
โข ((๐ต ยทe ๐ถ) โ โ*
โ (๐ต
ยทe ๐ถ)
โค (๐ต
ยทe ๐ถ)) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ (๐ต ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
127 | 121, 126 | eqbrtrd 5128 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ต = -โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
128 | 127 | adantlr 714 |
. . . . . . . . 9
โข
((((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด โ โ) โง ๐ต = -โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
129 | | elxr 13042 |
. . . . . . . . . . 11
โข (๐ต โ โ*
โ (๐ต โ โ
โจ ๐ต = +โ โจ
๐ต =
-โ)) |
130 | 30, 129 | sylib 217 |
. . . . . . . . . 10
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โ (๐ต โ โ โจ ๐ต = +โ โจ ๐ต = -โ)) |
131 | 130 | adantr 482 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด โ โ) โ (๐ต โ โ โจ ๐ต = +โ โจ ๐ต = -โ)) |
132 | 100, 111,
128, 131 | mpjao3dan 1432 |
. . . . . . . 8
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด โ โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
133 | | simplrr 777 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ ๐ด โค ๐ต) |
134 | 30 | adantr 482 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ ๐ต โ
โ*) |
135 | | pnfge 13056 |
. . . . . . . . . . . . 13
โข (๐ต โ โ*
โ ๐ต โค
+โ) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ ๐ต โค +โ) |
137 | | simpr 486 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ ๐ด = +โ) |
138 | 136, 137 | breqtrrd 5134 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ ๐ต โค ๐ด) |
139 | 118 | ad3antrrr 729 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ (๐ด = ๐ต โ (๐ด โค ๐ต โง ๐ต โค ๐ด))) |
140 | 133, 138,
139 | mpbir2and 712 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ ๐ด = ๐ต) |
141 | 140 | oveq1d 7373 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ (๐ด ยทe ๐ถ) = (๐ต ยทe ๐ถ)) |
142 | 123, 125 | syl 17 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (๐ต ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
143 | 142 | ad2antrr 725 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ (๐ต ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
144 | 141, 143 | eqbrtrd 5128 |
. . . . . . . 8
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = +โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
145 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ด = -โ โ (๐ด ยทe ๐ถ) = (-โ
ยทe ๐ถ)) |
146 | | xmulmnf2 13202 |
. . . . . . . . . . 11
โข ((๐ถ โ โ*
โง 0 < ๐ถ) โ
(-โ ยทe ๐ถ) = -โ) |
147 | 146 | ad2ant2lr 747 |
. . . . . . . . . 10
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โ (-โ ยทe
๐ถ) =
-โ) |
148 | 145, 147 | sylan9eqr 2795 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = -โ) โ (๐ด ยทe ๐ถ) = -โ) |
149 | 123 | ad2antrr 725 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = -โ) โ (๐ต ยทe ๐ถ) โ
โ*) |
150 | | mnfle 13060 |
. . . . . . . . . 10
โข ((๐ต ยทe ๐ถ) โ โ*
โ -โ โค (๐ต
ยทe ๐ถ)) |
151 | 149, 150 | syl 17 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = -โ) โ -โ โค (๐ต ยทe ๐ถ)) |
152 | 148, 151 | eqbrtrd 5128 |
. . . . . . . 8
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โง ๐ด = -โ) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
153 | | elxr 13042 |
. . . . . . . . 9
โข (๐ด โ โ*
โ (๐ด โ โ
โจ ๐ด = +โ โจ
๐ด =
-โ)) |
154 | 26, 153 | sylib 217 |
. . . . . . . 8
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โ (๐ด โ โ โจ ๐ด = +โ โจ ๐ด = -โ)) |
155 | 132, 144,
152, 154 | mpjao3dan 1432 |
. . . . . . 7
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โง (0 <
๐ถ โง ๐ด โค ๐ต)) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |
156 | 155 | exp32 422 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (0 <
๐ถ โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)))) |
157 | | xmul01 13192 |
. . . . . . . . . . 11
โข (๐ด โ โ*
โ (๐ด
ยทe 0) = 0) |
158 | 157 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (๐ด ยทe 0) =
0) |
159 | | xmul01 13192 |
. . . . . . . . . . 11
โข (๐ต โ โ*
โ (๐ต
ยทe 0) = 0) |
160 | 159 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (๐ต ยทe 0) =
0) |
161 | 158, 160 | breq12d 5119 |
. . . . . . . . 9
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ ((๐ด ยทe 0) โค
(๐ต ยทe 0)
โ 0 โค 0)) |
162 | 59, 161 | mpbiri 258 |
. . . . . . . 8
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (๐ด ยทe 0) โค
(๐ต ยทe
0)) |
163 | | oveq2 7366 |
. . . . . . . . 9
โข (0 =
๐ถ โ (๐ด ยทe 0) = (๐ด ยทe ๐ถ)) |
164 | | oveq2 7366 |
. . . . . . . . 9
โข (0 =
๐ถ โ (๐ต ยทe 0) = (๐ต ยทe ๐ถ)) |
165 | 163, 164 | breq12d 5119 |
. . . . . . . 8
โข (0 =
๐ถ โ ((๐ด ยทe 0) โค
(๐ต ยทe 0)
โ (๐ด
ยทe ๐ถ)
โค (๐ต
ยทe ๐ถ))) |
166 | 162, 165 | syl5ibcom 244 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (0 =
๐ถ โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |
167 | 166 | a1dd 50 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (0 =
๐ถ โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)))) |
168 | 156, 167 | jaod 858 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ ((0 <
๐ถ โจ 0 = ๐ถ) โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)))) |
169 | 4, 168 | sylbid 239 |
. . . 4
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ๐ถ โ โ*) โ (0 โค
๐ถ โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)))) |
170 | 169 | expimpd 455 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ ((๐ถ โ โ* โง 0 โค
๐ถ) โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)))) |
171 | 170 | 3impia 1118 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ* โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (๐ด โค ๐ต โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ))) |
172 | 171 | imp 408 |
1
โข (((๐ด โ โ*
โง ๐ต โ
โ* โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ด ยทe ๐ถ) โค (๐ต ยทe ๐ถ)) |