Step | Hyp | Ref
| Expression |
1 | | binomcxp.a |
. . 3
โข (๐ โ ๐ด โ
โ+) |
2 | | binomcxp.b |
. . 3
โข (๐ โ ๐ต โ โ) |
3 | | binomcxp.lt |
. . 3
โข (๐ โ (absโ๐ต) < (absโ๐ด)) |
4 | | binomcxp.c |
. . 3
โข (๐ โ ๐ถ โ โ) |
5 | 1, 2, 3, 4 | binomcxplemnn0 42703 |
. 2
โข ((๐ โง ๐ถ โ โ0) โ ((๐ด + ๐ต)โ๐๐ถ) = ฮฃ๐ โ โ0 ((๐ถC๐๐) ยท ((๐ดโ๐(๐ถ โ ๐)) ยท (๐ตโ๐)))) |
6 | | eqid 2737 |
. . 3
โข (๐ โ โ0
โฆ (๐ถC๐๐)) = (๐ โ โ0 โฆ (๐ถC๐๐)) |
7 | | fveq2 6847 |
. . . . . 6
โข (๐ฅ = ๐ โ ((๐ โ โ0 โฆ (๐ถC๐๐))โ๐ฅ) = ((๐ โ โ0 โฆ (๐ถC๐๐))โ๐)) |
8 | | oveq2 7370 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐โ๐ฅ) = (๐โ๐)) |
9 | 7, 8 | oveq12d 7380 |
. . . . 5
โข (๐ฅ = ๐ โ (((๐ โ โ0 โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ)) = (((๐ โ โ0 โฆ (๐ถC๐๐))โ๐) ยท (๐โ๐))) |
10 | 9 | cbvmptv 5223 |
. . . 4
โข (๐ฅ โ โ0
โฆ (((๐ โ
โ0 โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))) = (๐ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐) ยท (๐โ๐))) |
11 | 10 | mpteq2i 5215 |
. . 3
โข (๐ โ โ โฆ (๐ฅ โ โ0
โฆ (((๐ โ
โ0 โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ)))) = (๐ โ โ โฆ (๐ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐) ยท (๐โ๐)))) |
12 | | eqid 2737 |
. . 3
โข
sup({๐ โ
โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< ) = sup({๐ โ
โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< ) |
13 | | id 22 |
. . . . . . 7
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
14 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ฆ = ๐ โ (๐ถC๐๐ฆ) = (๐ถC๐๐)) |
15 | 14 | cbvmptv 5223 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โฆ (๐ถC๐๐ฆ)) = (๐ โ โ0 โฆ (๐ถC๐๐)) |
16 | 15 | a1i 11 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (๐ฆ โ โ0 โฆ (๐ถC๐๐ฆ)) = (๐ โ โ0 โฆ (๐ถC๐๐))) |
17 | 16, 13 | fveq12d 6854 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐ฆ โ โ0 โฆ (๐ถC๐๐ฆ))โ๐ฅ) = ((๐ โ โ0 โฆ (๐ถC๐๐))โ๐)) |
18 | 13, 17 | oveq12d 7380 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ ยท ((๐ฆ โ โ0 โฆ (๐ถC๐๐ฆ))โ๐ฅ)) = (๐ ยท ((๐ โ โ0 โฆ (๐ถC๐๐))โ๐))) |
19 | | oveq1 7369 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ฅ โ 1) = (๐ โ 1)) |
20 | 19 | oveq2d 7378 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐โ(๐ฅ โ 1)) = (๐โ(๐ โ 1))) |
21 | 18, 20 | oveq12d 7380 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐ฅ ยท ((๐ฆ โ โ0 โฆ (๐ถC๐๐ฆ))โ๐ฅ)) ยท (๐โ(๐ฅ โ 1))) = ((๐ ยท ((๐ โ โ0 โฆ (๐ถC๐๐))โ๐)) ยท (๐โ(๐ โ 1)))) |
22 | 21 | cbvmptv 5223 |
. . . 4
โข (๐ฅ โ โ โฆ ((๐ฅ ยท ((๐ฆ โ โ0 โฆ (๐ถC๐๐ฆ))โ๐ฅ)) ยท (๐โ(๐ฅ โ 1)))) = (๐ โ โ โฆ ((๐ ยท ((๐ โ โ0 โฆ (๐ถC๐๐))โ๐)) ยท (๐โ(๐ โ 1)))) |
23 | 22 | mpteq2i 5215 |
. . 3
โข (๐ โ โ โฆ (๐ฅ โ โ โฆ ((๐ฅ ยท ((๐ฆ โ โ0 โฆ (๐ถC๐๐ฆ))โ๐ฅ)) ยท (๐โ(๐ฅ โ 1))))) = (๐ โ โ โฆ (๐ โ โ โฆ ((๐ ยท ((๐ โ โ0 โฆ (๐ถC๐๐))โ๐)) ยท (๐โ(๐ โ 1))))) |
24 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ (๐ถC๐๐ฅ) = (๐ถC๐๐)) |
25 | 24 | cbvmptv 5223 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ0
โฆ (๐ถC๐๐ฅ)) = (๐ โ โ0 โฆ (๐ถC๐๐)) |
26 | 25 | fveq1i 6848 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ0
โฆ (๐ถC๐๐ฅ))โ๐ฅ) = ((๐ โ โ0 โฆ (๐ถC๐๐))โ๐ฅ) |
27 | 26 | oveq1i 7372 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ0
โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ)) = (((๐ โ โ0 โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ)) |
28 | 27 | mpteq2i 5215 |
. . . . . . . . . . 11
โข (๐ฅ โ โ0
โฆ (((๐ฅ โ
โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))) = (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))) |
29 | 28 | mpteq2i 5215 |
. . . . . . . . . 10
โข (๐ โ โ โฆ (๐ฅ โ โ0
โฆ (((๐ฅ โ
โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ)))) = (๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ)))) |
30 | 29 | fveq1i 6848 |
. . . . . . . . 9
โข ((๐ โ โ โฆ (๐ฅ โ โ0
โฆ (((๐ฅ โ
โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐) = ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐) |
31 | | seqeq3 13918 |
. . . . . . . . 9
โข (((๐ โ โ โฆ (๐ฅ โ โ0
โฆ (((๐ฅ โ
โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐) = ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐) โ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ฅ โ โ0
โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) = seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . 8
โข seq0( + ,
((๐ โ โ โฆ
(๐ฅ โ
โ0 โฆ (((๐ฅ โ โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) = seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) |
33 | 32 | eleq1i 2829 |
. . . . . . 7
โข (seq0( +
, ((๐ โ โ
โฆ (๐ฅ โ
โ0 โฆ (((๐ฅ โ โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ โ seq0( + ,
((๐ โ โ โฆ
(๐ฅ โ
โ0 โฆ (((๐ โ โ0 โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ ) |
34 | 33 | rabbii 3416 |
. . . . . 6
โข {๐ โ โ โฃ seq0( +
, ((๐ โ โ
โฆ (๐ฅ โ
โ0 โฆ (((๐ฅ โ โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ } = {๐ โ โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0
โฆ (((๐ โ
โ0 โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ } |
35 | 34 | supeq1i 9390 |
. . . . 5
โข
sup({๐ โ
โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ฅ โ โ0
โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< ) = sup({๐ โ
โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< ) |
36 | 35 | oveq2i 7373 |
. . . 4
โข
(0[,)sup({๐ โ
โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ฅ โ โ0
โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< )) = (0[,)sup({๐
โ โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< )) |
37 | 36 | imaeq2i 6016 |
. . 3
โข (โกabs โ (0[,)sup({๐ โ โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0
โฆ (((๐ฅ โ
โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< ))) = (โกabs โ
(0[,)sup({๐ โ โ
โฃ seq0( + , ((๐
โ โ โฆ (๐ฅ
โ โ0 โฆ (((๐ โ โ0 โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< ))) |
38 | | eqid 2737 |
. . 3
โข (๐ โ (โกabs โ (0[,)sup({๐ โ โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0
โฆ (((๐ฅ โ
โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< ))) โฆ ฮฃ๐
โ โ0 (((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)โ๐)) = (๐ โ (โกabs โ (0[,)sup({๐ โ โ โฃ seq0( + , ((๐ โ โ โฆ (๐ฅ โ โ0
โฆ (((๐ฅ โ
โ0 โฆ (๐ถC๐๐ฅ))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)) โ dom โ }, โ*,
< ))) โฆ ฮฃ๐
โ โ0 (((๐ โ โ โฆ (๐ฅ โ โ0 โฆ (((๐ โ โ0
โฆ (๐ถC๐๐))โ๐ฅ) ยท (๐โ๐ฅ))))โ๐)โ๐)) |
39 | 1, 2, 3, 4, 6, 11,
12, 23, 37, 38 | binomcxplemnotnn0 42710 |
. 2
โข ((๐ โง ยฌ ๐ถ โ โ0) โ ((๐ด + ๐ต)โ๐๐ถ) = ฮฃ๐ โ โ0 ((๐ถC๐๐) ยท ((๐ดโ๐(๐ถ โ ๐)) ยท (๐ตโ๐)))) |
40 | 5, 39 | pm2.61dan 812 |
1
โข (๐ โ ((๐ด + ๐ต)โ๐๐ถ) = ฮฃ๐ โ โ0 ((๐ถC๐๐) ยท ((๐ดโ๐(๐ถ โ ๐)) ยท (๐ตโ๐)))) |