Step | Hyp | Ref
| Expression |
1 | | birthday.t |
. . . . . . . 8
β’ π = {π β£ π:(1...πΎ)β1-1β(1...π)} |
2 | | abn0 4372 |
. . . . . . . . . . . 12
β’ ({π β£ π:(1...πΎ)β1-1β(1...π)} β β
β βπ π:(1...πΎ)β1-1β(1...π)) |
3 | | ovex 7434 |
. . . . . . . . . . . . 13
β’
(1...π) β
V |
4 | 3 | brdom 8952 |
. . . . . . . . . . . 12
β’
((1...πΎ) βΌ
(1...π) β βπ π:(1...πΎ)β1-1β(1...π)) |
5 | 2, 4 | bitr4i 278 |
. . . . . . . . . . 11
β’ ({π β£ π:(1...πΎ)β1-1β(1...π)} β β
β (1...πΎ) βΌ (1...π)) |
6 | | hashfz1 14303 |
. . . . . . . . . . . . 13
β’ (πΎ β β0
β (β―β(1...πΎ)) = πΎ) |
7 | | nnnn0 12476 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β0) |
8 | | hashfz1 14303 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (β―β(1...π)) = π) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β β
(β―β(1...π)) =
π) |
10 | 6, 9 | breqan12d 5154 |
. . . . . . . . . . . 12
β’ ((πΎ β β0
β§ π β β)
β ((β―β(1...πΎ)) β€ (β―β(1...π)) β πΎ β€ π)) |
11 | | fzfid 13935 |
. . . . . . . . . . . . 13
β’ ((πΎ β β0
β§ π β β)
β (1...πΎ) β
Fin) |
12 | | fzfid 13935 |
. . . . . . . . . . . . 13
β’ ((πΎ β β0
β§ π β β)
β (1...π) β
Fin) |
13 | | hashdom 14336 |
. . . . . . . . . . . . 13
β’
(((1...πΎ) β Fin
β§ (1...π) β Fin)
β ((β―β(1...πΎ)) β€ (β―β(1...π)) β (1...πΎ) βΌ (1...π))) |
14 | 11, 12, 13 | syl2anc 583 |
. . . . . . . . . . . 12
β’ ((πΎ β β0
β§ π β β)
β ((β―β(1...πΎ)) β€ (β―β(1...π)) β (1...πΎ) βΌ (1...π))) |
15 | | nn0re 12478 |
. . . . . . . . . . . . 13
β’ (πΎ β β0
β πΎ β
β) |
16 | | nnre 12216 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
17 | | lenlt 11289 |
. . . . . . . . . . . . 13
β’ ((πΎ β β β§ π β β) β (πΎ β€ π β Β¬ π < πΎ)) |
18 | 15, 16, 17 | syl2an 595 |
. . . . . . . . . . . 12
β’ ((πΎ β β0
β§ π β β)
β (πΎ β€ π β Β¬ π < πΎ)) |
19 | 10, 14, 18 | 3bitr3d 309 |
. . . . . . . . . . 11
β’ ((πΎ β β0
β§ π β β)
β ((1...πΎ) βΌ
(1...π) β Β¬ π < πΎ)) |
20 | 5, 19 | bitrid 283 |
. . . . . . . . . 10
β’ ((πΎ β β0
β§ π β β)
β ({π β£ π:(1...πΎ)β1-1β(1...π)} β β
β Β¬ π < πΎ)) |
21 | 20 | necon4abid 2973 |
. . . . . . . . 9
β’ ((πΎ β β0
β§ π β β)
β ({π β£ π:(1...πΎ)β1-1β(1...π)} = β
β π < πΎ)) |
22 | 21 | biimpar 477 |
. . . . . . . 8
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β {π β£ π:(1...πΎ)β1-1β(1...π)} = β
) |
23 | 1, 22 | eqtrid 2776 |
. . . . . . 7
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β π = β
) |
24 | 23 | fveq2d 6885 |
. . . . . 6
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β (β―βπ) =
(β―ββ
)) |
25 | | hash0 14324 |
. . . . . 6
β’
(β―ββ
) = 0 |
26 | 24, 25 | eqtrdi 2780 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β (β―βπ) = 0) |
27 | 26 | oveq1d 7416 |
. . . 4
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β ((β―βπ) / (β―βπ)) = (0 / (β―βπ))) |
28 | | birthday.s |
. . . . . . . . . 10
β’ π = {π β£ π:(1...πΎ)βΆ(1...π)} |
29 | 28, 1 | birthdaylem1 26799 |
. . . . . . . . 9
β’ (π β π β§ π β Fin β§ (π β β β π β β
)) |
30 | 29 | simp3i 1138 |
. . . . . . . 8
β’ (π β β β π β β
) |
31 | 30 | ad2antlr 724 |
. . . . . . 7
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β π β β
) |
32 | 29 | simp2i 1137 |
. . . . . . . 8
β’ π β Fin |
33 | | hashnncl 14323 |
. . . . . . . 8
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
34 | 32, 33 | ax-mp 5 |
. . . . . . 7
β’
((β―βπ)
β β β π
β β
) |
35 | 31, 34 | sylibr 233 |
. . . . . 6
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β (β―βπ) β
β) |
36 | 35 | nncnd 12225 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β (β―βπ) β
β) |
37 | 35 | nnne0d 12259 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β (β―βπ) β 0) |
38 | 36, 37 | div0d 11986 |
. . . 4
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β (0 /
(β―βπ)) =
0) |
39 | 27, 38 | eqtrd 2764 |
. . 3
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β ((β―βπ) / (β―βπ)) = 0) |
40 | 15 | adantr 480 |
. . . . . . . . . . 11
β’ ((πΎ β β0
β§ π β β)
β πΎ β
β) |
41 | 40 | resqcld 14087 |
. . . . . . . . . 10
β’ ((πΎ β β0
β§ π β β)
β (πΎβ2) β
β) |
42 | 41, 40 | resubcld 11639 |
. . . . . . . . 9
β’ ((πΎ β β0
β§ π β β)
β ((πΎβ2) β
πΎ) β
β) |
43 | 42 | rehalfcld 12456 |
. . . . . . . 8
β’ ((πΎ β β0
β§ π β β)
β (((πΎβ2) β
πΎ) / 2) β
β) |
44 | | nndivre 12250 |
. . . . . . . 8
β’
(((((πΎβ2)
β πΎ) / 2) β
β β§ π β
β) β ((((πΎβ2) β πΎ) / 2) / π) β β) |
45 | 43, 44 | sylancom 587 |
. . . . . . 7
β’ ((πΎ β β0
β§ π β β)
β ((((πΎβ2)
β πΎ) / 2) / π) β
β) |
46 | 45 | renegcld 11638 |
. . . . . 6
β’ ((πΎ β β0
β§ π β β)
β -((((πΎβ2)
β πΎ) / 2) / π) β
β) |
47 | 46 | adantr 480 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β -((((πΎβ2) β πΎ) / 2) / π) β β) |
48 | 47 | rpefcld 16045 |
. . . 4
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β (expβ-((((πΎβ2) β πΎ) / 2) / π)) β
β+) |
49 | 48 | rpge0d 13017 |
. . 3
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β 0 β€
(expβ-((((πΎβ2)
β πΎ) / 2) / π))) |
50 | 39, 49 | eqbrtrd 5160 |
. 2
β’ (((πΎ β β0
β§ π β β)
β§ π < πΎ) β ((β―βπ) / (β―βπ)) β€ (expβ-((((πΎβ2) β πΎ) / 2) / π))) |
51 | | simplr 766 |
. . . 4
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β π β β) |
52 | | simpr 484 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β πΎ β€ π) |
53 | | simpll 764 |
. . . . . . 7
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β πΎ β
β0) |
54 | | nn0uz 12861 |
. . . . . . 7
β’
β0 = (β€β₯β0) |
55 | 53, 54 | eleqtrdi 2835 |
. . . . . 6
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β πΎ β
(β€β₯β0)) |
56 | | nnz 12576 |
. . . . . . 7
β’ (π β β β π β
β€) |
57 | 56 | ad2antlr 724 |
. . . . . 6
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β π β β€) |
58 | | elfz5 13490 |
. . . . . 6
β’ ((πΎ β
(β€β₯β0) β§ π β β€) β (πΎ β (0...π) β πΎ β€ π)) |
59 | 55, 57, 58 | syl2anc 583 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (πΎ β (0...π) β πΎ β€ π)) |
60 | 52, 59 | mpbird 257 |
. . . 4
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β πΎ β (0...π)) |
61 | 28, 1 | birthdaylem2 26800 |
. . . 4
β’ ((π β β β§ πΎ β (0...π)) β ((β―βπ) / (β―βπ)) = (expβΞ£π β (0...(πΎ β 1))(logβ(1 β (π / π))))) |
62 | 51, 60, 61 | syl2anc 583 |
. . 3
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β ((β―βπ) / (β―βπ)) = (expβΞ£π β (0...(πΎ β 1))(logβ(1 β (π / π))))) |
63 | | fzfid 13935 |
. . . . . 6
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (0...(πΎ β 1)) β Fin) |
64 | | elfznn0 13591 |
. . . . . . . . . . . . 13
β’ (π β (0...(πΎ β 1)) β π β β0) |
65 | 64 | adantl 481 |
. . . . . . . . . . . 12
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π β β0) |
66 | 65 | nn0red 12530 |
. . . . . . . . . . 11
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π β β) |
67 | 53 | nn0red 12530 |
. . . . . . . . . . . . 13
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β πΎ β β) |
68 | | peano2rem 11524 |
. . . . . . . . . . . . 13
β’ (πΎ β β β (πΎ β 1) β
β) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (πΎ β 1) β β) |
70 | 69 | adantr 480 |
. . . . . . . . . . 11
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (πΎ β 1) β β) |
71 | 51 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π β β) |
72 | 71 | nnred 12224 |
. . . . . . . . . . 11
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π β β) |
73 | | elfzle2 13502 |
. . . . . . . . . . . 12
β’ (π β (0...(πΎ β 1)) β π β€ (πΎ β 1)) |
74 | 73 | adantl 481 |
. . . . . . . . . . 11
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π β€ (πΎ β 1)) |
75 | 51 | nnred 12224 |
. . . . . . . . . . . . 13
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β π β β) |
76 | 67 | ltm1d 12143 |
. . . . . . . . . . . . 13
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (πΎ β 1) < πΎ) |
77 | 69, 67, 75, 76, 52 | ltletrd 11371 |
. . . . . . . . . . . 12
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (πΎ β 1) < π) |
78 | 77 | adantr 480 |
. . . . . . . . . . 11
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (πΎ β 1) < π) |
79 | 66, 70, 72, 74, 78 | lelttrd 11369 |
. . . . . . . . . 10
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π < π) |
80 | 71 | nncnd 12225 |
. . . . . . . . . . 11
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π β β) |
81 | 80 | mulridd 11228 |
. . . . . . . . . 10
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (π Β· 1) = π) |
82 | 79, 81 | breqtrrd 5166 |
. . . . . . . . 9
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π < (π Β· 1)) |
83 | | 1red 11212 |
. . . . . . . . . 10
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β 1 β
β) |
84 | 71 | nngt0d 12258 |
. . . . . . . . . 10
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β 0 < π) |
85 | | ltdivmul 12086 |
. . . . . . . . . 10
β’ ((π β β β§ 1 β
β β§ (π β
β β§ 0 < π))
β ((π / π) < 1 β π < (π Β· 1))) |
86 | 66, 83, 72, 84, 85 | syl112anc 1371 |
. . . . . . . . 9
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β ((π / π) < 1 β π < (π Β· 1))) |
87 | 82, 86 | mpbird 257 |
. . . . . . . 8
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (π / π) < 1) |
88 | 66, 71 | nndivred 12263 |
. . . . . . . . 9
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (π / π) β β) |
89 | | 1re 11211 |
. . . . . . . . 9
β’ 1 β
β |
90 | | difrp 13009 |
. . . . . . . . 9
β’ (((π / π) β β β§ 1 β β)
β ((π / π) < 1 β (1 β
(π / π)) β
β+)) |
91 | 88, 89, 90 | sylancl 585 |
. . . . . . . 8
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β ((π / π) < 1 β (1 β (π / π)) β
β+)) |
92 | 87, 91 | mpbid 231 |
. . . . . . 7
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (1 β (π / π)) β
β+) |
93 | 92 | relogcld 26473 |
. . . . . 6
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (logβ(1 β
(π / π))) β β) |
94 | 88 | renegcld 11638 |
. . . . . 6
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β -(π / π) β β) |
95 | | elfzle1 13501 |
. . . . . . . . . . . 12
β’ (π β (0...(πΎ β 1)) β 0 β€ π) |
96 | 95 | adantl 481 |
. . . . . . . . . . 11
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β 0 β€ π) |
97 | | divge0 12080 |
. . . . . . . . . . 11
β’ (((π β β β§ 0 β€
π) β§ (π β β β§ 0 < π)) β 0 β€ (π / π)) |
98 | 66, 96, 72, 84, 97 | syl22anc 836 |
. . . . . . . . . 10
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β 0 β€ (π / π)) |
99 | 88, 98, 87 | eflegeo 16061 |
. . . . . . . . 9
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (expβ(π / π)) β€ (1 / (1 β (π / π)))) |
100 | 88 | reefcld 16028 |
. . . . . . . . . 10
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (expβ(π / π)) β β) |
101 | | efgt0 16043 |
. . . . . . . . . . 11
β’ ((π / π) β β β 0 <
(expβ(π / π))) |
102 | 88, 101 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β 0 <
(expβ(π / π))) |
103 | 92 | rpregt0d 13019 |
. . . . . . . . . 10
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β ((1 β (π / π)) β β β§ 0 < (1 β
(π / π)))) |
104 | | lerec2 12099 |
. . . . . . . . . 10
β’
((((expβ(π /
π)) β β β§ 0
< (expβ(π / π))) β§ ((1 β (π / π)) β β β§ 0 < (1 β
(π / π)))) β ((expβ(π / π)) β€ (1 / (1 β (π / π))) β (1 β (π / π)) β€ (1 / (expβ(π / π))))) |
105 | 100, 102,
103, 104 | syl21anc 835 |
. . . . . . . . 9
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β ((expβ(π / π)) β€ (1 / (1 β (π / π))) β (1 β (π / π)) β€ (1 / (expβ(π / π))))) |
106 | 99, 105 | mpbid 231 |
. . . . . . . 8
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (1 β (π / π)) β€ (1 / (expβ(π / π)))) |
107 | 92 | reeflogd 26474 |
. . . . . . . 8
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β
(expβ(logβ(1 β (π / π)))) = (1 β (π / π))) |
108 | 88 | recnd 11239 |
. . . . . . . . 9
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (π / π) β β) |
109 | | efneg 16038 |
. . . . . . . . 9
β’ ((π / π) β β β (expβ-(π / π)) = (1 / (expβ(π / π)))) |
110 | 108, 109 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (expβ-(π / π)) = (1 / (expβ(π / π)))) |
111 | 106, 107,
110 | 3brtr4d 5170 |
. . . . . . 7
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β
(expβ(logβ(1 β (π / π)))) β€ (expβ-(π / π))) |
112 | | efle 16058 |
. . . . . . . 8
β’
(((logβ(1 β (π / π))) β β β§ -(π / π) β β) β ((logβ(1
β (π / π))) β€ -(π / π) β (expβ(logβ(1 β
(π / π)))) β€ (expβ-(π / π)))) |
113 | 93, 94, 112 | syl2anc 583 |
. . . . . . 7
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β ((logβ(1 β
(π / π))) β€ -(π / π) β (expβ(logβ(1 β
(π / π)))) β€ (expβ-(π / π)))) |
114 | 111, 113 | mpbird 257 |
. . . . . 6
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β (logβ(1 β
(π / π))) β€ -(π / π)) |
115 | 63, 93, 94, 114 | fsumle 15742 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β Ξ£π β (0...(πΎ β 1))(logβ(1 β (π / π))) β€ Ξ£π β (0...(πΎ β 1))-(π / π)) |
116 | 63, 108 | fsumneg 15730 |
. . . . . 6
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β Ξ£π β (0...(πΎ β 1))-(π / π) = -Ξ£π β (0...(πΎ β 1))(π / π)) |
117 | 51 | nncnd 12225 |
. . . . . . . . 9
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β π β β) |
118 | 66 | recnd 11239 |
. . . . . . . . 9
β’ ((((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β§ π β (0...(πΎ β 1))) β π β β) |
119 | | nnne0 12243 |
. . . . . . . . . 10
β’ (π β β β π β 0) |
120 | 119 | ad2antlr 724 |
. . . . . . . . 9
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β π β 0) |
121 | 63, 117, 118, 120 | fsumdivc 15729 |
. . . . . . . 8
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (Ξ£π β (0...(πΎ β 1))π / π) = Ξ£π β (0...(πΎ β 1))(π / π)) |
122 | | arisum2 15804 |
. . . . . . . . . 10
β’ (πΎ β β0
β Ξ£π β
(0...(πΎ β 1))π = (((πΎβ2) β πΎ) / 2)) |
123 | 53, 122 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β Ξ£π β (0...(πΎ β 1))π = (((πΎβ2) β πΎ) / 2)) |
124 | 123 | oveq1d 7416 |
. . . . . . . 8
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (Ξ£π β (0...(πΎ β 1))π / π) = ((((πΎβ2) β πΎ) / 2) / π)) |
125 | 121, 124 | eqtr3d 2766 |
. . . . . . 7
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β Ξ£π β (0...(πΎ β 1))(π / π) = ((((πΎβ2) β πΎ) / 2) / π)) |
126 | 125 | negeqd 11451 |
. . . . . 6
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β -Ξ£π β (0...(πΎ β 1))(π / π) = -((((πΎβ2) β πΎ) / 2) / π)) |
127 | 116, 126 | eqtrd 2764 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β Ξ£π β (0...(πΎ β 1))-(π / π) = -((((πΎβ2) β πΎ) / 2) / π)) |
128 | 115, 127 | breqtrd 5164 |
. . . 4
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β Ξ£π β (0...(πΎ β 1))(logβ(1 β (π / π))) β€ -((((πΎβ2) β πΎ) / 2) / π)) |
129 | 63, 93 | fsumrecl 15677 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β Ξ£π β (0...(πΎ β 1))(logβ(1 β (π / π))) β β) |
130 | 46 | adantr 480 |
. . . . 5
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β -((((πΎβ2) β πΎ) / 2) / π) β β) |
131 | | efle 16058 |
. . . . 5
β’
((Ξ£π β
(0...(πΎ β
1))(logβ(1 β (π
/ π))) β β β§
-((((πΎβ2) β
πΎ) / 2) / π) β β) β (Ξ£π β (0...(πΎ β 1))(logβ(1 β (π / π))) β€ -((((πΎβ2) β πΎ) / 2) / π) β (expβΞ£π β (0...(πΎ β 1))(logβ(1 β (π / π)))) β€ (expβ-((((πΎβ2) β πΎ) / 2) / π)))) |
132 | 129, 130,
131 | syl2anc 583 |
. . . 4
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (Ξ£π β (0...(πΎ β 1))(logβ(1 β (π / π))) β€ -((((πΎβ2) β πΎ) / 2) / π) β (expβΞ£π β (0...(πΎ β 1))(logβ(1 β (π / π)))) β€ (expβ-((((πΎβ2) β πΎ) / 2) / π)))) |
133 | 128, 132 | mpbid 231 |
. . 3
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β (expβΞ£π β (0...(πΎ β 1))(logβ(1 β (π / π)))) β€ (expβ-((((πΎβ2) β πΎ) / 2) / π))) |
134 | 62, 133 | eqbrtrd 5160 |
. 2
β’ (((πΎ β β0
β§ π β β)
β§ πΎ β€ π) β ((β―βπ) / (β―βπ)) β€ (expβ-((((πΎβ2) β πΎ) / 2) / π))) |
135 | 16 | adantl 481 |
. 2
β’ ((πΎ β β0
β§ π β β)
β π β
β) |
136 | 50, 134, 135, 40 | ltlecasei 11319 |
1
β’ ((πΎ β β0
β§ π β β)
β ((β―βπ) /
(β―βπ)) β€
(expβ-((((πΎβ2)
β πΎ) / 2) / π))) |