Step | Hyp | Ref
| Expression |
1 | | 1re 11162 |
. . . . . . . 8
β’ 1 β
β |
2 | | eleq1 2826 |
. . . . . . . 8
β’ (πΏ = 1 β (πΏ β β β 1 β
β)) |
3 | 1, 2 | mpbiri 258 |
. . . . . . 7
β’ (πΏ = 1 β πΏ β β) |
4 | 3 | adantl 483 |
. . . . . 6
β’ ((π β§ πΏ = 1) β πΏ β β) |
5 | | 4re 12244 |
. . . . . . . 8
β’ 4 β
β |
6 | 5 | a1i 11 |
. . . . . . 7
β’ ((π β§ πΏ = 1) β 4 β
β) |
7 | | 3re 12240 |
. . . . . . . 8
β’ 3 β
β |
8 | 7 | a1i 11 |
. . . . . . 7
β’ ((π β§ πΏ = 1) β 3 β
β) |
9 | | 3ne0 12266 |
. . . . . . . 8
β’ 3 β
0 |
10 | 9 | a1i 11 |
. . . . . . 7
β’ ((π β§ πΏ = 1) β 3 β 0) |
11 | 6, 8, 10 | redivcld 11990 |
. . . . . 6
β’ ((π β§ πΏ = 1) β (4 / 3) β
β) |
12 | 4, 11 | resubcld 11590 |
. . . . 5
β’ ((π β§ πΏ = 1) β (πΏ β (4 / 3)) β
β) |
13 | | stoweidlem26.11 |
. . . . . . 7
β’ (π β πΈ β
β+) |
14 | 13 | rpred 12964 |
. . . . . 6
β’ (π β πΈ β β) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((π β§ πΏ = 1) β πΈ β β) |
16 | 12, 15 | remulcld 11192 |
. . . 4
β’ ((π β§ πΏ = 1) β ((πΏ β (4 / 3)) Β· πΈ) β β) |
17 | | 0red 11165 |
. . . 4
β’ ((π β§ πΏ = 1) β 0 β
β) |
18 | | fzfid 13885 |
. . . . . 6
β’ (π β (0...π) β Fin) |
19 | 14 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β πΈ β β) |
20 | | stoweidlem26.13 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β (πβπ):πβΆβ) |
21 | | stoweidlem26.9 |
. . . . . . . . . . . . . 14
β’ (π β π β ((π·βπΏ) β (π·β(πΏ β 1)))) |
22 | | eldif 3925 |
. . . . . . . . . . . . . 14
β’ (π β ((π·βπΏ) β (π·β(πΏ β 1))) β (π β (π·βπΏ) β§ Β¬ π β (π·β(πΏ β 1)))) |
23 | 21, 22 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π β (π β (π·βπΏ) β§ Β¬ π β (π·β(πΏ β 1)))) |
24 | 23 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β π β (π·βπΏ)) |
25 | | stoweidlem26.4 |
. . . . . . . . . . . . 13
β’ π· = (π β (0...π) β¦ {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)}) |
26 | | oveq1 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = πΏ β (π β (1 / 3)) = (πΏ β (1 / 3))) |
27 | 26 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π = πΏ β ((π β (1 / 3)) Β· πΈ) = ((πΏ β (1 / 3)) Β· πΈ)) |
28 | 27 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π = πΏ β ((πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ) β (πΉβπ‘) β€ ((πΏ β (1 / 3)) Β· πΈ))) |
29 | 28 | rabbidv 3418 |
. . . . . . . . . . . . 13
β’ (π = πΏ β {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} = {π‘ β π β£ (πΉβπ‘) β€ ((πΏ β (1 / 3)) Β· πΈ)}) |
30 | | fz1ssfz0 13544 |
. . . . . . . . . . . . . 14
β’
(1...π) β
(0...π) |
31 | | stoweidlem26.8 |
. . . . . . . . . . . . . 14
β’ (π β πΏ β (1...π)) |
32 | 30, 31 | sselid 3947 |
. . . . . . . . . . . . 13
β’ (π β πΏ β (0...π)) |
33 | | stoweidlem26.7 |
. . . . . . . . . . . . . 14
β’ (π β π β V) |
34 | | rabexg 5293 |
. . . . . . . . . . . . . 14
β’ (π β V β {π‘ β π β£ (πΉβπ‘) β€ ((πΏ β (1 / 3)) Β· πΈ)} β V) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β {π‘ β π β£ (πΉβπ‘) β€ ((πΏ β (1 / 3)) Β· πΈ)} β V) |
36 | 25, 29, 32, 35 | fvmptd3 6976 |
. . . . . . . . . . . 12
β’ (π β (π·βπΏ) = {π‘ β π β£ (πΉβπ‘) β€ ((πΏ β (1 / 3)) Β· πΈ)}) |
37 | 24, 36 | eleqtrd 2840 |
. . . . . . . . . . 11
β’ (π β π β {π‘ β π β£ (πΉβπ‘) β€ ((πΏ β (1 / 3)) Β· πΈ)}) |
38 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π‘π |
39 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π‘π |
40 | | stoweidlem26.1 |
. . . . . . . . . . . . . 14
β’
β²π‘πΉ |
41 | 40, 38 | nffv 6857 |
. . . . . . . . . . . . 13
β’
β²π‘(πΉβπ) |
42 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π‘
β€ |
43 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π‘((πΏ β (1 / 3)) Β· πΈ) |
44 | 41, 42, 43 | nfbr 5157 |
. . . . . . . . . . . 12
β’
β²π‘(πΉβπ) β€ ((πΏ β (1 / 3)) Β· πΈ) |
45 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (πΉβπ‘) = (πΉβπ)) |
46 | 45 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (π‘ = π β ((πΉβπ‘) β€ ((πΏ β (1 / 3)) Β· πΈ) β (πΉβπ) β€ ((πΏ β (1 / 3)) Β· πΈ))) |
47 | 38, 39, 44, 46 | elrabf 3646 |
. . . . . . . . . . 11
β’ (π β {π‘ β π β£ (πΉβπ‘) β€ ((πΏ β (1 / 3)) Β· πΈ)} β (π β π β§ (πΉβπ) β€ ((πΏ β (1 / 3)) Β· πΈ))) |
48 | 37, 47 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π β π β§ (πΉβπ) β€ ((πΏ β (1 / 3)) Β· πΈ))) |
49 | 48 | simpld 496 |
. . . . . . . . 9
β’ (π β π β π) |
50 | 49 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β π β π) |
51 | 20, 50 | ffvelcdmd 7041 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β ((πβπ)βπ) β β) |
52 | 19, 51 | remulcld 11192 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πΈ Β· ((πβπ)βπ)) β β) |
53 | 18, 52 | fsumrecl 15626 |
. . . . 5
β’ (π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)) β β) |
54 | 53 | adantr 482 |
. . . 4
β’ ((π β§ πΏ = 1) β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)) β β) |
55 | 5, 7, 9 | redivcli 11929 |
. . . . . . 7
β’ (4 / 3)
β β |
56 | 55 | a1i 11 |
. . . . . 6
β’ ((π β§ πΏ = 1) β (4 / 3) β
β) |
57 | 4, 56 | resubcld 11590 |
. . . . 5
β’ ((π β§ πΏ = 1) β (πΏ β (4 / 3)) β
β) |
58 | 4 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ πΏ = 1) β πΏ β β) |
59 | 58 | subid1d 11508 |
. . . . . . 7
β’ ((π β§ πΏ = 1) β (πΏ β 0) = πΏ) |
60 | | 3cn 12241 |
. . . . . . . . . 10
β’ 3 β
β |
61 | 60, 9 | dividi 11895 |
. . . . . . . . 9
β’ (3 / 3) =
1 |
62 | | 3lt4 12334 |
. . . . . . . . . 10
β’ 3 <
4 |
63 | | 3pos 12265 |
. . . . . . . . . . 11
β’ 0 <
3 |
64 | 7, 5, 7, 63 | ltdiv1ii 12091 |
. . . . . . . . . 10
β’ (3 < 4
β (3 / 3) < (4 / 3)) |
65 | 62, 64 | mpbi 229 |
. . . . . . . . 9
β’ (3 / 3)
< (4 / 3) |
66 | 61, 65 | eqbrtrri 5133 |
. . . . . . . 8
β’ 1 < (4
/ 3) |
67 | | breq1 5113 |
. . . . . . . . 9
β’ (πΏ = 1 β (πΏ < (4 / 3) β 1 < (4 /
3))) |
68 | 67 | adantl 483 |
. . . . . . . 8
β’ ((π β§ πΏ = 1) β (πΏ < (4 / 3) β 1 < (4 /
3))) |
69 | 66, 68 | mpbiri 258 |
. . . . . . 7
β’ ((π β§ πΏ = 1) β πΏ < (4 / 3)) |
70 | 59, 69 | eqbrtrd 5132 |
. . . . . 6
β’ ((π β§ πΏ = 1) β (πΏ β 0) < (4 / 3)) |
71 | 4, 17, 56, 70 | ltsub23d 11767 |
. . . . 5
β’ ((π β§ πΏ = 1) β (πΏ β (4 / 3)) < 0) |
72 | 13 | rpgt0d 12967 |
. . . . . 6
β’ (π β 0 < πΈ) |
73 | 72 | adantr 482 |
. . . . 5
β’ ((π β§ πΏ = 1) β 0 < πΈ) |
74 | | mulltgt0 43301 |
. . . . 5
β’ ((((πΏ β (4 / 3)) β β
β§ (πΏ β (4 / 3))
< 0) β§ (πΈ β
β β§ 0 < πΈ))
β ((πΏ β (4 / 3))
Β· πΈ) <
0) |
75 | 57, 71, 15, 73, 74 | syl22anc 838 |
. . . 4
β’ ((π β§ πΏ = 1) β ((πΏ β (4 / 3)) Β· πΈ) < 0) |
76 | | 0cn 11154 |
. . . . . . . 8
β’ 0 β
β |
77 | | fsumconst 15682 |
. . . . . . . 8
β’
(((0...π) β Fin
β§ 0 β β) β Ξ£π β (0...π)0 = ((β―β(0...π)) Β· 0)) |
78 | 18, 76, 77 | sylancl 587 |
. . . . . . 7
β’ (π β Ξ£π β (0...π)0 = ((β―β(0...π)) Β· 0)) |
79 | | hashcl 14263 |
. . . . . . . . 9
β’
((0...π) β Fin
β (β―β(0...π)) β
β0) |
80 | | nn0cn 12430 |
. . . . . . . . 9
β’
((β―β(0...π)) β β0 β
(β―β(0...π))
β β) |
81 | 18, 79, 80 | 3syl 18 |
. . . . . . . 8
β’ (π β (β―β(0...π)) β
β) |
82 | 81 | mul01d 11361 |
. . . . . . 7
β’ (π β ((β―β(0...π)) Β· 0) =
0) |
83 | 78, 82 | eqtrd 2777 |
. . . . . 6
β’ (π β Ξ£π β (0...π)0 = 0) |
84 | 83 | adantr 482 |
. . . . 5
β’ ((π β§ πΏ = 1) β Ξ£π β (0...π)0 = 0) |
85 | | 0red 11165 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β 0 β β) |
86 | 13 | rpge0d 12968 |
. . . . . . . . 9
β’ (π β 0 β€ πΈ) |
87 | 86 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β 0 β€ πΈ) |
88 | | stoweidlem26.3 |
. . . . . . . . . . . 12
β’
β²π‘π |
89 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π‘ π β (0...π) |
90 | 88, 89 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π‘(π β§ π β (0...π)) |
91 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π‘0 β€
((πβπ)βπ) |
92 | 90, 91 | nfim 1900 |
. . . . . . . . . 10
β’
β²π‘((π β§ π β (0...π)) β 0 β€ ((πβπ)βπ)) |
93 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π‘ = π β ((πβπ)βπ‘) = ((πβπ)βπ)) |
94 | 93 | breq2d 5122 |
. . . . . . . . . . 11
β’ (π‘ = π β (0 β€ ((πβπ)βπ‘) β 0 β€ ((πβπ)βπ))) |
95 | 94 | imbi2d 341 |
. . . . . . . . . 10
β’ (π‘ = π β (((π β§ π β (0...π)) β 0 β€ ((πβπ)βπ‘)) β ((π β§ π β (0...π)) β 0 β€ ((πβπ)βπ)))) |
96 | | stoweidlem26.14 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π) β§ π‘ β π) β 0 β€ ((πβπ)βπ‘)) |
97 | 96 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π)) β (π‘ β π β 0 β€ ((πβπ)βπ‘))) |
98 | 97 | com12 32 |
. . . . . . . . . 10
β’ (π‘ β π β ((π β§ π β (0...π)) β 0 β€ ((πβπ)βπ‘))) |
99 | 38, 92, 95, 98 | vtoclgaf 3536 |
. . . . . . . . 9
β’ (π β π β ((π β§ π β (0...π)) β 0 β€ ((πβπ)βπ))) |
100 | 50, 99 | mpcom 38 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β 0 β€ ((πβπ)βπ)) |
101 | 19, 51, 87, 100 | mulge0d 11739 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β 0 β€ (πΈ Β· ((πβπ)βπ))) |
102 | 18, 85, 52, 101 | fsumle 15691 |
. . . . . 6
β’ (π β Ξ£π β (0...π)0 β€ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
103 | 102 | adantr 482 |
. . . . 5
β’ ((π β§ πΏ = 1) β Ξ£π β (0...π)0 β€ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
104 | 84, 103 | eqbrtrrd 5134 |
. . . 4
β’ ((π β§ πΏ = 1) β 0 β€ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
105 | 16, 17, 54, 75, 104 | ltletrd 11322 |
. . 3
β’ ((π β§ πΏ = 1) β ((πΏ β (4 / 3)) Β· πΈ) < Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
106 | | elfzelz 13448 |
. . . . . . . . 9
β’ (πΏ β (1...π) β πΏ β β€) |
107 | | zre 12510 |
. . . . . . . . 9
β’ (πΏ β β€ β πΏ β
β) |
108 | 31, 106, 107 | 3syl 18 |
. . . . . . . 8
β’ (π β πΏ β β) |
109 | 5 | a1i 11 |
. . . . . . . . 9
β’ (π β 4 β
β) |
110 | 7 | a1i 11 |
. . . . . . . . 9
β’ (π β 3 β
β) |
111 | 9 | a1i 11 |
. . . . . . . . 9
β’ (π β 3 β 0) |
112 | 109, 110,
111 | redivcld 11990 |
. . . . . . . 8
β’ (π β (4 / 3) β
β) |
113 | 108, 112 | resubcld 11590 |
. . . . . . 7
β’ (π β (πΏ β (4 / 3)) β
β) |
114 | 113, 14 | remulcld 11192 |
. . . . . 6
β’ (π β ((πΏ β (4 / 3)) Β· πΈ) β β) |
115 | 114 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β ((πΏ β (4 / 3)) Β· πΈ) β β) |
116 | 1 | a1i 11 |
. . . . . . . . 9
β’ (π β 1 β
β) |
117 | | stoweidlem26.6 |
. . . . . . . . . 10
β’ (π β π β β) |
118 | 14, 117 | nndivred 12214 |
. . . . . . . . 9
β’ (π β (πΈ / π) β β) |
119 | 116, 118 | resubcld 11590 |
. . . . . . . 8
β’ (π β (1 β (πΈ / π)) β β) |
120 | 108, 116 | resubcld 11590 |
. . . . . . . 8
β’ (π β (πΏ β 1) β β) |
121 | 119, 120 | remulcld 11192 |
. . . . . . 7
β’ (π β ((1 β (πΈ / π)) Β· (πΏ β 1)) β
β) |
122 | 14, 121 | remulcld 11192 |
. . . . . 6
β’ (π β (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1))) β
β) |
123 | 122 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1))) β
β) |
124 | | fzfid 13885 |
. . . . . . . 8
β’ (π β (0...(πΏ β 2)) β Fin) |
125 | 31 | elfzelzd 13449 |
. . . . . . . . . . . . . 14
β’ (π β πΏ β β€) |
126 | | 2z 12542 |
. . . . . . . . . . . . . . 15
β’ 2 β
β€ |
127 | 126 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 2 β
β€) |
128 | 125, 127 | zsubcld 12619 |
. . . . . . . . . . . . 13
β’ (π β (πΏ β 2) β β€) |
129 | 117 | nnzd 12533 |
. . . . . . . . . . . . 13
β’ (π β π β β€) |
130 | 125 | zred 12614 |
. . . . . . . . . . . . . . 15
β’ (π β πΏ β β) |
131 | | 2re 12234 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β 2 β
β) |
133 | 130, 132 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ (π β (πΏ β 2) β β) |
134 | 117 | nnred 12175 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
135 | | 0le2 12262 |
. . . . . . . . . . . . . . . 16
β’ 0 β€
2 |
136 | | 0red 11165 |
. . . . . . . . . . . . . . . . 17
β’ (π β 0 β
β) |
137 | 136, 132,
130 | lesub2d 11770 |
. . . . . . . . . . . . . . . 16
β’ (π β (0 β€ 2 β (πΏ β 2) β€ (πΏ β 0))) |
138 | 135, 137 | mpbii 232 |
. . . . . . . . . . . . . . 15
β’ (π β (πΏ β 2) β€ (πΏ β 0)) |
139 | 125 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
β’ (π β πΏ β β) |
140 | 139 | subid1d 11508 |
. . . . . . . . . . . . . . 15
β’ (π β (πΏ β 0) = πΏ) |
141 | 138, 140 | breqtrd 5136 |
. . . . . . . . . . . . . 14
β’ (π β (πΏ β 2) β€ πΏ) |
142 | | elfzle2 13452 |
. . . . . . . . . . . . . . 15
β’ (πΏ β (1...π) β πΏ β€ π) |
143 | 31, 142 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΏ β€ π) |
144 | 133, 130,
134, 141, 143 | letrd 11319 |
. . . . . . . . . . . . 13
β’ (π β (πΏ β 2) β€ π) |
145 | 128, 129,
144 | 3jca 1129 |
. . . . . . . . . . . 12
β’ (π β ((πΏ β 2) β β€ β§ π β β€ β§ (πΏ β 2) β€ π)) |
146 | | eluz2 12776 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β(πΏ β 2)) β ((πΏ β 2) β β€ β§ π β β€ β§ (πΏ β 2) β€ π)) |
147 | 145, 146 | sylibr 233 |
. . . . . . . . . . 11
β’ (π β π β (β€β₯β(πΏ β 2))) |
148 | | fzss2 13488 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β(πΏ β 2)) β (0...(πΏ β 2)) β (0...π)) |
149 | 147, 148 | syl 17 |
. . . . . . . . . 10
β’ (π β (0...(πΏ β 2)) β (0...π)) |
150 | 149 | sselda 3949 |
. . . . . . . . 9
β’ ((π β§ π β (0...(πΏ β 2))) β π β (0...π)) |
151 | 150, 51 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π β (0...(πΏ β 2))) β ((πβπ)βπ) β β) |
152 | 124, 151 | fsumrecl 15626 |
. . . . . . 7
β’ (π β Ξ£π β (0...(πΏ β 2))((πβπ)βπ) β β) |
153 | 14, 152 | remulcld 11192 |
. . . . . 6
β’ (π β (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β β) |
154 | 153 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β β) |
155 | 14, 120 | remulcld 11192 |
. . . . . . . . 9
β’ (π β (πΈ Β· (πΏ β 1)) β
β) |
156 | 14, 14 | remulcld 11192 |
. . . . . . . . 9
β’ (π β (πΈ Β· πΈ) β β) |
157 | 155, 156 | resubcld 11590 |
. . . . . . . 8
β’ (π β ((πΈ Β· (πΏ β 1)) β (πΈ Β· πΈ)) β β) |
158 | 120, 117 | nndivred 12214 |
. . . . . . . . . 10
β’ (π β ((πΏ β 1) / π) β β) |
159 | 156, 158 | remulcld 11192 |
. . . . . . . . 9
β’ (π β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)) β β) |
160 | 155, 159 | resubcld 11590 |
. . . . . . . 8
β’ (π β ((πΈ Β· (πΏ β 1)) β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π))) β β) |
161 | 120, 14 | resubcld 11590 |
. . . . . . . . . 10
β’ (π β ((πΏ β 1) β πΈ) β β) |
162 | 116, 14 | readdcld 11191 |
. . . . . . . . . . . 12
β’ (π β (1 + πΈ) β β) |
163 | 1, 7, 9 | redivcli 11929 |
. . . . . . . . . . . . . . 15
β’ (1 / 3)
β β |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (1 / 3) β
β) |
165 | | stoweidlem26.12 |
. . . . . . . . . . . . . 14
β’ (π β πΈ < (1 / 3)) |
166 | 14, 164, 116, 165 | ltadd2dd 11321 |
. . . . . . . . . . . . 13
β’ (π β (1 + πΈ) < (1 + (1 / 3))) |
167 | | ax-1cn 11116 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
168 | 60, 167, 60, 9 | divdiri 11919 |
. . . . . . . . . . . . . 14
β’ ((3 + 1)
/ 3) = ((3 / 3) + (1 / 3)) |
169 | | 3p1e4 12305 |
. . . . . . . . . . . . . . 15
β’ (3 + 1) =
4 |
170 | 169 | oveq1i 7372 |
. . . . . . . . . . . . . 14
β’ ((3 + 1)
/ 3) = (4 / 3) |
171 | 61 | oveq1i 7372 |
. . . . . . . . . . . . . 14
β’ ((3 / 3)
+ (1 / 3)) = (1 + (1 / 3)) |
172 | 168, 170,
171 | 3eqtr3ri 2774 |
. . . . . . . . . . . . 13
β’ (1 + (1 /
3)) = (4 / 3) |
173 | 166, 172 | breqtrdi 5151 |
. . . . . . . . . . . 12
β’ (π β (1 + πΈ) < (4 / 3)) |
174 | 162, 112,
108, 173 | ltsub2dd 11775 |
. . . . . . . . . . 11
β’ (π β (πΏ β (4 / 3)) < (πΏ β (1 + πΈ))) |
175 | 167 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 1 β
β) |
176 | 13 | rpcnd 12966 |
. . . . . . . . . . . 12
β’ (π β πΈ β β) |
177 | 139, 175,
176 | subsub4d 11550 |
. . . . . . . . . . 11
β’ (π β ((πΏ β 1) β πΈ) = (πΏ β (1 + πΈ))) |
178 | 174, 177 | breqtrrd 5138 |
. . . . . . . . . 10
β’ (π β (πΏ β (4 / 3)) < ((πΏ β 1) β πΈ)) |
179 | 113, 161,
13, 178 | ltmul1dd 13019 |
. . . . . . . . 9
β’ (π β ((πΏ β (4 / 3)) Β· πΈ) < (((πΏ β 1) β πΈ) Β· πΈ)) |
180 | 139, 175 | subcld 11519 |
. . . . . . . . . . . 12
β’ (π β (πΏ β 1) β β) |
181 | 180, 176 | subcld 11519 |
. . . . . . . . . . 11
β’ (π β ((πΏ β 1) β πΈ) β β) |
182 | 176, 181 | mulcomd 11183 |
. . . . . . . . . 10
β’ (π β (πΈ Β· ((πΏ β 1) β πΈ)) = (((πΏ β 1) β πΈ) Β· πΈ)) |
183 | 176, 180,
176 | subdid 11618 |
. . . . . . . . . 10
β’ (π β (πΈ Β· ((πΏ β 1) β πΈ)) = ((πΈ Β· (πΏ β 1)) β (πΈ Β· πΈ))) |
184 | 182, 183 | eqtr3d 2779 |
. . . . . . . . 9
β’ (π β (((πΏ β 1) β πΈ) Β· πΈ) = ((πΈ Β· (πΏ β 1)) β (πΈ Β· πΈ))) |
185 | 179, 184 | breqtrd 5136 |
. . . . . . . 8
β’ (π β ((πΏ β (4 / 3)) Β· πΈ) < ((πΈ Β· (πΏ β 1)) β (πΈ Β· πΈ))) |
186 | | 1zzd 12541 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 β
β€) |
187 | | elfz 13437 |
. . . . . . . . . . . . . . . . 17
β’ ((πΏ β β€ β§ 1 β
β€ β§ π β
β€) β (πΏ β
(1...π) β (1 β€
πΏ β§ πΏ β€ π))) |
188 | 125, 186,
129, 187 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΏ β (1...π) β (1 β€ πΏ β§ πΏ β€ π))) |
189 | 31, 188 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β (1 β€ πΏ β§ πΏ β€ π)) |
190 | 189 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β πΏ β€ π) |
191 | | zlem1lt 12562 |
. . . . . . . . . . . . . . 15
β’ ((πΏ β β€ β§ π β β€) β (πΏ β€ π β (πΏ β 1) < π)) |
192 | 125, 129,
191 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (πΏ β€ π β (πΏ β 1) < π)) |
193 | 190, 192 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β (πΏ β 1) < π) |
194 | 117 | nngt0d 12209 |
. . . . . . . . . . . . . 14
β’ (π β 0 < π) |
195 | | ltdiv1 12026 |
. . . . . . . . . . . . . 14
β’ (((πΏ β 1) β β β§
π β β β§
(π β β β§ 0
< π)) β ((πΏ β 1) < π β ((πΏ β 1) / π) < (π / π))) |
196 | 120, 134,
134, 194, 195 | syl112anc 1375 |
. . . . . . . . . . . . 13
β’ (π β ((πΏ β 1) < π β ((πΏ β 1) / π) < (π / π))) |
197 | 193, 196 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β ((πΏ β 1) / π) < (π / π)) |
198 | 117 | nncnd 12176 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
199 | 117 | nnne0d 12210 |
. . . . . . . . . . . . 13
β’ (π β π β 0) |
200 | 198, 199 | dividd 11936 |
. . . . . . . . . . . 12
β’ (π β (π / π) = 1) |
201 | 197, 200 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (π β ((πΏ β 1) / π) < 1) |
202 | 14, 14, 72, 72 | mulgt0d 11317 |
. . . . . . . . . . . 12
β’ (π β 0 < (πΈ Β· πΈ)) |
203 | | ltmul2 12013 |
. . . . . . . . . . . 12
β’ ((((πΏ β 1) / π) β β β§ 1 β β
β§ ((πΈ Β· πΈ) β β β§ 0 <
(πΈ Β· πΈ))) β (((πΏ β 1) / π) < 1 β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)) < ((πΈ Β· πΈ) Β· 1))) |
204 | 158, 116,
156, 202, 203 | syl112anc 1375 |
. . . . . . . . . . 11
β’ (π β (((πΏ β 1) / π) < 1 β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)) < ((πΈ Β· πΈ) Β· 1))) |
205 | 201, 204 | mpbid 231 |
. . . . . . . . . 10
β’ (π β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)) < ((πΈ Β· πΈ) Β· 1)) |
206 | 176, 176 | mulcld 11182 |
. . . . . . . . . . 11
β’ (π β (πΈ Β· πΈ) β β) |
207 | 206 | mulid1d 11179 |
. . . . . . . . . 10
β’ (π β ((πΈ Β· πΈ) Β· 1) = (πΈ Β· πΈ)) |
208 | 205, 207 | breqtrd 5136 |
. . . . . . . . 9
β’ (π β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)) < (πΈ Β· πΈ)) |
209 | 159, 156,
155, 208 | ltsub2dd 11775 |
. . . . . . . 8
β’ (π β ((πΈ Β· (πΏ β 1)) β (πΈ Β· πΈ)) < ((πΈ Β· (πΏ β 1)) β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)))) |
210 | 114, 157,
160, 185, 209 | lttrd 11323 |
. . . . . . 7
β’ (π β ((πΏ β (4 / 3)) Β· πΈ) < ((πΈ Β· (πΏ β 1)) β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)))) |
211 | 176, 198,
199 | divcld 11938 |
. . . . . . . . . . 11
β’ (π β (πΈ / π) β β) |
212 | 175, 211,
180 | subdird 11619 |
. . . . . . . . . 10
β’ (π β ((1 β (πΈ / π)) Β· (πΏ β 1)) = ((1 Β· (πΏ β 1)) β ((πΈ / π) Β· (πΏ β 1)))) |
213 | 180 | mulid2d 11180 |
. . . . . . . . . . 11
β’ (π β (1 Β· (πΏ β 1)) = (πΏ β 1)) |
214 | 213 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π β ((1 Β· (πΏ β 1)) β ((πΈ / π) Β· (πΏ β 1))) = ((πΏ β 1) β ((πΈ / π) Β· (πΏ β 1)))) |
215 | 212, 214 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β ((1 β (πΈ / π)) Β· (πΏ β 1)) = ((πΏ β 1) β ((πΈ / π) Β· (πΏ β 1)))) |
216 | 215 | oveq2d 7378 |
. . . . . . . 8
β’ (π β (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1))) = (πΈ Β· ((πΏ β 1) β ((πΈ / π) Β· (πΏ β 1))))) |
217 | 211, 180 | mulcld 11182 |
. . . . . . . . 9
β’ (π β ((πΈ / π) Β· (πΏ β 1)) β
β) |
218 | 176, 180,
217 | subdid 11618 |
. . . . . . . 8
β’ (π β (πΈ Β· ((πΏ β 1) β ((πΈ / π) Β· (πΏ β 1)))) = ((πΈ Β· (πΏ β 1)) β (πΈ Β· ((πΈ / π) Β· (πΏ β 1))))) |
219 | 176, 198,
180, 199 | div32d 11961 |
. . . . . . . . . . 11
β’ (π β ((πΈ / π) Β· (πΏ β 1)) = (πΈ Β· ((πΏ β 1) / π))) |
220 | 219 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β (πΈ Β· ((πΈ / π) Β· (πΏ β 1))) = (πΈ Β· (πΈ Β· ((πΏ β 1) / π)))) |
221 | 180, 198,
199 | divcld 11938 |
. . . . . . . . . . 11
β’ (π β ((πΏ β 1) / π) β β) |
222 | 176, 176,
221 | mulassd 11185 |
. . . . . . . . . 10
β’ (π β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)) = (πΈ Β· (πΈ Β· ((πΏ β 1) / π)))) |
223 | 220, 222 | eqtr4d 2780 |
. . . . . . . . 9
β’ (π β (πΈ Β· ((πΈ / π) Β· (πΏ β 1))) = ((πΈ Β· πΈ) Β· ((πΏ β 1) / π))) |
224 | 223 | oveq2d 7378 |
. . . . . . . 8
β’ (π β ((πΈ Β· (πΏ β 1)) β (πΈ Β· ((πΈ / π) Β· (πΏ β 1)))) = ((πΈ Β· (πΏ β 1)) β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)))) |
225 | 216, 218,
224 | 3eqtrd 2781 |
. . . . . . 7
β’ (π β (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1))) = ((πΈ Β· (πΏ β 1)) β ((πΈ Β· πΈ) Β· ((πΏ β 1) / π)))) |
226 | 210, 225 | breqtrrd 5138 |
. . . . . 6
β’ (π β ((πΏ β (4 / 3)) Β· πΈ) < (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1)))) |
227 | 226 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β ((πΏ β (4 / 3)) Β· πΈ) < (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1)))) |
228 | 175, 211 | subcld 11519 |
. . . . . . . . . 10
β’ (π β (1 β (πΈ / π)) β β) |
229 | | fsumconst 15682 |
. . . . . . . . . 10
β’
(((0...(πΏ β
2)) β Fin β§ (1 β (πΈ / π)) β β) β Ξ£π β (0...(πΏ β 2))(1 β (πΈ / π)) = ((β―β(0...(πΏ β 2))) Β· (1 β (πΈ / π)))) |
230 | 124, 228,
229 | syl2anc 585 |
. . . . . . . . 9
β’ (π β Ξ£π β (0...(πΏ β 2))(1 β (πΈ / π)) = ((β―β(0...(πΏ β 2))) Β· (1 β (πΈ / π)))) |
231 | 230 | adantr 482 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β (0...(πΏ β 2))(1 β (πΈ / π)) = ((β―β(0...(πΏ β 2))) Β· (1 β (πΈ / π)))) |
232 | | 0zd 12518 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΏ = 1) β 0 β
β€) |
233 | 31 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΏ = 1) β πΏ β (1...π)) |
234 | 233 | elfzelzd 13449 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΏ = 1) β πΏ β β€) |
235 | 126 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΏ = 1) β 2 β
β€) |
236 | 234, 235 | zsubcld 12619 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΏ = 1) β (πΏ β 2) β β€) |
237 | | elnnuz 12814 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β
(β€β₯β1)) |
238 | 117, 237 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β
(β€β₯β1)) |
239 | | elfzp12 13527 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯β1) β (πΏ β (1...π) β (πΏ = 1 β¨ πΏ β ((1 + 1)...π)))) |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΏ β (1...π) β (πΏ = 1 β¨ πΏ β ((1 + 1)...π)))) |
241 | 31, 240 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΏ = 1 β¨ πΏ β ((1 + 1)...π))) |
242 | 241 | orcanai 1002 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΏ = 1) β πΏ β ((1 + 1)...π)) |
243 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . . . 18
β’ (1 + 1) =
2 |
244 | 243 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ πΏ = 1) β (1 + 1) = 2) |
245 | 244 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ πΏ = 1) β ((1 + 1)...π) = (2...π)) |
246 | 242, 245 | eleqtrd 2840 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΏ = 1) β πΏ β (2...π)) |
247 | | elfzle1 13451 |
. . . . . . . . . . . . . . 15
β’ (πΏ β (2...π) β 2 β€ πΏ) |
248 | 246, 247 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΏ = 1) β 2 β€ πΏ) |
249 | 108 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΏ = 1) β πΏ β β) |
250 | 131 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ πΏ = 1) β 2 β
β) |
251 | 249, 250 | subge0d 11752 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ πΏ = 1) β (0 β€ (πΏ β 2) β 2 β€ πΏ)) |
252 | 248, 251 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ πΏ = 1) β 0 β€ (πΏ β 2)) |
253 | 232, 236,
252 | 3jca 1129 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ πΏ = 1) β (0 β β€ β§ (πΏ β 2) β β€ β§
0 β€ (πΏ β
2))) |
254 | | eluz2 12776 |
. . . . . . . . . . . 12
β’ ((πΏ β 2) β
(β€β₯β0) β (0 β β€ β§ (πΏ β 2) β β€ β§
0 β€ (πΏ β
2))) |
255 | 253, 254 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ πΏ = 1) β (πΏ β 2) β
(β€β₯β0)) |
256 | | hashfz 14334 |
. . . . . . . . . . 11
β’ ((πΏ β 2) β
(β€β₯β0) β (β―β(0...(πΏ β 2))) = (((πΏ β 2) β 0) +
1)) |
257 | 255, 256 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΏ = 1) β (β―β(0...(πΏ β 2))) = (((πΏ β 2) β 0) +
1)) |
258 | | 2cn 12235 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
259 | 258 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β 2 β
β) |
260 | 139, 259 | subcld 11519 |
. . . . . . . . . . . . . 14
β’ (π β (πΏ β 2) β β) |
261 | 260 | subid1d 11508 |
. . . . . . . . . . . . 13
β’ (π β ((πΏ β 2) β 0) = (πΏ β 2)) |
262 | 261 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π β (((πΏ β 2) β 0) + 1) = ((πΏ β 2) +
1)) |
263 | 139, 259,
175 | subadd23d 11541 |
. . . . . . . . . . . 12
β’ (π β ((πΏ β 2) + 1) = (πΏ + (1 β 2))) |
264 | 258, 167 | negsubdi2i 11494 |
. . . . . . . . . . . . . . . 16
β’ -(2
β 1) = (1 β 2) |
265 | | 2m1e1 12286 |
. . . . . . . . . . . . . . . . 17
β’ (2
β 1) = 1 |
266 | 265 | negeqi 11401 |
. . . . . . . . . . . . . . . 16
β’ -(2
β 1) = -1 |
267 | 264, 266 | eqtr3i 2767 |
. . . . . . . . . . . . . . 15
β’ (1
β 2) = -1 |
268 | 267 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (1 β 2) =
-1) |
269 | 268 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π β (πΏ + (1 β 2)) = (πΏ + -1)) |
270 | 139, 175 | negsubd 11525 |
. . . . . . . . . . . . 13
β’ (π β (πΏ + -1) = (πΏ β 1)) |
271 | 269, 270 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (π β (πΏ + (1 β 2)) = (πΏ β 1)) |
272 | 262, 263,
271 | 3eqtrd 2781 |
. . . . . . . . . . 11
β’ (π β (((πΏ β 2) β 0) + 1) = (πΏ β 1)) |
273 | 272 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΏ = 1) β (((πΏ β 2) β 0) + 1) = (πΏ β 1)) |
274 | 257, 273 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΏ = 1) β (β―β(0...(πΏ β 2))) = (πΏ β 1)) |
275 | 274 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ = 1) β ((β―β(0...(πΏ β 2))) Β· (1
β (πΈ / π))) = ((πΏ β 1) Β· (1 β (πΈ / π)))) |
276 | 180, 228 | mulcomd 11183 |
. . . . . . . . 9
β’ (π β ((πΏ β 1) Β· (1 β (πΈ / π))) = ((1 β (πΈ / π)) Β· (πΏ β 1))) |
277 | 276 | adantr 482 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ = 1) β ((πΏ β 1) Β· (1 β (πΈ / π))) = ((1 β (πΈ / π)) Β· (πΏ β 1))) |
278 | 231, 275,
277 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β (0...(πΏ β 2))(1 β (πΈ / π)) = ((1 β (πΈ / π)) Β· (πΏ β 1))) |
279 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ = 1) β (0...(πΏ β 2)) β Fin) |
280 | | fzn0 13462 |
. . . . . . . . 9
β’
((0...(πΏ β 2))
β β
β (πΏ
β 2) β (β€β₯β0)) |
281 | 255, 280 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ = 1) β (0...(πΏ β 2)) β β
) |
282 | 119 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ Β¬ πΏ = 1) β§ π β (0...(πΏ β 2))) β (1 β (πΈ / π)) β β) |
283 | | simpll 766 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΏ = 1) β§ π β (0...(πΏ β 2))) β π) |
284 | 150 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΏ = 1) β§ π β (0...(πΏ β 2))) β π β (0...π)) |
285 | 283, 284,
51 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ Β¬ πΏ = 1) β§ π β (0...(πΏ β 2))) β ((πβπ)βπ) β β) |
286 | 49 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΏ β 2))) β π β π) |
287 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...(πΏ β 2)) β π β β€) |
288 | 287 | zred 12614 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...(πΏ β 2)) β π β β) |
289 | 288 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΏ β 2))) β π β β) |
290 | 163 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΏ β 2))) β (1 / 3) β
β) |
291 | 289, 290 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β (π + (1 / 3)) β β) |
292 | 14 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β πΈ β β) |
293 | 291, 292 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΏ β 2))) β ((π + (1 / 3)) Β· πΈ) β β) |
294 | 108 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...(πΏ β 2))) β πΏ β β) |
295 | 131 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...(πΏ β 2))) β 2 β
β) |
296 | 294, 295 | resubcld 11590 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΏ β 2))) β (πΏ β 2) β β) |
297 | 296, 290 | readdcld 11191 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β ((πΏ β 2) + (1 / 3)) β
β) |
298 | 297, 292 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΏ β 2))) β (((πΏ β 2) + (1 / 3)) Β· πΈ) β
β) |
299 | | stoweidlem26.10 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:πβΆβ) |
300 | 299, 49 | jca 513 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ:πβΆβ β§ π β π)) |
301 | 300 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β (πΉ:πβΆβ β§ π β π)) |
302 | | ffvelcdm 7037 |
. . . . . . . . . . . . . 14
β’ ((πΉ:πβΆβ β§ π β π) β (πΉβπ) β β) |
303 | 301, 302 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΏ β 2))) β (πΉβπ) β β) |
304 | | elfzle2 13452 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...(πΏ β 2)) β π β€ (πΏ β 2)) |
305 | 304 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΏ β 2))) β π β€ (πΏ β 2)) |
306 | 289, 296,
290, 305 | leadd1dd 11776 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β (π + (1 / 3)) β€ ((πΏ β 2) + (1 / 3))) |
307 | 14, 72 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΈ β β β§ 0 < πΈ)) |
308 | 307 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΏ β 2))) β (πΈ β β β§ 0 < πΈ)) |
309 | | lemul1 12014 |
. . . . . . . . . . . . . . 15
β’ (((π + (1 / 3)) β β β§
((πΏ β 2) + (1 / 3))
β β β§ (πΈ
β β β§ 0 < πΈ)) β ((π + (1 / 3)) β€ ((πΏ β 2) + (1 / 3)) β ((π + (1 / 3)) Β· πΈ) β€ (((πΏ β 2) + (1 / 3)) Β· πΈ))) |
310 | 291, 297,
308, 309 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β ((π + (1 / 3)) β€ ((πΏ β 2) + (1 / 3)) β ((π + (1 / 3)) Β· πΈ) β€ (((πΏ β 2) + (1 / 3)) Β· πΈ))) |
311 | 306, 310 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΏ β 2))) β ((π + (1 / 3)) Β· πΈ) β€ (((πΏ β 2) + (1 / 3)) Β· πΈ)) |
312 | 108, 132 | resubcld 11590 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΏ β 2) β β) |
313 | 312, 164 | readdcld 11191 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΏ β 2) + (1 / 3)) β
β) |
314 | 313, 14 | remulcld 11192 |
. . . . . . . . . . . . . . 15
β’ (π β (((πΏ β 2) + (1 / 3)) Β· πΈ) β
β) |
315 | 299, 49 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉβπ) β β) |
316 | 120, 164 | resubcld 11590 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πΏ β 1) β (1 / 3)) β
β) |
317 | 316, 14 | remulcld 11192 |
. . . . . . . . . . . . . . . 16
β’ (π β (((πΏ β 1) β (1 / 3)) Β· πΈ) β
β) |
318 | | addid1 11342 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (1 β
β β (1 + 0) = 1) |
319 | 318 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (1 β
β β 1 = (1 + 0)) |
320 | 167, 319 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 1 = (1 +
0)) |
321 | 175 | subidd 11507 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1 β 1) =
0) |
322 | 321 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β 0 = (1 β
1)) |
323 | 322 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1 + 0) = (1 + (1 β
1))) |
324 | | addsubass 11418 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((1
β β β§ 1 β β β§ 1 β β) β ((1 + 1)
β 1) = (1 + (1 β 1))) |
325 | 324 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((1
β β β§ 1 β β β§ 1 β β) β (1 + (1
β 1)) = ((1 + 1) β 1)) |
326 | 175, 175,
175, 325 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1 + (1 β 1)) = ((1
+ 1) β 1)) |
327 | 320, 323,
326 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β 1 = ((1 + 1) β
1)) |
328 | 327 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πΏ β 1) = (πΏ β ((1 + 1) β
1))) |
329 | 243 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1 + 1) =
2) |
330 | 329 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1 + 1) β 1) = (2
β 1)) |
331 | 330 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πΏ β ((1 + 1) β 1)) = (πΏ β (2 β
1))) |
332 | 139, 259,
175 | subsubd 11547 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πΏ β (2 β 1)) = ((πΏ β 2) +
1)) |
333 | 328, 331,
332 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΏ β 1) = ((πΏ β 2) + 1)) |
334 | 333 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((πΏ β 1) β (2 / 3)) = (((πΏ β 2) + 1) β (2 /
3))) |
335 | 258, 60, 9 | divcli 11904 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (2 / 3)
β β |
336 | 335 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (2 / 3) β
β) |
337 | 260, 175,
336 | addsubassd 11539 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((πΏ β 2) + 1) β (2 / 3)) = ((πΏ β 2) + (1 β (2 /
3)))) |
338 | 167, 60, 9 | divcli 11904 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 / 3)
β β |
339 | | df-3 12224 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 3 = (2 +
1) |
340 | 339 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (3 / 3) =
((2 + 1) / 3) |
341 | 258, 167,
60, 9 | divdiri 11919 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((2 + 1)
/ 3) = ((2 / 3) + (1 / 3)) |
342 | 340, 61, 341 | 3eqtr3ri 2774 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((2 / 3)
+ (1 / 3)) = 1 |
343 | 167, 335,
338, 342 | subaddrii 11497 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1
β (2 / 3)) = (1 / 3) |
344 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1 β (2 / 3)) = (1 /
3)) |
345 | 344 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((πΏ β 2) + (1 β (2 / 3))) = ((πΏ β 2) + (1 /
3))) |
346 | 334, 337,
345 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((πΏ β 1) β (2 / 3)) = ((πΏ β 2) + (1 /
3))) |
347 | 131, 7, 9 | redivcli 11929 |
. . . . . . . . . . . . . . . . . . . 20
β’ (2 / 3)
β β |
348 | 347 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (2 / 3) β
β) |
349 | | 1lt2 12331 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 <
2 |
350 | 7, 63 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (3 β
β β§ 0 < 3) |
351 | 1, 131, 350 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 β
β β§ 2 β β β§ (3 β β β§ 0 <
3)) |
352 | | ltdiv1 12026 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((1
β β β§ 2 β β β§ (3 β β β§ 0 < 3))
β (1 < 2 β (1 / 3) < (2 / 3))) |
353 | 351, 352 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1 < 2 β (1 / 3)
< (2 / 3))) |
354 | 349, 353 | mpbii 232 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1 / 3) < (2 /
3)) |
355 | 164, 348,
120, 354 | ltsub2dd 11775 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((πΏ β 1) β (2 / 3)) < ((πΏ β 1) β (1 /
3))) |
356 | 346, 355 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πΏ β 2) + (1 / 3)) < ((πΏ β 1) β (1 /
3))) |
357 | 313, 316,
13, 356 | ltmul1dd 13019 |
. . . . . . . . . . . . . . . 16
β’ (π β (((πΏ β 2) + (1 / 3)) Β· πΈ) < (((πΏ β 1) β (1 / 3)) Β· πΈ)) |
358 | 23 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β Β¬ π β (π·β(πΏ β 1))) |
359 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = (πΏ β 1) β (π β (1 / 3)) = ((πΏ β 1) β (1 /
3))) |
360 | 359 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (πΏ β 1) β ((π β (1 / 3)) Β· πΈ) = (((πΏ β 1) β (1 / 3)) Β· πΈ)) |
361 | 360 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (πΏ β 1) β ((πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ) β (πΉβπ‘) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) |
362 | 361 | rabbidv 3418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πΏ β 1) β {π‘ β π β£ (πΉβπ‘) β€ ((π β (1 / 3)) Β· πΈ)} = {π‘ β π β£ (πΉβπ‘) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)}) |
363 | 129 | peano2zd 12617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π + 1) β β€) |
364 | 189 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β 1 β€ πΏ) |
365 | 134, 116 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π + 1) β β) |
366 | 134 | lep1d 12093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β€ (π + 1)) |
367 | 108, 134,
365, 190, 366 | letrd 11319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β πΏ β€ (π + 1)) |
368 | 186, 363,
125, 364, 367 | elfzd 13439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β πΏ β (1...(π + 1))) |
369 | 139, 175 | npcand 11523 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((πΏ β 1) + 1) = πΏ) |
370 | | 0p1e1 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (0 + 1) =
1 |
371 | 370 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (0 + 1) =
1) |
372 | 371 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((0 + 1)...(π + 1)) = (1...(π + 1))) |
373 | 368, 369,
372 | 3eltr4d 2853 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((πΏ β 1) + 1) β ((0 + 1)...(π + 1))) |
374 | | 0zd 12518 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β 0 β
β€) |
375 | 125, 186 | zsubcld 12619 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (πΏ β 1) β β€) |
376 | | fzaddel 13482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((0
β β€ β§ π
β β€) β§ ((πΏ
β 1) β β€ β§ 1 β β€)) β ((πΏ β 1) β (0...π) β ((πΏ β 1) + 1) β ((0 + 1)...(π + 1)))) |
377 | 374, 129,
375, 186, 376 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((πΏ β 1) β (0...π) β ((πΏ β 1) + 1) β ((0 + 1)...(π + 1)))) |
378 | 373, 377 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (πΏ β 1) β (0...π)) |
379 | | rabexg 5293 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β V β {π‘ β π β£ (πΉβπ‘) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)} β V) |
380 | 33, 379 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β {π‘ β π β£ (πΉβπ‘) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)} β V) |
381 | 25, 362, 378, 380 | fvmptd3 6976 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π·β(πΏ β 1)) = {π‘ β π β£ (πΉβπ‘) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)}) |
382 | 358, 381 | neleqtrd 2860 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β Β¬ π β {π‘ β π β£ (πΉβπ‘) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)}) |
383 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π‘(((πΏ β 1) β (1 / 3)) Β· πΈ) |
384 | 41, 42, 383 | nfbr 5157 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π‘(πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) |
385 | 45 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π β ((πΉβπ‘) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) |
386 | 38, 39, 384, 385 | elrabf 3646 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β {π‘ β π β£ (πΉβπ‘) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)} β (π β π β§ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) |
387 | 382, 386 | sylnib 328 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Β¬ (π β π β§ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) |
388 | | ianor 981 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
(π β π β§ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)) β (Β¬ π β π β¨ Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) |
389 | 387, 388 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Β¬ π β π β¨ Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) |
390 | | olc 867 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β (Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ π β π)) |
391 | 390 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β π β§ (Β¬ π β π β¨ Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) β ((Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ π β π) β§ (Β¬ π β π β¨ Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)))) |
392 | 49, 389, 391 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ π β π) β§ (Β¬ π β π β¨ Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)))) |
393 | | orcom 869 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Β¬
π β π β¨ Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)) β (Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ Β¬ π β π)) |
394 | 393 | anbi2i 624 |
. . . . . . . . . . . . . . . . . . 19
β’ (((Β¬
(πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ π β π) β§ (Β¬ π β π β¨ Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) β ((Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ π β π) β§ (Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ Β¬ π β π))) |
395 | 392, 394 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ π β π) β§ (Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ Β¬ π β π))) |
396 | | pm4.43 1022 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
(πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β ((Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ π β π) β§ (Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ) β¨ Β¬ π β π))) |
397 | 395, 396 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (π β Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ)) |
398 | 317, 315 | ltnled 11309 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((((πΏ β 1) β (1 / 3)) Β· πΈ) < (πΉβπ) β Β¬ (πΉβπ) β€ (((πΏ β 1) β (1 / 3)) Β· πΈ))) |
399 | 397, 398 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (π β (((πΏ β 1) β (1 / 3)) Β· πΈ) < (πΉβπ)) |
400 | 314, 317,
315, 357, 399 | lttrd 11323 |
. . . . . . . . . . . . . . 15
β’ (π β (((πΏ β 2) + (1 / 3)) Β· πΈ) < (πΉβπ)) |
401 | 314, 315,
400 | ltled 11310 |
. . . . . . . . . . . . . 14
β’ (π β (((πΏ β 2) + (1 / 3)) Β· πΈ) β€ (πΉβπ)) |
402 | 401 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΏ β 2))) β (((πΏ β 2) + (1 / 3)) Β· πΈ) β€ (πΉβπ)) |
403 | 293, 298,
303, 311, 402 | letrd 11319 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΏ β 2))) β ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ)) |
404 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π‘((π + (1 / 3)) Β· πΈ) |
405 | 404, 42, 41 | nfbr 5157 |
. . . . . . . . . . . . 13
β’
β²π‘((π + (1 / 3)) Β· πΈ) β€ (πΉβπ) |
406 | 45 | breq2d 5122 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘) β ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ))) |
407 | 38, 39, 405, 406 | elrabf 3646 |
. . . . . . . . . . . 12
β’ (π β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β (π β π β§ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ))) |
408 | 286, 403,
407 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΏ β 2))) β π β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
409 | | stoweidlem26.5 |
. . . . . . . . . . . 12
β’ π΅ = (π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
410 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π + (1 / 3)) = (π + (1 / 3))) |
411 | 410 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π + (1 / 3)) Β· πΈ) = ((π + (1 / 3)) Β· πΈ)) |
412 | 411 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π = π β (((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘) β ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘))) |
413 | 412 | rabbidv 3418 |
. . . . . . . . . . . 12
β’ (π = π β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} = {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
414 | | rabexg 5293 |
. . . . . . . . . . . . . 14
β’ (π β V β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β V) |
415 | 33, 414 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β V) |
416 | 415 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΏ β 2))) β {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} β V) |
417 | 409, 413,
150, 416 | fvmptd3 6976 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΏ β 2))) β (π΅βπ) = {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
418 | 408, 417 | eleqtrrd 2841 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(πΏ β 2))) β π β (π΅βπ)) |
419 | 145 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2)) β§ π β (π΅βπ)) β ((πΏ β 2) β β€ β§ π β β€ β§ (πΏ β 2) β€ π)) |
420 | 419, 146 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΏ β 2)) β§ π β (π΅βπ)) β π β (β€β₯β(πΏ β 2))) |
421 | 420, 148 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΏ β 2)) β§ π β (π΅βπ)) β (0...(πΏ β 2)) β (0...π)) |
422 | | simp2 1138 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΏ β 2)) β§ π β (π΅βπ)) β π β (0...(πΏ β 2))) |
423 | 421, 422 | sseldd 3950 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΏ β 2)) β§ π β (π΅βπ)) β π β (0...π)) |
424 | | elex 3466 |
. . . . . . . . . . . . 13
β’ (π β (π΅βπ) β π β V) |
425 | 424 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...π) β§ π β (π΅βπ)) β π β V) |
426 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π‘(0...π) |
427 | | nfrab1 3429 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π‘{π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)} |
428 | 426, 427 | nfmpt 5217 |
. . . . . . . . . . . . . . . . . 18
β’
β²π‘(π β (0...π) β¦ {π‘ β π β£ ((π + (1 / 3)) Β· πΈ) β€ (πΉβπ‘)}) |
429 | 409, 428 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . 17
β’
β²π‘π΅ |
430 | | nfcv 2908 |
. . . . . . . . . . . . . . . . 17
β’
β²π‘π |
431 | 429, 430 | nffv 6857 |
. . . . . . . . . . . . . . . 16
β’
β²π‘(π΅βπ) |
432 | 431 | nfel2 2926 |
. . . . . . . . . . . . . . 15
β’
β²π‘ π β (π΅βπ) |
433 | 88, 89, 432 | nf3an 1905 |
. . . . . . . . . . . . . 14
β’
β²π‘(π β§ π β (0...π) β§ π β (π΅βπ)) |
434 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π‘(1 β
(πΈ / π)) < ((πβπ)βπ) |
435 | 433, 434 | nfim 1900 |
. . . . . . . . . . . . 13
β’
β²π‘((π β§ π β (0...π) β§ π β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ)) |
436 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
β’ (π‘ = π β (π‘ β (π΅βπ) β π β (π΅βπ))) |
437 | 436 | 3anbi3d 1443 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β ((π β§ π β (0...π) β§ π‘ β (π΅βπ)) β (π β§ π β (0...π) β§ π β (π΅βπ)))) |
438 | 93 | breq2d 5122 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β ((1 β (πΈ / π)) < ((πβπ)βπ‘) β (1 β (πΈ / π)) < ((πβπ)βπ))) |
439 | 437, 438 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (((π β§ π β (0...π) β§ π‘ β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ‘)) β ((π β§ π β (0...π) β§ π β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ)))) |
440 | | stoweidlem26.15 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...π) β§ π‘ β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ‘)) |
441 | 435, 439,
440 | vtoclg1f 3527 |
. . . . . . . . . . . 12
β’ (π β V β ((π β§ π β (0...π) β§ π β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ))) |
442 | 425, 441 | mpcom 38 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...π) β§ π β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ)) |
443 | 423, 442 | syld3an2 1412 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(πΏ β 2)) β§ π β (π΅βπ)) β (1 β (πΈ / π)) < ((πβπ)βπ)) |
444 | 418, 443 | mpd3an3 1463 |
. . . . . . . . 9
β’ ((π β§ π β (0...(πΏ β 2))) β (1 β (πΈ / π)) < ((πβπ)βπ)) |
445 | 444 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ Β¬ πΏ = 1) β§ π β (0...(πΏ β 2))) β (1 β (πΈ / π)) < ((πβπ)βπ)) |
446 | 279, 281,
282, 285, 445 | fsumlt 15692 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β (0...(πΏ β 2))(1 β (πΈ / π)) < Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) |
447 | 278, 446 | eqbrtrrd 5134 |
. . . . . 6
β’ ((π β§ Β¬ πΏ = 1) β ((1 β (πΈ / π)) Β· (πΏ β 1)) < Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) |
448 | 121 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β ((1 β (πΈ / π)) Β· (πΏ β 1)) β
β) |
449 | 152 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β (0...(πΏ β 2))((πβπ)βπ) β β) |
450 | 307 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β (πΈ β β β§ 0 < πΈ)) |
451 | | ltmul2 12013 |
. . . . . . 7
β’ ((((1
β (πΈ / π)) Β· (πΏ β 1)) β β β§
Ξ£π β (0...(πΏ β 2))((πβπ)βπ) β β β§ (πΈ β β β§ 0 < πΈ)) β (((1 β (πΈ / π)) Β· (πΏ β 1)) < Ξ£π β (0...(πΏ β 2))((πβπ)βπ) β (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1))) < (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)))) |
452 | 448, 449,
450, 451 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ Β¬ πΏ = 1) β (((1 β (πΈ / π)) Β· (πΏ β 1)) < Ξ£π β (0...(πΏ β 2))((πβπ)βπ) β (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1))) < (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)))) |
453 | 447, 452 | mpbid 231 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β (πΈ Β· ((1 β (πΈ / π)) Β· (πΏ β 1))) < (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ))) |
454 | 115, 123,
154, 227, 453 | lttrd 11323 |
. . . 4
β’ ((π β§ Β¬ πΏ = 1) β ((πΏ β (4 / 3)) Β· πΈ) < (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ))) |
455 | 150, 52 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(πΏ β 2))) β (πΈ Β· ((πβπ)βπ)) β β) |
456 | 455 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ Β¬ πΏ = 1) β§ π β (0...(πΏ β 2))) β (πΈ Β· ((πβπ)βπ)) β β) |
457 | 456 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ Β¬ πΏ = 1) β§ π β (0...(πΏ β 2))) β (πΈ Β· ((πβπ)βπ)) β β) |
458 | 279, 457 | fsumcl 15625 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ)) β β) |
459 | 458 | addid1d 11362 |
. . . . . 6
β’ ((π β§ Β¬ πΏ = 1) β (Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ)) + 0) = Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ))) |
460 | | 0red 11165 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β 0 β
β) |
461 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ = 1) β ((πΏ β 1)...π) β Fin) |
462 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΏ β 1)...π)) β πΈ β β) |
463 | | 0zd 12518 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΏ β 1)...π)) β 0 β β€) |
464 | 129 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΏ β 1)...π)) β π β β€) |
465 | | elfzelz 13448 |
. . . . . . . . . . . . 13
β’ (π β ((πΏ β 1)...π) β π β β€) |
466 | 465 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΏ β 1)...π)) β π β β€) |
467 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΏ β 1)...π)) β 0 β β) |
468 | 120 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΏ β 1)...π)) β (πΏ β 1) β β) |
469 | 465 | zred 12614 |
. . . . . . . . . . . . . 14
β’ (π β ((πΏ β 1)...π) β π β β) |
470 | 469 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΏ β 1)...π)) β π β β) |
471 | | 1m1e0 12232 |
. . . . . . . . . . . . . . 15
β’ (1
β 1) = 0 |
472 | 116, 108,
116, 364 | lesub1dd 11778 |
. . . . . . . . . . . . . . 15
β’ (π β (1 β 1) β€ (πΏ β 1)) |
473 | 471, 472 | eqbrtrrid 5146 |
. . . . . . . . . . . . . 14
β’ (π β 0 β€ (πΏ β 1)) |
474 | 473 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΏ β 1)...π)) β 0 β€ (πΏ β 1)) |
475 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πΏ β 1)...π)) β π β ((πΏ β 1)...π)) |
476 | 375 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((πΏ β 1)...π)) β (πΏ β 1) β β€) |
477 | | elfz 13437 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ (πΏ β 1) β β€ β§
π β β€) β
(π β ((πΏ β 1)...π) β ((πΏ β 1) β€ π β§ π β€ π))) |
478 | 466, 476,
464, 477 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((πΏ β 1)...π)) β (π β ((πΏ β 1)...π) β ((πΏ β 1) β€ π β§ π β€ π))) |
479 | 475, 478 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΏ β 1)...π)) β ((πΏ β 1) β€ π β§ π β€ π)) |
480 | 479 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΏ β 1)...π)) β (πΏ β 1) β€ π) |
481 | 467, 468,
470, 474, 480 | letrd 11319 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΏ β 1)...π)) β 0 β€ π) |
482 | | elfzle2 13452 |
. . . . . . . . . . . . 13
β’ (π β ((πΏ β 1)...π) β π β€ π) |
483 | 482 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΏ β 1)...π)) β π β€ π) |
484 | 463, 464,
466, 481, 483 | elfzd 13439 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΏ β 1)...π)) β π β (0...π)) |
485 | 484, 51 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΏ β 1)...π)) β ((πβπ)βπ) β β) |
486 | 462, 485 | remulcld 11192 |
. . . . . . . . 9
β’ ((π β§ π β ((πΏ β 1)...π)) β (πΈ Β· ((πβπ)βπ)) β β) |
487 | 486 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ Β¬ πΏ = 1) β§ π β ((πΏ β 1)...π)) β (πΈ Β· ((πβπ)βπ)) β β) |
488 | 461, 487 | fsumrecl 15626 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β ((πΏ β 1)...π)(πΈ Β· ((πβπ)βπ)) β β) |
489 | 279, 456 | fsumrecl 15626 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ)) β β) |
490 | | fzfid 13885 |
. . . . . . . . 9
β’ (π β ((πΏ β 1)...π) β Fin) |
491 | 176 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΏ β 1)...π)) β πΈ β β) |
492 | 491 | mul01d 11361 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΏ β 1)...π)) β (πΈ Β· 0) = 0) |
493 | 484, 100 | syldan 592 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΏ β 1)...π)) β 0 β€ ((πβπ)βπ)) |
494 | 307 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΏ β 1)...π)) β (πΈ β β β§ 0 < πΈ)) |
495 | | lemul2 12015 |
. . . . . . . . . . . 12
β’ ((0
β β β§ ((πβπ)βπ) β β β§ (πΈ β β β§ 0 < πΈ)) β (0 β€ ((πβπ)βπ) β (πΈ Β· 0) β€ (πΈ Β· ((πβπ)βπ)))) |
496 | 467, 485,
494, 495 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΏ β 1)...π)) β (0 β€ ((πβπ)βπ) β (πΈ Β· 0) β€ (πΈ Β· ((πβπ)βπ)))) |
497 | 493, 496 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΏ β 1)...π)) β (πΈ Β· 0) β€ (πΈ Β· ((πβπ)βπ))) |
498 | 492, 497 | eqbrtrrd 5134 |
. . . . . . . . 9
β’ ((π β§ π β ((πΏ β 1)...π)) β 0 β€ (πΈ Β· ((πβπ)βπ))) |
499 | 490, 486,
498 | fsumge0 15687 |
. . . . . . . 8
β’ (π β 0 β€ Ξ£π β ((πΏ β 1)...π)(πΈ Β· ((πβπ)βπ))) |
500 | 499 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β 0 β€ Ξ£π β ((πΏ β 1)...π)(πΈ Β· ((πβπ)βπ))) |
501 | 460, 488,
489, 500 | leadd2dd 11777 |
. . . . . 6
β’ ((π β§ Β¬ πΏ = 1) β (Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ)) + 0) β€ (Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ)) + Ξ£π β ((πΏ β 1)...π)(πΈ Β· ((πβπ)βπ)))) |
502 | 459, 501 | eqbrtrrd 5134 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ)) β€ (Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ)) + Ξ£π β ((πΏ β 1)...π)(πΈ Β· ((πβπ)βπ)))) |
503 | 151 | recnd 11190 |
. . . . . . 7
β’ ((π β§ π β (0...(πΏ β 2))) β ((πβπ)βπ) β β) |
504 | 124, 176,
503 | fsummulc2 15676 |
. . . . . 6
β’ (π β (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) = Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ))) |
505 | 504 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) = Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ))) |
506 | | stoweidlem26.2 |
. . . . . . . . 9
β’
β²ππ |
507 | | elfzelz 13448 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...(πΏ β 2)) β π β β€) |
508 | 507 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΏ β 2))) β π β β€) |
509 | 508 | zred 12614 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β π β β) |
510 | 312 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β (πΏ β 2) β β) |
511 | 120 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β (πΏ β 1) β β) |
512 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...(πΏ β 2))) β π β (0...(πΏ β 2))) |
513 | | 0zd 12518 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0...(πΏ β 2))) β 0 β
β€) |
514 | 128 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0...(πΏ β 2))) β (πΏ β 2) β β€) |
515 | | elfz 13437 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ 0 β
β€ β§ (πΏ β 2)
β β€) β (π
β (0...(πΏ β 2))
β (0 β€ π β§
π β€ (πΏ β 2)))) |
516 | 508, 513,
514, 515 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...(πΏ β 2))) β (π β (0...(πΏ β 2)) β (0 β€ π β§ π β€ (πΏ β 2)))) |
517 | 512, 516 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...(πΏ β 2))) β (0 β€ π β§ π β€ (πΏ β 2))) |
518 | 517 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β π β€ (πΏ β 2)) |
519 | 116, 132,
108 | ltsub2d 11772 |
. . . . . . . . . . . . . . . 16
β’ (π β (1 < 2 β (πΏ β 2) < (πΏ β 1))) |
520 | 349, 519 | mpbii 232 |
. . . . . . . . . . . . . . 15
β’ (π β (πΏ β 2) < (πΏ β 1)) |
521 | 520 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...(πΏ β 2))) β (πΏ β 2) < (πΏ β 1)) |
522 | 509, 510,
511, 518, 521 | lelttrd 11320 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΏ β 2))) β π < (πΏ β 1)) |
523 | 509, 511 | ltnled 11309 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0...(πΏ β 2))) β (π < (πΏ β 1) β Β¬ (πΏ β 1) β€ π)) |
524 | 522, 523 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΏ β 2))) β Β¬ (πΏ β 1) β€ π) |
525 | 524 | intnanrd 491 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΏ β 2))) β Β¬ ((πΏ β 1) β€ π β§ π β€ π)) |
526 | 375 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΏ β 2))) β (πΏ β 1) β β€) |
527 | 129 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (0...(πΏ β 2))) β π β β€) |
528 | | elfz 13437 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ (πΏ β 1) β β€ β§
π β β€) β
(π β ((πΏ β 1)...π) β ((πΏ β 1) β€ π β§ π β€ π))) |
529 | 508, 526,
527, 528 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(πΏ β 2))) β (π β ((πΏ β 1)...π) β ((πΏ β 1) β€ π β§ π β€ π))) |
530 | 525, 529 | mtbird 325 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(πΏ β 2))) β Β¬ π β ((πΏ β 1)...π)) |
531 | 530 | ex 414 |
. . . . . . . . 9
β’ (π β (π β (0...(πΏ β 2)) β Β¬ π β ((πΏ β 1)...π))) |
532 | 506, 531 | ralrimi 3243 |
. . . . . . . 8
β’ (π β βπ β (0...(πΏ β 2)) Β¬ π β ((πΏ β 1)...π)) |
533 | | disj 4412 |
. . . . . . . 8
β’
(((0...(πΏ β
2)) β© ((πΏ β
1)...π)) = β
β
βπ β
(0...(πΏ β 2)) Β¬
π β ((πΏ β 1)...π)) |
534 | 532, 533 | sylibr 233 |
. . . . . . 7
β’ (π β ((0...(πΏ β 2)) β© ((πΏ β 1)...π)) = β
) |
535 | 534 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ πΏ = 1) β ((0...(πΏ β 2)) β© ((πΏ β 1)...π)) = β
) |
536 | 144 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΏ = 1) β (πΏ β 2) β€ π) |
537 | 128, 374,
129 | 3jca 1129 |
. . . . . . . . . . 11
β’ (π β ((πΏ β 2) β β€ β§ 0 β
β€ β§ π β
β€)) |
538 | 537 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ Β¬ πΏ = 1) β ((πΏ β 2) β β€ β§ 0 β
β€ β§ π β
β€)) |
539 | | elfz 13437 |
. . . . . . . . . 10
β’ (((πΏ β 2) β β€ β§
0 β β€ β§ π
β β€) β ((πΏ
β 2) β (0...π)
β (0 β€ (πΏ β
2) β§ (πΏ β 2) β€
π))) |
540 | 538, 539 | syl 17 |
. . . . . . . . 9
β’ ((π β§ Β¬ πΏ = 1) β ((πΏ β 2) β (0...π) β (0 β€ (πΏ β 2) β§ (πΏ β 2) β€ π))) |
541 | 252, 536,
540 | mpbir2and 712 |
. . . . . . . 8
β’ ((π β§ Β¬ πΏ = 1) β (πΏ β 2) β (0...π)) |
542 | | fzsplit 13474 |
. . . . . . . 8
β’ ((πΏ β 2) β (0...π) β (0...π) = ((0...(πΏ β 2)) βͺ (((πΏ β 2) + 1)...π))) |
543 | 541, 542 | syl 17 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β (0...π) = ((0...(πΏ β 2)) βͺ (((πΏ β 2) + 1)...π))) |
544 | 263, 269,
270 | 3eqtrd 2781 |
. . . . . . . . . 10
β’ (π β ((πΏ β 2) + 1) = (πΏ β 1)) |
545 | 544 | oveq1d 7377 |
. . . . . . . . 9
β’ (π β (((πΏ β 2) + 1)...π) = ((πΏ β 1)...π)) |
546 | 545 | uneq2d 4128 |
. . . . . . . 8
β’ (π β ((0...(πΏ β 2)) βͺ (((πΏ β 2) + 1)...π)) = ((0...(πΏ β 2)) βͺ ((πΏ β 1)...π))) |
547 | 546 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ πΏ = 1) β ((0...(πΏ β 2)) βͺ (((πΏ β 2) + 1)...π)) = ((0...(πΏ β 2)) βͺ ((πΏ β 1)...π))) |
548 | 543, 547 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ Β¬ πΏ = 1) β (0...π) = ((0...(πΏ β 2)) βͺ ((πΏ β 1)...π))) |
549 | | fzfid 13885 |
. . . . . 6
β’ ((π β§ Β¬ πΏ = 1) β (0...π) β Fin) |
550 | 176 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β πΈ β β) |
551 | 51 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β ((πβπ)βπ) β β) |
552 | 550, 551 | mulcld 11182 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β (πΈ Β· ((πβπ)βπ)) β β) |
553 | 552 | adantlr 714 |
. . . . . 6
β’ (((π β§ Β¬ πΏ = 1) β§ π β (0...π)) β (πΈ Β· ((πβπ)βπ)) β β) |
554 | 535, 548,
549, 553 | fsumsplit 15633 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)) = (Ξ£π β (0...(πΏ β 2))(πΈ Β· ((πβπ)βπ)) + Ξ£π β ((πΏ β 1)...π)(πΈ Β· ((πβπ)βπ)))) |
555 | 502, 505,
554 | 3brtr4d 5142 |
. . . 4
β’ ((π β§ Β¬ πΏ = 1) β (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β€ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
556 | 114, 153,
53 | 3jca 1129 |
. . . . . 6
β’ (π β (((πΏ β (4 / 3)) Β· πΈ) β β β§ (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β β β§ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)) β β)) |
557 | 556 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ πΏ = 1) β (((πΏ β (4 / 3)) Β· πΈ) β β β§ (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β β β§ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)) β β)) |
558 | | ltletr 11254 |
. . . . 5
β’ ((((πΏ β (4 / 3)) Β· πΈ) β β β§ (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β β β§ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)) β β) β ((((πΏ β (4 / 3)) Β· πΈ) < (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β§ (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β€ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β ((πΏ β (4 / 3)) Β· πΈ) < Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)))) |
559 | 557, 558 | syl 17 |
. . . 4
β’ ((π β§ Β¬ πΏ = 1) β ((((πΏ β (4 / 3)) Β· πΈ) < (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β§ (πΈ Β· Ξ£π β (0...(πΏ β 2))((πβπ)βπ)) β€ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) β ((πΏ β (4 / 3)) Β· πΈ) < Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)))) |
560 | 454, 555,
559 | mp2and 698 |
. . 3
β’ ((π β§ Β¬ πΏ = 1) β ((πΏ β (4 / 3)) Β· πΈ) < Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
561 | 105, 560 | pm2.61dan 812 |
. 2
β’ (π β ((πΏ β (4 / 3)) Β· πΈ) < Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
562 | | sumex 15579 |
. . 3
β’
Ξ£π β
(0...π)(πΈ Β· ((πβπ)βπ)) β V |
563 | 93 | oveq2d 7378 |
. . . . 5
β’ (π‘ = π β (πΈ Β· ((πβπ)βπ‘)) = (πΈ Β· ((πβπ)βπ))) |
564 | 563 | sumeq2sdv 15596 |
. . . 4
β’ (π‘ = π β Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
565 | | eqid 2737 |
. . . 4
β’ (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) = (π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘))) |
566 | 564, 565 | fvmptg 6951 |
. . 3
β’ ((π β π β§ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ)) β V) β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
567 | 49, 562, 566 | sylancl 587 |
. 2
β’ (π β ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ) = Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ))) |
568 | 561, 567 | breqtrrd 5138 |
1
β’ (π β ((πΏ β (4 / 3)) Β· πΈ) < ((π‘ β π β¦ Ξ£π β (0...π)(πΈ Β· ((πβπ)βπ‘)))βπ)) |