Step | Hyp | Ref
| Expression |
1 | | stoweidlem11.2 |
. . 3
β’ (π β π‘ β π) |
2 | | sumex 15581 |
. . 3
β’
Ξ£π β
(0...π)(πΈ Β· ((πβπ)βπ‘)) β V |
3 | | eqid 2733 |
. . . 4
β’ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
4 | 3 | fvmpt2 6963 |
. . 3
β’ ((π‘ β π β§ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) β V) β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
5 | 1, 2, 4 | sylancl 587 |
. 2
β’ (π β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
6 | | fzfid 13887 |
. . . 4
β’ (π β (0...π) β Fin) |
7 | | stoweidlem11.7 |
. . . . . . 7
β’ (π β πΈ β
β+) |
8 | 7 | rpred 12965 |
. . . . . 6
β’ (π β πΈ β β) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0...π)) β πΈ β β) |
10 | | stoweidlem11.4 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πβπ):πβΆβ) |
11 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0...π)) β π‘ β π) |
12 | 10, 11 | ffvelcdmd 7040 |
. . . . 5
β’ ((π β§ π β (0...π)) β ((πβπ)βπ‘) β β) |
13 | 9, 12 | remulcld 11193 |
. . . 4
β’ ((π β§ π β (0...π)) β (πΈ Β· ((πβπ)βπ‘)) β β) |
14 | 6, 13 | fsumrecl 15627 |
. . 3
β’ (π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) β β) |
15 | | stoweidlem11.3 |
. . . . . . 7
β’ (π β π β (1...π)) |
16 | 15 | elfzelzd 13451 |
. . . . . 6
β’ (π β π β β€) |
17 | 16 | zred 12615 |
. . . . 5
β’ (π β π β β) |
18 | 8, 17 | remulcld 11193 |
. . . 4
β’ (π β (πΈ Β· π) β β) |
19 | | stoweidlem11.1 |
. . . . . . . 8
β’ (π β π β β) |
20 | 19 | nnred 12176 |
. . . . . . 7
β’ (π β π β β) |
21 | 20, 17 | resubcld 11591 |
. . . . . 6
β’ (π β (π β π) β β) |
22 | | 1red 11164 |
. . . . . 6
β’ (π β 1 β
β) |
23 | 21, 22 | readdcld 11192 |
. . . . 5
β’ (π β ((π β π) + 1) β β) |
24 | 8, 19 | nndivred 12215 |
. . . . . 6
β’ (π β (πΈ / π) β β) |
25 | 8, 24 | remulcld 11193 |
. . . . 5
β’ (π β (πΈ Β· (πΈ / π)) β β) |
26 | 23, 25 | remulcld 11193 |
. . . 4
β’ (π β (((π β π) + 1) Β· (πΈ Β· (πΈ / π))) β β) |
27 | 18, 26 | readdcld 11192 |
. . 3
β’ (π β ((πΈ Β· π) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) β β) |
28 | | 3re 12241 |
. . . . . . 7
β’ 3 β
β |
29 | 28 | a1i 11 |
. . . . . 6
β’ (π β 3 β
β) |
30 | | 3ne0 12267 |
. . . . . . 7
β’ 3 β
0 |
31 | 30 | a1i 11 |
. . . . . 6
β’ (π β 3 β 0) |
32 | 29, 31 | rereccld 11990 |
. . . . 5
β’ (π β (1 / 3) β
β) |
33 | 17, 32 | readdcld 11192 |
. . . 4
β’ (π β (π + (1 / 3)) β β) |
34 | 33, 8 | remulcld 11193 |
. . 3
β’ (π β ((π + (1 / 3)) Β· πΈ) β β) |
35 | | fzfid 13887 |
. . . . . 6
β’ (π β (0...(π β 1)) β Fin) |
36 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...(π β 1))) β πΈ β β) |
37 | | elfzelz 13450 |
. . . . . . . . . . . 12
β’ (π β (1...π) β π β β€) |
38 | | peano2zm 12554 |
. . . . . . . . . . . 12
β’ (π β β€ β (π β 1) β
β€) |
39 | 15, 37, 38 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β (π β 1) β β€) |
40 | 19 | nnzd 12534 |
. . . . . . . . . . 11
β’ (π β π β β€) |
41 | 17, 22 | resubcld 11591 |
. . . . . . . . . . . 12
β’ (π β (π β 1) β β) |
42 | 17 | lem1d 12096 |
. . . . . . . . . . . 12
β’ (π β (π β 1) β€ π) |
43 | | elfzuz3 13447 |
. . . . . . . . . . . . 13
β’ (π β (1...π) β π β (β€β₯βπ)) |
44 | | eluzle 12784 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β π β€ π) |
45 | 15, 43, 44 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β π β€ π) |
46 | 41, 17, 20, 42, 45 | letrd 11320 |
. . . . . . . . . . 11
β’ (π β (π β 1) β€ π) |
47 | | eluz2 12777 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β(π β 1)) β ((π β 1) β β€ β§ π β β€ β§ (π β 1) β€ π)) |
48 | 39, 40, 46, 47 | syl3anbrc 1344 |
. . . . . . . . . 10
β’ (π β π β (β€β₯β(π β 1))) |
49 | | fzss2 13490 |
. . . . . . . . . 10
β’ (π β
(β€β₯β(π β 1)) β (0...(π β 1)) β (0...π)) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
β’ (π β (0...(π β 1)) β (0...π)) |
51 | 50 | sselda 3948 |
. . . . . . . 8
β’ ((π β§ π β (0...(π β 1))) β π β (0...π)) |
52 | 51, 12 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β (0...(π β 1))) β ((πβπ)βπ‘) β β) |
53 | 36, 52 | remulcld 11193 |
. . . . . 6
β’ ((π β§ π β (0...(π β 1))) β (πΈ Β· ((πβπ)βπ‘)) β β) |
54 | 35, 53 | fsumrecl 15627 |
. . . . 5
β’ (π β Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) β β) |
55 | 54, 26 | readdcld 11192 |
. . . 4
β’ (π β (Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) β β) |
56 | 17 | ltm1d 12095 |
. . . . . . 7
β’ (π β (π β 1) < π) |
57 | | fzdisj 13477 |
. . . . . . 7
β’ ((π β 1) < π β ((0...(π β 1)) β© (π...π)) = β
) |
58 | 56, 57 | syl 17 |
. . . . . 6
β’ (π β ((0...(π β 1)) β© (π...π)) = β
) |
59 | | fzssp1 13493 |
. . . . . . . . . 10
β’
(0...(π β 1))
β (0...((π β 1)
+ 1)) |
60 | 19 | nncnd 12177 |
. . . . . . . . . . . 12
β’ (π β π β β) |
61 | | 1cnd 11158 |
. . . . . . . . . . . 12
β’ (π β 1 β
β) |
62 | 60, 61 | npcand 11524 |
. . . . . . . . . . 11
β’ (π β ((π β 1) + 1) = π) |
63 | 62 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π β (0...((π β 1) + 1)) = (0...π)) |
64 | 59, 63 | sseqtrid 4000 |
. . . . . . . . 9
β’ (π β (0...(π β 1)) β (0...π)) |
65 | | 1zzd 12542 |
. . . . . . . . . . . 12
β’ (π β 1 β
β€) |
66 | | fzsubel 13486 |
. . . . . . . . . . . 12
β’ (((1
β β€ β§ π
β β€) β§ (π
β β€ β§ 1 β β€)) β (π β (1...π) β (π β 1) β ((1 β 1)...(π β 1)))) |
67 | 65, 40, 16, 65, 66 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π β (π β (1...π) β (π β 1) β ((1 β 1)...(π β 1)))) |
68 | 15, 67 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (π β 1) β ((1 β 1)...(π β 1))) |
69 | | 1m1e0 12233 |
. . . . . . . . . . 11
β’ (1
β 1) = 0 |
70 | 69 | oveq1i 7371 |
. . . . . . . . . 10
β’ ((1
β 1)...(π β 1))
= (0...(π β
1)) |
71 | 68, 70 | eleqtrdi 2844 |
. . . . . . . . 9
β’ (π β (π β 1) β (0...(π β 1))) |
72 | 64, 71 | sseldd 3949 |
. . . . . . . 8
β’ (π β (π β 1) β (0...π)) |
73 | | fzsplit 13476 |
. . . . . . . 8
β’ ((π β 1) β (0...π) β (0...π) = ((0...(π β 1)) βͺ (((π β 1) + 1)...π))) |
74 | 72, 73 | syl 17 |
. . . . . . 7
β’ (π β (0...π) = ((0...(π β 1)) βͺ (((π β 1) + 1)...π))) |
75 | 16 | zcnd 12616 |
. . . . . . . . . 10
β’ (π β π β β) |
76 | 75, 61 | npcand 11524 |
. . . . . . . . 9
β’ (π β ((π β 1) + 1) = π) |
77 | 76 | oveq1d 7376 |
. . . . . . . 8
β’ (π β (((π β 1) + 1)...π) = (π...π)) |
78 | 77 | uneq2d 4127 |
. . . . . . 7
β’ (π β ((0...(π β 1)) βͺ (((π β 1) + 1)...π)) = ((0...(π β 1)) βͺ (π...π))) |
79 | 74, 78 | eqtrd 2773 |
. . . . . 6
β’ (π β (0...π) = ((0...(π β 1)) βͺ (π...π))) |
80 | 7 | rpcnd 12967 |
. . . . . . . 8
β’ (π β πΈ β β) |
81 | 80 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β πΈ β β) |
82 | 12 | recnd 11191 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β ((πβπ)βπ‘) β β) |
83 | 81, 82 | mulcld 11183 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πΈ Β· ((πβπ)βπ‘)) β β) |
84 | 58, 79, 6, 83 | fsumsplit 15634 |
. . . . 5
β’ (π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) = (Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) + Ξ£π β (π...π)(πΈ Β· ((πβπ)βπ‘)))) |
85 | | fzfid 13887 |
. . . . . . 7
β’ (π β (π...π) β Fin) |
86 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π...π)) β πΈ β β) |
87 | | 0zd 12519 |
. . . . . . . . . . . . 13
β’ (π β 0 β
β€) |
88 | | 0red 11166 |
. . . . . . . . . . . . . 14
β’ (π β 0 β
β) |
89 | | 0le1 11686 |
. . . . . . . . . . . . . . 15
β’ 0 β€
1 |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 0 β€ 1) |
91 | | elfzuz 13446 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β π β
(β€β₯β1)) |
92 | 15, 91 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
(β€β₯β1)) |
93 | | eluz2 12777 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β1) β (1 β β€ β§ π β β€ β§ 1 β€
π)) |
94 | 92, 93 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π β (1 β β€ β§
π β β€ β§ 1
β€ π)) |
95 | 94 | simp3d 1145 |
. . . . . . . . . . . . . 14
β’ (π β 1 β€ π) |
96 | 88, 22, 17, 90, 95 | letrd 11320 |
. . . . . . . . . . . . 13
β’ (π β 0 β€ π) |
97 | | eluz2 12777 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β0) β (0 β β€ β§ π β β€ β§ 0 β€
π)) |
98 | 87, 16, 96, 97 | syl3anbrc 1344 |
. . . . . . . . . . . 12
β’ (π β π β
(β€β₯β0)) |
99 | | fzss1 13489 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β0) β (π...π) β (0...π)) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π...π) β (0...π)) |
101 | 100 | sselda 3948 |
. . . . . . . . . 10
β’ ((π β§ π β (π...π)) β π β (0...π)) |
102 | 101, 10 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π β (π...π)) β (πβπ):πβΆβ) |
103 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π...π)) β π‘ β π) |
104 | 102, 103 | ffvelcdmd 7040 |
. . . . . . . 8
β’ ((π β§ π β (π...π)) β ((πβπ)βπ‘) β β) |
105 | 86, 104 | remulcld 11193 |
. . . . . . 7
β’ ((π β§ π β (π...π)) β (πΈ Β· ((πβπ)βπ‘)) β β) |
106 | 85, 105 | fsumrecl 15627 |
. . . . . 6
β’ (π β Ξ£π β (π...π)(πΈ Β· ((πβπ)βπ‘)) β β) |
107 | | eluzfz2 13458 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π β (π...π)) |
108 | | ne0i 4298 |
. . . . . . . . 9
β’ (π β (π...π) β (π...π) β β
) |
109 | 15, 43, 107, 108 | 4syl 19 |
. . . . . . . 8
β’ (π β (π...π) β β
) |
110 | 19 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π...π)) β π β β) |
111 | 86, 110 | nndivred 12215 |
. . . . . . . . 9
β’ ((π β§ π β (π...π)) β (πΈ / π) β β) |
112 | 86, 111 | remulcld 11193 |
. . . . . . . 8
β’ ((π β§ π β (π...π)) β (πΈ Β· (πΈ / π)) β β) |
113 | | stoweidlem11.6 |
. . . . . . . . 9
β’ ((π β§ π β (π...π)) β ((πβπ)βπ‘) < (πΈ / π)) |
114 | 7 | rpgt0d 12968 |
. . . . . . . . . . 11
β’ (π β 0 < πΈ) |
115 | 114 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π...π)) β 0 < πΈ) |
116 | | ltmul2 12014 |
. . . . . . . . . 10
β’ ((((πβπ)βπ‘) β β β§ (πΈ / π) β β β§ (πΈ β β β§ 0 < πΈ)) β (((πβπ)βπ‘) < (πΈ / π) β (πΈ Β· ((πβπ)βπ‘)) < (πΈ Β· (πΈ / π)))) |
117 | 104, 111,
86, 115, 116 | syl112anc 1375 |
. . . . . . . . 9
β’ ((π β§ π β (π...π)) β (((πβπ)βπ‘) < (πΈ / π) β (πΈ Β· ((πβπ)βπ‘)) < (πΈ Β· (πΈ / π)))) |
118 | 113, 117 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β (π...π)) β (πΈ Β· ((πβπ)βπ‘)) < (πΈ Β· (πΈ / π))) |
119 | 85, 109, 105, 112, 118 | fsumlt 15693 |
. . . . . . 7
β’ (π β Ξ£π β (π...π)(πΈ Β· ((πβπ)βπ‘)) < Ξ£π β (π...π)(πΈ Β· (πΈ / π))) |
120 | 19 | nnne0d 12211 |
. . . . . . . . . . 11
β’ (π β π β 0) |
121 | 80, 60, 120 | divcld 11939 |
. . . . . . . . . 10
β’ (π β (πΈ / π) β β) |
122 | 80, 121 | mulcld 11183 |
. . . . . . . . 9
β’ (π β (πΈ Β· (πΈ / π)) β β) |
123 | | fsumconst 15683 |
. . . . . . . . 9
β’ (((π...π) β Fin β§ (πΈ Β· (πΈ / π)) β β) β Ξ£π β (π...π)(πΈ Β· (πΈ / π)) = ((β―β(π...π)) Β· (πΈ Β· (πΈ / π)))) |
124 | 85, 122, 123 | syl2anc 585 |
. . . . . . . 8
β’ (π β Ξ£π β (π...π)(πΈ Β· (πΈ / π)) = ((β―β(π...π)) Β· (πΈ Β· (πΈ / π)))) |
125 | | hashfz 14336 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (β―β(π...π)) = ((π β π) + 1)) |
126 | 15, 43, 125 | 3syl 18 |
. . . . . . . . 9
β’ (π β (β―β(π...π)) = ((π β π) + 1)) |
127 | 126 | oveq1d 7376 |
. . . . . . . 8
β’ (π β ((β―β(π...π)) Β· (πΈ Β· (πΈ / π))) = (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) |
128 | 124, 127 | eqtrd 2773 |
. . . . . . 7
β’ (π β Ξ£π β (π...π)(πΈ Β· (πΈ / π)) = (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) |
129 | 119, 128 | breqtrd 5135 |
. . . . . 6
β’ (π β Ξ£π β (π...π)(πΈ Β· ((πβπ)βπ‘)) < (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) |
130 | 106, 26, 54, 129 | ltadd2dd 11322 |
. . . . 5
β’ (π β (Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) + Ξ£π β (π...π)(πΈ Β· ((πβπ)βπ‘))) < (Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π))))) |
131 | 84, 130 | eqbrtrd 5131 |
. . . 4
β’ (π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) < (Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π))))) |
132 | | stoweidlem11.5 |
. . . . . . . . . 10
β’ ((π β§ π β (0...π)) β ((πβπ)βπ‘) β€ 1) |
133 | 51, 132 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π β 1))) β ((πβπ)βπ‘) β€ 1) |
134 | | 1red 11164 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π β 1))) β 1 β
β) |
135 | 114 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π β 1))) β 0 < πΈ) |
136 | | lemul2 12016 |
. . . . . . . . . 10
β’ ((((πβπ)βπ‘) β β β§ 1 β β β§
(πΈ β β β§ 0
< πΈ)) β (((πβπ)βπ‘) β€ 1 β (πΈ Β· ((πβπ)βπ‘)) β€ (πΈ Β· 1))) |
137 | 52, 134, 36, 135, 136 | syl112anc 1375 |
. . . . . . . . 9
β’ ((π β§ π β (0...(π β 1))) β (((πβπ)βπ‘) β€ 1 β (πΈ Β· ((πβπ)βπ‘)) β€ (πΈ Β· 1))) |
138 | 133, 137 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β (0...(π β 1))) β (πΈ Β· ((πβπ)βπ‘)) β€ (πΈ Β· 1)) |
139 | 80 | mulid1d 11180 |
. . . . . . . . 9
β’ (π β (πΈ Β· 1) = πΈ) |
140 | 139 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...(π β 1))) β (πΈ Β· 1) = πΈ) |
141 | 138, 140 | breqtrd 5135 |
. . . . . . 7
β’ ((π β§ π β (0...(π β 1))) β (πΈ Β· ((πβπ)βπ‘)) β€ πΈ) |
142 | 35, 53, 36, 141 | fsumle 15692 |
. . . . . 6
β’ (π β Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) β€ Ξ£π β (0...(π β 1))πΈ) |
143 | | fsumconst 15683 |
. . . . . . . 8
β’
(((0...(π β
1)) β Fin β§ πΈ
β β) β Ξ£π β (0...(π β 1))πΈ = ((β―β(0...(π β 1))) Β· πΈ)) |
144 | 35, 80, 143 | syl2anc 585 |
. . . . . . 7
β’ (π β Ξ£π β (0...(π β 1))πΈ = ((β―β(0...(π β 1))) Β· πΈ)) |
145 | | 0z 12518 |
. . . . . . . . . . 11
β’ 0 β
β€ |
146 | | 1e0p1 12668 |
. . . . . . . . . . . . 13
β’ 1 = (0 +
1) |
147 | 146 | fveq2i 6849 |
. . . . . . . . . . . 12
β’
(β€β₯β1) = (β€β₯β(0 +
1)) |
148 | 92, 147 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (π β π β (β€β₯β(0 +
1))) |
149 | | eluzp1m1 12797 |
. . . . . . . . . . 11
β’ ((0
β β€ β§ π
β (β€β₯β(0 + 1))) β (π β 1) β
(β€β₯β0)) |
150 | 145, 148,
149 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (π β 1) β
(β€β₯β0)) |
151 | | hashfz 14336 |
. . . . . . . . . 10
β’ ((π β 1) β
(β€β₯β0) β (β―β(0...(π β 1))) = (((π β 1) β 0) + 1)) |
152 | 150, 151 | syl 17 |
. . . . . . . . 9
β’ (π β (β―β(0...(π β 1))) = (((π β 1) β 0) +
1)) |
153 | 75, 61 | subcld 11520 |
. . . . . . . . . . 11
β’ (π β (π β 1) β β) |
154 | 153 | subid1d 11509 |
. . . . . . . . . 10
β’ (π β ((π β 1) β 0) = (π β 1)) |
155 | 154 | oveq1d 7376 |
. . . . . . . . 9
β’ (π β (((π β 1) β 0) + 1) = ((π β 1) +
1)) |
156 | 152, 155,
76 | 3eqtrd 2777 |
. . . . . . . 8
β’ (π β (β―β(0...(π β 1))) = π) |
157 | 156 | oveq1d 7376 |
. . . . . . 7
β’ (π β
((β―β(0...(π
β 1))) Β· πΈ) =
(π Β· πΈ)) |
158 | 75, 80 | mulcomd 11184 |
. . . . . . 7
β’ (π β (π Β· πΈ) = (πΈ Β· π)) |
159 | 144, 157,
158 | 3eqtrd 2777 |
. . . . . 6
β’ (π β Ξ£π β (0...(π β 1))πΈ = (πΈ Β· π)) |
160 | 142, 159 | breqtrd 5135 |
. . . . 5
β’ (π β Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) β€ (πΈ Β· π)) |
161 | 54, 18, 26, 160 | leadd1dd 11777 |
. . . 4
β’ (π β (Ξ£π β (0...(π β 1))(πΈ Β· ((πβπ)βπ‘)) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) β€ ((πΈ Β· π) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π))))) |
162 | 14, 55, 27, 131, 161 | ltletrd 11323 |
. . 3
β’ (π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) < ((πΈ Β· π) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π))))) |
163 | 8, 8 | remulcld 11193 |
. . . . 5
β’ (π β (πΈ Β· πΈ) β β) |
164 | 18, 163 | readdcld 11192 |
. . . 4
β’ (π β ((πΈ Β· π) + (πΈ Β· πΈ)) β β) |
165 | 60, 75 | subcld 11520 |
. . . . . . . 8
β’ (π β (π β π) β β) |
166 | 165, 61 | addcld 11182 |
. . . . . . 7
β’ (π β ((π β π) + 1) β β) |
167 | 80, 166, 121 | mul12d 11372 |
. . . . . 6
β’ (π β (πΈ Β· (((π β π) + 1) Β· (πΈ / π))) = (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) |
168 | 167 | oveq2d 7377 |
. . . . 5
β’ (π β ((πΈ Β· π) + (πΈ Β· (((π β π) + 1) Β· (πΈ / π)))) = ((πΈ Β· π) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π))))) |
169 | 23, 24 | remulcld 11193 |
. . . . . . 7
β’ (π β (((π β π) + 1) Β· (πΈ / π)) β β) |
170 | 8, 169 | remulcld 11193 |
. . . . . 6
β’ (π β (πΈ Β· (((π β π) + 1) Β· (πΈ / π))) β β) |
171 | 166, 80, 60, 120 | div12d 11975 |
. . . . . . . 8
β’ (π β (((π β π) + 1) Β· (πΈ / π)) = (πΈ Β· (((π β π) + 1) / π))) |
172 | 22, 17 | resubcld 11591 |
. . . . . . . . . . . . . 14
β’ (π β (1 β π) β
β) |
173 | | elfzle1 13453 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β 1 β€ π) |
174 | 15, 173 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β€ π) |
175 | 22, 17 | suble0d 11754 |
. . . . . . . . . . . . . . 15
β’ (π β ((1 β π) β€ 0 β 1 β€ π)) |
176 | 174, 175 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (π β (1 β π) β€ 0) |
177 | 172, 88, 20, 176 | leadd2dd 11778 |
. . . . . . . . . . . . 13
β’ (π β (π + (1 β π)) β€ (π + 0)) |
178 | 60, 61, 75 | addsub12d 11543 |
. . . . . . . . . . . . . 14
β’ (π β (π + (1 β π)) = (1 + (π β π))) |
179 | 61, 165 | addcomd 11365 |
. . . . . . . . . . . . . 14
β’ (π β (1 + (π β π)) = ((π β π) + 1)) |
180 | 178, 179 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π β (π + (1 β π)) = ((π β π) + 1)) |
181 | 60 | addid1d 11363 |
. . . . . . . . . . . . 13
β’ (π β (π + 0) = π) |
182 | 177, 180,
181 | 3brtr3d 5140 |
. . . . . . . . . . . 12
β’ (π β ((π β π) + 1) β€ π) |
183 | 19 | nngt0d 12210 |
. . . . . . . . . . . . 13
β’ (π β 0 < π) |
184 | | lediv1 12028 |
. . . . . . . . . . . . 13
β’ ((((π β π) + 1) β β β§ π β β β§ (π β β β§ 0 < π)) β (((π β π) + 1) β€ π β (((π β π) + 1) / π) β€ (π / π))) |
185 | 23, 20, 20, 183, 184 | syl112anc 1375 |
. . . . . . . . . . . 12
β’ (π β (((π β π) + 1) β€ π β (((π β π) + 1) / π) β€ (π / π))) |
186 | 182, 185 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (((π β π) + 1) / π) β€ (π / π)) |
187 | 60, 120 | dividd 11937 |
. . . . . . . . . . 11
β’ (π β (π / π) = 1) |
188 | 186, 187 | breqtrd 5135 |
. . . . . . . . . 10
β’ (π β (((π β π) + 1) / π) β€ 1) |
189 | 23, 19 | nndivred 12215 |
. . . . . . . . . . 11
β’ (π β (((π β π) + 1) / π) β β) |
190 | 189, 22, 7 | lemul2d 13009 |
. . . . . . . . . 10
β’ (π β ((((π β π) + 1) / π) β€ 1 β (πΈ Β· (((π β π) + 1) / π)) β€ (πΈ Β· 1))) |
191 | 188, 190 | mpbid 231 |
. . . . . . . . 9
β’ (π β (πΈ Β· (((π β π) + 1) / π)) β€ (πΈ Β· 1)) |
192 | 191, 139 | breqtrd 5135 |
. . . . . . . 8
β’ (π β (πΈ Β· (((π β π) + 1) / π)) β€ πΈ) |
193 | 171, 192 | eqbrtrd 5131 |
. . . . . . 7
β’ (π β (((π β π) + 1) Β· (πΈ / π)) β€ πΈ) |
194 | 169, 8, 7 | lemul2d 13009 |
. . . . . . 7
β’ (π β ((((π β π) + 1) Β· (πΈ / π)) β€ πΈ β (πΈ Β· (((π β π) + 1) Β· (πΈ / π))) β€ (πΈ Β· πΈ))) |
195 | 193, 194 | mpbid 231 |
. . . . . 6
β’ (π β (πΈ Β· (((π β π) + 1) Β· (πΈ / π))) β€ (πΈ Β· πΈ)) |
196 | 170, 163,
18, 195 | leadd2dd 11778 |
. . . . 5
β’ (π β ((πΈ Β· π) + (πΈ Β· (((π β π) + 1) Β· (πΈ / π)))) β€ ((πΈ Β· π) + (πΈ Β· πΈ))) |
197 | 168, 196 | eqbrtrrd 5133 |
. . . 4
β’ (π β ((πΈ Β· π) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) β€ ((πΈ Β· π) + (πΈ Β· πΈ))) |
198 | 80, 75 | mulcomd 11184 |
. . . . . . 7
β’ (π β (πΈ Β· π) = (π Β· πΈ)) |
199 | 198 | oveq1d 7376 |
. . . . . 6
β’ (π β ((πΈ Β· π) + (πΈ Β· πΈ)) = ((π Β· πΈ) + (πΈ Β· πΈ))) |
200 | 75, 80, 80 | adddird 11188 |
. . . . . 6
β’ (π β ((π + πΈ) Β· πΈ) = ((π Β· πΈ) + (πΈ Β· πΈ))) |
201 | 199, 200 | eqtr4d 2776 |
. . . . 5
β’ (π β ((πΈ Β· π) + (πΈ Β· πΈ)) = ((π + πΈ) Β· πΈ)) |
202 | 17, 8 | readdcld 11192 |
. . . . . 6
β’ (π β (π + πΈ) β β) |
203 | | stoweidlem11.8 |
. . . . . . 7
β’ (π β πΈ < (1 / 3)) |
204 | 8, 32, 17, 203 | ltadd2dd 11322 |
. . . . . 6
β’ (π β (π + πΈ) < (π + (1 / 3))) |
205 | 202, 33, 7, 204 | ltmul1dd 13020 |
. . . . 5
β’ (π β ((π + πΈ) Β· πΈ) < ((π + (1 / 3)) Β· πΈ)) |
206 | 201, 205 | eqbrtrd 5131 |
. . . 4
β’ (π β ((πΈ Β· π) + (πΈ Β· πΈ)) < ((π + (1 / 3)) Β· πΈ)) |
207 | 27, 164, 34, 197, 206 | lelttrd 11321 |
. . 3
β’ (π β ((πΈ Β· π) + (((π β π) + 1) Β· (πΈ Β· (πΈ / π)))) < ((π + (1 / 3)) Β· πΈ)) |
208 | 14, 27, 34, 162, 207 | lttrd 11324 |
. 2
β’ (π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) < ((π + (1 / 3)) Β· πΈ)) |
209 | 5, 208 | eqbrtrd 5131 |
1
β’ (π β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ‘) < ((π + (1 / 3)) Β· πΈ)) |