Step | Hyp | Ref
| Expression |
1 | | binomcxp.a |
. . . . . . . 8
β’ (π β π΄ β
β+) |
2 | 1 | rpcnd 12967 |
. . . . . . 7
β’ (π β π΄ β β) |
3 | | binomcxp.b |
. . . . . . . 8
β’ (π β π΅ β β) |
4 | 3 | recnd 11191 |
. . . . . . 7
β’ (π β π΅ β β) |
5 | | binom 15723 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β0)
β ((π΄ + π΅)βπΆ) = Ξ£π β (0...πΆ)((πΆCπ) Β· ((π΄β(πΆ β π)) Β· (π΅βπ)))) |
6 | 5 | 3expia 1122 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β (πΆ β β0
β ((π΄ + π΅)βπΆ) = Ξ£π β (0...πΆ)((πΆCπ) Β· ((π΄β(πΆ β π)) Β· (π΅βπ))))) |
7 | 2, 4, 6 | syl2anc 585 |
. . . . . 6
β’ (π β (πΆ β β0 β ((π΄ + π΅)βπΆ) = Ξ£π β (0...πΆ)((πΆCπ) Β· ((π΄β(πΆ β π)) Β· (π΅βπ))))) |
8 | 7 | imp 408 |
. . . . 5
β’ ((π β§ πΆ β β0) β ((π΄ + π΅)βπΆ) = Ξ£π β (0...πΆ)((πΆCπ) Β· ((π΄β(πΆ β π)) Β· (π΅βπ)))) |
9 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΆ β β0) β π΄ β
β) |
10 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΆ β β0) β π΅ β
β) |
11 | 9, 10 | addcld 11182 |
. . . . . 6
β’ ((π β§ πΆ β β0) β (π΄ + π΅) β β) |
12 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΆ β β0) β πΆ β
β0) |
13 | | cxpexp 26046 |
. . . . . 6
β’ (((π΄ + π΅) β β β§ πΆ β β0) β ((π΄ + π΅)βππΆ) = ((π΄ + π΅)βπΆ)) |
14 | 11, 12, 13 | syl2anc 585 |
. . . . 5
β’ ((π β§ πΆ β β0) β ((π΄ + π΅)βππΆ) = ((π΄ + π΅)βπΆ)) |
15 | | elfznn0 13543 |
. . . . . . . 8
β’ (π β (0...πΆ) β π β β0) |
16 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ πΆ β β0) β§ π β β0)
β πΆ β
β0) |
17 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ πΆ β β0) β§ π β β0)
β π β
β0) |
18 | 16, 17 | bccbc 42717 |
. . . . . . . 8
β’ (((π β§ πΆ β β0) β§ π β β0)
β (πΆCππ) = (πΆCπ)) |
19 | 15, 18 | sylan2 594 |
. . . . . . 7
β’ (((π β§ πΆ β β0) β§ π β (0...πΆ)) β (πΆCππ) = (πΆCπ)) |
20 | 2 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ πΆ β β0) β§ π β (0...πΆ)) β π΄ β β) |
21 | | elfzle2 13454 |
. . . . . . . . . . 11
β’ (π β (0...πΆ) β π β€ πΆ) |
22 | 21 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β0) β§ π β (0...πΆ)) β π β€ πΆ) |
23 | | nn0sub 12471 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ πΆ β
β0) β (π β€ πΆ β (πΆ β π) β
β0)) |
24 | 23 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((πΆ β β0
β§ π β
β0) β (π β€ πΆ β (πΆ β π) β
β0)) |
25 | 24 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β β0) β§ π β β0)
β (π β€ πΆ β (πΆ β π) β
β0)) |
26 | 15, 25 | sylan2 594 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β0) β§ π β (0...πΆ)) β (π β€ πΆ β (πΆ β π) β
β0)) |
27 | 22, 26 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ πΆ β β0) β§ π β (0...πΆ)) β (πΆ β π) β
β0) |
28 | | cxpexp 26046 |
. . . . . . . . 9
β’ ((π΄ β β β§ (πΆ β π) β β0) β (π΄βπ(πΆ β π)) = (π΄β(πΆ β π))) |
29 | 20, 27, 28 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ πΆ β β0) β§ π β (0...πΆ)) β (π΄βπ(πΆ β π)) = (π΄β(πΆ β π))) |
30 | 29 | oveq1d 7376 |
. . . . . . 7
β’ (((π β§ πΆ β β0) β§ π β (0...πΆ)) β ((π΄βπ(πΆ β π)) Β· (π΅βπ)) = ((π΄β(πΆ β π)) Β· (π΅βπ))) |
31 | 19, 30 | oveq12d 7379 |
. . . . . 6
β’ (((π β§ πΆ β β0) β§ π β (0...πΆ)) β ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = ((πΆCπ) Β· ((π΄β(πΆ β π)) Β· (π΅βπ)))) |
32 | 31 | sumeq2dv 15596 |
. . . . 5
β’ ((π β§ πΆ β β0) β
Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = Ξ£π β (0...πΆ)((πΆCπ) Β· ((π΄β(πΆ β π)) Β· (π΅βπ)))) |
33 | 8, 14, 32 | 3eqtr4d 2783 |
. . . 4
β’ ((π β§ πΆ β β0) β ((π΄ + π΅)βππΆ) = Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
34 | | binomcxp.c |
. . . . . 6
β’ (π β πΆ β β) |
35 | 34 | adantr 482 |
. . . . 5
β’ ((π β§ πΆ β β0) β πΆ β
β) |
36 | 11, 35 | cxpcld 26086 |
. . . 4
β’ ((π β§ πΆ β β0) β ((π΄ + π΅)βππΆ) β β) |
37 | 33, 36 | eqeltrrd 2835 |
. . 3
β’ ((π β§ πΆ β β0) β
Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) β β) |
38 | 37 | addridd 11363 |
. 2
β’ ((π β§ πΆ β β0) β
(Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) + 0) = Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
39 | | nn0uz 12813 |
. . . 4
β’
β0 = (β€β₯β0) |
40 | | eqid 2733 |
. . . 4
β’
(β€β₯β(πΆ + 1)) =
(β€β₯β(πΆ + 1)) |
41 | | 1nn0 12437 |
. . . . . 6
β’ 1 β
β0 |
42 | 41 | a1i 11 |
. . . . 5
β’ ((π β§ πΆ β β0) β 1 β
β0) |
43 | 12, 42 | nn0addcld 12485 |
. . . 4
β’ ((π β§ πΆ β β0) β (πΆ + 1) β
β0) |
44 | | eqidd 2734 |
. . . . 5
β’ (((π β§ πΆ β β0) β§ π β β0)
β (π β
β0 β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) = (π β β0 β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))) |
45 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ πΆ β β0) β§ π β β0)
β§ π = π) β π = π) |
46 | 45 | oveq2d 7377 |
. . . . . 6
β’ ((((π β§ πΆ β β0) β§ π β β0)
β§ π = π) β (πΆCππ) = (πΆCππ)) |
47 | 45 | oveq2d 7377 |
. . . . . . . 8
β’ ((((π β§ πΆ β β0) β§ π β β0)
β§ π = π) β (πΆ β π) = (πΆ β π)) |
48 | 47 | oveq2d 7377 |
. . . . . . 7
β’ ((((π β§ πΆ β β0) β§ π β β0)
β§ π = π) β (π΄βπ(πΆ β π)) = (π΄βπ(πΆ β π))) |
49 | 45 | oveq2d 7377 |
. . . . . . 7
β’ ((((π β§ πΆ β β0) β§ π β β0)
β§ π = π) β (π΅βπ) = (π΅βπ)) |
50 | 48, 49 | oveq12d 7379 |
. . . . . 6
β’ ((((π β§ πΆ β β0) β§ π β β0)
β§ π = π) β ((π΄βπ(πΆ β π)) Β· (π΅βπ)) = ((π΄βπ(πΆ β π)) Β· (π΅βπ))) |
51 | 46, 50 | oveq12d 7379 |
. . . . 5
β’ ((((π β§ πΆ β β0) β§ π β β0)
β§ π = π) β ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
52 | 34 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ πΆ β β0) β§ π β β0)
β πΆ β
β) |
53 | 52, 17 | bcccl 42711 |
. . . . . 6
β’ (((π β§ πΆ β β0) β§ π β β0)
β (πΆCππ) β β) |
54 | 2 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ πΆ β β0) β§ π β β0)
β π΄ β
β) |
55 | 17 | nn0cnd 12483 |
. . . . . . . . 9
β’ (((π β§ πΆ β β0) β§ π β β0)
β π β
β) |
56 | 52, 55 | subcld 11520 |
. . . . . . . 8
β’ (((π β§ πΆ β β0) β§ π β β0)
β (πΆ β π) β
β) |
57 | 54, 56 | cxpcld 26086 |
. . . . . . 7
β’ (((π β§ πΆ β β0) β§ π β β0)
β (π΄βπ(πΆ β π)) β β) |
58 | 4 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ πΆ β β0) β§ π β β0)
β π΅ β
β) |
59 | 58, 17 | expcld 14060 |
. . . . . . 7
β’ (((π β§ πΆ β β0) β§ π β β0)
β (π΅βπ) β
β) |
60 | 57, 59 | mulcld 11183 |
. . . . . 6
β’ (((π β§ πΆ β β0) β§ π β β0)
β ((π΄βπ(πΆ β π)) Β· (π΅βπ)) β β) |
61 | 53, 60 | mulcld 11183 |
. . . . 5
β’ (((π β§ πΆ β β0) β§ π β β0)
β ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) β β) |
62 | 44, 51, 17, 61 | fvmptd 6959 |
. . . 4
β’ (((π β§ πΆ β β0) β§ π β β0)
β ((π β
β0 β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ) = ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
63 | | peano2nn0 12461 |
. . . . . 6
β’ (πΆ β β0
β (πΆ + 1) β
β0) |
64 | 63 | adantl 483 |
. . . . 5
β’ ((π β§ πΆ β β0) β (πΆ + 1) β
β0) |
65 | | c0ex 11157 |
. . . . . . . . 9
β’ 0 β
V |
66 | 65 | fconst 6732 |
. . . . . . . 8
β’
(β0 Γ
{0}):β0βΆ{0} |
67 | 66 | a1i 11 |
. . . . . . 7
β’ ((π β§ πΆ β β0) β
(β0 Γ
{0}):β0βΆ{0}) |
68 | | 0red 11166 |
. . . . . . . 8
β’ ((π β§ πΆ β β0) β 0 β
β) |
69 | 68 | snssd 4773 |
. . . . . . 7
β’ ((π β§ πΆ β β0) β {0}
β β) |
70 | 67, 69 | fssd 6690 |
. . . . . 6
β’ ((π β§ πΆ β β0) β
(β0 Γ
{0}):β0βΆβ) |
71 | 70 | ffvelcdmda 7039 |
. . . . 5
β’ (((π β§ πΆ β β0) β§ π β β0)
β ((β0 Γ {0})βπ) β β) |
72 | 62, 61 | eqeltrd 2834 |
. . . . 5
β’ (((π β§ πΆ β β0) β§ π β β0)
β ((π β
β0 β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ) β β) |
73 | | climrel 15383 |
. . . . . . 7
β’ Rel
β |
74 | 39 | xpeq1i 5663 |
. . . . . . . . 9
β’
(β0 Γ {0}) = ((β€β₯β0)
Γ {0}) |
75 | | seqeq3 13920 |
. . . . . . . . 9
β’
((β0 Γ {0}) = ((β€β₯β0)
Γ {0}) β seq0( + , (β0 Γ {0})) = seq0( + ,
((β€β₯β0) Γ {0}))) |
76 | 74, 75 | ax-mp 5 |
. . . . . . . 8
β’ seq0( + ,
(β0 Γ {0})) = seq0( + ,
((β€β₯β0) Γ {0})) |
77 | | 0z 12518 |
. . . . . . . . 9
β’ 0 β
β€ |
78 | | serclim0 15468 |
. . . . . . . . 9
β’ (0 β
β€ β seq0( + , ((β€β₯β0) Γ {0}))
β 0) |
79 | 77, 78 | ax-mp 5 |
. . . . . . . 8
β’ seq0( + ,
((β€β₯β0) Γ {0})) β 0 |
80 | 76, 79 | eqbrtri 5130 |
. . . . . . 7
β’ seq0( + ,
(β0 Γ {0})) β 0 |
81 | | releldm 5903 |
. . . . . . 7
β’ ((Rel
β β§ seq0( + , (β0 Γ {0})) β 0) β
seq0( + , (β0 Γ {0})) β dom β
) |
82 | 73, 80, 81 | mp2an 691 |
. . . . . 6
β’ seq0( + ,
(β0 Γ {0})) β dom β |
83 | 82 | a1i 11 |
. . . . 5
β’ ((π β§ πΆ β β0) β seq0( +
, (β0 Γ {0})) β dom β ) |
84 | | eluznn0 12850 |
. . . . . . . . . . . 12
β’ (((πΆ + 1) β β0
β§ π β
(β€β₯β(πΆ + 1))) β π β β0) |
85 | 64, 84 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β π β β0) |
86 | 85, 62 | syldan 592 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β ((π β β0 β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ) = ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
87 | | 0zd 12519 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β 0 β
β€) |
88 | 85 | nn0zd 12533 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β π β β€) |
89 | | 1zzd 12542 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β 1 β
β€) |
90 | 88, 89 | zsubcld 12620 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (π β 1) β β€) |
91 | 12 | nn0zd 12533 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΆ β β0) β πΆ β
β€) |
92 | 91 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β πΆ β β€) |
93 | 12 | nn0ge0d 12484 |
. . . . . . . . . . . . . . 15
β’ ((π β§ πΆ β β0) β 0 β€
πΆ) |
94 | 93 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β 0 β€ πΆ) |
95 | | eluzle 12784 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β(πΆ + 1)) β (πΆ + 1) β€ π) |
96 | 95 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (πΆ + 1) β€ π) |
97 | 92 | zred 12615 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β πΆ β β) |
98 | | 1red 11164 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β 1 β
β) |
99 | 85 | nn0red 12482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β π β β) |
100 | | leaddsub 11639 |
. . . . . . . . . . . . . . . 16
β’ ((πΆ β β β§ 1 β
β β§ π β
β) β ((πΆ + 1)
β€ π β πΆ β€ (π β 1))) |
101 | 97, 98, 99, 100 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β ((πΆ + 1) β€ π β πΆ β€ (π β 1))) |
102 | 96, 101 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β πΆ β€ (π β 1)) |
103 | 87, 90, 92, 94, 102 | elfzd 13441 |
. . . . . . . . . . . . 13
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β πΆ β (0...(π β 1))) |
104 | 34 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β πΆ β β) |
105 | 104, 85 | bcc0 42712 |
. . . . . . . . . . . . 13
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β ((πΆCππ) = 0 β πΆ β (0...(π β 1)))) |
106 | 103, 105 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (πΆCππ) = 0) |
107 | 106 | oveq1d 7376 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = (0 Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
108 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β π΄ β β) |
109 | | eluzelcn 12783 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β(πΆ + 1)) β π β β) |
110 | 109 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β π β β) |
111 | 104, 110 | subcld 11520 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (πΆ β π) β β) |
112 | 108, 111 | cxpcld 26086 |
. . . . . . . . . . . . 13
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (π΄βπ(πΆ β π)) β β) |
113 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β π΅ β β) |
114 | 113, 85 | expcld 14060 |
. . . . . . . . . . . . 13
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (π΅βπ) β β) |
115 | 112, 114 | mulcld 11183 |
. . . . . . . . . . . 12
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β ((π΄βπ(πΆ β π)) Β· (π΅βπ)) β β) |
116 | 115 | mul02d 11361 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (0 Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = 0) |
117 | 107, 116 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = 0) |
118 | 86, 117 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β ((π β β0 β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ) = 0) |
119 | 118 | abs00bd 15185 |
. . . . . . . 8
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (absβ((π β β0
β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ)) = 0) |
120 | | 0re 11165 |
. . . . . . . 8
β’ 0 β
β |
121 | 119, 120 | eqeltrdi 2842 |
. . . . . . 7
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (absβ((π β β0
β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ)) β β) |
122 | | eqle 11265 |
. . . . . . 7
β’
(((absβ((π
β β0 β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ)) β β β§ (absβ((π β β0
β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ)) = 0) β (absβ((π β β0
β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ)) β€ 0) |
123 | 121, 119,
122 | syl2anc 585 |
. . . . . 6
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (absβ((π β β0
β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ)) β€ 0) |
124 | 71 | recnd 11191 |
. . . . . . . 8
β’ (((π β§ πΆ β β0) β§ π β β0)
β ((β0 Γ {0})βπ) β β) |
125 | 85, 124 | syldan 592 |
. . . . . . 7
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β ((β0 Γ
{0})βπ) β
β) |
126 | 125 | mul02d 11361 |
. . . . . 6
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (0 Β·
((β0 Γ {0})βπ)) = 0) |
127 | 123, 126 | breqtrrd 5137 |
. . . . 5
β’ (((π β§ πΆ β β0) β§ π β
(β€β₯β(πΆ + 1))) β (absβ((π β β0
β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))βπ)) β€ (0 Β· ((β0
Γ {0})βπ))) |
128 | 39, 64, 71, 72, 83, 68, 127 | cvgcmpce 15711 |
. . . 4
β’ ((π β§ πΆ β β0) β seq0( +
, (π β
β0 β¦ ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))) β dom β ) |
129 | 39, 40, 43, 62, 61, 128 | isumsplit 15733 |
. . 3
β’ ((π β§ πΆ β β0) β
Ξ£π β
β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = (Ξ£π β (0...((πΆ + 1) β 1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) + Ξ£π β (β€β₯β(πΆ + 1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))) |
130 | | 1cnd 11158 |
. . . . . . 7
β’ ((π β§ πΆ β β0) β 1 β
β) |
131 | 35, 130 | pncand 11521 |
. . . . . 6
β’ ((π β§ πΆ β β0) β ((πΆ + 1) β 1) = πΆ) |
132 | 131 | oveq2d 7377 |
. . . . 5
β’ ((π β§ πΆ β β0) β
(0...((πΆ + 1) β 1)) =
(0...πΆ)) |
133 | 132 | sumeq1d 15594 |
. . . 4
β’ ((π β§ πΆ β β0) β
Ξ£π β
(0...((πΆ + 1) β
1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |
134 | 133 | oveq1d 7376 |
. . 3
β’ ((π β§ πΆ β β0) β
(Ξ£π β
(0...((πΆ + 1) β
1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) + Ξ£π β (β€β₯β(πΆ + 1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) = (Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) + Ξ£π β (β€β₯β(πΆ + 1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))))) |
135 | 117 | sumeq2dv 15596 |
. . . . 5
β’ ((π β§ πΆ β β0) β
Ξ£π β
(β€β₯β(πΆ + 1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = Ξ£π β (β€β₯β(πΆ + 1))0) |
136 | | ssid 3970 |
. . . . . . 7
β’
(β€β₯β(πΆ + 1)) β
(β€β₯β(πΆ + 1)) |
137 | 136 | orci 864 |
. . . . . 6
β’
((β€β₯β(πΆ + 1)) β
(β€β₯β(πΆ + 1)) β¨
(β€β₯β(πΆ + 1)) β Fin) |
138 | | sumz 15615 |
. . . . . 6
β’
(((β€β₯β(πΆ + 1)) β
(β€β₯β(πΆ + 1)) β¨
(β€β₯β(πΆ + 1)) β Fin) β Ξ£π β
(β€β₯β(πΆ + 1))0 = 0) |
139 | 137, 138 | ax-mp 5 |
. . . . 5
β’
Ξ£π β
(β€β₯β(πΆ + 1))0 = 0 |
140 | 135, 139 | eqtrdi 2789 |
. . . 4
β’ ((π β§ πΆ β β0) β
Ξ£π β
(β€β₯β(πΆ + 1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = 0) |
141 | 140 | oveq2d 7377 |
. . 3
β’ ((π β§ πΆ β β0) β
(Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) + Ξ£π β (β€β₯β(πΆ + 1))((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) = (Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) + 0)) |
142 | 129, 134,
141 | 3eqtrd 2777 |
. 2
β’ ((π β§ πΆ β β0) β
Ξ£π β
β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) = (Ξ£π β (0...πΆ)((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ))) + 0)) |
143 | 38, 142, 33 | 3eqtr4rd 2784 |
1
β’ ((π β§ πΆ β β0) β ((π΄ + π΅)βππΆ) = Ξ£π β β0 ((πΆCππ) Β· ((π΄βπ(πΆ β π)) Β· (π΅βπ)))) |