Step | Hyp | Ref
| Expression |
1 | | chpcl 26489 |
. . . . 5
β’ (π΄ β β β
(Οβπ΄) β
β) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π΄ β β β§ 1 β€
π΄) β
(Οβπ΄) β
β) |
3 | | chtcl 26474 |
. . . . 5
β’ (π΄ β β β
(ΞΈβπ΄) β
β) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π΄ β β β§ 1 β€
π΄) β
(ΞΈβπ΄) β
β) |
5 | 2, 4 | resubcld 11588 |
. . 3
β’ ((π΄ β β β§ 1 β€
π΄) β
((Οβπ΄) β
(ΞΈβπ΄)) β
β) |
6 | | simpl 484 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β π΄ β β) |
7 | | 0red 11163 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β€
π΄) β 0 β
β) |
8 | | 1red 11161 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β€
π΄) β 1 β
β) |
9 | | 0lt1 11682 |
. . . . . . . . . 10
β’ 0 <
1 |
10 | 9 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β€
π΄) β 0 <
1) |
11 | | simpr 486 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β€
π΄) β 1 β€ π΄) |
12 | 7, 8, 6, 10, 11 | ltletrd 11320 |
. . . . . . . 8
β’ ((π΄ β β β§ 1 β€
π΄) β 0 < π΄) |
13 | 6, 12 | elrpd 12959 |
. . . . . . 7
β’ ((π΄ β β β§ 1 β€
π΄) β π΄ β
β+) |
14 | 13 | rpge0d 12966 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β 0 β€ π΄) |
15 | 6, 14 | resqrtcld 15308 |
. . . . 5
β’ ((π΄ β β β§ 1 β€
π΄) β
(ββπ΄) β
β) |
16 | | ppifi 26471 |
. . . . 5
β’
((ββπ΄)
β β β ((0[,](ββπ΄)) β© β) β
Fin) |
17 | 15, 16 | syl 17 |
. . . 4
β’ ((π΄ β β β§ 1 β€
π΄) β
((0[,](ββπ΄))
β© β) β Fin) |
18 | 13 | adantr 482 |
. . . . 5
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β π΄ β
β+) |
19 | 18 | relogcld 25994 |
. . . 4
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(logβπ΄) β
β) |
20 | 17, 19 | fsumrecl 15624 |
. . 3
β’ ((π΄ β β β§ 1 β€
π΄) β Ξ£π β
((0[,](ββπ΄))
β© β)(logβπ΄)
β β) |
21 | 13 | relogcld 25994 |
. . . 4
β’ ((π΄ β β β§ 1 β€
π΄) β (logβπ΄) β
β) |
22 | 15, 21 | remulcld 11190 |
. . 3
β’ ((π΄ β β β§ 1 β€
π΄) β
((ββπ΄) Β·
(logβπ΄)) β
β) |
23 | | ppifi 26471 |
. . . . . . 7
β’ (π΄ β β β
((0[,]π΄) β© β)
β Fin) |
24 | 23 | adantr 482 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β ((0[,]π΄) β© β) β
Fin) |
25 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π β ((0[,]π΄) β© β)) |
26 | 25 | elin2d 4160 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π β β) |
27 | | prmnn 16555 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π β β) |
29 | 28 | nnrpd 12960 |
. . . . . . . . 9
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π β β+) |
30 | 29 | relogcld 25994 |
. . . . . . . 8
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β) |
31 | 21 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β (logβπ΄) β
β) |
32 | 28 | nnred 12173 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π β β) |
33 | | prmuz2 16577 |
. . . . . . . . . . . . 13
β’ (π β β β π β
(β€β₯β2)) |
34 | 26, 33 | syl 17 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π β
(β€β₯β2)) |
35 | | eluz2gt1 12850 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β2) β 1 < π) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β 1 < π) |
37 | 32, 36 | rplogcld 26000 |
. . . . . . . . . 10
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β+) |
38 | 31, 37 | rerpdivcld 12993 |
. . . . . . . . 9
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β ((logβπ΄) / (logβπ)) β
β) |
39 | | reflcl 13707 |
. . . . . . . . 9
β’
(((logβπ΄) /
(logβπ)) β
β β (ββ((logβπ΄) / (logβπ))) β β) |
40 | 38, 39 | syl 17 |
. . . . . . . 8
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β
(ββ((logβπ΄) / (logβπ))) β β) |
41 | 30, 40 | remulcld 11190 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β ((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β β) |
42 | 41 | recnd 11188 |
. . . . . 6
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β ((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β β) |
43 | 30 | recnd 11188 |
. . . . . 6
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β (logβπ) β
β) |
44 | 24, 42, 43 | fsumsub 15678 |
. . . . 5
β’ ((π΄ β β β§ 1 β€
π΄) β Ξ£π β ((0[,]π΄) β© β)(((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ)) = (Ξ£π β ((0[,]π΄) β© β)((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β Ξ£π β ((0[,]π΄) β© β)(logβπ))) |
45 | | 0le0 12259 |
. . . . . . . . 9
β’ 0 β€
0 |
46 | 45 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β β β§ 1 β€
π΄) β 0 β€
0) |
47 | 8, 6, 6, 14, 11 | lemul2ad 12100 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 1 β€
π΄) β (π΄ Β· 1) β€ (π΄ Β· π΄)) |
48 | 6 | recnd 11188 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ 1 β€
π΄) β π΄ β β) |
49 | 48 | sqsqrtd 15330 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 1 β€
π΄) β
((ββπ΄)β2)
= π΄) |
50 | 48 | mulid1d 11177 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 1 β€
π΄) β (π΄ Β· 1) = π΄) |
51 | 49, 50 | eqtr4d 2776 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 1 β€
π΄) β
((ββπ΄)β2)
= (π΄ Β·
1)) |
52 | 48 | sqvald 14054 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 1 β€
π΄) β (π΄β2) = (π΄ Β· π΄)) |
53 | 47, 51, 52 | 3brtr4d 5138 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β€
π΄) β
((ββπ΄)β2)
β€ (π΄β2)) |
54 | 6, 14 | sqrtge0d 15311 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 1 β€
π΄) β 0 β€
(ββπ΄)) |
55 | 15, 6, 54, 14 | le2sqd 14166 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β€
π΄) β
((ββπ΄) β€
π΄ β
((ββπ΄)β2)
β€ (π΄β2))) |
56 | 53, 55 | mpbird 257 |
. . . . . . . 8
β’ ((π΄ β β β§ 1 β€
π΄) β
(ββπ΄) β€
π΄) |
57 | | iccss 13338 |
. . . . . . . 8
β’ (((0
β β β§ π΄
β β) β§ (0 β€ 0 β§ (ββπ΄) β€ π΄)) β (0[,](ββπ΄)) β (0[,]π΄)) |
58 | 7, 6, 46, 56, 57 | syl22anc 838 |
. . . . . . 7
β’ ((π΄ β β β§ 1 β€
π΄) β
(0[,](ββπ΄))
β (0[,]π΄)) |
59 | 58 | ssrind 4196 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β
((0[,](ββπ΄))
β© β) β ((0[,]π΄) β© β)) |
60 | 59 | sselda 3945 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β π β ((0[,]π΄) β© β)) |
61 | 41, 30 | resubcld 11588 |
. . . . . . . 8
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β (((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ)) β β) |
62 | 61 | recnd 11188 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β (((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ)) β β) |
63 | 60, 62 | syldan 592 |
. . . . . 6
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ)) β β) |
64 | | eldifi 4087 |
. . . . . . . . . . . . . . 15
β’ (π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β)) β π
β ((0[,]π΄) β©
β)) |
65 | 64, 43 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (logβπ) β β) |
66 | 65 | mulid2d 11178 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (1 Β· (logβπ)) = (logβπ)) |
67 | 25 | elin1d 4159 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π β (0[,]π΄)) |
68 | | 0re 11162 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
β |
69 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π΄ β β) |
70 | | elicc2 13335 |
. . . . . . . . . . . . . . . . . 18
β’ ((0
β β β§ π΄
β β) β (π
β (0[,]π΄) β
(π β β β§ 0
β€ π β§ π β€ π΄))) |
71 | 68, 69, 70 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β (π β (0[,]π΄) β (π β β β§ 0 β€ π β§ π β€ π΄))) |
72 | 67, 71 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β (π β β β§ 0 β€ π β§ π β€ π΄)) |
73 | 72 | simp3d 1145 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,]π΄) β© β)) β π β€ π΄) |
74 | 64, 73 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π
β€ π΄) |
75 | 64, 29 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π
β β+) |
76 | 13 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π΄
β β+) |
77 | 75, 76 | logled 25998 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (π
β€ π΄ β
(logβπ) β€
(logβπ΄))) |
78 | 74, 77 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (logβπ) β€ (logβπ΄)) |
79 | 66, 78 | eqbrtrd 5128 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (1 Β· (logβπ)) β€ (logβπ΄)) |
80 | | 1red 11161 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β 1 β β) |
81 | 21 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (logβπ΄) β β) |
82 | 64, 37 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (logβπ) β
β+) |
83 | 80, 81, 82 | lemuldivd 13011 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((1 Β· (logβπ)) β€ (logβπ΄) β 1 β€ ((logβπ΄) / (logβπ)))) |
84 | 79, 83 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β 1 β€ ((logβπ΄) / (logβπ))) |
85 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π΄
β β) |
86 | 85 | recnd 11188 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π΄
β β) |
87 | 86 | sqsqrtd 15330 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((ββπ΄)β2) = π΄) |
88 | | eldifn 4088 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β)) β Β¬ π β ((0[,](ββπ΄)) β©
β)) |
89 | 88 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β Β¬ π β ((0[,](ββπ΄)) β©
β)) |
90 | 64, 26 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π
β β) |
91 | | elin 3927 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
((0[,](ββπ΄))
β© β) β (π
β (0[,](ββπ΄)) β§ π β β)) |
92 | 91 | rbaib 540 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β (π β
((0[,](ββπ΄))
β© β) β π
β (0[,](ββπ΄)))) |
93 | 90, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (π
β ((0[,](ββπ΄)) β© β) β π β (0[,](ββπ΄)))) |
94 | | 0red 11163 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β 0 β β) |
95 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (ββπ΄) β β) |
96 | 64, 28 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π
β β) |
97 | 96 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π
β β) |
98 | 75 | rpge0d 12966 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β 0 β€ π) |
99 | | elicc2 13335 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((0
β β β§ (ββπ΄) β β) β (π β (0[,](ββπ΄)) β (π β β β§ 0 β€ π β§ π β€ (ββπ΄)))) |
100 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ 0 β€
π β§ π β€ (ββπ΄)) β ((π β β β§ 0 β€ π) β§ π β€ (ββπ΄))) |
101 | 99, 100 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((0
β β β§ (ββπ΄) β β) β (π β (0[,](ββπ΄)) β ((π β β β§ 0 β€ π) β§ π β€ (ββπ΄)))) |
102 | 101 | baibd 541 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((0
β β β§ (ββπ΄) β β) β§ (π β β β§ 0 β€ π)) β (π β (0[,](ββπ΄)) β π β€ (ββπ΄))) |
103 | 94, 95, 97, 98, 102 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (π
β (0[,](ββπ΄)) β π β€ (ββπ΄))) |
104 | 93, 103 | bitrd 279 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (π
β ((0[,](ββπ΄)) β© β) β π β€ (ββπ΄))) |
105 | 89, 104 | mtbid 324 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β Β¬ π β€ (ββπ΄)) |
106 | 95, 97 | ltnled 11307 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((ββπ΄) < π β Β¬ π β€ (ββπ΄))) |
107 | 105, 106 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (ββπ΄) < π) |
108 | 54 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β 0 β€ (ββπ΄)) |
109 | 95, 97, 108, 98 | lt2sqd 14165 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((ββπ΄) < π β ((ββπ΄)β2) < (πβ2))) |
110 | 107, 109 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((ββπ΄)β2) < (πβ2)) |
111 | 87, 110 | eqbrtrrd 5130 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β π΄
< (πβ2)) |
112 | 96 | nnsqcld 14153 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (πβ2) β β) |
113 | 112 | nnrpd 12960 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (πβ2) β
β+) |
114 | | logltb 25971 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β+
β§ (πβ2) β
β+) β (π΄ < (πβ2) β (logβπ΄) < (logβ(πβ2)))) |
115 | 76, 113, 114 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (π΄
< (πβ2) β
(logβπ΄) <
(logβ(πβ2)))) |
116 | 111, 115 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (logβπ΄) < (logβ(πβ2))) |
117 | | 2z 12540 |
. . . . . . . . . . . . . . 15
β’ 2 β
β€ |
118 | | relogexp 25967 |
. . . . . . . . . . . . . . 15
β’ ((π β β+
β§ 2 β β€) β (logβ(πβ2)) = (2 Β· (logβπ))) |
119 | 75, 117, 118 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (logβ(πβ2)) = (2 Β· (logβπ))) |
120 | 116, 119 | breqtrd 5132 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (logβπ΄) < (2 Β· (logβπ))) |
121 | | 2re 12232 |
. . . . . . . . . . . . . . 15
β’ 2 β
β |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β 2 β β) |
123 | 81, 122, 82 | ltdivmul2d 13014 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (((logβπ΄) / (logβπ)) < 2 β (logβπ΄) < (2 Β· (logβπ)))) |
124 | 120, 123 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((logβπ΄) / (logβπ)) < 2) |
125 | | df-2 12221 |
. . . . . . . . . . . 12
β’ 2 = (1 +
1) |
126 | 124, 125 | breqtrdi 5147 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((logβπ΄) / (logβπ)) < (1 + 1)) |
127 | 64, 38 | sylan2 594 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((logβπ΄) / (logβπ)) β β) |
128 | | 1z 12538 |
. . . . . . . . . . . 12
β’ 1 β
β€ |
129 | | flbi 13727 |
. . . . . . . . . . . 12
β’
((((logβπ΄) /
(logβπ)) β
β β§ 1 β β€) β ((ββ((logβπ΄) / (logβπ))) = 1 β (1 β€
((logβπ΄) /
(logβπ)) β§
((logβπ΄) /
(logβπ)) < (1 +
1)))) |
130 | 127, 128,
129 | sylancl 587 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((ββ((logβπ΄) / (logβπ))) = 1 β (1 β€ ((logβπ΄) / (logβπ)) β§ ((logβπ΄) / (logβπ)) < (1 +
1)))) |
131 | 84, 126, 130 | mpbir2and 712 |
. . . . . . . . . 10
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (ββ((logβπ΄) / (logβπ))) = 1) |
132 | 131 | oveq2d 7374 |
. . . . . . . . 9
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((logβπ) Β· (ββ((logβπ΄) / (logβπ)))) = ((logβπ) Β· 1)) |
133 | 65 | mulid1d 11177 |
. . . . . . . . 9
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((logβπ) Β· 1) = (logβπ)) |
134 | 132, 133 | eqtrd 2773 |
. . . . . . . 8
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((logβπ) Β· (ββ((logβπ΄) / (logβπ)))) = (logβπ)) |
135 | 134 | oveq1d 7373 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (((logβπ) Β· (ββ((logβπ΄) / (logβπ)))) β (logβπ)) = ((logβπ) β (logβπ))) |
136 | 65 | subidd 11505 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β ((logβπ) β (logβπ)) = 0) |
137 | 135, 136 | eqtrd 2773 |
. . . . . 6
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β (((0[,]π΄) β© β) β
((0[,](ββπ΄))
β© β))) β (((logβπ) Β· (ββ((logβπ΄) / (logβπ)))) β (logβπ)) = 0) |
138 | 59, 63, 137, 24 | fsumss 15615 |
. . . . 5
β’ ((π΄ β β β§ 1 β€
π΄) β Ξ£π β
((0[,](ββπ΄))
β© β)(((logβπ) Β· (ββ((logβπ΄) / (logβπ)))) β (logβπ)) = Ξ£π β ((0[,]π΄) β© β)(((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ))) |
139 | | chpval2 26582 |
. . . . . . 7
β’ (π΄ β β β
(Οβπ΄) =
Ξ£π β ((0[,]π΄) β©
β)((logβπ)
Β· (ββ((logβπ΄) / (logβπ))))) |
140 | 139 | adantr 482 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β
(Οβπ΄) =
Ξ£π β ((0[,]π΄) β©
β)((logβπ)
Β· (ββ((logβπ΄) / (logβπ))))) |
141 | | chtval 26475 |
. . . . . . 7
β’ (π΄ β β β
(ΞΈβπ΄) =
Ξ£π β ((0[,]π΄) β© β)(logβπ)) |
142 | 141 | adantr 482 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β
(ΞΈβπ΄) =
Ξ£π β ((0[,]π΄) β© β)(logβπ)) |
143 | 140, 142 | oveq12d 7376 |
. . . . 5
β’ ((π΄ β β β§ 1 β€
π΄) β
((Οβπ΄) β
(ΞΈβπ΄)) =
(Ξ£π β
((0[,]π΄) β©
β)((logβπ)
Β· (ββ((logβπ΄) / (logβπ)))) β Ξ£π β ((0[,]π΄) β© β)(logβπ))) |
144 | 44, 138, 143 | 3eqtr4rd 2784 |
. . . 4
β’ ((π΄ β β β§ 1 β€
π΄) β
((Οβπ΄) β
(ΞΈβπ΄)) =
Ξ£π β
((0[,](ββπ΄))
β© β)(((logβπ) Β· (ββ((logβπ΄) / (logβπ)))) β (logβπ))) |
145 | 60, 61 | syldan 592 |
. . . . 5
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ)) β β) |
146 | 60, 41 | syldan 592 |
. . . . . 6
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β β) |
147 | 60, 37 | syldan 592 |
. . . . . . . 8
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(logβπ) β
β+) |
148 | 147 | rpge0d 12966 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β 0 β€
(logβπ)) |
149 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β π β
((0[,](ββπ΄))
β© β)) |
150 | 149 | elin2d 4160 |
. . . . . . . . . . 11
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β π β
β) |
151 | 150, 27 | syl 17 |
. . . . . . . . . 10
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β π β
β) |
152 | 151 | nnrpd 12960 |
. . . . . . . . 9
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β π β
β+) |
153 | 152 | relogcld 25994 |
. . . . . . . 8
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(logβπ) β
β) |
154 | 146, 153 | subge02d 11752 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β (0
β€ (logβπ) β
(((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ)) β€ ((logβπ) Β· (ββ((logβπ΄) / (logβπ)))))) |
155 | 148, 154 | mpbid 231 |
. . . . . 6
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ)) β€ ((logβπ) Β· (ββ((logβπ΄) / (logβπ))))) |
156 | 60, 38 | syldan 592 |
. . . . . . . 8
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
((logβπ΄) /
(logβπ)) β
β) |
157 | | flle 13710 |
. . . . . . . 8
β’
(((logβπ΄) /
(logβπ)) β
β β (ββ((logβπ΄) / (logβπ))) β€ ((logβπ΄) / (logβπ))) |
158 | 156, 157 | syl 17 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(ββ((logβπ΄) / (logβπ))) β€ ((logβπ΄) / (logβπ))) |
159 | 60, 40 | syldan 592 |
. . . . . . . 8
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(ββ((logβπ΄) / (logβπ))) β β) |
160 | 159, 19, 147 | lemuldiv2d 13012 |
. . . . . . 7
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β€ (logβπ΄) β (ββ((logβπ΄) / (logβπ))) β€ ((logβπ΄) / (logβπ)))) |
161 | 158, 160 | mpbird 257 |
. . . . . 6
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β€ (logβπ΄)) |
162 | 145, 146,
19, 155, 161 | letrd 11317 |
. . . . 5
β’ (((π΄ β β β§ 1 β€
π΄) β§ π β ((0[,](ββπ΄)) β© β)) β
(((logβπ) Β·
(ββ((logβπ΄) / (logβπ)))) β (logβπ)) β€ (logβπ΄)) |
163 | 17, 145, 19, 162 | fsumle 15689 |
. . . 4
β’ ((π΄ β β β§ 1 β€
π΄) β Ξ£π β
((0[,](ββπ΄))
β© β)(((logβπ) Β· (ββ((logβπ΄) / (logβπ)))) β (logβπ)) β€ Ξ£π β
((0[,](ββπ΄))
β© β)(logβπ΄)) |
164 | 144, 163 | eqbrtrd 5128 |
. . 3
β’ ((π΄ β β β§ 1 β€
π΄) β
((Οβπ΄) β
(ΞΈβπ΄)) β€
Ξ£π β
((0[,](ββπ΄))
β© β)(logβπ΄)) |
165 | 21 | recnd 11188 |
. . . . 5
β’ ((π΄ β β β§ 1 β€
π΄) β (logβπ΄) β
β) |
166 | | fsumconst 15680 |
. . . . 5
β’
((((0[,](ββπ΄)) β© β) β Fin β§
(logβπ΄) β
β) β Ξ£π
β ((0[,](ββπ΄)) β© β)(logβπ΄) =
((β―β((0[,](ββπ΄)) β© β)) Β· (logβπ΄))) |
167 | 17, 165, 166 | syl2anc 585 |
. . . 4
β’ ((π΄ β β β§ 1 β€
π΄) β Ξ£π β
((0[,](ββπ΄))
β© β)(logβπ΄)
= ((β―β((0[,](ββπ΄)) β© β)) Β· (logβπ΄))) |
168 | | hashcl 14262 |
. . . . . . 7
β’
(((0[,](ββπ΄)) β© β) β Fin β
(β―β((0[,](ββπ΄)) β© β)) β
β0) |
169 | 17, 168 | syl 17 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β
(β―β((0[,](ββπ΄)) β© β)) β
β0) |
170 | 169 | nn0red 12479 |
. . . . 5
β’ ((π΄ β β β§ 1 β€
π΄) β
(β―β((0[,](ββπ΄)) β© β)) β
β) |
171 | | logge0 25976 |
. . . . 5
β’ ((π΄ β β β§ 1 β€
π΄) β 0 β€
(logβπ΄)) |
172 | | reflcl 13707 |
. . . . . . 7
β’
((ββπ΄)
β β β (ββ(ββπ΄)) β β) |
173 | 15, 172 | syl 17 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β
(ββ(ββπ΄)) β β) |
174 | | fzfid 13884 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β€
π΄) β
(1...(ββ(ββπ΄))) β Fin) |
175 | | ppisval 26469 |
. . . . . . . . . . 11
β’
((ββπ΄)
β β β ((0[,](ββπ΄)) β© β) =
((2...(ββ(ββπ΄))) β© β)) |
176 | 15, 175 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 1 β€
π΄) β
((0[,](ββπ΄))
β© β) = ((2...(ββ(ββπ΄))) β© β)) |
177 | | inss1 4189 |
. . . . . . . . . . 11
β’
((2...(ββ(ββπ΄))) β© β) β
(2...(ββ(ββπ΄))) |
178 | | 2eluzge1 12824 |
. . . . . . . . . . . 12
β’ 2 β
(β€β₯β1) |
179 | | fzss1 13486 |
. . . . . . . . . . . 12
β’ (2 β
(β€β₯β1) β
(2...(ββ(ββπ΄))) β
(1...(ββ(ββπ΄)))) |
180 | 178, 179 | mp1i 13 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ 1 β€
π΄) β
(2...(ββ(ββπ΄))) β
(1...(ββ(ββπ΄)))) |
181 | 177, 180 | sstrid 3956 |
. . . . . . . . . 10
β’ ((π΄ β β β§ 1 β€
π΄) β
((2...(ββ(ββπ΄))) β© β) β
(1...(ββ(ββπ΄)))) |
182 | 176, 181 | eqsstrd 3983 |
. . . . . . . . 9
β’ ((π΄ β β β§ 1 β€
π΄) β
((0[,](ββπ΄))
β© β) β (1...(ββ(ββπ΄)))) |
183 | | ssdomg 8943 |
. . . . . . . . 9
β’
((1...(ββ(ββπ΄))) β Fin β
(((0[,](ββπ΄))
β© β) β (1...(ββ(ββπ΄))) β ((0[,](ββπ΄)) β© β) βΌ
(1...(ββ(ββπ΄))))) |
184 | 174, 182,
183 | sylc 65 |
. . . . . . . 8
β’ ((π΄ β β β§ 1 β€
π΄) β
((0[,](ββπ΄))
β© β) βΌ (1...(ββ(ββπ΄)))) |
185 | | hashdom 14285 |
. . . . . . . . 9
β’
((((0[,](ββπ΄)) β© β) β Fin β§
(1...(ββ(ββπ΄))) β Fin) β
((β―β((0[,](ββπ΄)) β© β)) β€
(β―β(1...(ββ(ββπ΄)))) β ((0[,](ββπ΄)) β© β) βΌ
(1...(ββ(ββπ΄))))) |
186 | 17, 174, 185 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β β β§ 1 β€
π΄) β
((β―β((0[,](ββπ΄)) β© β)) β€
(β―β(1...(ββ(ββπ΄)))) β ((0[,](ββπ΄)) β© β) βΌ
(1...(ββ(ββπ΄))))) |
187 | 184, 186 | mpbird 257 |
. . . . . . 7
β’ ((π΄ β β β§ 1 β€
π΄) β
(β―β((0[,](ββπ΄)) β© β)) β€
(β―β(1...(ββ(ββπ΄))))) |
188 | | flge0nn0 13731 |
. . . . . . . . 9
β’
(((ββπ΄)
β β β§ 0 β€ (ββπ΄)) β
(ββ(ββπ΄)) β
β0) |
189 | 15, 54, 188 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β β β§ 1 β€
π΄) β
(ββ(ββπ΄)) β
β0) |
190 | | hashfz1 14252 |
. . . . . . . 8
β’
((ββ(ββπ΄)) β β0 β
(β―β(1...(ββ(ββπ΄)))) = (ββ(ββπ΄))) |
191 | 189, 190 | syl 17 |
. . . . . . 7
β’ ((π΄ β β β§ 1 β€
π΄) β
(β―β(1...(ββ(ββπ΄)))) = (ββ(ββπ΄))) |
192 | 187, 191 | breqtrd 5132 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β
(β―β((0[,](ββπ΄)) β© β)) β€
(ββ(ββπ΄))) |
193 | | flle 13710 |
. . . . . . 7
β’
((ββπ΄)
β β β (ββ(ββπ΄)) β€ (ββπ΄)) |
194 | 15, 193 | syl 17 |
. . . . . 6
β’ ((π΄ β β β§ 1 β€
π΄) β
(ββ(ββπ΄)) β€ (ββπ΄)) |
195 | 170, 173,
15, 192, 194 | letrd 11317 |
. . . . 5
β’ ((π΄ β β β§ 1 β€
π΄) β
(β―β((0[,](ββπ΄)) β© β)) β€ (ββπ΄)) |
196 | 170, 15, 21, 171, 195 | lemul1ad 12099 |
. . . 4
β’ ((π΄ β β β§ 1 β€
π΄) β
((β―β((0[,](ββπ΄)) β© β)) Β· (logβπ΄)) β€ ((ββπ΄) Β· (logβπ΄))) |
197 | 167, 196 | eqbrtrd 5128 |
. . 3
β’ ((π΄ β β β§ 1 β€
π΄) β Ξ£π β
((0[,](ββπ΄))
β© β)(logβπ΄)
β€ ((ββπ΄)
Β· (logβπ΄))) |
198 | 5, 20, 22, 164, 197 | letrd 11317 |
. 2
β’ ((π΄ β β β§ 1 β€
π΄) β
((Οβπ΄) β
(ΞΈβπ΄)) β€
((ββπ΄) Β·
(logβπ΄))) |
199 | 2, 4, 22 | lesubadd2d 11759 |
. 2
β’ ((π΄ β β β§ 1 β€
π΄) β
(((Οβπ΄) β
(ΞΈβπ΄)) β€
((ββπ΄) Β·
(logβπ΄)) β
(Οβπ΄) β€
((ΞΈβπ΄) +
((ββπ΄) Β·
(logβπ΄))))) |
200 | 198, 199 | mpbid 231 |
1
β’ ((π΄ β β β§ 1 β€
π΄) β
(Οβπ΄) β€
((ΞΈβπ΄) +
((ββπ΄) Β·
(logβπ΄)))) |