Step | Hyp | Ref
| Expression |
1 | | chtppilim.1 |
. . . . . . 7
β’ (π β π΄ β
β+) |
2 | 1 | rpred 12964 |
. . . . . 6
β’ (π β π΄ β β) |
3 | 2 | recnd 11190 |
. . . . 5
β’ (π β π΄ β β) |
4 | 3 | sqvald 14055 |
. . . 4
β’ (π β (π΄β2) = (π΄ Β· π΄)) |
5 | 4 | oveq1d 7377 |
. . 3
β’ (π β ((π΄β2) Β· ((Οβπ) Β· (logβπ))) = ((π΄ Β· π΄) Β· ((Οβπ) Β· (logβπ)))) |
6 | | chtppilim.3 |
. . . . . . . . 9
β’ (π β π β (2[,)+β)) |
7 | | 2re 12234 |
. . . . . . . . . 10
β’ 2 β
β |
8 | | elicopnf 13369 |
. . . . . . . . . 10
β’ (2 β
β β (π β
(2[,)+β) β (π
β β β§ 2 β€ π))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
β’ (π β (2[,)+β) β
(π β β β§ 2
β€ π)) |
10 | 6, 9 | sylib 217 |
. . . . . . . 8
β’ (π β (π β β β§ 2 β€ π)) |
11 | 10 | simpld 496 |
. . . . . . 7
β’ (π β π β β) |
12 | | ppicl 26496 |
. . . . . . 7
β’ (π β β β
(Οβπ)
β β0) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ (π β (Οβπ) β
β0) |
14 | 13 | nn0red 12481 |
. . . . 5
β’ (π β (Οβπ) β
β) |
15 | 14 | recnd 11190 |
. . . 4
β’ (π β (Οβπ) β
β) |
16 | | 0red 11165 |
. . . . . . . 8
β’ (π β 0 β
β) |
17 | 7 | a1i 11 |
. . . . . . . 8
β’ (π β 2 β
β) |
18 | | 2pos 12263 |
. . . . . . . . 9
β’ 0 <
2 |
19 | 18 | a1i 11 |
. . . . . . . 8
β’ (π β 0 < 2) |
20 | 10 | simprd 497 |
. . . . . . . 8
β’ (π β 2 β€ π) |
21 | 16, 17, 11, 19, 20 | ltletrd 11322 |
. . . . . . 7
β’ (π β 0 < π) |
22 | 11, 21 | elrpd 12961 |
. . . . . 6
β’ (π β π β
β+) |
23 | 22 | relogcld 25994 |
. . . . 5
β’ (π β (logβπ) β
β) |
24 | 23 | recnd 11190 |
. . . 4
β’ (π β (logβπ) β
β) |
25 | 3, 3, 15, 24 | mul4d 11374 |
. . 3
β’ (π β ((π΄ Β· π΄) Β· ((Οβπ) Β· (logβπ))) = ((π΄ Β· (Οβπ)) Β· (π΄ Β· (logβπ)))) |
26 | 5, 25 | eqtrd 2777 |
. 2
β’ (π β ((π΄β2) Β· ((Οβπ) Β· (logβπ))) = ((π΄ Β· (Οβπ)) Β· (π΄ Β· (logβπ)))) |
27 | 2, 14 | remulcld 11192 |
. . . 4
β’ (π β (π΄ Β· (Οβπ)) β
β) |
28 | 2, 23 | remulcld 11192 |
. . . 4
β’ (π β (π΄ Β· (logβπ)) β β) |
29 | 27, 28 | remulcld 11192 |
. . 3
β’ (π β ((π΄ Β· (Οβπ)) Β· (π΄ Β· (logβπ))) β β) |
30 | 22, 2 | rpcxpcld 26103 |
. . . . . . . 8
β’ (π β (πβππ΄) β
β+) |
31 | 30 | rpred 12964 |
. . . . . . 7
β’ (π β (πβππ΄) β β) |
32 | | ppicl 26496 |
. . . . . . 7
β’ ((πβππ΄) β β β
(Οβ(πβππ΄)) β
β0) |
33 | 31, 32 | syl 17 |
. . . . . 6
β’ (π β (Οβ(πβππ΄)) β
β0) |
34 | 33 | nn0red 12481 |
. . . . 5
β’ (π β (Οβ(πβππ΄)) β
β) |
35 | 14, 34 | resubcld 11590 |
. . . 4
β’ (π β ((Οβπ) β
(Οβ(πβππ΄))) β β) |
36 | 35, 28 | remulcld 11192 |
. . 3
β’ (π β (((Οβπ) β
(Οβ(πβππ΄))) Β· (π΄ Β· (logβπ))) β β) |
37 | | chtcl 26474 |
. . . 4
β’ (π β β β
(ΞΈβπ) β
β) |
38 | 11, 37 | syl 17 |
. . 3
β’ (π β (ΞΈβπ) β
β) |
39 | | 1red 11163 |
. . . . . . 7
β’ (π β 1 β
β) |
40 | | 1lt2 12331 |
. . . . . . . 8
β’ 1 <
2 |
41 | 40 | a1i 11 |
. . . . . . 7
β’ (π β 1 < 2) |
42 | 39, 17, 11, 41, 20 | ltletrd 11322 |
. . . . . 6
β’ (π β 1 < π) |
43 | 11, 42 | rplogcld 26000 |
. . . . 5
β’ (π β (logβπ) β
β+) |
44 | 1, 43 | rpmulcld 12980 |
. . . 4
β’ (π β (π΄ Β· (logβπ)) β
β+) |
45 | 14, 31 | resubcld 11590 |
. . . . 5
β’ (π β ((Οβπ) β (πβππ΄)) β β) |
46 | | ppinncl 26539 |
. . . . . . . . . 10
β’ ((π β β β§ 2 β€
π) β
(Οβπ)
β β) |
47 | 10, 46 | syl 17 |
. . . . . . . . 9
β’ (π β (Οβπ) β
β) |
48 | 31, 47 | nndivred 12214 |
. . . . . . . 8
β’ (π β ((πβππ΄) / (Οβπ)) β β) |
49 | | chtppilim.4 |
. . . . . . . 8
β’ (π β ((πβππ΄) / (Οβπ)) < (1 β π΄)) |
50 | 48, 39, 2, 49 | ltsub13d 11768 |
. . . . . . 7
β’ (π β π΄ < (1 β ((πβππ΄) / (Οβπ)))) |
51 | 31 | recnd 11190 |
. . . . . . . . 9
β’ (π β (πβππ΄) β β) |
52 | 47 | nnrpd 12962 |
. . . . . . . . . 10
β’ (π β (Οβπ) β
β+) |
53 | 52 | rpcnne0d 12973 |
. . . . . . . . 9
β’ (π β ((Οβπ) β β β§
(Οβπ) β
0)) |
54 | | divsubdir 11856 |
. . . . . . . . 9
β’
(((Οβπ) β β β§ (πβππ΄) β β β§
((Οβπ)
β β β§ (Οβπ) β 0)) β (((Οβπ) β (πβππ΄)) / (Οβπ)) = (((Οβπ) / (Οβπ)) β ((πβππ΄) / (Οβπ)))) |
55 | 15, 51, 53, 54 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (((Οβπ) β (πβππ΄)) / (Οβπ)) = (((Οβπ) / (Οβπ)) β ((πβππ΄) / (Οβπ)))) |
56 | | divid 11849 |
. . . . . . . . . 10
β’
(((Οβπ) β β β§
(Οβπ) β
0) β ((Οβπ) / (Οβπ)) = 1) |
57 | 53, 56 | syl 17 |
. . . . . . . . 9
β’ (π β ((Οβπ) / (Οβπ)) = 1) |
58 | 57 | oveq1d 7377 |
. . . . . . . 8
β’ (π β (((Οβπ) / (Οβπ)) β ((πβππ΄) / (Οβπ))) = (1 β ((πβππ΄) / (Οβπ)))) |
59 | 55, 58 | eqtrd 2777 |
. . . . . . 7
β’ (π β (((Οβπ) β (πβππ΄)) / (Οβπ)) = (1 β ((πβππ΄) / (Οβπ)))) |
60 | 50, 59 | breqtrrd 5138 |
. . . . . 6
β’ (π β π΄ < (((Οβπ) β (πβππ΄)) / (Οβπ))) |
61 | 2, 45, 52 | ltmuldivd 13011 |
. . . . . 6
β’ (π β ((π΄ Β· (Οβπ)) <
((Οβπ)
β (πβππ΄)) β π΄ < (((Οβπ) β (πβππ΄)) / (Οβπ)))) |
62 | 60, 61 | mpbird 257 |
. . . . 5
β’ (π β (π΄ Β· (Οβπ)) <
((Οβπ)
β (πβππ΄))) |
63 | | ppiltx 26542 |
. . . . . . 7
β’ ((πβππ΄) β β+
β (Οβ(πβππ΄)) < (πβππ΄)) |
64 | 30, 63 | syl 17 |
. . . . . 6
β’ (π β (Οβ(πβππ΄)) < (πβππ΄)) |
65 | 34, 31, 14, 64 | ltsub2dd 11775 |
. . . . 5
β’ (π β ((Οβπ) β (πβππ΄)) < ((Οβπ) β
(Οβ(πβππ΄)))) |
66 | 27, 45, 35, 62, 65 | lttrd 11323 |
. . . 4
β’ (π β (π΄ Β· (Οβπ)) <
((Οβπ)
β (Οβ(πβππ΄)))) |
67 | 27, 35, 44, 66 | ltmul1dd 13019 |
. . 3
β’ (π β ((π΄ Β· (Οβπ)) Β· (π΄ Β· (logβπ))) < (((Οβπ) β
(Οβ(πβππ΄))) Β· (π΄ Β· (logβπ)))) |
68 | | fzfid 13885 |
. . . . . 6
β’ (π β (((ββ(πβππ΄)) + 1)...(ββπ)) β Fin) |
69 | | inss1 4193 |
. . . . . 6
β’
((((ββ(πβππ΄)) + 1)...(ββπ)) β© β) β
(((ββ(πβππ΄)) + 1)...(ββπ)) |
70 | | ssfi 9124 |
. . . . . 6
β’
(((((ββ(πβππ΄)) + 1)...(ββπ)) β Fin β§ ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β) β
(((ββ(πβππ΄)) + 1)...(ββπ))) β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β) β
Fin) |
71 | 68, 69, 70 | sylancl 587 |
. . . . 5
β’ (π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β) β
Fin) |
72 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) |
73 | 72 | elin2d 4164 |
. . . . . . 7
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β π β β) |
74 | | prmnn 16557 |
. . . . . . . 8
β’ (π β β β π β
β) |
75 | 74 | nnrpd 12962 |
. . . . . . 7
β’ (π β β β π β
β+) |
76 | 73, 75 | syl 17 |
. . . . . 6
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β π β β+) |
77 | 76 | relogcld 25994 |
. . . . 5
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β (logβπ) β
β) |
78 | 71, 77 | fsumrecl 15626 |
. . . 4
β’ (π β Ξ£π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(logβπ) β
β) |
79 | 28 | recnd 11190 |
. . . . . . 7
β’ (π β (π΄ Β· (logβπ)) β β) |
80 | | fsumconst 15682 |
. . . . . . 7
β’
((((((ββ(πβππ΄)) + 1)...(ββπ)) β© β) β Fin β§ (π΄ Β· (logβπ)) β β) β
Ξ£π β
((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(π΄ Β· (logβπ)) =
((β―β((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) Β· (π΄ Β· (logβπ)))) |
81 | 71, 79, 80 | syl2anc 585 |
. . . . . 6
β’ (π β Ξ£π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(π΄ Β· (logβπ)) =
((β―β((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) Β· (π΄ Β· (logβπ)))) |
82 | | ppifl 26525 |
. . . . . . . . . 10
β’ (π β β β
(Οβ(ββπ)) = (Οβπ)) |
83 | 11, 82 | syl 17 |
. . . . . . . . 9
β’ (π β
(Οβ(ββπ)) = (Οβπ)) |
84 | | ppifl 26525 |
. . . . . . . . . 10
β’ ((πβππ΄) β β β
(Οβ(ββ(πβππ΄))) = (Οβ(πβππ΄))) |
85 | 31, 84 | syl 17 |
. . . . . . . . 9
β’ (π β
(Οβ(ββ(πβππ΄))) = (Οβ(πβππ΄))) |
86 | 83, 85 | oveq12d 7380 |
. . . . . . . 8
β’ (π β
((Οβ(ββπ)) β
(Οβ(ββ(πβππ΄)))) = ((Οβπ) β (Οβ(πβππ΄)))) |
87 | 39, 11, 42 | ltled 11310 |
. . . . . . . . . . . 12
β’ (π β 1 β€ π) |
88 | | chtppilim.2 |
. . . . . . . . . . . . 13
β’ (π β π΄ < 1) |
89 | | 1re 11162 |
. . . . . . . . . . . . . 14
β’ 1 β
β |
90 | | ltle 11250 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β β§ 1 β
β) β (π΄ < 1
β π΄ β€
1)) |
91 | 2, 89, 90 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (π β (π΄ < 1 β π΄ β€ 1)) |
92 | 88, 91 | mpd 15 |
. . . . . . . . . . . 12
β’ (π β π΄ β€ 1) |
93 | 11, 87, 2, 39, 92 | cxplead 26092 |
. . . . . . . . . . 11
β’ (π β (πβππ΄) β€ (πβπ1)) |
94 | 11 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π β π β β) |
95 | 94 | cxp1d 26077 |
. . . . . . . . . . 11
β’ (π β (πβπ1) = π) |
96 | 93, 95 | breqtrd 5136 |
. . . . . . . . . 10
β’ (π β (πβππ΄) β€ π) |
97 | | flword2 13725 |
. . . . . . . . . 10
β’ (((πβππ΄) β β β§ π β β β§ (πβππ΄) β€ π) β (ββπ) β
(β€β₯β(ββ(πβππ΄)))) |
98 | 31, 11, 96, 97 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (ββπ) β
(β€β₯β(ββ(πβππ΄)))) |
99 | | ppidif 26528 |
. . . . . . . . 9
β’
((ββπ)
β (β€β₯β(ββ(πβππ΄))) β
((Οβ(ββπ)) β
(Οβ(ββ(πβππ΄)))) =
(β―β((((ββ(πβππ΄)) + 1)...(ββπ)) β© β))) |
100 | 98, 99 | syl 17 |
. . . . . . . 8
β’ (π β
((Οβ(ββπ)) β
(Οβ(ββ(πβππ΄)))) =
(β―β((((ββ(πβππ΄)) + 1)...(ββπ)) β© β))) |
101 | 86, 100 | eqtr3d 2779 |
. . . . . . 7
β’ (π β ((Οβπ) β
(Οβ(πβππ΄))) =
(β―β((((ββ(πβππ΄)) + 1)...(ββπ)) β© β))) |
102 | 101 | oveq1d 7377 |
. . . . . 6
β’ (π β (((Οβπ) β
(Οβ(πβππ΄))) Β· (π΄ Β· (logβπ))) =
((β―β((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) Β· (π΄ Β· (logβπ)))) |
103 | 81, 102 | eqtr4d 2780 |
. . . . 5
β’ (π β Ξ£π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(π΄ Β· (logβπ)) = (((Οβπ) β (Οβ(πβππ΄))) Β· (π΄ Β· (logβπ)))) |
104 | 28 | adantr 482 |
. . . . . 6
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β (π΄ Β· (logβπ)) β β) |
105 | 31 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β (πβππ΄) β β) |
106 | | reflcl 13708 |
. . . . . . . . . . 11
β’ ((πβππ΄) β β β
(ββ(πβππ΄)) β β) |
107 | | peano2re 11335 |
. . . . . . . . . . 11
β’
((ββ(πβππ΄)) β β β
((ββ(πβππ΄)) + 1) β β) |
108 | 31, 106, 107 | 3syl 18 |
. . . . . . . . . 10
β’ (π β ((ββ(πβππ΄)) + 1) β
β) |
109 | 108 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β
((ββ(πβππ΄)) + 1) β β) |
110 | 76 | rpred 12964 |
. . . . . . . . 9
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β π β β) |
111 | | fllep1 13713 |
. . . . . . . . . . 11
β’ ((πβππ΄) β β β (πβππ΄) β€ ((ββ(πβππ΄)) + 1)) |
112 | 31, 111 | syl 17 |
. . . . . . . . . 10
β’ (π β (πβππ΄) β€ ((ββ(πβππ΄)) + 1)) |
113 | 112 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β (πβππ΄) β€ ((ββ(πβππ΄)) + 1)) |
114 | 72 | elin1d 4163 |
. . . . . . . . . 10
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β π β (((ββ(πβππ΄)) + 1)...(ββπ))) |
115 | | elfzle1 13451 |
. . . . . . . . . 10
β’ (π β (((ββ(πβππ΄)) + 1)...(ββπ)) β ((ββ(πβππ΄)) + 1) β€ π) |
116 | 114, 115 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β
((ββ(πβππ΄)) + 1) β€ π) |
117 | 105, 109,
110, 113, 116 | letrd 11319 |
. . . . . . . 8
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β (πβππ΄) β€ π) |
118 | 22 | rpne0d 12969 |
. . . . . . . . . . 11
β’ (π β π β 0) |
119 | 94, 118, 3 | cxpefd 26083 |
. . . . . . . . . 10
β’ (π β (πβππ΄) = (expβ(π΄ Β· (logβπ)))) |
120 | 119 | eqcomd 2743 |
. . . . . . . . 9
β’ (π β (expβ(π΄ Β· (logβπ))) = (πβππ΄)) |
121 | 120 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β (expβ(π΄ Β· (logβπ))) = (πβππ΄)) |
122 | 76 | reeflogd 25995 |
. . . . . . . 8
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β
(expβ(logβπ)) =
π) |
123 | 117, 121,
122 | 3brtr4d 5142 |
. . . . . . 7
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β (expβ(π΄ Β· (logβπ))) β€
(expβ(logβπ))) |
124 | | efle 16007 |
. . . . . . . 8
β’ (((π΄ Β· (logβπ)) β β β§
(logβπ) β
β) β ((π΄
Β· (logβπ))
β€ (logβπ) β
(expβ(π΄ Β·
(logβπ))) β€
(expβ(logβπ)))) |
125 | 104, 77, 124 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β ((π΄ Β· (logβπ)) β€ (logβπ) β (expβ(π΄ Β· (logβπ))) β€
(expβ(logβπ)))) |
126 | 123, 125 | mpbird 257 |
. . . . . 6
β’ ((π β§ π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)) β (π΄ Β· (logβπ)) β€ (logβπ)) |
127 | 71, 104, 77, 126 | fsumle 15691 |
. . . . 5
β’ (π β Ξ£π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(π΄ Β· (logβπ)) β€ Ξ£π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(logβπ)) |
128 | 103, 127 | eqbrtrrd 5134 |
. . . 4
β’ (π β (((Οβπ) β
(Οβ(πβππ΄))) Β· (π΄ Β· (logβπ))) β€ Ξ£π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(logβπ)) |
129 | | fzfid 13885 |
. . . . . . 7
β’ (π β (1...(ββπ)) β Fin) |
130 | | inss1 4193 |
. . . . . . 7
β’
((1...(ββπ)) β© β) β
(1...(ββπ)) |
131 | | ssfi 9124 |
. . . . . . 7
β’
(((1...(ββπ)) β Fin β§
((1...(ββπ))
β© β) β (1...(ββπ))) β ((1...(ββπ)) β© β) β
Fin) |
132 | 129, 130,
131 | sylancl 587 |
. . . . . 6
β’ (π β ((1...(ββπ)) β© β) β
Fin) |
133 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((1...(ββπ)) β© β)) β π β
((1...(ββπ))
β© β)) |
134 | 133 | elin2d 4164 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((1...(ββπ)) β© β)) β π β
β) |
135 | | prmuz2 16579 |
. . . . . . . . . . . 12
β’ (π β β β π β
(β€β₯β2)) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β ((1...(ββπ)) β© β)) β π β
(β€β₯β2)) |
137 | | eluz2b2 12853 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β (π β β β§ 1 < π)) |
138 | 136, 137 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β ((1...(ββπ)) β© β)) β (π β β β§ 1 <
π)) |
139 | 138 | simpld 496 |
. . . . . . . . 9
β’ ((π β§ π β ((1...(ββπ)) β© β)) β π β
β) |
140 | 139 | nnred 12175 |
. . . . . . . 8
β’ ((π β§ π β ((1...(ββπ)) β© β)) β π β
β) |
141 | 138 | simprd 497 |
. . . . . . . 8
β’ ((π β§ π β ((1...(ββπ)) β© β)) β 1 <
π) |
142 | 140, 141 | rplogcld 26000 |
. . . . . . 7
β’ ((π β§ π β ((1...(ββπ)) β© β)) β
(logβπ) β
β+) |
143 | 142 | rpred 12964 |
. . . . . 6
β’ ((π β§ π β ((1...(ββπ)) β© β)) β
(logβπ) β
β) |
144 | 142 | rpge0d 12968 |
. . . . . 6
β’ ((π β§ π β ((1...(ββπ)) β© β)) β 0 β€
(logβπ)) |
145 | 30 | rpge0d 12968 |
. . . . . . . . . 10
β’ (π β 0 β€ (πβππ΄)) |
146 | | flge0nn0 13732 |
. . . . . . . . . 10
β’ (((πβππ΄) β β β§ 0 β€
(πβππ΄)) β (ββ(πβππ΄)) β
β0) |
147 | 31, 145, 146 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (ββ(πβππ΄)) β
β0) |
148 | | nn0p1nn 12459 |
. . . . . . . . 9
β’
((ββ(πβππ΄)) β β0 β
((ββ(πβππ΄)) + 1) β β) |
149 | 147, 148 | syl 17 |
. . . . . . . 8
β’ (π β ((ββ(πβππ΄)) + 1) β
β) |
150 | | nnuz 12813 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
151 | 149, 150 | eleqtrdi 2848 |
. . . . . . 7
β’ (π β ((ββ(πβππ΄)) + 1) β
(β€β₯β1)) |
152 | | fzss1 13487 |
. . . . . . 7
β’
(((ββ(πβππ΄)) + 1) β
(β€β₯β1) β (((ββ(πβππ΄)) + 1)...(ββπ)) β (1...(ββπ))) |
153 | | ssrin 4198 |
. . . . . . 7
β’
((((ββ(πβππ΄)) + 1)...(ββπ)) β (1...(ββπ)) β
((((ββ(πβππ΄)) + 1)...(ββπ)) β© β) β
((1...(ββπ))
β© β)) |
154 | 151, 152,
153 | 3syl 18 |
. . . . . 6
β’ (π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β) β
((1...(ββπ))
β© β)) |
155 | 132, 143,
144, 154 | fsumless 15688 |
. . . . 5
β’ (π β Ξ£π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(logβπ) β€ Ξ£π β ((1...(ββπ)) β©
β)(logβπ)) |
156 | | chtval 26475 |
. . . . . . 7
β’ (π β β β
(ΞΈβπ) =
Ξ£π β ((0[,]π) β© β)(logβπ)) |
157 | 11, 156 | syl 17 |
. . . . . 6
β’ (π β (ΞΈβπ) = Ξ£π β ((0[,]π) β© β)(logβπ)) |
158 | | 2eluzge1 12826 |
. . . . . . . 8
β’ 2 β
(β€β₯β1) |
159 | | ppisval2 26470 |
. . . . . . . 8
β’ ((π β β β§ 2 β
(β€β₯β1)) β ((0[,]π) β© β) =
((1...(ββπ))
β© β)) |
160 | 11, 158, 159 | sylancl 587 |
. . . . . . 7
β’ (π β ((0[,]π) β© β) =
((1...(ββπ))
β© β)) |
161 | 160 | sumeq1d 15593 |
. . . . . 6
β’ (π β Ξ£π β ((0[,]π) β© β)(logβπ) = Ξ£π β ((1...(ββπ)) β©
β)(logβπ)) |
162 | 157, 161 | eqtrd 2777 |
. . . . 5
β’ (π β (ΞΈβπ) = Ξ£π β ((1...(ββπ)) β©
β)(logβπ)) |
163 | 155, 162 | breqtrrd 5138 |
. . . 4
β’ (π β Ξ£π β ((((ββ(πβππ΄)) + 1)...(ββπ)) β© β)(logβπ) β€ (ΞΈβπ)) |
164 | 36, 78, 38, 128, 163 | letrd 11319 |
. . 3
β’ (π β (((Οβπ) β
(Οβ(πβππ΄))) Β· (π΄ Β· (logβπ))) β€ (ΞΈβπ)) |
165 | 29, 36, 38, 67, 164 | ltletrd 11322 |
. 2
β’ (π β ((π΄ Β· (Οβπ)) Β· (π΄ Β· (logβπ))) < (ΞΈβπ)) |
166 | 26, 165 | eqbrtrd 5132 |
1
β’ (π β ((π΄β2) Β· ((Οβπ) Β· (logβπ))) < (ΞΈβπ)) |