Step | Hyp | Ref
| Expression |
1 | | fzfid 13884 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (1...๐) โ Fin) |
2 | | simpl21 1252 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ๐ถ โ (๐ผโ๐)) |
3 | | fveere 27892 |
. . . . . . . . . . . . 13
โข ((๐ถ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
4 | 2, 3 | sylancom 589 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ถโ๐) โ โ) |
5 | | simpl22 1253 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ๐ท โ (๐ผโ๐)) |
6 | | fveere 27892 |
. . . . . . . . . . . . 13
โข ((๐ท โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ทโ๐) โ โ) |
7 | 5, 6 | sylancom 589 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ทโ๐) โ โ) |
8 | 4, 7 | resubcld 11588 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((๐ถโ๐) โ (๐ทโ๐)) โ โ) |
9 | 8 | resqcld 14036 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((๐ถโ๐) โ (๐ทโ๐))โ2) โ โ) |
10 | 1, 9 | fsumrecl 15624 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) โ โ) |
11 | 10 | recnd 11188 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) โ โ) |
12 | 11 | adantr 482 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) โ โ) |
13 | | simpl32 1256 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ๐บ โ (๐ผโ๐)) |
14 | | fveere 27892 |
. . . . . . . . . . . . 13
โข ((๐บ โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐บโ๐) โ โ) |
15 | 13, 14 | sylancom 589 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐บโ๐) โ โ) |
16 | | simpl33 1257 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ๐ป โ (๐ผโ๐)) |
17 | | fveere 27892 |
. . . . . . . . . . . . 13
โข ((๐ป โ (๐ผโ๐) โง ๐ โ (1...๐)) โ (๐ปโ๐) โ โ) |
18 | 16, 17 | sylancom 589 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (๐ปโ๐) โ โ) |
19 | 15, 18 | resubcld 11588 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ ((๐บโ๐) โ (๐ปโ๐)) โ โ) |
20 | 19 | resqcld 14036 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง ๐ โ (1...๐)) โ (((๐บโ๐) โ (๐ปโ๐))โ2) โ โ) |
21 | 1, 20 | fsumrecl 15624 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2) โ โ) |
22 | 21 | recnd 11188 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2) โ โ) |
23 | 22 | adantr 482 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2) โ โ) |
24 | | elicc01 13389 |
. . . . . . . . . . . 12
โข (๐ก โ (0[,]1) โ (๐ก โ โ โง 0 โค
๐ก โง ๐ก โค 1)) |
25 | 24 | simp1bi 1146 |
. . . . . . . . . . 11
โข (๐ก โ (0[,]1) โ ๐ก โ
โ) |
26 | 25 | recnd 11188 |
. . . . . . . . . 10
โข (๐ก โ (0[,]1) โ ๐ก โ
โ) |
27 | 26 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โ ๐ก โ โ) |
28 | 27 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ ๐ก โ โ) |
29 | 28 | adantl 483 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ก โ โ) |
30 | | simpl11 1249 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ โ โ) |
31 | | simp12 1205 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ๐ด โ (๐ผโ๐)) |
32 | | simp13 1206 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ๐ต โ (๐ผโ๐)) |
33 | | simp21 1207 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ๐ถ โ (๐ผโ๐)) |
34 | 31, 32, 33 | 3jca 1129 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) |
35 | 34 | adantr 482 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) |
36 | | simprrl 780 |
. . . . . . . . . 10
โข (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โ โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐)))) |
37 | 36 | 3ad2ant1 1134 |
. . . . . . . . 9
โข ((((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐)))) |
38 | 37 | adantl 483 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐)))) |
39 | | simp1rl 1239 |
. . . . . . . . 9
โข ((((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ ๐ด โ ๐ต) |
40 | 39 | adantl 483 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ด โ ๐ต) |
41 | | ax5seglem4 27923 |
. . . . . . . 8
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐))) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง ๐ด โ ๐ต) โ ๐ก โ 0) |
42 | 30, 35, 38, 40, 41 | syl211anc 1377 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ก โ 0) |
43 | | simpr3r 1236 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ) |
44 | | simpl13 1251 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ต โ (๐ผโ๐)) |
45 | | simpl22 1253 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ท โ (๐ผโ๐)) |
46 | | simpl31 1255 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐น โ (๐ผโ๐)) |
47 | | simpl33 1257 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ป โ (๐ผโ๐)) |
48 | | brcgr 27891 |
. . . . . . . . . . . 12
โข (((๐ต โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐นโ๐) โ (๐ปโ๐))โ2))) |
49 | 44, 45, 46, 47, 48 | syl22anc 838 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐นโ๐) โ (๐ปโ๐))โ2))) |
50 | 43, 49 | mpbid 231 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐นโ๐) โ (๐ปโ๐))โ2)) |
51 | | simp23 1209 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ๐ธ โ (๐ผโ๐)) |
52 | | simp31 1210 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ๐น โ (๐ผโ๐)) |
53 | | simp32 1211 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ๐บ โ (๐ผโ๐)) |
54 | 51, 52, 53 | 3jca 1129 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐))) |
55 | 34, 54 | jca 513 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐)))) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐)))) |
57 | | simpr1l 1231 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ก โ (0[,]1) โง ๐ โ (0[,]1))) |
58 | | simprrr 781 |
. . . . . . . . . . . . . . . 16
โข (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โ โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))) |
59 | 58 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
โข ((((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))) |
60 | 59 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))) |
61 | 38, 60 | jca 513 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) |
62 | | simpr2l 1233 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ) |
63 | | simpr2r 1234 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) |
64 | | ax5seglem6 27925 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐)))) โง (๐ด โ ๐ต โง (๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ)) โ ๐ก = ๐ ) |
65 | 30, 56, 40, 57, 61, 62, 63, 64 | syl232anc 1398 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ก = ๐ ) |
66 | 65 | oveq2d 7374 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (1 โ ๐ก) = (1 โ ๐ )) |
67 | 54 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐))) |
68 | | ax5seglem3 27922 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โง (๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐))) โง ((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ)) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐บโ๐))โ2)) |
69 | 30, 35, 67, 57, 61, 62, 63, 68 | syl322anc 1399 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐บโ๐))โ2)) |
70 | 65, 69 | oveq12d 7376 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ก ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2)) = (๐ ยท ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐บโ๐))โ2))) |
71 | | simpr3l 1235 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ) |
72 | | simpl12 1250 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ด โ (๐ผโ๐)) |
73 | | simpl23 1254 |
. . . . . . . . . . . . . 14
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ธ โ (๐ผโ๐)) |
74 | | brcgr 27891 |
. . . . . . . . . . . . . 14
โข (((๐ด โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)) โง (๐ธ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐ปโ๐))โ2))) |
75 | 72, 45, 73, 47, 74 | syl22anc 838 |
. . . . . . . . . . . . 13
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐ปโ๐))โ2))) |
76 | 71, 75 | mpbid 231 |
. . . . . . . . . . . 12
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐ปโ๐))โ2)) |
77 | 70, 76 | oveq12d 7376 |
. . . . . . . . . . 11
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ((๐ก ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2)) = ((๐ ยท ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐บโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐ปโ๐))โ2))) |
78 | 66, 77 | oveq12d 7376 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ((1 โ ๐ก) ยท ((๐ก ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2))) = ((1 โ ๐ ) ยท ((๐ ยท ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐บโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐ปโ๐))โ2)))) |
79 | 50, 78 | oveq12d 7376 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ทโ๐))โ2) + ((1 โ ๐ก) ยท ((๐ก ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2)))) = (ฮฃ๐ โ (1...๐)(((๐นโ๐) โ (๐ปโ๐))โ2) + ((1 โ ๐ ) ยท ((๐ ยท ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐บโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐ปโ๐))โ2))))) |
80 | 31, 32 | jca 513 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐))) |
81 | | simp22 1208 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ๐ท โ (๐ผโ๐)) |
82 | 80, 33, 81 | jca32 517 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) |
83 | 82 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) |
84 | | simp1ll 1237 |
. . . . . . . . . . 11
โข ((((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ ๐ก โ (0[,]1)) |
85 | 84 | adantl 483 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ก โ (0[,]1)) |
86 | | ax5seglem9 27928 |
. . . . . . . . . 10
โข (((๐ โ โ โง ((๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)))) โง (๐ก โ (0[,]1) โง โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))))) โ (๐ก ยท ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) = (ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ทโ๐))โ2) + ((1 โ ๐ก) ยท ((๐ก ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2))))) |
87 | 30, 83, 85, 38, 86 | syl22anc 838 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ก ยท ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) = (ฮฃ๐ โ (1...๐)(((๐ตโ๐) โ (๐ทโ๐))โ2) + ((1 โ ๐ก) ยท ((๐ก ยท ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ถโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ดโ๐) โ (๐ทโ๐))โ2))))) |
88 | | 3simpc 1151 |
. . . . . . . . . . . . 13
โข ((๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐)) โ (๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) |
89 | 88 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) |
90 | 51, 52, 89 | jca31 516 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐)) โง (๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐)))) |
91 | 90 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ((๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐)) โง (๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐)))) |
92 | | simp1lr 1238 |
. . . . . . . . . . 11
โข ((((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ ๐ โ (0[,]1)) |
93 | 92 | adantl 483 |
. . . . . . . . . 10
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ๐ โ (0[,]1)) |
94 | | ax5seglem9 27928 |
. . . . . . . . . 10
โข (((๐ โ โ โง ((๐ธ โ (๐ผโ๐) โง ๐น โ (๐ผโ๐)) โง (๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐)))) โง (๐ โ (0[,]1) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โ (๐ ยท ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2)) = (ฮฃ๐ โ (1...๐)(((๐นโ๐) โ (๐ปโ๐))โ2) + ((1 โ ๐ ) ยท ((๐ ยท ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐บโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐ปโ๐))โ2))))) |
95 | 30, 91, 93, 60, 94 | syl22anc 838 |
. . . . . . . . 9
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ ยท ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2)) = (ฮฃ๐ โ (1...๐)(((๐นโ๐) โ (๐ปโ๐))โ2) + ((1 โ ๐ ) ยท ((๐ ยท ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐บโ๐))โ2)) โ ฮฃ๐ โ (1...๐)(((๐ธโ๐) โ (๐ปโ๐))โ2))))) |
96 | 79, 87, 95 | 3eqtr4d 2783 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ก ยท ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) = (๐ ยท ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2))) |
97 | 65 | oveq1d 7373 |
. . . . . . . 8
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ก ยท ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2)) = (๐ ยท ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2))) |
98 | 96, 97 | eqtr4d 2776 |
. . . . . . 7
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ (๐ก ยท ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2)) = (๐ก ยท ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2))) |
99 | 12, 23, 29, 42, 98 | mulcanad 11795 |
. . . . . 6
โข ((((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โง (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ))) โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2)) |
100 | 99 | 3exp2 1355 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โง (๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) โ ((โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โ ((โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ) โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2))))) |
101 | 100 | expd 417 |
. . . 4
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((๐ก โ (0[,]1) โง ๐ โ (0[,]1)) โ ((๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โ ((โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โ ((โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ) โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2)))))) |
102 | 101 | rexlimdvv 3201 |
. . 3
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (โ๐ก โ (0[,]1)โ๐ โ (0[,]1)(๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โ ((โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โ ((โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ) โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2))))) |
103 | 102 | 3impd 1349 |
. 2
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((โ๐ก โ (0[,]1)โ๐ โ (0[,]1)(๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2))) |
104 | | brbtwn 27890 |
. . . . . . . 8
โข ((๐ต โ (๐ผโ๐) โง ๐ด โ (๐ผโ๐) โง ๐ถ โ (๐ผโ๐)) โ (๐ต Btwn โจ๐ด, ๐ถโฉ โ โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))))) |
105 | 32, 31, 33, 104 | syl3anc 1372 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (๐ต Btwn โจ๐ด, ๐ถโฉ โ โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))))) |
106 | | brbtwn 27890 |
. . . . . . . 8
โข ((๐น โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐)) โ (๐น Btwn โจ๐ธ, ๐บโฉ โ โ๐ โ (0[,]1)โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) |
107 | 52, 51, 53, 106 | syl3anc 1372 |
. . . . . . 7
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (๐น Btwn โจ๐ธ, ๐บโฉ โ โ๐ โ (0[,]1)โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) |
108 | 105, 107 | anbi12d 632 |
. . . . . 6
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (0[,]1)โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) |
109 | | reeanv 3216 |
. . . . . 6
โข
(โ๐ก โ
(0[,]1)โ๐ โ
(0[,]1)(โ๐ โ
(1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))) โ (โ๐ก โ (0[,]1)โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (0[,]1)โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) |
110 | 108, 109 | bitr4di 289 |
. . . . 5
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ) โ โ๐ก โ (0[,]1)โ๐ โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) |
111 | 110 | anbi2d 630 |
. . . 4
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((๐ด โ ๐ต โง (๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ)) โ (๐ด โ ๐ต โง โ๐ก โ (0[,]1)โ๐ โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))))) |
112 | | 3anass 1096 |
. . . 4
โข ((๐ด โ ๐ต โง ๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ) โ (๐ด โ ๐ต โง (๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ))) |
113 | | r19.42v 3184 |
. . . . . 6
โข
(โ๐ โ
(0[,]1)(๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โ (๐ด โ ๐ต โง โ๐ โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) |
114 | 113 | rexbii 3094 |
. . . . 5
โข
(โ๐ก โ
(0[,]1)โ๐ โ
(0[,]1)(๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โ โ๐ก โ (0[,]1)(๐ด โ ๐ต โง โ๐ โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) |
115 | | r19.42v 3184 |
. . . . 5
โข
(โ๐ก โ
(0[,]1)(๐ด โ ๐ต โง โ๐ โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โ (๐ด โ ๐ต โง โ๐ก โ (0[,]1)โ๐ โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) |
116 | 114, 115 | bitri 275 |
. . . 4
โข
(โ๐ก โ
(0[,]1)โ๐ โ
(0[,]1)(๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โ (๐ด โ ๐ต โง โ๐ก โ (0[,]1)โ๐ โ (0[,]1)(โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐)))))) |
117 | 111, 112,
116 | 3bitr4g 314 |
. . 3
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ((๐ด โ ๐ต โง ๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ) โ โ๐ก โ (0[,]1)โ๐ โ (0[,]1)(๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))))) |
118 | 117 | 3anbi1d 1441 |
. 2
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (((๐ด โ ๐ต โง ๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ (โ๐ก โ (0[,]1)โ๐ โ (0[,]1)(๐ด โ ๐ต โง (โ๐ โ (1...๐)(๐ตโ๐) = (((1 โ ๐ก) ยท (๐ดโ๐)) + (๐ก ยท (๐ถโ๐))) โง โ๐ โ (1...๐)(๐นโ๐) = (((1 โ ๐ ) ยท (๐ธโ๐)) + (๐ ยท (๐บโ๐))))) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)))) |
119 | | simp33 1212 |
. . 3
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ ๐ป โ (๐ผโ๐)) |
120 | | brcgr 27891 |
. . 3
โข (((๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐)) โง (๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (โจ๐ถ, ๐ทโฉCgrโจ๐บ, ๐ปโฉ โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2))) |
121 | 33, 81, 53, 119, 120 | syl22anc 838 |
. 2
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (โจ๐ถ, ๐ทโฉCgrโจ๐บ, ๐ปโฉ โ ฮฃ๐ โ (1...๐)(((๐ถโ๐) โ (๐ทโ๐))โ2) = ฮฃ๐ โ (1...๐)(((๐บโ๐) โ (๐ปโ๐))โ2))) |
122 | 103, 118,
121 | 3imtr4d 294 |
1
โข (((๐ โ โ โง ๐ด โ (๐ผโ๐) โง ๐ต โ (๐ผโ๐)) โง (๐ถ โ (๐ผโ๐) โง ๐ท โ (๐ผโ๐) โง ๐ธ โ (๐ผโ๐)) โง (๐น โ (๐ผโ๐) โง ๐บ โ (๐ผโ๐) โง ๐ป โ (๐ผโ๐))) โ (((๐ด โ ๐ต โง ๐ต Btwn โจ๐ด, ๐ถโฉ โง ๐น Btwn โจ๐ธ, ๐บโฉ) โง (โจ๐ด, ๐ตโฉCgrโจ๐ธ, ๐นโฉ โง โจ๐ต, ๐ถโฉCgrโจ๐น, ๐บโฉ) โง (โจ๐ด, ๐ทโฉCgrโจ๐ธ, ๐ปโฉ โง โจ๐ต, ๐ทโฉCgrโจ๐น, ๐ปโฉ)) โ โจ๐ถ, ๐ทโฉCgrโจ๐บ, ๐ปโฉ)) |