Step | Hyp | Ref
| Expression |
1 | | icccmp.13 |
. . . . . . 7
β’ πΊ = sup(π, β, < ) |
2 | | icccmp.4 |
. . . . . . . . . 10
β’ π = {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} |
3 | 2 | ssrab3 4044 |
. . . . . . . . 9
β’ π β (π΄[,]π΅) |
4 | | icccmp.5 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
5 | | icccmp.6 |
. . . . . . . . . 10
β’ (π β π΅ β β) |
6 | | iccssre 13355 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
7 | 4, 5, 6 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π΄[,]π΅) β β) |
8 | 3, 7 | sstrid 3959 |
. . . . . . . 8
β’ (π β π β β) |
9 | | icccmp.1 |
. . . . . . . . . . 11
β’ π½ = (topGenβran
(,)) |
10 | | icccmp.2 |
. . . . . . . . . . 11
β’ π = (π½ βΎt (π΄[,]π΅)) |
11 | | icccmp.3 |
. . . . . . . . . . 11
β’ π· = ((abs β β )
βΎ (β Γ β)) |
12 | | icccmp.7 |
. . . . . . . . . . 11
β’ (π β π΄ β€ π΅) |
13 | | icccmp.8 |
. . . . . . . . . . 11
β’ (π β π β π½) |
14 | | icccmp.9 |
. . . . . . . . . . 11
β’ (π β (π΄[,]π΅) β βͺ π) |
15 | 9, 10, 11, 2, 4, 5,
12, 13, 14 | icccmplem1 24208 |
. . . . . . . . . 10
β’ (π β (π΄ β π β§ βπ¦ β π π¦ β€ π΅)) |
16 | 15 | simpld 496 |
. . . . . . . . 9
β’ (π β π΄ β π) |
17 | 16 | ne0d 4299 |
. . . . . . . 8
β’ (π β π β β
) |
18 | 15 | simprd 497 |
. . . . . . . . 9
β’ (π β βπ¦ β π π¦ β€ π΅) |
19 | | brralrspcev 5169 |
. . . . . . . . 9
β’ ((π΅ β β β§
βπ¦ β π π¦ β€ π΅) β βπ β β βπ¦ β π π¦ β€ π) |
20 | 5, 18, 19 | syl2anc 585 |
. . . . . . . 8
β’ (π β βπ β β βπ¦ β π π¦ β€ π) |
21 | 8, 17, 20 | suprcld 12126 |
. . . . . . 7
β’ (π β sup(π, β, < ) β
β) |
22 | 1, 21 | eqeltrid 2838 |
. . . . . 6
β’ (π β πΊ β β) |
23 | | icccmp.11 |
. . . . . . 7
β’ (π β πΆ β
β+) |
24 | 23 | rphalfcld 12977 |
. . . . . 6
β’ (π β (πΆ / 2) β
β+) |
25 | 22, 24 | ltaddrpd 12998 |
. . . . 5
β’ (π β πΊ < (πΊ + (πΆ / 2))) |
26 | 24 | rpred 12965 |
. . . . . . 7
β’ (π β (πΆ / 2) β β) |
27 | 22, 26 | readdcld 11192 |
. . . . . 6
β’ (π β (πΊ + (πΆ / 2)) β β) |
28 | 22, 27 | ltnled 11310 |
. . . . 5
β’ (π β (πΊ < (πΊ + (πΆ / 2)) β Β¬ (πΊ + (πΆ / 2)) β€ πΊ)) |
29 | 25, 28 | mpbid 231 |
. . . 4
β’ (π β Β¬ (πΊ + (πΆ / 2)) β€ πΊ) |
30 | | icccmp.14 |
. . . . . . . . . 10
β’ π
= if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) |
31 | 27, 5 | ifcld 4536 |
. . . . . . . . . 10
β’ (π β if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β β) |
32 | 30, 31 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β π
β β) |
33 | 8, 17, 20, 16 | suprubd 12125 |
. . . . . . . . . . . . 13
β’ (π β π΄ β€ sup(π, β, < )) |
34 | 33, 1 | breqtrrdi 5151 |
. . . . . . . . . . . 12
β’ (π β π΄ β€ πΊ) |
35 | 22, 27, 25 | ltled 11311 |
. . . . . . . . . . . 12
β’ (π β πΊ β€ (πΊ + (πΆ / 2))) |
36 | 4, 22, 27, 34, 35 | letrd 11320 |
. . . . . . . . . . 11
β’ (π β π΄ β€ (πΊ + (πΆ / 2))) |
37 | | breq2 5113 |
. . . . . . . . . . . 12
β’ ((πΊ + (πΆ / 2)) = if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β (π΄ β€ (πΊ + (πΆ / 2)) β π΄ β€ if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅))) |
38 | | breq2 5113 |
. . . . . . . . . . . 12
β’ (π΅ = if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β (π΄ β€ π΅ β π΄ β€ if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅))) |
39 | 37, 38 | ifboth 4529 |
. . . . . . . . . . 11
β’ ((π΄ β€ (πΊ + (πΆ / 2)) β§ π΄ β€ π΅) β π΄ β€ if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅)) |
40 | 36, 12, 39 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π΄ β€ if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅)) |
41 | 40, 30 | breqtrrdi 5151 |
. . . . . . . . 9
β’ (π β π΄ β€ π
) |
42 | | min2 13118 |
. . . . . . . . . . 11
β’ (((πΊ + (πΆ / 2)) β β β§ π΅ β β) β
if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β€ π΅) |
43 | 27, 5, 42 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β€ π΅) |
44 | 30, 43 | eqbrtrid 5144 |
. . . . . . . . 9
β’ (π β π
β€ π΅) |
45 | | elicc2 13338 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΅ β β) β (π
β (π΄[,]π΅) β (π
β β β§ π΄ β€ π
β§ π
β€ π΅))) |
46 | 4, 5, 45 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π
β (π΄[,]π΅) β (π
β β β§ π΄ β€ π
β§ π
β€ π΅))) |
47 | 32, 41, 44, 46 | mpbir3and 1343 |
. . . . . . . 8
β’ (π β π
β (π΄[,]π΅)) |
48 | 22, 23 | ltsubrpd 12997 |
. . . . . . . . . . 11
β’ (π β (πΊ β πΆ) < πΊ) |
49 | 48, 1 | breqtrdi 5150 |
. . . . . . . . . 10
β’ (π β (πΊ β πΆ) < sup(π, β, < )) |
50 | 23 | rpred 12965 |
. . . . . . . . . . . 12
β’ (π β πΆ β β) |
51 | 22, 50 | resubcld 11591 |
. . . . . . . . . . 11
β’ (π β (πΊ β πΆ) β β) |
52 | | suprlub 12127 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β
β§ βπ β β βπ¦ β π π¦ β€ π) β§ (πΊ β πΆ) β β) β ((πΊ β πΆ) < sup(π, β, < ) β βπ£ β π (πΊ β πΆ) < π£)) |
53 | 8, 17, 20, 51, 52 | syl31anc 1374 |
. . . . . . . . . 10
β’ (π β ((πΊ β πΆ) < sup(π, β, < ) β βπ£ β π (πΊ β πΆ) < π£)) |
54 | 49, 53 | mpbid 231 |
. . . . . . . . 9
β’ (π β βπ£ β π (πΊ β πΆ) < π£) |
55 | | oveq2 7369 |
. . . . . . . . . . . . . 14
β’ (π₯ = π£ β (π΄[,]π₯) = (π΄[,]π£)) |
56 | 55 | sseq1d 3979 |
. . . . . . . . . . . . 13
β’ (π₯ = π£ β ((π΄[,]π₯) β βͺ π§ β (π΄[,]π£) β βͺ π§)) |
57 | 56 | rexbidv 3172 |
. . . . . . . . . . . 12
β’ (π₯ = π£ β (βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§ β βπ§ β (π« π β© Fin)(π΄[,]π£) β βͺ π§)) |
58 | 57, 2 | elrab2 3652 |
. . . . . . . . . . 11
β’ (π£ β π β (π£ β (π΄[,]π΅) β§ βπ§ β (π« π β© Fin)(π΄[,]π£) β βͺ π§)) |
59 | | unieq 4880 |
. . . . . . . . . . . . . . 15
β’ (π§ = π€ β βͺ π§ = βͺ
π€) |
60 | 59 | sseq2d 3980 |
. . . . . . . . . . . . . 14
β’ (π§ = π€ β ((π΄[,]π£) β βͺ π§ β (π΄[,]π£) β βͺ π€)) |
61 | 60 | cbvrexvw 3225 |
. . . . . . . . . . . . 13
β’
(βπ§ β
(π« π β©
Fin)(π΄[,]π£) β βͺ π§ β βπ€ β (π« π β© Fin)(π΄[,]π£) β βͺ π€) |
62 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π€ β (π« π β© Fin)) |
63 | | elin 3930 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β (π« π β© Fin) β (π€ β π« π β§ π€ β Fin)) |
64 | 62, 63 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π€ β π« π β§ π€ β Fin)) |
65 | 64 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π€ β π« π) |
66 | 65 | elpwid 4573 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π€ β π) |
67 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π) |
68 | | icccmp.10 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β π) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π β π) |
70 | 69 | snssd 4773 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β {π} β π) |
71 | 66, 70 | unssd 4150 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π€ βͺ {π}) β π) |
72 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . 20
β’ π€ β V |
73 | | snex 5392 |
. . . . . . . . . . . . . . . . . . . 20
β’ {π} β V |
74 | 72, 73 | unex 7684 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ βͺ {π}) β V |
75 | 74 | elpw 4568 |
. . . . . . . . . . . . . . . . . 18
β’ ((π€ βͺ {π}) β π« π β (π€ βͺ {π}) β π) |
76 | 71, 75 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π€ βͺ {π}) β π« π) |
77 | 64 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π€ β Fin) |
78 | | snfi 8994 |
. . . . . . . . . . . . . . . . . 18
β’ {π} β Fin |
79 | | unfi 9122 |
. . . . . . . . . . . . . . . . . 18
β’ ((π€ β Fin β§ {π} β Fin) β (π€ βͺ {π}) β Fin) |
80 | 77, 78, 79 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π€ βͺ {π}) β Fin) |
81 | 76, 80 | elind 4158 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π€ βͺ {π}) β (π« π β© Fin)) |
82 | | simplr2 1217 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π‘ β€ π£)) β (π΄[,]π£) β βͺ π€) |
83 | | ssun1 4136 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ βͺ π€
β (βͺ π€ βͺ π) |
84 | 82, 83 | sstrdi 3960 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π‘ β€ π£)) β (π΄[,]π£) β (βͺ π€ βͺ π)) |
85 | 67, 4 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π΄ β β) |
86 | 67, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π
β β) |
87 | | elicc2 13338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π΄ β β β§ π
β β) β (π‘ β (π΄[,]π
) β (π‘ β β β§ π΄ β€ π‘ β§ π‘ β€ π
))) |
88 | 85, 86, 87 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π‘ β (π΄[,]π
) β (π‘ β β β§ π΄ β€ π‘ β§ π‘ β€ π
))) |
89 | 88 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β (π‘ β β β§ π΄ β€ π‘ β§ π‘ β€ π
)) |
90 | 89 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β π‘ β β) |
91 | 90 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π‘ β€ π£)) β π‘ β β) |
92 | 89 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β π΄ β€ π‘) |
93 | 92 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π‘ β€ π£)) β π΄ β€ π‘) |
94 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π‘ β€ π£)) β π‘ β€ π£) |
95 | 67, 7 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π΄[,]π΅) β β) |
96 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π£ β (π΄[,]π΅)) |
97 | 95, 96 | sseldd 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β π£ β β) |
98 | | elicc2 13338 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π΄ β β β§ π£ β β) β (π‘ β (π΄[,]π£) β (π‘ β β β§ π΄ β€ π‘ β§ π‘ β€ π£))) |
99 | 85, 97, 98 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π‘ β (π΄[,]π£) β (π‘ β β β§ π΄ β€ π‘ β§ π‘ β€ π£))) |
100 | 99 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π‘ β€ π£)) β (π‘ β (π΄[,]π£) β (π‘ β β β§ π΄ β€ π‘ β§ π‘ β€ π£))) |
101 | 91, 93, 94, 100 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π‘ β€ π£)) β π‘ β (π΄[,]π£)) |
102 | 84, 101 | sseldd 3949 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π‘ β€ π£)) β π‘ β (βͺ π€ βͺ π)) |
103 | 102 | expr 458 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β (π‘ β€ π£ β π‘ β (βͺ π€ βͺ π))) |
104 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π) |
105 | | icccmp.12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (πΊ(ballβπ·)πΆ) β π) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β (πΊ(ballβπ·)πΆ) β π) |
107 | 90 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π‘ β β) |
108 | 104, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β (πΊ β πΆ) β β) |
109 | 97 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π£ β β) |
110 | | simplr3 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β (πΊ β πΆ) < π£) |
111 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π£ < π‘) |
112 | 108, 109,
107, 110, 111 | lttrd 11324 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β (πΊ β πΆ) < π‘) |
113 | 104, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π
β β) |
114 | 22, 50 | readdcld 11192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (πΊ + πΆ) β β) |
115 | 104, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β (πΊ + πΆ) β β) |
116 | 89 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β π‘ β€ π
) |
117 | 116 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π‘ β€ π
) |
118 | | min1 13117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((πΊ + (πΆ / 2)) β β β§ π΅ β β) β
if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β€ (πΊ + (πΆ / 2))) |
119 | 27, 5, 118 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) β€ (πΊ + (πΆ / 2))) |
120 | 30, 119 | eqbrtrid 5144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π
β€ (πΊ + (πΆ / 2))) |
121 | | rphalflt 12952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (πΆ β β+
β (πΆ / 2) < πΆ) |
122 | 23, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (πΆ / 2) < πΆ) |
123 | 26, 50, 22, 122 | ltadd2dd 11322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (πΊ + (πΆ / 2)) < (πΊ + πΆ)) |
124 | 32, 27, 114, 120, 123 | lelttrd 11321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π
< (πΊ + πΆ)) |
125 | 104, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π
< (πΊ + πΆ)) |
126 | 107, 113,
115, 117, 125 | lelttrd 11321 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π‘ < (πΊ + πΆ)) |
127 | | rexr 11209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΊ β πΆ) β β β (πΊ β πΆ) β
β*) |
128 | | rexr 11209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πΊ + πΆ) β β β (πΊ + πΆ) β
β*) |
129 | | elioo2 13314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΊ β πΆ) β β* β§ (πΊ + πΆ) β β*) β (π‘ β ((πΊ β πΆ)(,)(πΊ + πΆ)) β (π‘ β β β§ (πΊ β πΆ) < π‘ β§ π‘ < (πΊ + πΆ)))) |
130 | 127, 128,
129 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((πΊ β πΆ) β β β§ (πΊ + πΆ) β β) β (π‘ β ((πΊ β πΆ)(,)(πΊ + πΆ)) β (π‘ β β β§ (πΊ β πΆ) < π‘ β§ π‘ < (πΊ + πΆ)))) |
131 | 108, 115,
130 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β (π‘ β ((πΊ β πΆ)(,)(πΊ + πΆ)) β (π‘ β β β§ (πΊ β πΆ) < π‘ β§ π‘ < (πΊ + πΆ)))) |
132 | 107, 112,
126, 131 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π‘ β ((πΊ β πΆ)(,)(πΊ + πΆ))) |
133 | 104, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β πΊ β β) |
134 | 104, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β πΆ β
β+) |
135 | 134 | rpred 12965 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β πΆ β β) |
136 | 11 | bl2ioo 24178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΊ β β β§ πΆ β β) β (πΊ(ballβπ·)πΆ) = ((πΊ β πΆ)(,)(πΊ + πΆ))) |
137 | 133, 135,
136 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β (πΊ(ballβπ·)πΆ) = ((πΊ β πΆ)(,)(πΊ + πΆ))) |
138 | 132, 137 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π‘ β (πΊ(ballβπ·)πΆ)) |
139 | 106, 138 | sseldd 3949 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π‘ β π) |
140 | | elun2 4141 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ β π β π‘ β (βͺ π€ βͺ π)) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ (π‘ β (π΄[,]π
) β§ π£ < π‘)) β π‘ β (βͺ π€ βͺ π)) |
142 | 141 | expr 458 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β (π£ < π‘ β π‘ β (βͺ π€ βͺ π))) |
143 | 97 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β π£ β β) |
144 | | lelttric 11270 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π‘ β β β§ π£ β β) β (π‘ β€ π£ β¨ π£ < π‘)) |
145 | 90, 143, 144 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β (π‘ β€ π£ β¨ π£ < π‘)) |
146 | 103, 142,
145 | mpjaod 859 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β§ π‘ β (π΄[,]π
)) β π‘ β (βͺ π€ βͺ π)) |
147 | 146 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π‘ β (π΄[,]π
) β π‘ β (βͺ π€ βͺ π))) |
148 | 147 | ssrdv 3954 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π΄[,]π
) β (βͺ
π€ βͺ π)) |
149 | | uniun 4895 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ (π€
βͺ {π}) = (βͺ π€
βͺ βͺ {π}) |
150 | | unisng 4890 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β βͺ {π} = π) |
151 | 69, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β βͺ {π} = π) |
152 | 151 | uneq2d 4127 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (βͺ π€ βͺ βͺ {π})
= (βͺ π€ βͺ π)) |
153 | 149, 152 | eqtrid 2785 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β βͺ (π€ βͺ {π}) = (βͺ π€ βͺ π)) |
154 | 148, 153 | sseqtrrd 3989 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β (π΄[,]π
) β βͺ
(π€ βͺ {π})) |
155 | | unieq 4880 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (π€ βͺ {π}) β βͺ π¦ = βͺ
(π€ βͺ {π})) |
156 | 155 | sseq2d 3980 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (π€ βͺ {π}) β ((π΄[,]π
) β βͺ π¦ β (π΄[,]π
) β βͺ
(π€ βͺ {π}))) |
157 | 156 | rspcev 3583 |
. . . . . . . . . . . . . . . 16
β’ (((π€ βͺ {π}) β (π« π β© Fin) β§ (π΄[,]π
) β βͺ
(π€ βͺ {π})) β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦) |
158 | 81, 154, 157 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π£ β (π΄[,]π΅)) β§ (π€ β (π« π β© Fin) β§ (π΄[,]π£) β βͺ π€ β§ (πΊ β πΆ) < π£)) β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦) |
159 | 158 | 3exp2 1355 |
. . . . . . . . . . . . . 14
β’ ((π β§ π£ β (π΄[,]π΅)) β (π€ β (π« π β© Fin) β ((π΄[,]π£) β βͺ π€ β ((πΊ β πΆ) < π£ β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦)))) |
160 | 159 | rexlimdv 3147 |
. . . . . . . . . . . . 13
β’ ((π β§ π£ β (π΄[,]π΅)) β (βπ€ β (π« π β© Fin)(π΄[,]π£) β βͺ π€ β ((πΊ β πΆ) < π£ β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦))) |
161 | 61, 160 | biimtrid 241 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β (π΄[,]π΅)) β (βπ§ β (π« π β© Fin)(π΄[,]π£) β βͺ π§ β ((πΊ β πΆ) < π£ β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦))) |
162 | 161 | expimpd 455 |
. . . . . . . . . . 11
β’ (π β ((π£ β (π΄[,]π΅) β§ βπ§ β (π« π β© Fin)(π΄[,]π£) β βͺ π§) β ((πΊ β πΆ) < π£ β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦))) |
163 | 58, 162 | biimtrid 241 |
. . . . . . . . . 10
β’ (π β (π£ β π β ((πΊ β πΆ) < π£ β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦))) |
164 | 163 | rexlimdv 3147 |
. . . . . . . . 9
β’ (π β (βπ£ β π (πΊ β πΆ) < π£ β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦)) |
165 | 54, 164 | mpd 15 |
. . . . . . . 8
β’ (π β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦) |
166 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π£ = π
β (π΄[,]π£) = (π΄[,]π
)) |
167 | 166 | sseq1d 3979 |
. . . . . . . . . 10
β’ (π£ = π
β ((π΄[,]π£) β βͺ π¦ β (π΄[,]π
) β βͺ π¦)) |
168 | 167 | rexbidv 3172 |
. . . . . . . . 9
β’ (π£ = π
β (βπ¦ β (π« π β© Fin)(π΄[,]π£) β βͺ π¦ β βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦)) |
169 | | unieq 4880 |
. . . . . . . . . . . . . 14
β’ (π§ = π¦ β βͺ π§ = βͺ
π¦) |
170 | 169 | sseq2d 3980 |
. . . . . . . . . . . . 13
β’ (π§ = π¦ β ((π΄[,]π£) β βͺ π§ β (π΄[,]π£) β βͺ π¦)) |
171 | 170 | cbvrexvw 3225 |
. . . . . . . . . . . 12
β’
(βπ§ β
(π« π β©
Fin)(π΄[,]π£) β βͺ π§ β βπ¦ β (π« π β© Fin)(π΄[,]π£) β βͺ π¦) |
172 | 57, 171 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π₯ = π£ β (βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§ β βπ¦ β (π« π β© Fin)(π΄[,]π£) β βͺ π¦)) |
173 | 172 | cbvrabv 3416 |
. . . . . . . . . 10
β’ {π₯ β (π΄[,]π΅) β£ βπ§ β (π« π β© Fin)(π΄[,]π₯) β βͺ π§} = {π£ β (π΄[,]π΅) β£ βπ¦ β (π« π β© Fin)(π΄[,]π£) β βͺ π¦} |
174 | 2, 173 | eqtri 2761 |
. . . . . . . . 9
β’ π = {π£ β (π΄[,]π΅) β£ βπ¦ β (π« π β© Fin)(π΄[,]π£) β βͺ π¦} |
175 | 168, 174 | elrab2 3652 |
. . . . . . . 8
β’ (π
β π β (π
β (π΄[,]π΅) β§ βπ¦ β (π« π β© Fin)(π΄[,]π
) β βͺ π¦)) |
176 | 47, 165, 175 | sylanbrc 584 |
. . . . . . 7
β’ (π β π
β π) |
177 | 8, 17, 20, 176 | suprubd 12125 |
. . . . . 6
β’ (π β π
β€ sup(π, β, < )) |
178 | 177, 1 | breqtrrdi 5151 |
. . . . 5
β’ (π β π
β€ πΊ) |
179 | | iftrue 4496 |
. . . . . . 7
β’ ((πΊ + (πΆ / 2)) β€ π΅ β if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) = (πΊ + (πΆ / 2))) |
180 | 30, 179 | eqtrid 2785 |
. . . . . 6
β’ ((πΊ + (πΆ / 2)) β€ π΅ β π
= (πΊ + (πΆ / 2))) |
181 | 180 | breq1d 5119 |
. . . . 5
β’ ((πΊ + (πΆ / 2)) β€ π΅ β (π
β€ πΊ β (πΊ + (πΆ / 2)) β€ πΊ)) |
182 | 178, 181 | syl5ibcom 244 |
. . . 4
β’ (π β ((πΊ + (πΆ / 2)) β€ π΅ β (πΊ + (πΆ / 2)) β€ πΊ)) |
183 | 29, 182 | mtod 197 |
. . 3
β’ (π β Β¬ (πΊ + (πΆ / 2)) β€ π΅) |
184 | | iffalse 4499 |
. . . 4
β’ (Β¬
(πΊ + (πΆ / 2)) β€ π΅ β if((πΊ + (πΆ / 2)) β€ π΅, (πΊ + (πΆ / 2)), π΅) = π΅) |
185 | 30, 184 | eqtrid 2785 |
. . 3
β’ (Β¬
(πΊ + (πΆ / 2)) β€ π΅ β π
= π΅) |
186 | 183, 185 | syl 17 |
. 2
β’ (π β π
= π΅) |
187 | 186, 176 | eqeltrrd 2835 |
1
β’ (π β π΅ β π) |