Step | Hyp | Ref
| Expression |
1 | | iblsplit.3 |
. . . 4
β’ ((π β§ π₯ β π) β πΆ β β) |
2 | 1 | fmpttd 7068 |
. . 3
β’ (π β (π₯ β π β¦ πΆ):πβΆβ) |
3 | | ssun1 4137 |
. . . . . 6
β’ π΄ β (π΄ βͺ π΅) |
4 | | iblsplit.2 |
. . . . . 6
β’ (π β π = (π΄ βͺ π΅)) |
5 | 3, 4 | sseqtrrid 4002 |
. . . . 5
β’ (π β π΄ β π) |
6 | 5 | resmptd 5999 |
. . . 4
β’ (π β ((π₯ β π β¦ πΆ) βΎ π΄) = (π₯ β π΄ β¦ πΆ)) |
7 | | iblsplit.4 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ πΆ) β
πΏ1) |
8 | | eqidd 2738 |
. . . . . . 7
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ¦)))), (ββ(πΆ / (iβπ¦))), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ¦)))), (ββ(πΆ / (iβπ¦))), 0))) |
9 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β (ββ(πΆ / (iβπ¦))) = (ββ(πΆ / (iβπ¦)))) |
10 | 5 | sseld 3948 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β π₯ β π)) |
11 | 10 | imdistani 570 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (π β§ π₯ β π)) |
12 | 11, 1 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β πΆ β β) |
13 | 8, 9, 12 | isibl2 25147 |
. . . . . 6
β’ (π β ((π₯ β π΄ β¦ πΆ) β πΏ1 β
((π₯ β π΄ β¦ πΆ) β MblFn β§ βπ¦ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ¦)))), (ββ(πΆ / (iβπ¦))), 0))) β β))) |
14 | 7, 13 | mpbid 231 |
. . . . 5
β’ (π β ((π₯ β π΄ β¦ πΆ) β MblFn β§ βπ¦ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ¦)))), (ββ(πΆ / (iβπ¦))), 0))) β β)) |
15 | 14 | simpld 496 |
. . . 4
β’ (π β (π₯ β π΄ β¦ πΆ) β MblFn) |
16 | 6, 15 | eqeltrd 2838 |
. . 3
β’ (π β ((π₯ β π β¦ πΆ) βΎ π΄) β MblFn) |
17 | | ssun2 4138 |
. . . . . 6
β’ π΅ β (π΄ βͺ π΅) |
18 | 17, 4 | sseqtrrid 4002 |
. . . . 5
β’ (π β π΅ β π) |
19 | 18 | resmptd 5999 |
. . . 4
β’ (π β ((π₯ β π β¦ πΆ) βΎ π΅) = (π₯ β π΅ β¦ πΆ)) |
20 | | iblsplit.5 |
. . . . . 6
β’ (π β (π₯ β π΅ β¦ πΆ) β
πΏ1) |
21 | | eqidd 2738 |
. . . . . . 7
β’ (π β (π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ¦)))), (ββ(πΆ / (iβπ¦))), 0)) = (π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ¦)))), (ββ(πΆ / (iβπ¦))), 0))) |
22 | | eqidd 2738 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β (ββ(πΆ / (iβπ¦))) = (ββ(πΆ / (iβπ¦)))) |
23 | 18 | sseld 3948 |
. . . . . . . . 9
β’ (π β (π₯ β π΅ β π₯ β π)) |
24 | 23 | imdistani 570 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (π β§ π₯ β π)) |
25 | 24, 1 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β πΆ β β) |
26 | 21, 22, 25 | isibl2 25147 |
. . . . . 6
β’ (π β ((π₯ β π΅ β¦ πΆ) β πΏ1 β
((π₯ β π΅ β¦ πΆ) β MblFn β§ βπ¦ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ¦)))), (ββ(πΆ / (iβπ¦))), 0))) β β))) |
27 | 20, 26 | mpbid 231 |
. . . . 5
β’ (π β ((π₯ β π΅ β¦ πΆ) β MblFn β§ βπ¦ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ¦)))), (ββ(πΆ / (iβπ¦))), 0))) β β)) |
28 | 27 | simpld 496 |
. . . 4
β’ (π β (π₯ β π΅ β¦ πΆ) β MblFn) |
29 | 19, 28 | eqeltrd 2838 |
. . 3
β’ (π β ((π₯ β π β¦ πΆ) βΎ π΅) β MblFn) |
30 | 4 | eqcomd 2743 |
. . 3
β’ (π β (π΄ βͺ π΅) = π) |
31 | 2, 16, 29, 30 | mbfres2cn 44273 |
. 2
β’ (π β (π₯ β π β¦ πΆ) β MblFn) |
32 | 15, 12 | mbfdm2 25017 |
. . . . . 6
β’ (π β π΄ β dom vol) |
33 | 32 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0...3)) β π΄ β dom vol) |
34 | 28, 25 | mbfdm2 25017 |
. . . . . 6
β’ (π β π΅ β dom vol) |
35 | 34 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0...3)) β π΅ β dom vol) |
36 | | iblsplit.1 |
. . . . . 6
β’ (π β (vol*β(π΄ β© π΅)) = 0) |
37 | 36 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0...3)) β (vol*β(π΄ β© π΅)) = 0) |
38 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0...3)) β π = (π΄ βͺ π΅)) |
39 | 1 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...3)) β§ π₯ β π) β πΆ β β) |
40 | | ax-icn 11117 |
. . . . . . . . . . . . . 14
β’ i β
β |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (0...3) β i β
β) |
42 | | elfznn0 13541 |
. . . . . . . . . . . . 13
β’ (π β (0...3) β π β
β0) |
43 | 41, 42 | expcld 14058 |
. . . . . . . . . . . 12
β’ (π β (0...3) β
(iβπ) β
β) |
44 | 43 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...3)) β§ π₯ β π) β (iβπ) β β) |
45 | 40 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...3)) β§ π₯ β π) β i β β) |
46 | | ine0 11597 |
. . . . . . . . . . . . 13
β’ i β
0 |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...3)) β§ π₯ β π) β i β 0) |
48 | | elfzelz 13448 |
. . . . . . . . . . . . 13
β’ (π β (0...3) β π β
β€) |
49 | 48 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...3)) β§ π₯ β π) β π β β€) |
50 | 45, 47, 49 | expne0d 14064 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...3)) β§ π₯ β π) β (iβπ) β 0) |
51 | 39, 44, 50 | divcld 11938 |
. . . . . . . . . 10
β’ (((π β§ π β (0...3)) β§ π₯ β π) β (πΆ / (iβπ)) β β) |
52 | 51 | recld 15086 |
. . . . . . . . 9
β’ (((π β§ π β (0...3)) β§ π₯ β π) β (ββ(πΆ / (iβπ))) β β) |
53 | 52 | rexrd 11212 |
. . . . . . . 8
β’ (((π β§ π β (0...3)) β§ π₯ β π) β (ββ(πΆ / (iβπ))) β
β*) |
54 | 53 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π β (0...3)) β§ π₯ β π) β§ 0 β€ (ββ(πΆ / (iβπ)))) β (ββ(πΆ / (iβπ))) β
β*) |
55 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ π β (0...3)) β§ π₯ β π) β§ 0 β€ (ββ(πΆ / (iβπ)))) β 0 β€ (ββ(πΆ / (iβπ)))) |
56 | | pnfge 13058 |
. . . . . . . 8
β’
((ββ(πΆ /
(iβπ))) β
β* β (ββ(πΆ / (iβπ))) β€ +β) |
57 | 54, 56 | syl 17 |
. . . . . . 7
β’ ((((π β§ π β (0...3)) β§ π₯ β π) β§ 0 β€ (ββ(πΆ / (iβπ)))) β (ββ(πΆ / (iβπ))) β€ +β) |
58 | | 0xr 11209 |
. . . . . . . 8
β’ 0 β
β* |
59 | | pnfxr 11216 |
. . . . . . . 8
β’ +β
β β* |
60 | | elicc1 13315 |
. . . . . . . 8
β’ ((0
β β* β§ +β β β*) β
((ββ(πΆ /
(iβπ))) β
(0[,]+β) β ((ββ(πΆ / (iβπ))) β β* β§ 0 β€
(ββ(πΆ /
(iβπ))) β§
(ββ(πΆ /
(iβπ))) β€
+β))) |
61 | 58, 59, 60 | mp2an 691 |
. . . . . . 7
β’
((ββ(πΆ /
(iβπ))) β
(0[,]+β) β ((ββ(πΆ / (iβπ))) β β* β§ 0 β€
(ββ(πΆ /
(iβπ))) β§
(ββ(πΆ /
(iβπ))) β€
+β)) |
62 | 54, 55, 57, 61 | syl3anbrc 1344 |
. . . . . 6
β’ ((((π β§ π β (0...3)) β§ π₯ β π) β§ 0 β€ (ββ(πΆ / (iβπ)))) β (ββ(πΆ / (iβπ))) β (0[,]+β)) |
63 | | 0e0iccpnf 13383 |
. . . . . . 7
β’ 0 β
(0[,]+β) |
64 | 63 | a1i 11 |
. . . . . 6
β’ ((((π β§ π β (0...3)) β§ π₯ β π) β§ Β¬ 0 β€ (ββ(πΆ / (iβπ)))) β 0 β
(0[,]+β)) |
65 | 62, 64 | ifclda 4526 |
. . . . 5
β’ (((π β§ π β (0...3)) β§ π₯ β π) β if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0) β
(0[,]+β)) |
66 | | eqid 2737 |
. . . . 5
β’ (π₯ β β β¦ if(π₯ β π΄, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0)) = (π₯ β β β¦ if(π₯ β π΄, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0)) |
67 | | eqid 2737 |
. . . . 5
β’ (π₯ β β β¦ if(π₯ β π΅, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0)) = (π₯ β β β¦ if(π₯ β π΅, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0)) |
68 | | ifan 4544 |
. . . . . 6
β’ if((π₯ β π β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0) = if(π₯ β π, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0) |
69 | 68 | mpteq2i 5215 |
. . . . 5
β’ (π₯ β β β¦
if((π₯ β π β§ 0 β€
(ββ(πΆ /
(iβπ)))),
(ββ(πΆ /
(iβπ))), 0)) = (π₯ β β β¦ if(π₯ β π, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0)) |
70 | | ifan 4544 |
. . . . . . . . . 10
β’ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0) = if(π₯ β π΄, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0) |
71 | 70 | eqcomi 2746 |
. . . . . . . . 9
β’ if(π₯ β π΄, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0) = if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0) |
72 | 71 | mpteq2i 5215 |
. . . . . . . 8
β’ (π₯ β β β¦ if(π₯ β π΄, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0)) |
73 | 72 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (0...3)) β (π₯ β β β¦ if(π₯ β π΄, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) |
74 | 73 | fveq2d 6851 |
. . . . . 6
β’ ((π β§ π β (0...3)) β
(β«2β(π₯
β β β¦ if(π₯
β π΄, if(0 β€
(ββ(πΆ /
(iβπ))),
(ββ(πΆ /
(iβπ))), 0), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0)))) |
75 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) |
76 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β (ββ(πΆ / (iβπ))) = (ββ(πΆ / (iβπ)))) |
77 | 75, 76, 12 | isibl2 25147 |
. . . . . . . . 9
β’ (π β ((π₯ β π΄ β¦ πΆ) β πΏ1 β
((π₯ β π΄ β¦ πΆ) β MblFn β§ βπ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β))) |
78 | 7, 77 | mpbid 231 |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β¦ πΆ) β MblFn β§ βπ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β)) |
79 | 78 | simprd 497 |
. . . . . . 7
β’ (π β βπ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β) |
80 | 79 | r19.21bi 3237 |
. . . . . 6
β’ ((π β§ π β (0...3)) β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β) |
81 | 74, 80 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ π β (0...3)) β
(β«2β(π₯
β β β¦ if(π₯
β π΄, if(0 β€
(ββ(πΆ /
(iβπ))),
(ββ(πΆ /
(iβπ))), 0), 0)))
β β) |
82 | | ifan 4544 |
. . . . . . . . 9
β’ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0) = if(π₯ β π΅, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0) |
83 | 82 | eqcomi 2746 |
. . . . . . . 8
β’ if(π₯ β π΅, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0) = if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0) |
84 | 83 | mpteq2i 5215 |
. . . . . . 7
β’ (π₯ β β β¦ if(π₯ β π΅, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0)) = (π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0)) |
85 | 84 | fveq2i 6850 |
. . . . . 6
β’
(β«2β(π₯ β β β¦ if(π₯ β π΅, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0))) =
(β«2β(π₯
β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) |
86 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π β (π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0)) = (π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) |
87 | | eqidd 2738 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΅) β (ββ(πΆ / (iβπ))) = (ββ(πΆ / (iβπ)))) |
88 | 86, 87, 25 | isibl2 25147 |
. . . . . . . . 9
β’ (π β ((π₯ β π΅ β¦ πΆ) β πΏ1 β
((π₯ β π΅ β¦ πΆ) β MblFn β§ βπ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β))) |
89 | 20, 88 | mpbid 231 |
. . . . . . . 8
β’ (π β ((π₯ β π΅ β¦ πΆ) β MblFn β§ βπ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β)) |
90 | 89 | simprd 497 |
. . . . . . 7
β’ (π β βπ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β) |
91 | 90 | r19.21bi 3237 |
. . . . . 6
β’ ((π β§ π β (0...3)) β
(β«2β(π₯
β β β¦ if((π₯ β π΅ β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β) |
92 | 85, 91 | eqeltrid 2842 |
. . . . 5
β’ ((π β§ π β (0...3)) β
(β«2β(π₯
β β β¦ if(π₯
β π΅, if(0 β€
(ββ(πΆ /
(iβπ))),
(ββ(πΆ /
(iβπ))), 0), 0)))
β β) |
93 | 33, 35, 37, 38, 65, 66, 67, 69, 81, 92 | itg2split 25130 |
. . . 4
β’ ((π β§ π β (0...3)) β
(β«2β(π₯
β β β¦ if((π₯ β π β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) = ((β«2β(π₯ β β β¦ if(π₯ β π΄, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0))) +
(β«2β(π₯
β β β¦ if(π₯
β π΅, if(0 β€
(ββ(πΆ /
(iβπ))),
(ββ(πΆ /
(iβπ))), 0),
0))))) |
94 | 81, 92 | readdcld 11191 |
. . . 4
β’ ((π β§ π β (0...3)) β
((β«2β(π₯ β β β¦ if(π₯ β π΄, if(0 β€ (ββ(πΆ / (iβπ))), (ββ(πΆ / (iβπ))), 0), 0))) +
(β«2β(π₯
β β β¦ if(π₯
β π΅, if(0 β€
(ββ(πΆ /
(iβπ))),
(ββ(πΆ /
(iβπ))), 0), 0))))
β β) |
95 | 93, 94 | eqeltrd 2838 |
. . 3
β’ ((π β§ π β (0...3)) β
(β«2β(π₯
β β β¦ if((π₯ β π β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β) |
96 | 95 | ralrimiva 3144 |
. 2
β’ (π β βπ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β) |
97 | | eqidd 2738 |
. . 3
β’ (π β (π₯ β β β¦ if((π₯ β π β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0)) = (π₯ β β β¦ if((π₯ β π β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) |
98 | | eqidd 2738 |
. . 3
β’ ((π β§ π₯ β π) β (ββ(πΆ / (iβπ))) = (ββ(πΆ / (iβπ)))) |
99 | 97, 98, 1 | isibl2 25147 |
. 2
β’ (π β ((π₯ β π β¦ πΆ) β πΏ1 β
((π₯ β π β¦ πΆ) β MblFn β§ βπ β
(0...3)(β«2β(π₯ β β β¦ if((π₯ β π β§ 0 β€ (ββ(πΆ / (iβπ)))), (ββ(πΆ / (iβπ))), 0))) β β))) |
100 | 31, 96, 99 | mpbir2and 712 |
1
β’ (π β (π₯ β π β¦ πΆ) β
πΏ1) |