Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
โข (๐ โ ( L โ๐ด), ๐ โ ( L โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = (๐ โ ( L โ๐ด), ๐ โ ( L โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
2 | 1 | rnmpo 7542 |
. . . . 5
โข ran
(๐ โ ( L โ๐ด), ๐ โ ( L โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
3 | | fvex 6905 |
. . . . . . 7
โข ( L
โ๐ด) โ
V |
4 | | fvex 6905 |
. . . . . . 7
โข ( L
โ๐ต) โ
V |
5 | 3, 4 | mpoex 8066 |
. . . . . 6
โข (๐ โ ( L โ๐ด), ๐ โ ( L โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V |
6 | 5 | rnex 7903 |
. . . . 5
โข ran
(๐ โ ( L โ๐ด), ๐ โ ( L โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V |
7 | 2, 6 | eqeltrri 2831 |
. . . 4
โข {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ V |
8 | | eqid 2733 |
. . . . . 6
โข (๐ โ ( R โ๐ด), ๐ โ ( R โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) = (๐ โ ( R โ๐ด), ๐ โ ( R โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) |
9 | 8 | rnmpo 7542 |
. . . . 5
โข ran
(๐ โ ( R โ๐ด), ๐ โ ( R โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) = {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} |
10 | | fvex 6905 |
. . . . . . 7
โข ( R
โ๐ด) โ
V |
11 | | fvex 6905 |
. . . . . . 7
โข ( R
โ๐ต) โ
V |
12 | 10, 11 | mpoex 8066 |
. . . . . 6
โข (๐ โ ( R โ๐ด), ๐ โ ( R โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โ V |
13 | 12 | rnex 7903 |
. . . . 5
โข ran
(๐ โ ( R โ๐ด), ๐ โ ( R โ๐ต) โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โ V |
14 | 9, 13 | eqeltrri 2831 |
. . . 4
โข {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} โ V |
15 | 7, 14 | unex 7733 |
. . 3
โข ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ V |
16 | 15 | a1i 11 |
. 2
โข (๐ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ V) |
17 | | eqid 2733 |
. . . . . 6
โข (๐ก โ ( L โ๐ด), ๐ข โ ( R โ๐ต) โฆ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) = (๐ก โ ( L โ๐ด), ๐ข โ ( R โ๐ต) โฆ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) |
18 | 17 | rnmpo 7542 |
. . . . 5
โข ran
(๐ก โ ( L โ๐ด), ๐ข โ ( R โ๐ต) โฆ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) = {๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} |
19 | 3, 11 | mpoex 8066 |
. . . . . 6
โข (๐ก โ ( L โ๐ด), ๐ข โ ( R โ๐ต) โฆ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โ V |
20 | 19 | rnex 7903 |
. . . . 5
โข ran
(๐ก โ ( L โ๐ด), ๐ข โ ( R โ๐ต) โฆ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โ V |
21 | 18, 20 | eqeltrri 2831 |
. . . 4
โข {๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โ V |
22 | | eqid 2733 |
. . . . . 6
โข (๐ฃ โ ( R โ๐ด), ๐ค โ ( L โ๐ต) โฆ (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) = (๐ฃ โ ( R โ๐ด), ๐ค โ ( L โ๐ต) โฆ (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) |
23 | 22 | rnmpo 7542 |
. . . . 5
โข ran
(๐ฃ โ ( R โ๐ด), ๐ค โ ( L โ๐ต) โฆ (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) = {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))} |
24 | 10, 4 | mpoex 8066 |
. . . . . 6
โข (๐ฃ โ ( R โ๐ด), ๐ค โ ( L โ๐ต) โฆ (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) โ V |
25 | 24 | rnex 7903 |
. . . . 5
โข ran
(๐ฃ โ ( R โ๐ด), ๐ค โ ( L โ๐ต) โฆ (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) โ V |
26 | 23, 25 | eqeltrri 2831 |
. . . 4
โข {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))} โ V |
27 | 21, 26 | unex 7733 |
. . 3
โข ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) โ V |
28 | 27 | a1i 11 |
. 2
โข (๐ โ ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) โ V) |
29 | | mulsproplem.1 |
. . . . . . . . . 10
โข (๐ โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
30 | 29 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
31 | | leftssold 27373 |
. . . . . . . . . 10
โข ( L
โ๐ด) โ ( O
โ( bday โ๐ด)) |
32 | | simprl 770 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ ๐ โ ( L โ๐ด)) |
33 | 31, 32 | sselid 3981 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ ๐ โ ( O โ(
bday โ๐ด))) |
34 | | mulsproplem9.2 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ No
) |
35 | 34 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ ๐ต โ No
) |
36 | 30, 33, 35 | mulsproplem2 27573 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (๐ ยทs ๐ต) โ No
) |
37 | | mulsproplem9.1 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ No
) |
38 | 37 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ ๐ด โ No
) |
39 | | leftssold 27373 |
. . . . . . . . . 10
โข ( L
โ๐ต) โ ( O
โ( bday โ๐ต)) |
40 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ ๐ โ ( L โ๐ต)) |
41 | 39, 40 | sselid 3981 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ ๐ โ ( O โ(
bday โ๐ต))) |
42 | 30, 38, 41 | mulsproplem3 27574 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (๐ด ยทs ๐) โ No
) |
43 | 36, 42 | addscld 27464 |
. . . . . . 7
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ ((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) โ No
) |
44 | 30, 33, 41 | mulsproplem4 27575 |
. . . . . . 7
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (๐ ยทs ๐) โ No
) |
45 | 43, 44 | subscld 27535 |
. . . . . 6
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ No
) |
46 | | eleq1 2822 |
. . . . . 6
โข (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (๐ โ No
โ (((๐
ยทs ๐ต)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))
โ No )) |
47 | 45, 46 | syl5ibrcom 246 |
. . . . 5
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
48 | 47 | rexlimdvva 3212 |
. . . 4
โข (๐ โ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
49 | 48 | abssdv 4066 |
. . 3
โข (๐ โ {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ No
) |
50 | 29 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
51 | | rightssold 27374 |
. . . . . . . . . 10
โข ( R
โ๐ด) โ ( O
โ( bday โ๐ด)) |
52 | | simprl 770 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ ๐ โ ( R โ๐ด)) |
53 | 51, 52 | sselid 3981 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ ๐ โ ( O โ(
bday โ๐ด))) |
54 | 34 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ ๐ต โ No
) |
55 | 50, 53, 54 | mulsproplem2 27573 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (๐ ยทs ๐ต) โ No
) |
56 | 37 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ ๐ด โ No
) |
57 | | rightssold 27374 |
. . . . . . . . . 10
โข ( R
โ๐ต) โ ( O
โ( bday โ๐ต)) |
58 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ ๐ โ ( R โ๐ต)) |
59 | 57, 58 | sselid 3981 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ ๐ โ ( O โ(
bday โ๐ต))) |
60 | 50, 56, 59 | mulsproplem3 27574 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (๐ด ยทs ๐ ) โ No
) |
61 | 55, 60 | addscld 27464 |
. . . . . . 7
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ ((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) โ No
) |
62 | 50, 53, 59 | mulsproplem4 27575 |
. . . . . . 7
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (๐ ยทs ๐ ) โ No
) |
63 | 61, 62 | subscld 27535 |
. . . . . 6
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ No
) |
64 | | eleq1 2822 |
. . . . . 6
โข (โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ (โ โ No
โ (((๐
ยทs ๐ต)
+s (๐ด
ยทs ๐ ))
-s (๐
ยทs ๐ ))
โ No )) |
65 | 63, 64 | syl5ibrcom 246 |
. . . . 5
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ โ โ No
)) |
66 | 65 | rexlimdvva 3212 |
. . . 4
โข (๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ โ โ No
)) |
67 | 66 | abssdv 4066 |
. . 3
โข (๐ โ {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} โ No
) |
68 | 49, 67 | unssd 4187 |
. 2
โข (๐ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ No
) |
69 | 29 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
70 | | simprl 770 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ ๐ก โ ( L โ๐ด)) |
71 | 31, 70 | sselid 3981 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ ๐ก โ ( O โ(
bday โ๐ด))) |
72 | 34 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ ๐ต โ No
) |
73 | 69, 71, 72 | mulsproplem2 27573 |
. . . . . . . 8
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ (๐ก ยทs ๐ต) โ No
) |
74 | 37 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ ๐ด โ No
) |
75 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ ๐ข โ ( R โ๐ต)) |
76 | 57, 75 | sselid 3981 |
. . . . . . . . 9
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ ๐ข โ ( O โ(
bday โ๐ต))) |
77 | 69, 74, 76 | mulsproplem3 27574 |
. . . . . . . 8
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ (๐ด ยทs ๐ข) โ No
) |
78 | 73, 77 | addscld 27464 |
. . . . . . 7
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ ((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) โ No
) |
79 | 69, 71, 76 | mulsproplem4 27575 |
. . . . . . 7
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ (๐ก ยทs ๐ข) โ No
) |
80 | 78, 79 | subscld 27535 |
. . . . . 6
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ No
) |
81 | | eleq1 2822 |
. . . . . 6
โข (๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (๐ โ No
โ (((๐ก
ยทs ๐ต)
+s (๐ด
ยทs ๐ข))
-s (๐ก
ยทs ๐ข))
โ No )) |
82 | 80, 81 | syl5ibrcom 246 |
. . . . 5
โข ((๐ โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ (๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ โ No
)) |
83 | 82 | rexlimdvva 3212 |
. . . 4
โข (๐ โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ โ No
)) |
84 | 83 | abssdv 4066 |
. . 3
โข (๐ โ {๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โ No
) |
85 | 29 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
86 | | simprl 770 |
. . . . . . . . . 10
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ ๐ฃ โ ( R โ๐ด)) |
87 | 51, 86 | sselid 3981 |
. . . . . . . . 9
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ ๐ฃ โ ( O โ(
bday โ๐ด))) |
88 | 34 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ ๐ต โ No
) |
89 | 85, 87, 88 | mulsproplem2 27573 |
. . . . . . . 8
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ (๐ฃ ยทs ๐ต) โ No
) |
90 | 37 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ ๐ด โ No
) |
91 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ ๐ค โ ( L โ๐ต)) |
92 | 39, 91 | sselid 3981 |
. . . . . . . . 9
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ ๐ค โ ( O โ(
bday โ๐ต))) |
93 | 85, 90, 92 | mulsproplem3 27574 |
. . . . . . . 8
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ (๐ด ยทs ๐ค) โ No
) |
94 | 89, 93 | addscld 27464 |
. . . . . . 7
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ ((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) โ No
) |
95 | 85, 87, 92 | mulsproplem4 27575 |
. . . . . . 7
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ (๐ฃ ยทs ๐ค) โ No
) |
96 | 94, 95 | subscld 27535 |
. . . . . 6
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ No
) |
97 | | eleq1 2822 |
. . . . . 6
โข (๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (๐ โ No
โ (((๐ฃ
ยทs ๐ต)
+s (๐ด
ยทs ๐ค))
-s (๐ฃ
ยทs ๐ค))
โ No )) |
98 | 96, 97 | syl5ibrcom 246 |
. . . . 5
โข ((๐ โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ (๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ โ No
)) |
99 | 98 | rexlimdvva 3212 |
. . . 4
โข (๐ โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ โ No
)) |
100 | 99 | abssdv 4066 |
. . 3
โข (๐ โ {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))} โ No
) |
101 | 84, 100 | unssd 4187 |
. 2
โข (๐ โ ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) โ No
) |
102 | | elun 4149 |
. . . . . . 7
โข (๐ฅ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ (๐ฅ โ {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โจ ๐ฅ โ {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))})) |
103 | | vex 3479 |
. . . . . . . . 9
โข ๐ฅ โ V |
104 | | eqeq1 2737 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
105 | 104 | 2rexbidv 3220 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
106 | 103, 105 | elab 3669 |
. . . . . . . 8
โข (๐ฅ โ {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
107 | | eqeq1 2737 |
. . . . . . . . . 10
โข (โ = ๐ฅ โ (โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
108 | 107 | 2rexbidv 3220 |
. . . . . . . . 9
โข (โ = ๐ฅ โ (โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
109 | 103, 108 | elab 3669 |
. . . . . . . 8
โข (๐ฅ โ {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} โ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) |
110 | 106, 109 | orbi12i 914 |
. . . . . . 7
โข ((๐ฅ โ {๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โจ ๐ฅ โ {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
111 | 102, 110 | bitri 275 |
. . . . . 6
โข (๐ฅ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
112 | | elun 4149 |
. . . . . . 7
โข (๐ฆ โ ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) โ (๐ฆ โ {๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โจ ๐ฆ โ {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) |
113 | | vex 3479 |
. . . . . . . . 9
โข ๐ฆ โ V |
114 | | eqeq1 2737 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)))) |
115 | 114 | 2rexbidv 3220 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)))) |
116 | 113, 115 | elab 3669 |
. . . . . . . 8
โข (๐ฆ โ {๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) |
117 | | eqeq1 2737 |
. . . . . . . . . 10
โข (๐ = ๐ฆ โ (๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) |
118 | 117 | 2rexbidv 3220 |
. . . . . . . . 9
โข (๐ = ๐ฆ โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) |
119 | 113, 118 | elab 3669 |
. . . . . . . 8
โข (๐ฆ โ {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))} โ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) |
120 | 116, 119 | orbi12i 914 |
. . . . . . 7
โข ((๐ฆ โ {๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โจ ๐ฆ โ {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โจ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) |
121 | 112, 120 | bitri 275 |
. . . . . 6
โข (๐ฆ โ ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))}) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โจ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) |
122 | 111, 121 | anbi12i 628 |
. . . . 5
โข ((๐ฅ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โง ๐ฆ โ ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) โ ((โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โง (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โจ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))))) |
123 | | anddi 1010 |
. . . . 5
โข
(((โ๐ โ (
L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โง (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โจ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) โ (((โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โจ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) โจ ((โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โจ (โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))))) |
124 | 122, 123 | bitri 275 |
. . . 4
โข ((๐ฅ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โง ๐ฆ โ ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) โ (((โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โจ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) โจ ((โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โจ (โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))))) |
125 | 29 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
126 | 37 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ด โ No
) |
127 | 34 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ต โ No
) |
128 | | simprll 778 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ โ ( L โ๐ด)) |
129 | | simprlr 779 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ โ ( L โ๐ต)) |
130 | | simprrl 780 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ก โ ( L โ๐ด)) |
131 | | simprrr 781 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ข โ ( R โ๐ต)) |
132 | 125, 126,
127, 128, 129, 130, 131 | mulsproplem5 27576 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) |
133 | | breq2 5153 |
. . . . . . . . . . . 12
โข (๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ((((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)))) |
134 | 132, 133 | syl5ibrcom 246 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ (๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ)) |
135 | 134 | anassrs 469 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ (๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ)) |
136 | 135 | rexlimdvva 3212 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ)) |
137 | | breq1 5152 |
. . . . . . . . . 10
โข (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (๐ฅ <s ๐ฆ โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ)) |
138 | 137 | imbi2d 341 |
. . . . . . . . 9
โข (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ((โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ฅ <s ๐ฆ) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ))) |
139 | 136, 138 | syl5ibrcom 246 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ฅ <s ๐ฆ))) |
140 | 139 | rexlimdvva 3212 |
. . . . . . 7
โข (๐ โ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ฅ <s ๐ฆ))) |
141 | 140 | impd 412 |
. . . . . 6
โข (๐ โ ((โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โ ๐ฅ <s ๐ฆ)) |
142 | 29 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
143 | 37 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ด โ No
) |
144 | 34 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ต โ No
) |
145 | | simprll 778 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ โ ( L โ๐ด)) |
146 | | simprlr 779 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ โ ( L โ๐ต)) |
147 | | simprrl 780 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ฃ โ ( R โ๐ด)) |
148 | | simprrr 781 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ค โ ( L โ๐ต)) |
149 | 142, 143,
144, 145, 146, 147, 148 | mulsproplem6 27577 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) |
150 | | breq2 5153 |
. . . . . . . . . . . 12
โข (๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ((((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) |
151 | 149, 150 | syl5ibrcom 246 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ (๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ)) |
152 | 151 | anassrs 469 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ (๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ)) |
153 | 152 | rexlimdvva 3212 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ)) |
154 | 137 | imbi2d 341 |
. . . . . . . . 9
โข (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ((โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ฅ <s ๐ฆ) โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s ๐ฆ))) |
155 | 153, 154 | syl5ibrcom 246 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( L โ๐ด) โง ๐ โ ( L โ๐ต))) โ (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ฅ <s ๐ฆ))) |
156 | 155 | rexlimdvva 3212 |
. . . . . . 7
โข (๐ โ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ฅ <s ๐ฆ))) |
157 | 156 | impd 412 |
. . . . . 6
โข (๐ โ ((โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) โ ๐ฅ <s ๐ฆ)) |
158 | 141, 157 | jaod 858 |
. . . . 5
โข (๐ โ (((โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โจ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) โ ๐ฅ <s ๐ฆ)) |
159 | 29 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
160 | 37 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ด โ No
) |
161 | 34 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ต โ No
) |
162 | | simprll 778 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ โ ( R โ๐ด)) |
163 | | simprlr 779 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ โ ( R โ๐ต)) |
164 | | simprrl 780 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ก โ ( L โ๐ด)) |
165 | | simprrr 781 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ ๐ข โ ( R โ๐ต)) |
166 | 159, 160,
161, 162, 163, 164, 165 | mulsproplem7 27578 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) |
167 | | breq2 5153 |
. . . . . . . . . . . 12
โข (๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ((((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)))) |
168 | 166, 167 | syl5ibrcom 246 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต)))) โ (๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ)) |
169 | 168 | anassrs 469 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โง (๐ก โ ( L โ๐ด) โง ๐ข โ ( R โ๐ต))) โ (๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ)) |
170 | 169 | rexlimdvva 3212 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ)) |
171 | | breq1 5152 |
. . . . . . . . . 10
โข (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ (๐ฅ <s ๐ฆ โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ)) |
172 | 171 | imbi2d 341 |
. . . . . . . . 9
โข (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ((โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ฅ <s ๐ฆ) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ))) |
173 | 170, 172 | syl5ibrcom 246 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ฅ <s ๐ฆ))) |
174 | 173 | rexlimdvva 3212 |
. . . . . . 7
โข (๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ (โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข)) โ ๐ฅ <s ๐ฆ))) |
175 | 174 | impd 412 |
. . . . . 6
โข (๐ โ ((โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โ ๐ฅ <s ๐ฆ)) |
176 | 29 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No โ๐ โ No
โ๐ โ No (((( bday โ๐) +no (
bday โ๐))
โช (((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))) โช
((( bday โ๐) +no ( bday
โ๐)) โช
(( bday โ๐) +no ( bday
โ๐))))) โ
((( bday โ๐ด) +no ( bday
โ๐ต)) โช
(((( bday โ๐ถ) +no ( bday
โ๐ธ)) โช
(( bday โ๐ท) +no ( bday
โ๐น))) โช
((( bday โ๐ถ) +no ( bday
โ๐น)) โช
(( bday โ๐ท) +no ( bday
โ๐ธ))))) โ
((๐ ยทs
๐) โ No โง ((๐ <s ๐ โง ๐ <s ๐) โ ((๐ ยทs ๐) -s (๐ ยทs ๐)) <s ((๐ ยทs ๐) -s (๐ ยทs ๐)))))) |
177 | 37 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ด โ No
) |
178 | 34 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ต โ No
) |
179 | | simprll 778 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ โ ( R โ๐ด)) |
180 | | simprlr 779 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ โ ( R โ๐ต)) |
181 | | simprrl 780 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ฃ โ ( R โ๐ด)) |
182 | | simprrr 781 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ ๐ค โ ( L โ๐ต)) |
183 | 176, 177,
178, 179, 180, 181, 182 | mulsproplem8 27579 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) |
184 | | breq2 5153 |
. . . . . . . . . . . 12
โข (๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ((((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) |
185 | 183, 184 | syl5ibrcom 246 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต)) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต)))) โ (๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ)) |
186 | 185 | anassrs 469 |
. . . . . . . . . 10
โข (((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โง (๐ฃ โ ( R โ๐ด) โง ๐ค โ ( L โ๐ต))) โ (๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ)) |
187 | 186 | rexlimdvva 3212 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ)) |
188 | 171 | imbi2d 341 |
. . . . . . . . 9
โข (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ((โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ฅ <s ๐ฆ) โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s ๐ฆ))) |
189 | 187, 188 | syl5ibrcom 246 |
. . . . . . . 8
โข ((๐ โง (๐ โ ( R โ๐ด) โง ๐ โ ( R โ๐ต))) โ (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ฅ <s ๐ฆ))) |
190 | 189 | rexlimdvva 3212 |
. . . . . . 7
โข (๐ โ (โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ (โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)) โ ๐ฅ <s ๐ฆ))) |
191 | 190 | impd 412 |
. . . . . 6
โข (๐ โ ((โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))) โ ๐ฅ <s ๐ฆ)) |
192 | 175, 191 | jaod 858 |
. . . . 5
โข (๐ โ (((โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โจ (โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) โ ๐ฅ <s ๐ฆ)) |
193 | 158, 192 | jaod 858 |
. . . 4
โข (๐ โ ((((โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โจ (โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค)))) โจ ((โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ฆ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))) โจ (โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โง โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ฆ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))))) โ ๐ฅ <s ๐ฆ)) |
194 | 124, 193 | biimtrid 241 |
. . 3
โข (๐ โ ((๐ฅ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โง ๐ฆ โ ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) โ ๐ฅ <s ๐ฆ)) |
195 | 194 | 3impib 1117 |
. 2
โข ((๐ โง ๐ฅ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โง ๐ฆ โ ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) โ ๐ฅ <s ๐ฆ) |
196 | 16, 28, 68, 101, 195 | ssltd 27293 |
1
โข (๐ โ ({๐ โฃ โ๐ โ ( L โ๐ด)โ๐ โ ( L โ๐ต)๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {โ โฃ โ๐ โ ( R โ๐ด)โ๐ โ ( R โ๐ต)โ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) <<s ({๐ โฃ โ๐ก โ ( L โ๐ด)โ๐ข โ ( R โ๐ต)๐ = (((๐ก ยทs ๐ต) +s (๐ด ยทs ๐ข)) -s (๐ก ยทs ๐ข))} โช {๐ โฃ โ๐ฃ โ ( R โ๐ด)โ๐ค โ ( L โ๐ต)๐ = (((๐ฃ ยทs ๐ต) +s (๐ด ยทs ๐ค)) -s (๐ฃ ยทs ๐ค))})) |