Step | Hyp | Ref
| Expression |
1 | | axsegconlem1 27908 |
. . . . 5
โข ((๐ด = ๐ต โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
2 | 1 | ex 414 |
. . . 4
โข (๐ด = ๐ต โ (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) |
3 | | simprll 778 |
. . . . . 6
โข ((๐ด โ ๐ต โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โ ๐ด โ (๐ผโ๐)) |
4 | | simprlr 779 |
. . . . . 6
โข ((๐ด โ ๐ต โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โ ๐ต โ (๐ผโ๐)) |
5 | | simpl 484 |
. . . . . 6
โข ((๐ด โ ๐ต โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โ ๐ด โ ๐ต) |
6 | | simprr 772 |
. . . . . 6
โข ((๐ด โ ๐ต โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โ (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) |
7 | | eqid 2733 |
. . . . . . . 8
โข
ฮฃ๐ โ
(1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2) |
8 | | eqid 2733 |
. . . . . . . 8
โข
ฮฃ๐ โ
(1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) |
9 | | eqid 2733 |
. . . . . . . 8
โข (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) |
10 | 7, 8, 9 | axsegconlem8 27915 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ (๐ผโ๐)) |
11 | 7, 8 | axsegconlem7 27914 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ
(0[,]1)) |
12 | 7, 8, 9 | axsegconlem10 27917 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))))) ยท (๐ดโ๐)) + (((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐)))) |
13 | 7, 8, 9 | axsegconlem9 27916 |
. . . . . . 7
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) |
14 | | fveq1 6842 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ (๐ฅโ๐) = ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐)) |
15 | 14 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ (๐ก ยท (๐ฅโ๐)) = (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) |
16 | 15 | oveq2d 7374 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐)))) |
17 | 16 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ ((๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โ (๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))))) |
18 | 17 | ralbidv 3171 |
. . . . . . . . 9
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โ โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))))) |
19 | 14 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ ((๐ตโ๐) โ (๐ฅโ๐)) = ((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) |
20 | 19 | oveq1d 7373 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ (((๐ตโ๐) โ (๐ฅโ๐))โ2) = (((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))โ2)) |
21 | 20 | sumeq2sdv 15594 |
. . . . . . . . . 10
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))โ2)) |
22 | 21 | eqeq1d 2735 |
. . . . . . . . 9
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ (ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
23 | 18, 22 | anbi12d 632 |
. . . . . . . 8
โข (๐ฅ = (๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ ((โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) โ (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) |
24 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ก = ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ (1 โ ๐ก) = (1 โ
((โโฮฃ๐
โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))))) |
25 | 24 | oveq1d 7373 |
. . . . . . . . . . . 12
โข (๐ก = ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ ((1 โ ๐ก) ยท (๐ดโ๐)) = ((1 โ ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))))) ยท (๐ดโ๐))) |
26 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ก = ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐)) = (((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) |
27 | 25, 26 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ก = ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) = (((1 โ
((โโฮฃ๐
โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))))) ยท (๐ดโ๐)) + (((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐)))) |
28 | 27 | eqeq2d 2744 |
. . . . . . . . . 10
โข (๐ก = ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ ((๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) โ (๐ตโ๐) = (((1 โ ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))))) ยท (๐ดโ๐)) + (((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))))) |
29 | 28 | ralbidv 3171 |
. . . . . . . . 9
โข (๐ก = ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) โ โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))))) ยท (๐ดโ๐)) + (((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))))) |
30 | 29 | anbi1d 631 |
. . . . . . . 8
โข (๐ก = ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ ((โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) โ (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))))) ยท (๐ดโ๐)) + (((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) |
31 | 23, 30 | rspc2ev 3591 |
. . . . . . 7
โข (((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)))) โ (๐ผโ๐) โง
((โโฮฃ๐
โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) โ (0[,]1) โง
(โ๐ โ
(1...๐)(๐ตโ๐) = (((1 โ ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))))) ยท (๐ดโ๐)) + (((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) / ((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) ยท ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ ((๐ โ (1...๐) โฆ (((((โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2)) + (โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) ยท (๐ตโ๐)) โ ((โโฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) ยท (๐ดโ๐))) / (โโฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ตโ๐))โ2))))โ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
32 | 10, 11, 12, 13, 31 | syl112anc 1375 |
. . . . . 6
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ด โ ๐ต) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
33 | 3, 4, 5, 6, 32 | syl31anc 1374 |
. . . . 5
โข ((๐ด โ ๐ต โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
34 | 33 | ex 414 |
. . . 4
โข (๐ด โ ๐ต โ (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) |
35 | 2, 34 | pm2.61ine 3025 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
36 | | simpllr 775 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ ๐ต โ (๐ผโ๐)) |
37 | | simplll 774 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ ๐ด โ (๐ผโ๐)) |
38 | | simpr 486 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ ๐ฅ โ (๐ผโ๐)) |
39 | | brbtwn 27890 |
. . . . . . 7
โข ((๐ต โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐) โง ๐ฅ โ (๐ผโ๐)) โ (๐ต Btwn โจ๐ด, ๐ฅโฉ โ โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))))) |
40 | 36, 37, 38, 39 | syl3anc 1372 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ (๐ต Btwn โจ๐ด, ๐ฅโฉ โ โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))))) |
41 | | simplrl 776 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ ๐ถ โ (๐ผโ๐)) |
42 | | simplrr 777 |
. . . . . . 7
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ ๐ท โ (๐ผโ๐)) |
43 | | brcgr 27891 |
. . . . . . 7
โข (((๐ต โ (๐ผโ๐) โง ๐ฅ โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ (โจ๐ต, ๐ฅโฉCgrโจ๐ถ, ๐ทโฉ โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
44 | 36, 38, 41, 42, 43 | syl22anc 838 |
. . . . . 6
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ (โจ๐ต, ๐ฅโฉCgrโจ๐ถ, ๐ทโฉ โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
45 | 40, 44 | anbi12d 632 |
. . . . 5
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ ((๐ต Btwn โจ๐ด, ๐ฅโฉ โง โจ๐ต, ๐ฅโฉCgrโจ๐ถ, ๐ทโฉ) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) |
46 | | r19.41v 3182 |
. . . . 5
โข
(โ๐ก โ
(0[,]1)(โ๐ โ
(1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2))) |
47 | 45, 46 | bitr4di 289 |
. . . 4
โข ((((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โง ๐ฅ โ (๐ผโ๐)) โ ((๐ต Btwn โจ๐ด, ๐ฅโฉ โง โจ๐ต, ๐ฅโฉCgrโจ๐ถ, ๐ทโฉ) โ โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) |
48 | 47 | rexbidva 3170 |
. . 3
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ (โ๐ฅ โ (๐ผโ๐)(๐ต Btwn โจ๐ด, ๐ฅโฉ โง โจ๐ต, ๐ฅโฉCgrโจ๐ถ, ๐ทโฉ) โ โ๐ฅ โ (๐ผโ๐)โ๐ก โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ฅโ๐))) โง ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ฅโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)))) |
49 | 35, 48 | mpbird 257 |
. 2
โข (((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ฅ โ (๐ผโ๐)(๐ต Btwn โจ๐ด, ๐ฅโฉ โง โจ๐ต, ๐ฅโฉCgrโจ๐ถ, ๐ทโฉ)) |
50 | 49 | 3adant1 1131 |
1
โข ((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐))) โ โ๐ฅ โ (๐ผโ๐)(๐ต Btwn โจ๐ด, ๐ฅโฉ โง โจ๐ต, ๐ฅโฉCgrโจ๐ถ, ๐ทโฉ)) |