Step | Hyp | Ref
| Expression |
1 | | 00id 11335 |
. . . . 5
β’ (0 + 0) =
0 |
2 | | sum0 15611 |
. . . . . 6
β’
Ξ£π β
β
π΅ =
0 |
3 | | sum0 15611 |
. . . . . 6
β’
Ξ£π β
β
πΆ =
0 |
4 | 2, 3 | oveq12i 7370 |
. . . . 5
β’
(Ξ£π β
β
π΅ + Ξ£π β β
πΆ) = (0 + 0) |
5 | | sum0 15611 |
. . . . 5
β’
Ξ£π β
β
(π΅ + πΆ) = 0 |
6 | 1, 4, 5 | 3eqtr4ri 2772 |
. . . 4
β’
Ξ£π β
β
(π΅ + πΆ) = (Ξ£π β β
π΅ + Ξ£π β β
πΆ) |
7 | | sumeq1 15579 |
. . . 4
β’ (π΄ = β
β Ξ£π β π΄ (π΅ + πΆ) = Ξ£π β β
(π΅ + πΆ)) |
8 | | sumeq1 15579 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ π΅ = Ξ£π β β
π΅) |
9 | | sumeq1 15579 |
. . . . 5
β’ (π΄ = β
β Ξ£π β π΄ πΆ = Ξ£π β β
πΆ) |
10 | 8, 9 | oveq12d 7376 |
. . . 4
β’ (π΄ = β
β (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ) = (Ξ£π β β
π΅ + Ξ£π β β
πΆ)) |
11 | 6, 7, 10 | 3eqtr4a 2799 |
. . 3
β’ (π΄ = β
β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ)) |
12 | 11 | a1i 11 |
. 2
β’ (π β (π΄ = β
β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ))) |
13 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
14 | | nnuz 12811 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
15 | 13, 14 | eleqtrdi 2844 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
16 | | fsumadd.2 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π΅ β β) |
17 | 16 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β π΅ β β) |
18 | 17 | fmpttd 7064 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ π΅):π΄βΆβ) |
19 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
20 | | f1of 6785 |
. . . . . . . . . . 11
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
22 | | fco 6693 |
. . . . . . . . . 10
β’ (((π β π΄ β¦ π΅):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
23 | 18, 21, 22 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆβ) |
24 | 23 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) β β) |
25 | | fsumadd.3 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β πΆ β β) |
26 | 25 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β πΆ β β) |
27 | 26 | fmpttd 7064 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ πΆ):π΄βΆβ) |
28 | | fco 6693 |
. . . . . . . . . 10
β’ (((π β π΄ β¦ πΆ):π΄βΆβ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ πΆ) β π):(1...(β―βπ΄))βΆβ) |
29 | 27, 21, 28 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ πΆ) β π):(1...(β―βπ΄))βΆβ) |
30 | 29 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) β β) |
31 | 21 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (πβπ) β π΄) |
32 | | ovex 7391 |
. . . . . . . . . . . . . . 15
β’ (π΅ + πΆ) β V |
33 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ (π΅ + πΆ)) = (π β π΄ β¦ (π΅ + πΆ)) |
34 | 33 | fvmpt2 6960 |
. . . . . . . . . . . . . . 15
β’ ((π β π΄ β§ (π΅ + πΆ) β V) β ((π β π΄ β¦ (π΅ + πΆ))βπ) = (π΅ + πΆ)) |
35 | 32, 34 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β ((π β π΄ β¦ (π΅ + πΆ))βπ) = (π΅ + πΆ)) |
36 | 35 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β ((π β π΄ β¦ (π΅ + πΆ))βπ) = (π΅ + πΆ)) |
37 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π β π΄) |
38 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ π΅) = (π β π΄ β¦ π΅) |
39 | 38 | fvmpt2 6960 |
. . . . . . . . . . . . . . 15
β’ ((π β π΄ β§ π΅ β β) β ((π β π΄ β¦ π΅)βπ) = π΅) |
40 | 37, 16, 39 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) = π΅) |
41 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β¦ πΆ) = (π β π΄ β¦ πΆ) |
42 | 41 | fvmpt2 6960 |
. . . . . . . . . . . . . . 15
β’ ((π β π΄ β§ πΆ β β) β ((π β π΄ β¦ πΆ)βπ) = πΆ) |
43 | 37, 25, 42 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) = πΆ) |
44 | 40, 43 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΄) β (((π β π΄ β¦ π΅)βπ) + ((π β π΄ β¦ πΆ)βπ)) = (π΅ + πΆ)) |
45 | 36, 44 | eqtr4d 2776 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β ((π β π΄ β¦ (π΅ + πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) + ((π β π΄ β¦ πΆ)βπ))) |
46 | 45 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ (π β βπ β π΄ ((π β π΄ β¦ (π΅ + πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) + ((π β π΄ β¦ πΆ)βπ))) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β βπ β π΄ ((π β π΄ β¦ (π΅ + πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) + ((π β π΄ β¦ πΆ)βπ))) |
48 | | nffvmpt1 6854 |
. . . . . . . . . . . 12
β’
β²π((π β π΄ β¦ (π΅ + πΆ))β(πβπ)) |
49 | | nffvmpt1 6854 |
. . . . . . . . . . . . 13
β’
β²π((π β π΄ β¦ π΅)β(πβπ)) |
50 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π
+ |
51 | | nffvmpt1 6854 |
. . . . . . . . . . . . 13
β’
β²π((π β π΄ β¦ πΆ)β(πβπ)) |
52 | 49, 50, 51 | nfov 7388 |
. . . . . . . . . . . 12
β’
β²π(((π β π΄ β¦ π΅)β(πβπ)) + ((π β π΄ β¦ πΆ)β(πβπ))) |
53 | 48, 52 | nfeq 2917 |
. . . . . . . . . . 11
β’
β²π((π β π΄ β¦ (π΅ + πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) + ((π β π΄ β¦ πΆ)β(πβπ))) |
54 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β ((π β π΄ β¦ (π΅ + πΆ))βπ) = ((π β π΄ β¦ (π΅ + πΆ))β(πβπ))) |
55 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
56 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((π β π΄ β¦ πΆ)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
57 | 55, 56 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (((π β π΄ β¦ π΅)βπ) + ((π β π΄ β¦ πΆ)βπ)) = (((π β π΄ β¦ π΅)β(πβπ)) + ((π β π΄ β¦ πΆ)β(πβπ)))) |
58 | 54, 57 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π = (πβπ) β (((π β π΄ β¦ (π΅ + πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) + ((π β π΄ β¦ πΆ)βπ)) β ((π β π΄ β¦ (π΅ + πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) + ((π β π΄ β¦ πΆ)β(πβπ))))) |
59 | 53, 58 | rspc 3568 |
. . . . . . . . . 10
β’ ((πβπ) β π΄ β (βπ β π΄ ((π β π΄ β¦ (π΅ + πΆ))βπ) = (((π β π΄ β¦ π΅)βπ) + ((π β π΄ β¦ πΆ)βπ)) β ((π β π΄ β¦ (π΅ + πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) + ((π β π΄ β¦ πΆ)β(πβπ))))) |
60 | 31, 47, 59 | sylc 65 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((π β π΄ β¦ (π΅ + πΆ))β(πβπ)) = (((π β π΄ β¦ π΅)β(πβπ)) + ((π β π΄ β¦ πΆ)β(πβπ)))) |
61 | | fvco3 6941 |
. . . . . . . . . 10
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ + πΆ)) β π)βπ) = ((π β π΄ β¦ (π΅ + πΆ))β(πβπ))) |
62 | 21, 61 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ + πΆ)) β π)βπ) = ((π β π΄ β¦ (π΅ + πΆ))β(πβπ))) |
63 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
64 | 21, 63 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
65 | | fvco3 6941 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
66 | 21, 65 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ πΆ) β π)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
67 | 64, 66 | oveq12d 7376 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β ((((π β π΄ β¦ π΅) β π)βπ) + (((π β π΄ β¦ πΆ) β π)βπ)) = (((π β π΄ β¦ π΅)β(πβπ)) + ((π β π΄ β¦ πΆ)β(πβπ)))) |
68 | 60, 62, 67 | 3eqtr4d 2783 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β (1...(β―βπ΄))) β (((π β π΄ β¦ (π΅ + πΆ)) β π)βπ) = ((((π β π΄ β¦ π΅) β π)βπ) + (((π β π΄ β¦ πΆ) β π)βπ))) |
69 | 15, 24, 30, 68 | seradd 13956 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (seq1( + , ((π β π΄ β¦ (π΅ + πΆ)) β π))β(β―βπ΄)) = ((seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄)) + (seq1( + , ((π β π΄ β¦ πΆ) β π))β(β―βπ΄)))) |
70 | | fveq2 6843 |
. . . . . . . 8
β’ (π = (πβπ) β ((π β π΄ β¦ (π΅ + πΆ))βπ) = ((π β π΄ β¦ (π΅ + πΆ))β(πβπ))) |
71 | 17, 26 | addcld 11179 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β (π΅ + πΆ) β β) |
72 | 71 | fmpttd 7064 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (π β π΄ β¦ (π΅ + πΆ)):π΄βΆβ) |
73 | 72 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ (π΅ + πΆ))βπ) β β) |
74 | 70, 13, 19, 73, 62 | fsum 15610 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ (π΅ + πΆ))βπ) = (seq1( + , ((π β π΄ β¦ (π΅ + πΆ)) β π))β(β―βπ΄))) |
75 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ))) |
76 | 18 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
77 | 75, 13, 19, 76, 64 | fsum 15610 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
78 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΄ β¦ πΆ)βπ) = ((π β π΄ β¦ πΆ)β(πβπ))) |
79 | 27 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) β β) |
80 | 78, 13, 19, 79, 66 | fsum 15610 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = (seq1( + , ((π β π΄ β¦ πΆ) β π))β(β―βπ΄))) |
81 | 77, 80 | oveq12d 7376 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) + Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ)) = ((seq1( + , ((π β π΄ β¦ π΅) β π))β(β―βπ΄)) + (seq1( + , ((π β π΄ β¦ πΆ) β π))β(β―βπ΄)))) |
82 | 69, 74, 81 | 3eqtr4d 2783 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ ((π β π΄ β¦ (π΅ + πΆ))βπ) = (Ξ£π β π΄ ((π β π΄ β¦ π΅)βπ) + Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ))) |
83 | | sumfc 15599 |
. . . . . 6
β’
Ξ£π β
π΄ ((π β π΄ β¦ (π΅ + πΆ))βπ) = Ξ£π β π΄ (π΅ + πΆ) |
84 | | sumfc 15599 |
. . . . . . 7
β’
Ξ£π β
π΄ ((π β π΄ β¦ π΅)βπ) = Ξ£π β π΄ π΅ |
85 | | sumfc 15599 |
. . . . . . 7
β’
Ξ£π β
π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΄ πΆ |
86 | 84, 85 | oveq12i 7370 |
. . . . . 6
β’
(Ξ£π β
π΄ ((π β π΄ β¦ π΅)βπ) + Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ)) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ) |
87 | 82, 83, 86 | 3eqtr3g 2796 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ)) |
88 | 87 | expr 458 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ))) |
89 | 88 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ))) |
90 | 89 | expimpd 455 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ))) |
91 | | fsumadd.1 |
. . 3
β’ (π β π΄ β Fin) |
92 | | fz1f1o 15600 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
93 | 91, 92 | syl 17 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
94 | 12, 90, 93 | mpjaod 859 |
1
β’ (π β Ξ£π β π΄ (π΅ + πΆ) = (Ξ£π β π΄ π΅ + Ξ£π β π΄ πΆ)) |