Step | Hyp | Ref
| Expression |
1 | | stoweidlem38.3 |
. . . . . 6
β’ (π β π β β) |
2 | 1 | nnrecred 12212 |
. . . . 5
β’ (π β (1 / π) β β) |
3 | 2 | adantr 482 |
. . . 4
β’ ((π β§ π β π) β (1 / π) β β) |
4 | | fzfid 13887 |
. . . . 5
β’ ((π β§ π β π) β (1...π) β Fin) |
5 | | stoweidlem38.1 |
. . . . . . . 8
β’ π = {β β π΄ β£ ((ββπ) = 0 β§ βπ‘ β π (0 β€ (ββπ‘) β§ (ββπ‘) β€ 1))} |
6 | | stoweidlem38.4 |
. . . . . . . 8
β’ (π β πΊ:(1...π)βΆπ) |
7 | | stoweidlem38.5 |
. . . . . . . 8
β’ ((π β§ π β π΄) β π:πβΆβ) |
8 | 5, 6, 7 | stoweidlem15 44346 |
. . . . . . 7
β’ (((π β§ π β (1...π)) β§ π β π) β (((πΊβπ)βπ) β β β§ 0 β€ ((πΊβπ)βπ) β§ ((πΊβπ)βπ) β€ 1)) |
9 | 8 | simp1d 1143 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β π) β ((πΊβπ)βπ) β β) |
10 | 9 | an32s 651 |
. . . . 5
β’ (((π β§ π β π) β§ π β (1...π)) β ((πΊβπ)βπ) β β) |
11 | 4, 10 | fsumrecl 15627 |
. . . 4
β’ ((π β§ π β π) β Ξ£π β (1...π)((πΊβπ)βπ) β β) |
12 | | 1red 11164 |
. . . . . 6
β’ (π β 1 β
β) |
13 | | 0le1 11686 |
. . . . . . 7
β’ 0 β€
1 |
14 | 13 | a1i 11 |
. . . . . 6
β’ (π β 0 β€ 1) |
15 | 1 | nnred 12176 |
. . . . . 6
β’ (π β π β β) |
16 | 1 | nngt0d 12210 |
. . . . . 6
β’ (π β 0 < π) |
17 | | divge0 12032 |
. . . . . 6
β’ (((1
β β β§ 0 β€ 1) β§ (π β β β§ 0 < π)) β 0 β€ (1 / π)) |
18 | 12, 14, 15, 16, 17 | syl22anc 838 |
. . . . 5
β’ (π β 0 β€ (1 / π)) |
19 | 18 | adantr 482 |
. . . 4
β’ ((π β§ π β π) β 0 β€ (1 / π)) |
20 | 8 | simp2d 1144 |
. . . . . 6
β’ (((π β§ π β (1...π)) β§ π β π) β 0 β€ ((πΊβπ)βπ)) |
21 | 20 | an32s 651 |
. . . . 5
β’ (((π β§ π β π) β§ π β (1...π)) β 0 β€ ((πΊβπ)βπ)) |
22 | 4, 10, 21 | fsumge0 15688 |
. . . 4
β’ ((π β§ π β π) β 0 β€ Ξ£π β (1...π)((πΊβπ)βπ)) |
23 | 3, 11, 19, 22 | mulge0d 11740 |
. . 3
β’ ((π β§ π β π) β 0 β€ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ))) |
24 | | stoweidlem38.2 |
. . . 4
β’ π = (π‘ β π β¦ ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ‘))) |
25 | 5, 24, 1, 6, 7 | stoweidlem30 44361 |
. . 3
β’ ((π β§ π β π) β (πβπ) = ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ))) |
26 | 23, 25 | breqtrrd 5137 |
. 2
β’ ((π β§ π β π) β 0 β€ (πβπ)) |
27 | | 1red 11164 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (1...π)) β 1 β β) |
28 | 8 | simp3d 1145 |
. . . . . . . 8
β’ (((π β§ π β (1...π)) β§ π β π) β ((πΊβπ)βπ) β€ 1) |
29 | 28 | an32s 651 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (1...π)) β ((πΊβπ)βπ) β€ 1) |
30 | 4, 10, 27, 29 | fsumle 15692 |
. . . . . 6
β’ ((π β§ π β π) β Ξ£π β (1...π)((πΊβπ)βπ) β€ Ξ£π β (1...π)1) |
31 | | fzfid 13887 |
. . . . . . . . 9
β’ (π β (1...π) β Fin) |
32 | | ax-1cn 11117 |
. . . . . . . . 9
β’ 1 β
β |
33 | | fsumconst 15683 |
. . . . . . . . 9
β’
(((1...π) β Fin
β§ 1 β β) β Ξ£π β (1...π)1 = ((β―β(1...π)) Β· 1)) |
34 | 31, 32, 33 | sylancl 587 |
. . . . . . . 8
β’ (π β Ξ£π β (1...π)1 = ((β―β(1...π)) Β· 1)) |
35 | 1 | nnnn0d 12481 |
. . . . . . . . . 10
β’ (π β π β
β0) |
36 | | hashfz1 14255 |
. . . . . . . . . 10
β’ (π β β0
β (β―β(1...π)) = π) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
β’ (π β (β―β(1...π)) = π) |
38 | 37 | oveq1d 7376 |
. . . . . . . 8
β’ (π β ((β―β(1...π)) Β· 1) = (π Β· 1)) |
39 | 1 | nncnd 12177 |
. . . . . . . . 9
β’ (π β π β β) |
40 | 39 | mulid1d 11180 |
. . . . . . . 8
β’ (π β (π Β· 1) = π) |
41 | 34, 38, 40 | 3eqtrd 2777 |
. . . . . . 7
β’ (π β Ξ£π β (1...π)1 = π) |
42 | 41 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β Ξ£π β (1...π)1 = π) |
43 | 30, 42 | breqtrd 5135 |
. . . . 5
β’ ((π β§ π β π) β Ξ£π β (1...π)((πΊβπ)βπ) β€ π) |
44 | 15 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β π β β) |
45 | | 1red 11164 |
. . . . . . 7
β’ ((π β§ π β π) β 1 β β) |
46 | | 0lt1 11685 |
. . . . . . . 8
β’ 0 <
1 |
47 | 46 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π) β 0 < 1) |
48 | 15, 16 | jca 513 |
. . . . . . . 8
β’ (π β (π β β β§ 0 < π)) |
49 | 48 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β (π β β β§ 0 < π)) |
50 | | divgt0 12031 |
. . . . . . 7
β’ (((1
β β β§ 0 < 1) β§ (π β β β§ 0 < π)) β 0 < (1 / π)) |
51 | 45, 47, 49, 50 | syl21anc 837 |
. . . . . 6
β’ ((π β§ π β π) β 0 < (1 / π)) |
52 | | lemul2 12016 |
. . . . . 6
β’
((Ξ£π β
(1...π)((πΊβπ)βπ) β β β§ π β β β§ ((1 / π) β β β§ 0 < (1
/ π))) β (Ξ£π β (1...π)((πΊβπ)βπ) β€ π β ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ)) β€ ((1 / π) Β· π))) |
53 | 11, 44, 3, 51, 52 | syl112anc 1375 |
. . . . 5
β’ ((π β§ π β π) β (Ξ£π β (1...π)((πΊβπ)βπ) β€ π β ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ)) β€ ((1 / π) Β· π))) |
54 | 43, 53 | mpbid 231 |
. . . 4
β’ ((π β§ π β π) β ((1 / π) Β· Ξ£π β (1...π)((πΊβπ)βπ)) β€ ((1 / π) Β· π)) |
55 | 25, 54 | eqbrtrd 5131 |
. . 3
β’ ((π β§ π β π) β (πβπ) β€ ((1 / π) Β· π)) |
56 | 32 | a1i 11 |
. . . . . 6
β’ (π β 1 β
β) |
57 | 1 | nnne0d 12211 |
. . . . . 6
β’ (π β π β 0) |
58 | 56, 39, 57 | 3jca 1129 |
. . . . 5
β’ (π β (1 β β β§
π β β β§
π β 0)) |
59 | 58 | adantr 482 |
. . . 4
β’ ((π β§ π β π) β (1 β β β§ π β β β§ π β 0)) |
60 | | divcan1 11830 |
. . . 4
β’ ((1
β β β§ π
β β β§ π β
0) β ((1 / π) Β·
π) = 1) |
61 | 59, 60 | syl 17 |
. . 3
β’ ((π β§ π β π) β ((1 / π) Β· π) = 1) |
62 | 55, 61 | breqtrd 5135 |
. 2
β’ ((π β§ π β π) β (πβπ) β€ 1) |
63 | 26, 62 | jca 513 |
1
β’ ((π β§ π β π) β (0 β€ (πβπ) β§ (πβπ) β€ 1)) |