Step | Hyp | Ref
| Expression |
1 | | poimir.r |
. . . . . . . . . . . 12
β’ π
=
(βtβ((1...π) Γ {(topGenβran
(,))})) |
2 | | fzfi 13884 |
. . . . . . . . . . . . 13
β’
(1...π) β
Fin |
3 | | retop 24141 |
. . . . . . . . . . . . . 14
β’
(topGenβran (,)) β Top |
4 | 3 | fconst6 6737 |
. . . . . . . . . . . . 13
β’
((1...π) Γ
{(topGenβran (,))}):(1...π)βΆTop |
5 | | pttop 22949 |
. . . . . . . . . . . . 13
β’
(((1...π) β Fin
β§ ((1...π) Γ
{(topGenβran (,))}):(1...π)βΆTop) β
(βtβ((1...π) Γ {(topGenβran (,))})) β
Top) |
6 | 2, 4, 5 | mp2an 691 |
. . . . . . . . . . . 12
β’
(βtβ((1...π) Γ {(topGenβran (,))})) β
Top |
7 | 1, 6 | eqeltri 2834 |
. . . . . . . . . . 11
β’ π
β Top |
8 | | poimir.i |
. . . . . . . . . . . 12
β’ πΌ = ((0[,]1) βm
(1...π)) |
9 | | ovex 7395 |
. . . . . . . . . . . 12
β’ ((0[,]1)
βm (1...π))
β V |
10 | 8, 9 | eqeltri 2834 |
. . . . . . . . . . 11
β’ πΌ β V |
11 | | elrest 17316 |
. . . . . . . . . . 11
β’ ((π
β Top β§ πΌ β V) β (π£ β (π
βΎt πΌ) β βπ§ β π
π£ = (π§ β© πΌ))) |
12 | 7, 10, 11 | mp2an 691 |
. . . . . . . . . 10
β’ (π£ β (π
βΎt πΌ) β βπ§ β π
π£ = (π§ β© πΌ)) |
13 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ ((abs
β β ) βΎ (β Γ β)) = ((abs β β )
βΎ (β Γ β)) |
14 | 1, 13 | ptrecube 36107 |
. . . . . . . . . . . . 13
β’ ((π§ β π
β§ πΆ β π§) β βπ β β+ Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π§) |
15 | 14 | ex 414 |
. . . . . . . . . . . 12
β’ (π§ β π
β (πΆ β π§ β βπ β β+ Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π§)) |
16 | | inss1 4193 |
. . . . . . . . . . . . . . 15
β’ (π§ β© πΌ) β π§ |
17 | | sseq1 3974 |
. . . . . . . . . . . . . . 15
β’ (π£ = (π§ β© πΌ) β (π£ β π§ β (π§ β© πΌ) β π§)) |
18 | 16, 17 | mpbiri 258 |
. . . . . . . . . . . . . 14
β’ (π£ = (π§ β© πΌ) β π£ β π§) |
19 | 18 | sseld 3948 |
. . . . . . . . . . . . 13
β’ (π£ = (π§ β© πΌ) β (πΆ β π£ β πΆ β π§)) |
20 | | ssrin 4198 |
. . . . . . . . . . . . . . 15
β’ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π§ β (Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β (π§ β© πΌ)) |
21 | | sseq2 3975 |
. . . . . . . . . . . . . . 15
β’ (π£ = (π§ β© πΌ) β ((Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β (Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β (π§ β© πΌ))) |
22 | 20, 21 | syl5ibr 246 |
. . . . . . . . . . . . . 14
β’ (π£ = (π§ β© πΌ) β (Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π§ β (Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£)) |
23 | 22 | reximdv 3168 |
. . . . . . . . . . . . 13
β’ (π£ = (π§ β© πΌ) β (βπ β β+ Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π§ β βπ β β+ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£)) |
24 | 19, 23 | imim12d 81 |
. . . . . . . . . . . 12
β’ (π£ = (π§ β© πΌ) β ((πΆ β π§ β βπ β β+ Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β π§) β (πΆ β π£ β βπ β β+ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£))) |
25 | 15, 24 | syl5com 31 |
. . . . . . . . . . 11
β’ (π§ β π
β (π£ = (π§ β© πΌ) β (πΆ β π£ β βπ β β+ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£))) |
26 | 25 | rexlimiv 3146 |
. . . . . . . . . 10
β’
(βπ§ β
π
π£ = (π§ β© πΌ) β (πΆ β π£ β βπ β β+ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£)) |
27 | 12, 26 | sylbi 216 |
. . . . . . . . 9
β’ (π£ β (π
βΎt πΌ) β (πΆ β π£ β βπ β β+ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£)) |
28 | 27 | imp 408 |
. . . . . . . 8
β’ ((π£ β (π
βΎt πΌ) β§ πΆ β π£) β βπ β β+ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£) |
29 | 28 | adantl 483 |
. . . . . . 7
β’ ((π β§ (π£ β (π
βΎt πΌ) β§ πΆ β π£)) β βπ β β+ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£) |
30 | | resttop 22527 |
. . . . . . . . . . 11
β’ ((π
β Top β§ πΌ β V) β (π
βΎt πΌ) β Top) |
31 | 7, 10, 30 | mp2an 691 |
. . . . . . . . . 10
β’ (π
βΎt πΌ) β Top |
32 | | reex 11149 |
. . . . . . . . . . . . . 14
β’ β
β V |
33 | | unitssre 13423 |
. . . . . . . . . . . . . 14
β’ (0[,]1)
β β |
34 | | mapss 8834 |
. . . . . . . . . . . . . 14
β’ ((β
β V β§ (0[,]1) β β) β ((0[,]1) βm
(1...π)) β (β
βm (1...π))) |
35 | 32, 33, 34 | mp2an 691 |
. . . . . . . . . . . . 13
β’ ((0[,]1)
βm (1...π))
β (β βm (1...π)) |
36 | 8, 35 | eqsstri 3983 |
. . . . . . . . . . . 12
β’ πΌ β (β
βm (1...π)) |
37 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’
(1...π) β
V |
38 | | uniretop 24142 |
. . . . . . . . . . . . . . 15
β’ β =
βͺ (topGenβran (,)) |
39 | 1, 38 | ptuniconst 22965 |
. . . . . . . . . . . . . 14
β’
(((1...π) β V
β§ (topGenβran (,)) β Top) β (β βm
(1...π)) = βͺ π
) |
40 | 37, 3, 39 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (β
βm (1...π))
= βͺ π
|
41 | 40 | restuni 22529 |
. . . . . . . . . . . 12
β’ ((π
β Top β§ πΌ β (β
βm (1...π))) β πΌ = βͺ (π
βΎt πΌ)) |
42 | 7, 36, 41 | mp2an 691 |
. . . . . . . . . . 11
β’ πΌ = βͺ
(π
βΎt
πΌ) |
43 | 42 | eltopss 22272 |
. . . . . . . . . 10
β’ (((π
βΎt πΌ) β Top β§ π£ β (π
βΎt πΌ)) β π£ β πΌ) |
44 | 31, 43 | mpan 689 |
. . . . . . . . 9
β’ (π£ β (π
βΎt πΌ) β π£ β πΌ) |
45 | 44 | sselda 3949 |
. . . . . . . 8
β’ ((π£ β (π
βΎt πΌ) β§ πΆ β π£) β πΆ β πΌ) |
46 | | 2rp 12927 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β+ |
47 | | rpdivcl 12947 |
. . . . . . . . . . . . . . . . 17
β’ ((2
β β+ β§ π β β+) β (2 /
π) β
β+) |
48 | 46, 47 | mpan 689 |
. . . . . . . . . . . . . . . 16
β’ (π β β+
β (2 / π) β
β+) |
49 | 48 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β (2 / π) β
β) |
50 | | ceicl 13753 |
. . . . . . . . . . . . . . 15
β’ ((2 /
π) β β β
-(ββ-(2 / π))
β β€) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β β+
β -(ββ-(2 / π)) β β€) |
52 | | 0red 11165 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β 0 β β) |
53 | 51 | zred 12614 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β -(ββ-(2 / π)) β β) |
54 | 48 | rpgt0d 12967 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β 0 < (2 / π)) |
55 | | ceige 13756 |
. . . . . . . . . . . . . . . 16
β’ ((2 /
π) β β β (2
/ π) β€
-(ββ-(2 / π))) |
56 | 49, 55 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β (2 / π) β€
-(ββ-(2 / π))) |
57 | 52, 49, 53, 54, 56 | ltletrd 11322 |
. . . . . . . . . . . . . 14
β’ (π β β+
β 0 < -(ββ-(2 / π))) |
58 | | elnnz 12516 |
. . . . . . . . . . . . . 14
β’
(-(ββ-(2 / π)) β β β (-(ββ-(2
/ π)) β β€ β§
0 < -(ββ-(2 / π)))) |
59 | 51, 57, 58 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (π β β+
β -(ββ-(2 / π)) β β) |
60 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = -(ββ-(2 / π)) β
(β€β₯βπ) =
(β€β₯β-(ββ-(2 / π)))) |
61 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . 18
β’ (π = -(ββ-(2 / π)) β (1 / π) = (1 / -(ββ-(2 /
π)))) |
62 | 61 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π = -(ββ-(2 / π)) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) = ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π))))) |
63 | 62 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
β’ (π = -(ββ-(2 / π)) β ((((1st
β(πΊβπ)) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β (((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))))) |
64 | 63 | ralbidv 3175 |
. . . . . . . . . . . . . . 15
β’ (π = -(ββ-(2 / π)) β (βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))))) |
65 | 60, 64 | rexeqbidv 3323 |
. . . . . . . . . . . . . 14
β’ (π = -(ββ-(2 / π)) β (βπ β
(β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β
(β€β₯β-(ββ-(2 / π)))βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))))) |
66 | 65 | rspcv 3580 |
. . . . . . . . . . . . 13
β’
(-(ββ-(2 / π)) β β β (βπ β β βπ β
(β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β
(β€β₯β-(ββ-(2 / π)))βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))))) |
67 | 59, 66 | syl 17 |
. . . . . . . . . . . 12
β’ (π β β+
β (βπ β
β βπ β
(β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β
(β€β₯β-(ββ-(2 / π)))βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))))) |
68 | 67 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β πΌ) β§ π β β+) β
(βπ β β
βπ β
(β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β
(β€β₯β-(ββ-(2 / π)))βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))))) |
69 | | uznnssnn 12827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(-(ββ-(2 / π)) β β β
(β€β₯β-(ββ-(2 / π))) β β) |
70 | 59, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β+
β (β€β₯β-(ββ-(2 / π))) β β) |
71 | 70 | sseld 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β+
β (π β
(β€β₯β-(ββ-(2 / π))) β π β β)) |
72 | 71 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ πΆ β πΌ) β§ π β β+) β (π β
(β€β₯β-(ββ-(2 / π))) β π β β)) |
73 | 72 | imdistani 570 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β (((π β§ πΆ β πΌ) β§ π β β+) β§ π β
β)) |
74 | 59 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β β+
β -(ββ-(2 / π)) β
β+) |
75 | 48, 74 | lerecd 12983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β+
β ((2 / π) β€
-(ββ-(2 / π))
β (1 / -(ββ-(2 / π))) β€ (1 / (2 / π)))) |
76 | 56, 75 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β+
β (1 / -(ββ-(2 / π))) β€ (1 / (2 / π))) |
77 | | rpcn 12932 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β+
β π β
β) |
78 | | rpne0 12938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β+
β π β
0) |
79 | | 2cn 12235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 2 β
β |
80 | | 2ne0 12264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ 2 β
0 |
81 | | recdiv 11868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((2
β β β§ 2 β 0) β§ (π β β β§ π β 0)) β (1 / (2 / π)) = (π / 2)) |
82 | 79, 80, 81 | mpanl12 701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β β β§ π β 0) β (1 / (2 / π)) = (π / 2)) |
83 | 77, 78, 82 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β+
β (1 / (2 / π)) =
(π / 2)) |
84 | 76, 83 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β+
β (1 / -(ββ-(2 / π))) β€ (π / 2)) |
85 | 84 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (1 / -(ββ-(2 / π))) β€ (π / 2)) |
86 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (πΆ β ((0[,]1)
βm (1...π))
β πΆ:(1...π)βΆ(0[,]1)) |
87 | 86, 8 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (πΆ β πΌ β πΆ:(1...π)βΆ(0[,]1)) |
88 | 87 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β πΆ:(1...π)βΆ(0[,]1)) |
89 | 88 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (πΆβπ) β (0[,]1)) |
90 | 33, 89 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (πΆβπ) β β) |
91 | | simp-4l 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β π) |
92 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β π β β) |
93 | 91, 92 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β (π β§ π β β)) |
94 | | poimirlem30.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β πΊ:ββΆ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
95 | 94 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β§ π β β) β (πΊβπ) β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
96 | | xp1st 7958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((πΊβπ) β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (1st β(πΊβπ)) β (β0
βm (1...π))) |
97 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((1st β(πΊβπ)) β (β0
βm (1...π))
β (1st β(πΊβπ)):(1...π)βΆβ0) |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ π β β) β (1st
β(πΊβπ)):(1...π)βΆβ0) |
99 | 98 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β β) β§ π β (1...π)) β ((1st β(πΊβπ))βπ) β
β0) |
100 | 99 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π β β) β§ π β (1...π)) β ((1st β(πΊβπ))βπ) β β) |
101 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
102 | 100, 101 | nndivred 12214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π β β) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) / π) β β) |
103 | 93, 102 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) / π) β β) |
104 | 90, 103 | resubcld 11590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) β β) |
105 | 104 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) β β) |
106 | 105 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) β β) |
107 | 59 | nnrecred 12211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β+
β (1 / -(ββ-(2 / π))) β β) |
108 | 107 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (1 / -(ββ-(2 / π))) β
β) |
109 | | rphalfcl 12949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β+
β (π / 2) β
β+) |
110 | 109 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β+
β (π / 2) β
β) |
111 | 110 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (π / 2) β β) |
112 | | ltletr 11254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) β β β§ (1 /
-(ββ-(2 / π)))
β β β§ (π /
2) β β) β (((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π))) β§ (1 /
-(ββ-(2 / π)))
β€ (π / 2)) β
(absβ((πΆβπ) β (((1st
β(πΊβπ))βπ) / π))) < (π / 2))) |
113 | 106, 108,
111, 112 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π))) β§ (1 /
-(ββ-(2 / π)))
β€ (π / 2)) β
(absβ((πΆβπ) β (((1st
β(πΊβπ))βπ) / π))) < (π / 2))) |
114 | 85, 113 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π))) β (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (π / 2))) |
115 | 73, 114 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π))) β (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (π / 2))) |
116 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ πΆ β πΌ) β π) |
117 | 70 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β π β β) |
118 | 116, 117 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ πΆ β πΌ) β§ (π β β+ β§ π β
(β€β₯β-(ββ-(2 / π))))) β (π β§ π β β)) |
119 | 118 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β (π β§ π β β)) |
120 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ 1 β
β |
121 | | snssi 4773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (1 β
β β {1} β β) |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ {1}
β β |
123 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ 0 β
β |
124 | | snssi 4773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (0 β
β β {0} β β) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ {0}
β β |
126 | 122, 125 | unssi 4150 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ({1}
βͺ {0}) β β |
127 | | 1ex 11158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ 1 β
V |
128 | 127 | fconst 6733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((2nd β(πΊβπ)) β (1...π)) Γ {1}):((2nd
β(πΊβπ)) β (1...π))βΆ{1} |
129 | | c0ex 11156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ 0 β
V |
130 | 129 | fconst 6733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}):((2nd
β(πΊβπ)) β ((π + 1)...π))βΆ{0} |
131 | 128, 130 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((2nd β(πΊβπ)) β (1...π)) Γ {1}):((2nd
β(πΊβπ)) β (1...π))βΆ{1} β§
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}):((2nd
β(πΊβπ)) β ((π + 1)...π))βΆ{0}) |
132 | | xp2nd 7959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((πΊβπ) β ((β0
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (2nd β(πΊβπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
133 | 95, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ π β β) β (2nd
β(πΊβπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
134 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
(2nd β(πΊβπ)) β V |
135 | | f1oeq1 6777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π = (2nd β(πΊβπ)) β (π:(1...π)β1-1-ontoβ(1...π) β (2nd β(πΊβπ)):(1...π)β1-1-ontoβ(1...π))) |
136 | 134, 135 | elab 3635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((2nd β(πΊβπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β (2nd β(πΊβπ)):(1...π)β1-1-ontoβ(1...π)) |
137 | 133, 136 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β§ π β β) β (2nd
β(πΊβπ)):(1...π)β1-1-ontoβ(1...π)) |
138 | | dff1o3 6795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
((2nd β(πΊβπ)):(1...π)β1-1-ontoβ(1...π) β ((2nd β(πΊβπ)):(1...π)βontoβ(1...π) β§ Fun β‘(2nd β(πΊβπ)))) |
139 | 138 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((2nd β(πΊβπ)):(1...π)β1-1-ontoβ(1...π) β Fun β‘(2nd β(πΊβπ))) |
140 | | imain 6591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (Fun
β‘(2nd β(πΊβπ)) β ((2nd β(πΊβπ)) β ((1...π) β© ((π + 1)...π))) = (((2nd β(πΊβπ)) β (1...π)) β© ((2nd β(πΊβπ)) β ((π + 1)...π)))) |
141 | 137, 139,
140 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β§ π β β) β ((2nd
β(πΊβπ)) β ((1...π) β© ((π + 1)...π))) = (((2nd β(πΊβπ)) β (1...π)) β© ((2nd β(πΊβπ)) β ((π + 1)...π)))) |
142 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π β (0...π) β π β β0) |
143 | 142 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β (0...π) β π β β) |
144 | 143 | ltp1d 12092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β (0...π) β π < (π + 1)) |
145 | | fzdisj 13475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π < (π + 1) β ((1...π) β© ((π + 1)...π)) = β
) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β (0...π) β ((1...π) β© ((π + 1)...π)) = β
) |
147 | 146 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β (0...π) β ((2nd β(πΊβπ)) β ((1...π) β© ((π + 1)...π))) = ((2nd β(πΊβπ)) β β
)) |
148 | | ima0 6034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((2nd β(πΊβπ)) β β
) =
β
|
149 | 147, 148 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β (0...π) β ((2nd β(πΊβπ)) β ((1...π) β© ((π + 1)...π))) = β
) |
150 | 141, 149 | sylan9req 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ π β β) β§ π β (0...π)) β (((2nd β(πΊβπ)) β (1...π)) β© ((2nd β(πΊβπ)) β ((π + 1)...π))) = β
) |
151 | | fun 6709 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}):((2nd
β(πΊβπ)) β (1...π))βΆ{1} β§
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}):((2nd
β(πΊβπ)) β ((π + 1)...π))βΆ{0}) β§ (((2nd
β(πΊβπ)) β (1...π)) β© ((2nd
β(πΊβπ)) β ((π + 1)...π))) = β
) β ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0})):(((2nd
β(πΊβπ)) β (1...π)) βͺ ((2nd
β(πΊβπ)) β ((π + 1)...π)))βΆ({1} βͺ {0})) |
152 | 131, 150,
151 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β β) β§ π β (0...π)) β ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0})):(((2nd
β(πΊβπ)) β (1...π)) βͺ ((2nd
β(πΊβπ)) β ((π + 1)...π)))βΆ({1} βͺ {0})) |
153 | | imaundi 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((2nd β(πΊβπ)) β ((1...π) βͺ ((π + 1)...π))) = (((2nd β(πΊβπ)) β (1...π)) βͺ ((2nd β(πΊβπ)) β ((π + 1)...π))) |
154 | | nn0p1nn 12459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (π β β0
β (π + 1) β
β) |
155 | 142, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π β (0...π) β (π + 1) β β) |
156 | | nnuz 12813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ β =
(β€β₯β1) |
157 | 155, 156 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β (0...π) β (π + 1) β
(β€β₯β1)) |
158 | | elfzuz3 13445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β (0...π) β π β (β€β₯βπ)) |
159 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (((π + 1) β
(β€β₯β1) β§ π β (β€β₯βπ)) β (1...π) = ((1...π) βͺ ((π + 1)...π))) |
160 | 157, 158,
159 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β (0...π) β (1...π) = ((1...π) βͺ ((π + 1)...π))) |
161 | 160 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β (0...π) β ((2nd β(πΊβπ)) β (1...π)) = ((2nd β(πΊβπ)) β ((1...π) βͺ ((π + 1)...π)))) |
162 | | f1ofo 6796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((2nd β(πΊβπ)):(1...π)β1-1-ontoβ(1...π) β (2nd β(πΊβπ)):(1...π)βontoβ(1...π)) |
163 | | foima 6766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’
((2nd β(πΊβπ)):(1...π)βontoβ(1...π) β ((2nd β(πΊβπ)) β (1...π)) = (1...π)) |
164 | 137, 162,
163 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ π β β) β ((2nd
β(πΊβπ)) β (1...π)) = (1...π)) |
165 | 161, 164 | sylan9req 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β (0...π) β§ (π β§ π β β)) β ((2nd
β(πΊβπ)) β ((1...π) βͺ ((π + 1)...π))) = (1...π)) |
166 | 165 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β§ π β β) β§ π β (0...π)) β ((2nd β(πΊβπ)) β ((1...π) βͺ ((π + 1)...π))) = (1...π)) |
167 | 153, 166 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ π β β) β§ π β (0...π)) β (((2nd β(πΊβπ)) β (1...π)) βͺ ((2nd β(πΊβπ)) β ((π + 1)...π))) = (1...π)) |
168 | 167 | feq2d 6659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π β β) β§ π β (0...π)) β (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0})):(((2nd
β(πΊβπ)) β (1...π)) βͺ ((2nd
β(πΊβπ)) β ((π + 1)...π)))βΆ({1} βͺ {0}) β
((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0})):(1...π)βΆ({1} βͺ {0}))) |
169 | 152, 168 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π β β) β§ π β (0...π)) β ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0})):(1...π)βΆ({1} βͺ {0})) |
170 | 169 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β ({1} βͺ {0})) |
171 | 126, 170 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β β) |
172 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β π β β) |
173 | 171, 172 | nndivred 12214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π) β β) |
174 | 173 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π) β β) |
175 | 174 | absnegd 15341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) = (absβ((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) |
176 | 119, 175 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) = (absβ((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) |
177 | 119, 170 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β ({1} βͺ {0})) |
178 | | elun 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β ({1} βͺ {0}) β
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β¨ (((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0})) |
179 | 177, 178 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β¨ (((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0})) |
180 | | nnrecre 12202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β β (1 /
π) β
β) |
181 | | nnrp 12933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β β β π β
β+) |
182 | 181 | rpreccld 12974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β β (1 /
π) β
β+) |
183 | 182 | rpge0d 12968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β β 0 β€ (1
/ π)) |
184 | 180, 183 | absidd 15314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β β β
(absβ(1 / π)) = (1 /
π)) |
185 | 117, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (absβ(1 / π)) = (1 / π)) |
186 | 117 | nnrecred 12211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (1 / π) β β) |
187 | 107 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (1 / -(ββ-(2 / π))) β
β) |
188 | 110 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (π / 2) β β) |
189 | | eluzle 12783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β
(β€β₯β-(ββ-(2 / π))) β -(ββ-(2 / π)) β€ π) |
190 | 189 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β -(ββ-(2 / π)) β€ π) |
191 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β -(ββ-(2 / π)) β
β) |
192 | 191 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β -(ββ-(2 / π)) β
β+) |
193 | 117 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β π β β+) |
194 | 192, 193 | lerecd 12983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (-(ββ-(2 / π)) β€ π β (1 / π) β€ (1 / -(ββ-(2 / π))))) |
195 | 190, 194 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (1 / π) β€ (1 / -(ββ-(2 / π)))) |
196 | 84 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (1 / -(ββ-(2 / π))) β€ (π / 2)) |
197 | 186, 187,
188, 195, 196 | letrd 11319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (1 / π) β€ (π / 2)) |
198 | 185, 197 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (absβ(1 / π)) β€ (π / 2)) |
199 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β (((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) = 1) |
200 | 199 | fvoveq1d 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β
(absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) = (absβ(1 / π))) |
201 | 200 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β
((absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2) β (absβ(1 / π)) β€ (π / 2))) |
202 | 198, 201 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β ((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β
(absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2))) |
203 | 109 | rpge0d 12968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β β+
β 0 β€ (π /
2)) |
204 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β β β π β
β) |
205 | | nnne0 12194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β β β π β 0) |
206 | 204, 205 | div0d 11937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β β β (0 /
π) = 0) |
207 | 206 | abs00bd 15183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β β β
(absβ(0 / π)) =
0) |
208 | 207 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β β
((absβ(0 / π)) β€
(π / 2) β 0 β€
(π / 2))) |
209 | 208 | biimparc 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((0 β€
(π / 2) β§ π β β) β
(absβ(0 / π)) β€
(π / 2)) |
210 | 203, 209 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β β+
β§ π β β)
β (absβ(0 / π))
β€ (π /
2)) |
211 | 117, 210 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (absβ(0 / π)) β€ (π / 2)) |
212 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0} β (((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) = 0) |
213 | 212 | fvoveq1d 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0} β
(absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) = (absβ(0 / π))) |
214 | 213 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0} β
((absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2) β (absβ(0 / π)) β€ (π / 2))) |
215 | 211, 214 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β ((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0} β
(absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2))) |
216 | 202, 215 | jaod 858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β β+
β§ π β
(β€β₯β-(ββ-(2 / π)))) β (((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β¨ (((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0}) β
(absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2))) |
217 | 216 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β (((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β¨ (((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0}) β
(absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2))) |
218 | 217 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {1} β¨ (((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β {0}) β
(absβ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2))) |
219 | 179, 218 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (absβ((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2)) |
220 | 176, 219 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2)) |
221 | 73, 106 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) β β) |
222 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ πΆ β πΌ) β§ π β β+) β π) |
223 | 222 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β (π β§ π β β)) |
224 | 173 | renegcld 11589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β -((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π) β β) |
225 | 223, 224 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β -((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π) β β) |
226 | 225 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β -((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π) β β) |
227 | 226 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β β) |
228 | 73, 227 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β β) |
229 | 110, 110 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β+
β ((π / 2) β
β β§ (π / 2)
β β)) |
230 | 229 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((π / 2) β β β§ (π / 2) β
β)) |
231 | | ltleadd 11645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) β β β§
(absβ-((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β β) β§ ((π / 2) β β β§ (π / 2) β β)) β
(((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (π / 2) β§ (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2)) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
232 | 221, 228,
230, 231 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (π / 2) β§ (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β€ (π / 2)) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
233 | 220, 232 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (π / 2) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
234 | 105, 226 | abstrid 15348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β€ ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)))) |
235 | 104, 225 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β β) |
236 | 235 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) β β) |
237 | 236 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β β) |
238 | 106, 227 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β β) |
239 | 110, 110 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β+
β ((π / 2) + (π / 2)) β
β) |
240 | 239 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((π / 2) + (π / 2)) β β) |
241 | | lelttr 11252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β β β§ ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β β β§ ((π / 2) + (π / 2)) β β) β
(((absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β€ ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β§ ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2))) β (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
242 | 237, 238,
240, 241 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β€ ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) β§ ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2))) β (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
243 | 234, 242 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)) β (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
244 | 73, 243 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) + (absβ-((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)) β (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
245 | 115, 233,
244 | 3syld 60 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π))) β (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
246 | 100 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((1st β(πΊβπ))βπ) β β) |
247 | 246, 171 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) β β) |
248 | 247, 172 | nndivred 12214 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β) |
249 | 119, 248 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β) |
250 | 245, 249 | jctild 527 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π))) β (((((1st
β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β β§ (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2))))) |
251 | 250 | adantld 492 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β β β§ (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π)))) β (((((1st
β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β β§ (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2))))) |
252 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β (((π β§ πΆ β πΌ) β§ π β β+) β§ π β
β)) |
253 | 87 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β πΆ:(1...π)βΆ(0[,]1)) |
254 | 253 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β (πΆβπ) β (0[,]1)) |
255 | 33, 254 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β (πΆβπ) β β) |
256 | 74 | rpreccld 12974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β+
β (1 / -(ββ-(2 / π))) β
β+) |
257 | 256 | rpxrd 12965 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β+
β (1 / -(ββ-(2 / π))) β
β*) |
258 | 257 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β (1 / -(ββ-(2 / π))) β
β*) |
259 | 13 | rexmet 24170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((abs
β β ) βΎ (β Γ β)) β
(βMetββ) |
260 | | elbl 23757 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§ (πΆβπ) β β β§ (1 /
-(ββ-(2 / π)))
β β*) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β β β§ ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ)) < (1 / -(ββ-(2 / π)))))) |
261 | 259, 260 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πΆβπ) β β β§ (1 /
-(ββ-(2 / π)))
β β*) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β β β§ ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ)) < (1 / -(ββ-(2 / π)))))) |
262 | 255, 258,
261 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β β β§ ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ)) < (1 / -(ββ-(2 / π)))))) |
263 | | elmapfn 8810 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((1st β(πΊβπ)) β (β0
βm (1...π))
β (1st β(πΊβπ)) Fn (1...π)) |
264 | 95, 96, 263 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β) β (1st
β(πΊβπ)) Fn (1...π)) |
265 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ π β V |
266 | | fnconstg 6735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β V β ((1...π) Γ {π}) Fn (1...π)) |
267 | 265, 266 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β) β ((1...π) Γ {π}) Fn (1...π)) |
268 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ π β β) β (1...π) β Fin) |
269 | | inidm 4183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
((1...π) β©
(1...π)) = (1...π) |
270 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ π β (1...π)) β ((1st β(πΊβπ))βπ) = ((1st β(πΊβπ))βπ)) |
271 | 265 | fvconst2 7158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (1...π) β (((1...π) Γ {π})βπ) = π) |
272 | 271 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ π β (1...π)) β (((1...π) Γ {π})βπ) = π) |
273 | 264, 267,
268, 268, 269, 270, 272 | ofval 7633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π β (1...π)) β (((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) = (((1st β(πΊβπ))βπ) / π)) |
274 | 273 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ π β (1...π)) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ)) = ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ))βπ) / π))) |
275 | 222, 274 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ)) = ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ))βπ) / π))) |
276 | 222, 102 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) / π) β β) |
277 | 13 | remetdval 24168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((πΆβπ) β β β§ (((1st
β(πΊβπ))βπ) / π) β β) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ))βπ) / π)) = (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π)))) |
278 | 255, 276,
277 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ))βπ) / π)) = (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π)))) |
279 | 275, 278 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ)) = (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π)))) |
280 | 279 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β (((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ)) < (1 / -(ββ-(2 / π))) β (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π))))) |
281 | 280 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β (((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β β β§ ((πΆβπ)((abs β β ) βΎ (β
Γ β))(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ)) < (1 / -(ββ-(2 / π)))) β ((((1st
β(πΊβπ)) βf /
((1...π) Γ {π}))βπ) β β β§ (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π)))))) |
282 | 262, 281 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (1...π)) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β β β§ (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π)))))) |
283 | 252, 282 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β β β§ (absβ((πΆβπ) β (((1st β(πΊβπ))βπ) / π))) < (1 / -(ββ-(2 / π)))))) |
284 | | rpxr 12931 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β+
β π β
β*) |
285 | 284 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β π β β*) |
286 | | elbl 23757 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((abs
β β ) βΎ (β Γ β)) β
(βMetββ) β§ (πΆβπ) β β β§ π β β*) β
(((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β β β§ ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ)) < π))) |
287 | 259, 286 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((πΆβπ) β β β§ π β β*) β
(((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β β β§ ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ)) < π))) |
288 | 90, 285, 287 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β β β§ ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ)) < π))) |
289 | | elun 4113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π§ β ({1} βͺ {0}) β
(π§ β {1} β¨ π§ β {0})) |
290 | | fzofzp1 13676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π£ β (0..^π) β (π£ + 1) β (0...π)) |
291 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π§ β {1} β π§ = 1) |
292 | 291 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π§ β {1} β (π£ + π§) = (π£ + 1)) |
293 | 292 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π§ β {1} β ((π£ + π§) β (0...π) β (π£ + 1) β (0...π))) |
294 | 290, 293 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π£ β (0..^π) β (π§ β {1} β (π£ + π§) β (0...π))) |
295 | | elfzonn0 13624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π£ β (0..^π) β π£ β β0) |
296 | 295 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π£ β (0..^π) β π£ β β) |
297 | 296 | addid1d 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π£ β (0..^π) β (π£ + 0) = π£) |
298 | | elfzofz 13595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π£ β (0..^π) β π£ β (0...π)) |
299 | 297, 298 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π£ β (0..^π) β (π£ + 0) β (0...π)) |
300 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π§ β {0} β π§ = 0) |
301 | 300 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π§ β {0} β (π£ + π§) = (π£ + 0)) |
302 | 301 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π§ β {0} β ((π£ + π§) β (0...π) β (π£ + 0) β (0...π))) |
303 | 299, 302 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π£ β (0..^π) β (π§ β {0} β (π£ + π§) β (0...π))) |
304 | 294, 303 | jaod 858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π£ β (0..^π) β ((π§ β {1} β¨ π§ β {0}) β (π£ + π§) β (0...π))) |
305 | 289, 304 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π£ β (0..^π) β (π§ β ({1} βͺ {0}) β (π£ + π§) β (0...π))) |
306 | 305 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π£ β (0..^π) β§ π§ β ({1} βͺ {0})) β (π£ + π§) β (0...π)) |
307 | 306 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ π β β) β§ π β (0...π)) β§ (π£ β (0..^π) β§ π§ β ({1} βͺ {0}))) β (π£ + π§) β (0...π)) |
308 | | dffn3 6686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
((1st β(πΊβπ)) Fn (1...π) β (1st β(πΊβπ)):(1...π)βΆran (1st β(πΊβπ))) |
309 | 264, 308 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β β) β (1st
β(πΊβπ)):(1...π)βΆran (1st β(πΊβπ))) |
310 | | poimirlem30.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ π β β) β ran (1st
β(πΊβπ)) β (0..^π)) |
311 | 309, 310 | fssd 6691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ π β β) β (1st
β(πΊβπ)):(1...π)βΆ(0..^π)) |
312 | 311 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ π β (0...π)) β (1st β(πΊβπ)):(1...π)βΆ(0..^π)) |
313 | | fzfid 13885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β β) β§ π β (0...π)) β (1...π) β Fin) |
314 | 307, 312,
169, 313, 313, 269 | off 7640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π β (0...π)) β ((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))):(1...π)βΆ(0...π)) |
315 | 314 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ π β (0...π)) β ((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) Fn (1...π)) |
316 | 265, 266 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β β) β§ π β (0...π)) β ((1...π) Γ {π}) Fn (1...π)) |
317 | 264 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π β (0...π)) β (1st β(πΊβπ)) Fn (1...π)) |
318 | 169 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β β) β§ π β (0...π)) β ((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0})) Fn (1...π)) |
319 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((1st β(πΊβπ))βπ) = ((1st β(πΊβπ))βπ)) |
320 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) = (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) |
321 | 317, 318,
313, 313, 269, 319, 320 | ofval 7633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0})))βπ) = (((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ))) |
322 | 271 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((1...π) Γ {π})βπ) = π) |
323 | 315, 316,
313, 313, 269, 321, 322 | ofval 7633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) = ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)) |
324 | 323 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β β β ((((1st
β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β)) |
325 | 223, 324 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β β β ((((1st
β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β)) |
326 | 323 | adantl3r 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) = ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)) |
327 | 326 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ)) = ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π))) |
328 | 87 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β πΆ:(1...π)βΆ(0[,]1)) |
329 | 328 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (πΆβπ) β (0[,]1)) |
330 | 33, 329 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (πΆβπ) β β) |
331 | 248 | adantl3r 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β) |
332 | 13 | remetdval 24168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((πΆβπ) β β β§ ((((1st
β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)) = (absβ((πΆβπ) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)))) |
333 | 330, 331,
332 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)) = (absβ((πΆβπ) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)))) |
334 | 246 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((1st β(πΊβπ))βπ) β β) |
335 | 171 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) β β) |
336 | 204 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β π β β) |
337 | 205 | ad3antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β π β 0) |
338 | 334, 335,
336, 337 | divdird 11976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) = ((((1st β(πΊβπ))βπ) / π) + ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) |
339 | 102 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ π β β) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) / π) β β) |
340 | 339 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) / π) β β) |
341 | 340, 174 | subnegd 11526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ))βπ) / π) β -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)) = ((((1st β(πΊβπ))βπ) / π) + ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) |
342 | 338, 341 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) = ((((1st β(πΊβπ))βπ) / π) β -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) |
343 | 342 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)) = ((πΆβπ) β ((((1st β(πΊβπ))βπ) / π) β -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)))) |
344 | 343 | adantl3r 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)) = ((πΆβπ) β ((((1st β(πΊβπ))βπ) / π) β -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)))) |
345 | 330 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (πΆβπ) β β) |
346 | 102 | adantllr 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ πΆ β πΌ) β§ π β β) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) / π) β β) |
347 | 346 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) / π) β β) |
348 | 347 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((1st β(πΊβπ))βπ) / π) β β) |
349 | 174 | adantl3r 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π) β β) |
350 | 349 | negcld 11506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β -((((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π) β β) |
351 | 345, 348,
350 | subsubd 11547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ) β ((((1st β(πΊβπ))βπ) / π) β -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) = (((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) |
352 | 344, 351 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π)) = (((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) |
353 | 352 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (absβ((πΆβπ) β ((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π))) = (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)))) |
354 | 327, 333,
353 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ πΆ β πΌ) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ)) = (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)))) |
355 | 354 | adantl3r 749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ)) = (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π)))) |
356 | 77 | 2halvesd 12406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β+
β ((π / 2) + (π / 2)) = π) |
357 | 356 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β+
β π = ((π / 2) + (π / 2))) |
358 | 357 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β π = ((π / 2) + (π / 2))) |
359 | 355, 358 | breq12d 5123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ)) < π β (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2)))) |
360 | 325, 359 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β ((((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β β β§ ((πΆβπ)((abs β β ) βΎ (β
Γ β))((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ)) < π) β (((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β β§ (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2))))) |
361 | 288, 360 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β β) β§ π β (0...π)) β§ π β (1...π)) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β (((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β β§ (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2))))) |
362 | 73, 361 | sylanl1 679 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β (((((1st β(πΊβπ))βπ) + (((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ)) / π) β β β§ (absβ(((πΆβπ) β (((1st β(πΊβπ))βπ) / π)) + -((((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))βπ) / π))) < ((π / 2) + (π / 2))))) |
363 | 251, 283,
362 | 3imtr4d 294 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β§ π β (1...π)) β ((((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π))) |
364 | 363 | ralimdva 3165 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β (βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β βπ β (1...π)((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π))) |
365 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β) β§ π β (0...π)) β π β β) |
366 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π£ β (0...π) β π£ β β0) |
367 | 366 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π£ β (0...π) β π£ β β) |
368 | | nndivre 12201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π£ β β β§ π β β) β (π£ / π) β β) |
369 | 367, 368 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π£ β (0...π) β§ π β β) β (π£ / π) β β) |
370 | | elfzle1 13451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π£ β (0...π) β 0 β€ π£) |
371 | 367, 370 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π£ β (0...π) β (π£ β β β§ 0 β€ π£)) |
372 | 181 | rpregt0d 12970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β β (π β β β§ 0 <
π)) |
373 | | divge0 12031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π£ β β β§ 0 β€
π£) β§ (π β β β§ 0 <
π)) β 0 β€ (π£ / π)) |
374 | 371, 372,
373 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π£ β (0...π) β§ π β β) β 0 β€ (π£ / π)) |
375 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π£ β (0...π) β π£ β€ π) |
376 | 375 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π£ β (0...π) β§ π β β) β π£ β€ π) |
377 | 367 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π£ β (0...π) β§ π β β) β π£ β β) |
378 | | 1red 11163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π£ β (0...π) β§ π β β) β 1 β
β) |
379 | 181 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π£ β (0...π) β§ π β β) β π β β+) |
380 | 377, 378,
379 | ledivmuld 13017 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π£ β (0...π) β§ π β β) β ((π£ / π) β€ 1 β π£ β€ (π Β· 1))) |
381 | 204 | mulid1d 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β β β (π Β· 1) = π) |
382 | 381 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β β β (π£ β€ (π Β· 1) β π£ β€ π)) |
383 | 382 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π£ β (0...π) β§ π β β) β (π£ β€ (π Β· 1) β π£ β€ π)) |
384 | 380, 383 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π£ β (0...π) β§ π β β) β ((π£ / π) β€ 1 β π£ β€ π)) |
385 | 376, 384 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π£ β (0...π) β§ π β β) β (π£ / π) β€ 1) |
386 | | elicc01 13390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π£ / π) β (0[,]1) β ((π£ / π) β β β§ 0 β€ (π£ / π) β§ (π£ / π) β€ 1)) |
387 | 369, 374,
385, 386 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π£ β (0...π) β§ π β β) β (π£ / π) β (0[,]1)) |
388 | 387 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β β§ π£ β (0...π)) β (π£ / π) β (0[,]1)) |
389 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ β {π} β π§ = π) |
390 | 389 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ β {π} β (π£ / π§) = (π£ / π)) |
391 | 390 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ β {π} β ((π£ / π§) β (0[,]1) β (π£ / π) β (0[,]1))) |
392 | 388, 391 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β β β§ π£ β (0...π)) β (π§ β {π} β (π£ / π§) β (0[,]1))) |
393 | 392 | impr 456 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β β§ (π£ β (0...π) β§ π§ β {π})) β (π£ / π§) β (0[,]1)) |
394 | 365, 393 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β β) β§ π β (0...π)) β§ (π£ β (0...π) β§ π§ β {π})) β (π£ / π§) β (0[,]1)) |
395 | 265 | fconst 6733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((1...π) Γ
{π}):(1...π)βΆ{π} |
396 | 395 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β) β§ π β (0...π)) β ((1...π) Γ {π}):(1...π)βΆ{π}) |
397 | 394, 314,
396, 313, 313, 269 | off 7640 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β (0...π)) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})):(1...π)βΆ(0[,]1)) |
398 | 397 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π β (0...π)) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) Fn (1...π)) |
399 | 119, 398 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) Fn (1...π)) |
400 | 364, 399 | jctild 527 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β (βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) Fn (1...π) β§ βπ β (1...π)((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π)))) |
401 | 8 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β ((0[,]1)
βm (1...π))) |
402 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0[,]1)
β V |
403 | 402, 37 | elmap 8816 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β ((0[,]1)
βm (1...π))
β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})):(1...π)βΆ(0[,]1)) |
404 | 401, 403 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})):(1...π)βΆ(0[,]1)) |
405 | 397, 404 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π β (0...π)) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ) |
406 | 119, 405 | sylan 581 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ) |
407 | 400, 406 | jctird 528 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β (βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) Fn (1...π) β§ βπ β (1...π)((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π)) β§ (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ))) |
408 | | elin 3931 |
. . . . . . . . . . . . . . . . . . 19
β’
((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β ((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β§ (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ)) |
409 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β V |
410 | 409 | elixp 8849 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β ((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) Fn (1...π) β§ βπ β (1...π)((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π))) |
411 | 410 | anbi1i 625 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β§ (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) Fn (1...π) β§ βπ β (1...π)((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π)) β§ (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ)) |
412 | 408, 411 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
β’
((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β (((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) Fn (1...π) β§ βπ β (1...π)((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π)) β§ (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β πΌ)) |
413 | 407, 412 | syl6ibr 252 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β (βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ))) |
414 | | ssel 3942 |
. . . . . . . . . . . . . . . . . 18
β’ ((Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β ((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£)) |
415 | 414 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’
((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β ((Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£)) |
416 | 413, 415 | syl6 35 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β (βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£))) |
417 | 416 | impd 412 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β§ π β (0...π)) β ((βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β§ (Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£) β (((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£)) |
418 | 417 | ralrimdva 3152 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β ((βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β§ (Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£) β βπ β (0...π)(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£)) |
419 | 418 | expd 417 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β (βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β βπ β (0...π)(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£))) |
420 | | poimirlem30.4 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β β β§ π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0ππ) |
421 | 420 | 3exp2 1355 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β β β (π β (1...π) β (π β { β€ , β‘ β€ } β βπ β (0...π)0ππ)))) |
422 | 421 | imp43 429 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π β (1...π) β§ π β { β€ , β‘ β€ })) β βπ β (0...π)0ππ) |
423 | | r19.29 3118 |
. . . . . . . . . . . . . . . . . . . 20
β’
((βπ β
(0...π)(((1st
β(πΊβπ)) βf +
((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β§ βπ β (0...π)0ππ) β βπ β (0...π)((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β§ 0ππ)) |
424 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ = (((1st
β(πΊβπ)) βf +
((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β (πΉβπ§) = (πΉβ(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))) |
425 | 424 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ = (((1st
β(πΊβπ)) βf +
((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β ((πΉβπ§)βπ) = ((πΉβ(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ)) |
426 | | poimirlem30.x |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ π = ((πΉβ(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})))βπ) |
427 | 425, 426 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ = (((1st
β(πΊβπ)) βf +
((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β ((πΉβπ§)βπ) = π) |
428 | 427 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ = (((1st
β(πΊβπ)) βf +
((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β (0π((πΉβπ§)βπ) β 0ππ)) |
429 | 428 | rspcev 3584 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β§ 0ππ) β βπ§ β π£ 0π((πΉβπ§)βπ)) |
430 | 429 | rexlimivw 3149 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
(0...π)((((1st
β(πΊβπ)) βf +
((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β§ 0ππ) β βπ§ β π£ 0π((πΉβπ§)βπ)) |
431 | 423, 430 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
((βπ β
(0...π)(((1st
β(πΊβπ)) βf +
((((2nd β(πΊβπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β§ βπ β (0...π)0ππ) β βπ§ β π£ 0π((πΉβπ§)βπ)) |
432 | 431 | expcom 415 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
(0...π)0ππ β (βπ β (0...π)(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β βπ§ β π£ 0π((πΉβπ§)βπ))) |
433 | 422, 432 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π β (1...π) β§ π β { β€ , β‘ β€ })) β (βπ β (0...π)(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β βπ§ β π£ 0π((πΉβπ§)βπ))) |
434 | 433 | ralrimdvva 3204 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (βπ β (0...π)(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
435 | 117, 434 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β+ β§ π β
(β€β₯β-(ββ-(2 / π))))) β (βπ β (0...π)(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
436 | 435 | anassrs 469 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β (βπ β (0...π)(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
437 | 436 | adantllr 718 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β (βπ β (0...π)(((1st β(πΊβπ)) βf + ((((2nd
β(πΊβπ)) β (1...π)) Γ {1}) βͺ
(((2nd β(πΊβπ)) β ((π + 1)...π)) Γ {0}))) βf /
((1...π) Γ {π})) β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
438 | 419, 437 | syl6d 75 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β πΌ) β§ π β β+) β§ π β
(β€β₯β-(ββ-(2 / π)))) β (βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
439 | 438 | rexlimdva 3153 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β πΌ) β§ π β β+) β
(βπ β
(β€β₯β-(ββ-(2 / π)))βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / -(ββ-(2 / π)))) β ((Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
440 | 68, 439 | syld 47 |
. . . . . . . . . 10
β’ (((π β§ πΆ β πΌ) β§ π β β+) β
(βπ β β
βπ β
(β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β ((Xπ β (1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
441 | 440 | com23 86 |
. . . . . . . . 9
β’ (((π β§ πΆ β πΌ) β§ π β β+) β ((Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£ β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
442 | 441 | impr 456 |
. . . . . . . 8
β’ (((π β§ πΆ β πΌ) β§ (π β β+ β§ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£)) β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
443 | 45, 442 | sylanl2 680 |
. . . . . . 7
β’ (((π β§ (π£ β (π
βΎt πΌ) β§ πΆ β π£)) β§ (π β β+ β§ (Xπ β
(1...π)((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))π) β© πΌ) β π£)) β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
444 | 29, 443 | rexlimddv 3159 |
. . . . . 6
β’ ((π β§ (π£ β (π
βΎt πΌ) β§ πΆ β π£)) β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
445 | 444 | expr 458 |
. . . . 5
β’ ((π β§ π£ β (π
βΎt πΌ)) β (πΆ β π£ β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
446 | 445 | com23 86 |
. . . 4
β’ ((π β§ π£ β (π
βΎt πΌ)) β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β (πΆ β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
447 | | r19.21v 3177 |
. . . 4
β’
(βπ β
(1...π)(πΆ β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β (πΆ β π£ β βπ β (1...π)βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
448 | 446, 447 | syl6ibr 252 |
. . 3
β’ ((π β§ π£ β (π
βΎt πΌ)) β (βπ β β βπ β (β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β (1...π)(πΆ β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
449 | 448 | ralrimdva 3152 |
. 2
β’ (π β (βπ β β βπ β
(β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ£ β (π
βΎt πΌ)βπ β (1...π)(πΆ β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |
450 | | ralcom 3275 |
. 2
β’
(βπ£ β
(π
βΎt
πΌ)βπ β (1...π)(πΆ β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)) β βπ β (1...π)βπ£ β (π
βΎt πΌ)(πΆ β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ))) |
451 | 449, 450 | syl6ib 251 |
1
β’ (π β (βπ β β βπ β
(β€β₯βπ)βπ β (1...π)(((1st β(πΊβπ)) βf / ((1...π) Γ {π}))βπ) β ((πΆβπ)(ballβ((abs β β ) βΎ
(β Γ β)))(1 / π)) β βπ β (1...π)βπ£ β (π
βΎt πΌ)(πΆ β π£ β βπ β { β€ , β‘ β€ }βπ§ β π£ 0π((πΉβπ§)βπ)))) |