Step | Hyp | Ref
| Expression |
1 | | iccss2 13395 |
. . . . . . 7
โข ((๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต)) โ (๐ถ[,]๐ท) โ (๐ด[,]๐ต)) |
2 | 1 | adantl 483 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต))) โ (๐ถ[,]๐ท) โ (๐ด[,]๐ต)) |
3 | 2 | 3adantr3 1172 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ (๐ถ[,]๐ท) โ (๐ด[,]๐ต)) |
4 | 3 | adantr 482 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ถ < ๐ท) โ (๐ถ[,]๐ท) โ (๐ด[,]๐ต)) |
5 | | iccssre 13406 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด[,]๐ต) โ โ) |
6 | 5 | sselda 3983 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ (๐ด[,]๐ต)) โ ๐ถ โ โ) |
7 | 6 | adantrr 716 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต))) โ ๐ถ โ โ) |
8 | 5 | sselda 3983 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ท โ (๐ด[,]๐ต)) โ ๐ท โ โ) |
9 | 8 | adantrl 715 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต))) โ ๐ท โ โ) |
10 | 7, 9 | jca 513 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต))) โ (๐ถ โ โ โง ๐ท โ โ)) |
11 | 10 | 3adantr3 1172 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ (๐ถ โ โ โง ๐ท โ โ)) |
12 | | simpr3 1197 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ ๐ โ (0[,]1)) |
13 | 11, 12 | jca 513 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ ((๐ถ โ โ โง ๐ท โ โ) โง ๐ โ (0[,]1))) |
14 | | lincmb01cmp 13472 |
. . . . . . . . 9
โข (((๐ถ โ โ โง ๐ท โ โ โง ๐ถ < ๐ท) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ถ[,]๐ท)) |
15 | 14 | ex 414 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ท โ โ โง ๐ถ < ๐ท) โ (๐ โ (0[,]1) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ถ[,]๐ท))) |
16 | 15 | 3expa 1119 |
. . . . . . 7
โข (((๐ถ โ โ โง ๐ท โ โ) โง ๐ถ < ๐ท) โ (๐ โ (0[,]1) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ถ[,]๐ท))) |
17 | 16 | imp 408 |
. . . . . 6
โข ((((๐ถ โ โ โง ๐ท โ โ) โง ๐ถ < ๐ท) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ถ[,]๐ท)) |
18 | 17 | an32s 651 |
. . . . 5
โข ((((๐ถ โ โ โง ๐ท โ โ) โง ๐ โ (0[,]1)) โง ๐ถ < ๐ท) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ถ[,]๐ท)) |
19 | 13, 18 | sylan 581 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ถ < ๐ท) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ถ[,]๐ท)) |
20 | 4, 19 | sseldd 3984 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ถ < ๐ท) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ด[,]๐ต)) |
21 | | oveq2 7417 |
. . . . . 6
โข (๐ถ = ๐ท โ ((1 โ ๐) ยท ๐ถ) = ((1 โ ๐) ยท ๐ท)) |
22 | 21 | oveq1d 7424 |
. . . . 5
โข (๐ถ = ๐ท โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) = (((1 โ ๐) ยท ๐ท) + (๐ ยท ๐ท))) |
23 | | unitssre 13476 |
. . . . . . . . . 10
โข (0[,]1)
โ โ |
24 | 23 | sseli 3979 |
. . . . . . . . 9
โข (๐ โ (0[,]1) โ ๐ โ
โ) |
25 | 24 | recnd 11242 |
. . . . . . . 8
โข (๐ โ (0[,]1) โ ๐ โ
โ) |
26 | 25 | ad2antll 728 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ ๐ โ โ) |
27 | 8 | recnd 11242 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ท โ (๐ด[,]๐ต)) โ ๐ท โ โ) |
28 | 27 | adantrr 716 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ ๐ท โ โ) |
29 | | ax-1cn 11168 |
. . . . . . . . . . 11
โข 1 โ
โ |
30 | | npcan 11469 |
. . . . . . . . . . 11
โข ((1
โ โ โง ๐
โ โ) โ ((1 โ ๐) + ๐) = 1) |
31 | 29, 30 | mpan 689 |
. . . . . . . . . 10
โข (๐ โ โ โ ((1
โ ๐) + ๐) = 1) |
32 | 31 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ท โ โ) โ ((1
โ ๐) + ๐) = 1) |
33 | 32 | oveq1d 7424 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ท โ โ) โ (((1
โ ๐) + ๐) ยท ๐ท) = (1 ยท ๐ท)) |
34 | | subcl 11459 |
. . . . . . . . . . 11
โข ((1
โ โ โง ๐
โ โ) โ (1 โ ๐) โ โ) |
35 | 29, 34 | mpan 689 |
. . . . . . . . . 10
โข (๐ โ โ โ (1
โ ๐) โ
โ) |
36 | 35 | ancri 551 |
. . . . . . . . 9
โข (๐ โ โ โ ((1
โ ๐) โ โ
โง ๐ โ
โ)) |
37 | | adddir 11205 |
. . . . . . . . . 10
โข (((1
โ ๐) โ โ
โง ๐ โ โ
โง ๐ท โ โ)
โ (((1 โ ๐) +
๐) ยท ๐ท) = (((1 โ ๐) ยท ๐ท) + (๐ ยท ๐ท))) |
38 | 37 | 3expa 1119 |
. . . . . . . . 9
โข ((((1
โ ๐) โ โ
โง ๐ โ โ)
โง ๐ท โ โ)
โ (((1 โ ๐) +
๐) ยท ๐ท) = (((1 โ ๐) ยท ๐ท) + (๐ ยท ๐ท))) |
39 | 36, 38 | sylan 581 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ท โ โ) โ (((1
โ ๐) + ๐) ยท ๐ท) = (((1 โ ๐) ยท ๐ท) + (๐ ยท ๐ท))) |
40 | | mullid 11213 |
. . . . . . . . 9
โข (๐ท โ โ โ (1
ยท ๐ท) = ๐ท) |
41 | 40 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ท โ โ) โ (1
ยท ๐ท) = ๐ท) |
42 | 33, 39, 41 | 3eqtr3d 2781 |
. . . . . . 7
โข ((๐ โ โ โง ๐ท โ โ) โ (((1
โ ๐) ยท ๐ท) + (๐ ยท ๐ท)) = ๐ท) |
43 | 26, 28, 42 | syl2anc 585 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ (((1 โ ๐) ยท ๐ท) + (๐ ยท ๐ท)) = ๐ท) |
44 | 43 | 3adantr1 1170 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ (((1 โ ๐) ยท ๐ท) + (๐ ยท ๐ท)) = ๐ท) |
45 | 22, 44 | sylan9eqr 2795 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ถ = ๐ท) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) = ๐ท) |
46 | | simplr2 1217 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ถ = ๐ท) โ ๐ท โ (๐ด[,]๐ต)) |
47 | 45, 46 | eqeltrd 2834 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ถ = ๐ท) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ด[,]๐ต)) |
48 | | iccss2 13395 |
. . . . . . . 8
โข ((๐ท โ (๐ด[,]๐ต) โง ๐ถ โ (๐ด[,]๐ต)) โ (๐ท[,]๐ถ) โ (๐ด[,]๐ต)) |
49 | 48 | adantl 483 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ท โ (๐ด[,]๐ต) โง ๐ถ โ (๐ด[,]๐ต))) โ (๐ท[,]๐ถ) โ (๐ด[,]๐ต)) |
50 | 49 | ancom2s 649 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต))) โ (๐ท[,]๐ถ) โ (๐ด[,]๐ต)) |
51 | 50 | 3adantr3 1172 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ (๐ท[,]๐ถ) โ (๐ด[,]๐ต)) |
52 | 51 | adantr 482 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ท < ๐ถ) โ (๐ท[,]๐ถ) โ (๐ด[,]๐ต)) |
53 | 9, 7 | jca 513 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต))) โ (๐ท โ โ โง ๐ถ โ โ)) |
54 | 53 | 3adantr3 1172 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ (๐ท โ โ โง ๐ถ โ โ)) |
55 | 54, 12 | jca 513 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ ((๐ท โ โ โง ๐ถ โ โ) โง ๐ โ (0[,]1))) |
56 | | iirev 24445 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (0[,]1) โ (1
โ ๐) โ
(0[,]1)) |
57 | 23, 56 | sselid 3981 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (0[,]1) โ (1
โ ๐) โ
โ) |
58 | 57 | recnd 11242 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0[,]1) โ (1
โ ๐) โ
โ) |
59 | | recn 11200 |
. . . . . . . . . . . . . . 15
โข (๐ถ โ โ โ ๐ถ โ
โ) |
60 | | mulcl 11194 |
. . . . . . . . . . . . . . 15
โข (((1
โ ๐) โ โ
โง ๐ถ โ โ)
โ ((1 โ ๐)
ยท ๐ถ) โ
โ) |
61 | 58, 59, 60 | syl2anr 598 |
. . . . . . . . . . . . . 14
โข ((๐ถ โ โ โง ๐ โ (0[,]1)) โ ((1
โ ๐) ยท ๐ถ) โ
โ) |
62 | 61 | adantll 713 |
. . . . . . . . . . . . 13
โข (((๐ท โ โ โง ๐ถ โ โ) โง ๐ โ (0[,]1)) โ ((1
โ ๐) ยท ๐ถ) โ
โ) |
63 | | recn 11200 |
. . . . . . . . . . . . . . 15
โข (๐ท โ โ โ ๐ท โ
โ) |
64 | | mulcl 11194 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ท โ โ) โ (๐ ยท ๐ท) โ โ) |
65 | 25, 63, 64 | syl2anr 598 |
. . . . . . . . . . . . . 14
โข ((๐ท โ โ โง ๐ โ (0[,]1)) โ (๐ ยท ๐ท) โ โ) |
66 | 65 | adantlr 714 |
. . . . . . . . . . . . 13
โข (((๐ท โ โ โง ๐ถ โ โ) โง ๐ โ (0[,]1)) โ (๐ ยท ๐ท) โ โ) |
67 | 62, 66 | addcomd 11416 |
. . . . . . . . . . . 12
โข (((๐ท โ โ โง ๐ถ โ โ) โง ๐ โ (0[,]1)) โ (((1
โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + ((1 โ ๐) ยท ๐ถ))) |
68 | 67 | 3adantl3 1169 |
. . . . . . . . . . 11
โข (((๐ท โ โ โง ๐ถ โ โ โง ๐ท < ๐ถ) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) = ((๐ ยท ๐ท) + ((1 โ ๐) ยท ๐ถ))) |
69 | | nncan 11489 |
. . . . . . . . . . . . . . . . 17
โข ((1
โ โ โง ๐
โ โ) โ (1 โ (1 โ ๐)) = ๐) |
70 | 29, 69 | mpan 689 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ โ (1
โ (1 โ ๐)) =
๐) |
71 | 70 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ = (1 โ (1 โ ๐))) |
72 | 71 | oveq1d 7424 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ ยท ๐ท) = ((1 โ (1 โ ๐)) ยท ๐ท)) |
73 | 72 | oveq1d 7424 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐ ยท ๐ท) + ((1 โ ๐) ยท ๐ถ)) = (((1 โ (1 โ ๐)) ยท ๐ท) + ((1 โ ๐) ยท ๐ถ))) |
74 | 25, 73 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (0[,]1) โ ((๐ ยท ๐ท) + ((1 โ ๐) ยท ๐ถ)) = (((1 โ (1 โ ๐)) ยท ๐ท) + ((1 โ ๐) ยท ๐ถ))) |
75 | 74 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ท โ โ โง ๐ถ โ โ โง ๐ท < ๐ถ) โง ๐ โ (0[,]1)) โ ((๐ ยท ๐ท) + ((1 โ ๐) ยท ๐ถ)) = (((1 โ (1 โ ๐)) ยท ๐ท) + ((1 โ ๐) ยท ๐ถ))) |
76 | 68, 75 | eqtrd 2773 |
. . . . . . . . . 10
โข (((๐ท โ โ โง ๐ถ โ โ โง ๐ท < ๐ถ) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) = (((1 โ (1 โ ๐)) ยท ๐ท) + ((1 โ ๐) ยท ๐ถ))) |
77 | | lincmb01cmp 13472 |
. . . . . . . . . . 11
โข (((๐ท โ โ โง ๐ถ โ โ โง ๐ท < ๐ถ) โง (1 โ ๐) โ (0[,]1)) โ (((1 โ (1
โ ๐)) ยท ๐ท) + ((1 โ ๐) ยท ๐ถ)) โ (๐ท[,]๐ถ)) |
78 | 56, 77 | sylan2 594 |
. . . . . . . . . 10
โข (((๐ท โ โ โง ๐ถ โ โ โง ๐ท < ๐ถ) โง ๐ โ (0[,]1)) โ (((1 โ (1
โ ๐)) ยท ๐ท) + ((1 โ ๐) ยท ๐ถ)) โ (๐ท[,]๐ถ)) |
79 | 76, 78 | eqeltrd 2834 |
. . . . . . . . 9
โข (((๐ท โ โ โง ๐ถ โ โ โง ๐ท < ๐ถ) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ท[,]๐ถ)) |
80 | 79 | ex 414 |
. . . . . . . 8
โข ((๐ท โ โ โง ๐ถ โ โ โง ๐ท < ๐ถ) โ (๐ โ (0[,]1) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ท[,]๐ถ))) |
81 | 80 | 3expa 1119 |
. . . . . . 7
โข (((๐ท โ โ โง ๐ถ โ โ) โง ๐ท < ๐ถ) โ (๐ โ (0[,]1) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ท[,]๐ถ))) |
82 | 81 | imp 408 |
. . . . . 6
โข ((((๐ท โ โ โง ๐ถ โ โ) โง ๐ท < ๐ถ) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ท[,]๐ถ)) |
83 | 82 | an32s 651 |
. . . . 5
โข ((((๐ท โ โ โง ๐ถ โ โ) โง ๐ โ (0[,]1)) โง ๐ท < ๐ถ) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ท[,]๐ถ)) |
84 | 55, 83 | sylan 581 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ท < ๐ถ) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ท[,]๐ถ)) |
85 | 52, 84 | sseldd 3984 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โง ๐ท < ๐ถ) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ด[,]๐ต)) |
86 | 7, 9 | lttri4d 11355 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต))) โ (๐ถ < ๐ท โจ ๐ถ = ๐ท โจ ๐ท < ๐ถ)) |
87 | 86 | 3adantr3 1172 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ (๐ถ < ๐ท โจ ๐ถ = ๐ท โจ ๐ท < ๐ถ)) |
88 | 20, 47, 85, 87 | mpjao3dan 1432 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1))) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ด[,]๐ต)) |
89 | 88 | ex 414 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ถ โ (๐ด[,]๐ต) โง ๐ท โ (๐ด[,]๐ต) โง ๐ โ (0[,]1)) โ (((1 โ ๐) ยท ๐ถ) + (๐ ยท ๐ท)) โ (๐ด[,]๐ต))) |