Step | Hyp | Ref
| Expression |
1 | | elioore 13300 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (1(,)+β) β
π₯ β
β) |
2 | 1 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β) |
3 | | 1rp 12924 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
β+ |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β+) |
5 | | 1red 11161 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β) |
6 | | eliooord 13329 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (1(,)+β) β (1
< π₯ β§ π₯ <
+β)) |
7 | 6 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β€ β§ π₯
β (1(,)+β)) β (1 < π₯ β§ π₯ < +β)) |
8 | 7 | simpld 496 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€ β§ π₯
β (1(,)+β)) β 1 < π₯) |
9 | 5, 2, 8 | ltled 11308 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β€ π₯) |
10 | 2, 4, 9 | rpgecld 13001 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β+) |
11 | 10 | rprege0d 12969 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ β β β§ 0 β€ π₯)) |
12 | | flge0nn0 13731 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββπ₯) β
β0) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€ β§ π₯
β (1(,)+β)) β (ββπ₯) β
β0) |
14 | | nn0p1nn 12457 |
. . . . . . . . . . . . . . . . . . . 20
β’
((ββπ₯)
β β0 β ((ββπ₯) + 1) β β) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β ((ββπ₯) + 1) β β) |
16 | 15 | nnrpd 12960 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β ((ββπ₯) + 1) β
β+) |
17 | 10, 16 | rpdivcld 12979 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ / ((ββπ₯) + 1)) β
β+) |
18 | | pntrlog2bnd.r |
. . . . . . . . . . . . . . . . . 18
β’ π
= (π β β+ β¦
((Οβπ) β
π)) |
19 | 18 | pntrval 26926 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ / ((ββπ₯) + 1)) β
β+ β (π
β(π₯ / ((ββπ₯) + 1))) = ((Οβ(π₯ / ((ββπ₯) + 1))) β (π₯ / ((ββπ₯) + 1)))) |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (π
β(π₯ / ((ββπ₯) + 1))) = ((Οβ(π₯ / ((ββπ₯) + 1))) β (π₯ / ((ββπ₯) + 1)))) |
21 | 2, 15 | nndivred 12212 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ / ((ββπ₯) + 1)) β β) |
22 | | 2re 12232 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β 2 β β) |
24 | | flltp1 13711 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β β β π₯ < ((ββπ₯) + 1)) |
25 | 2, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ < ((ββπ₯) + 1)) |
26 | 15 | nncnd 12174 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β€ β§ π₯
β (1(,)+β)) β ((ββπ₯) + 1) β β) |
27 | 26 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β€ β§ π₯
β (1(,)+β)) β (((ββπ₯) + 1) Β· 1) = ((ββπ₯) + 1)) |
28 | 25, 27 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ < (((ββπ₯) + 1) Β· 1)) |
29 | 2, 5, 16 | ltdivmuld 13013 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β€ β§ π₯
β (1(,)+β)) β ((π₯ / ((ββπ₯) + 1)) < 1 β π₯ < (((ββπ₯) + 1) Β· 1))) |
30 | 28, 29 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ / ((ββπ₯) + 1)) < 1) |
31 | | 1lt2 12329 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 <
2 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β 1 < 2) |
33 | 21, 5, 23, 30, 32 | lttrd 11321 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ / ((ββπ₯) + 1)) < 2) |
34 | | chpeq0 26572 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ / ((ββπ₯) + 1)) β β β
((Οβ(π₯ /
((ββπ₯) + 1))) =
0 β (π₯ /
((ββπ₯) + 1))
< 2)) |
35 | 21, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β ((Οβ(π₯ / ((ββπ₯) + 1))) = 0 β (π₯ / ((ββπ₯) + 1)) < 2)) |
36 | 33, 35 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (Οβ(π₯ / ((ββπ₯) + 1))) = 0) |
37 | 36 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β ((Οβ(π₯ / ((ββπ₯) + 1))) β (π₯ / ((ββπ₯) + 1))) = (0 β (π₯ / ((ββπ₯) + 1)))) |
38 | 20, 37 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (π
β(π₯ / ((ββπ₯) + 1))) = (0 β (π₯ / ((ββπ₯) + 1)))) |
39 | 38 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(π
β(π₯ / ((ββπ₯) + 1)))) = (absβ(0 β (π₯ / ((ββπ₯) + 1))))) |
40 | | 0red 11163 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β β) |
41 | 17 | rpge0d 12966 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ (π₯ / ((ββπ₯) + 1))) |
42 | 40, 21, 41 | abssuble0d 15323 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(0 β (π₯ / ((ββπ₯) + 1)))) = ((π₯ / ((ββπ₯) + 1)) β 0)) |
43 | 21 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ / ((ββπ₯) + 1)) β β) |
44 | 43 | subid1d 11506 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β ((π₯ / ((ββπ₯) + 1)) β 0) = (π₯ / ((ββπ₯) + 1))) |
45 | 39, 42, 44 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(π
β(π₯ / ((ββπ₯) + 1)))) = (π₯ / ((ββπ₯) + 1))) |
46 | 13 | nn0red 12479 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (ββπ₯) β β) |
47 | | pntsval.1 |
. . . . . . . . . . . . . . . . 17
β’ π = (π β β β¦ Ξ£π β
(1...(ββπ))((Ξβπ) Β· ((logβπ) + (Οβ(π / π))))) |
48 | 47 | pntsval2 26940 |
. . . . . . . . . . . . . . . 16
β’
((ββπ₯)
β β β (πβ(ββπ₯)) = Ξ£π β
(1...(ββ(ββπ₯)))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (πβ(ββπ₯)) = Ξ£π β
(1...(ββ(ββπ₯)))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
50 | 13 | nn0cnd 12480 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (ββπ₯) β β) |
51 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β β) |
52 | 50, 51 | pncand 11518 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (((ββπ₯) + 1) β 1) = (ββπ₯)) |
53 | 52 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (πβ(((ββπ₯) + 1) β 1)) = (πβ(ββπ₯))) |
54 | 47 | pntsval2 26940 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β (πβπ₯) = Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
55 | 2, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (πβπ₯) = Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
56 | | flidm 13720 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β
(ββ(ββπ₯)) = (ββπ₯)) |
57 | 2, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β (ββ(ββπ₯)) = (ββπ₯)) |
58 | 57 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (1...(ββ(ββπ₯))) = (1...(ββπ₯))) |
59 | 58 | sumeq1d 15591 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β
(1...(ββ(ββπ₯)))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π)))) = Ξ£π β (1...(ββπ₯))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
60 | 55, 59 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (πβπ₯) = Ξ£π β
(1...(ββ(ββπ₯)))(((Ξβπ) Β· (logβπ)) + Ξ£π β {π¦ β β β£ π¦ β₯ π} ((Ξβπ) Β· (Ξβ(π / π))))) |
61 | 49, 53, 60 | 3eqtr4d 2783 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (πβ(((ββπ₯) + 1) β 1)) = (πβπ₯)) |
62 | 52 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (πβ(((ββπ₯) + 1) β 1)) = (πβ(ββπ₯))) |
63 | 62 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· (πβ(((ββπ₯) + 1) β 1))) = (2 Β· (πβ(ββπ₯)))) |
64 | 61, 63 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β 1)))) = ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) |
65 | 45, 64 | oveq12d 7376 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ(π
β(π₯ / ((ββπ₯) + 1)))) Β· ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β 1))))) = ((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯)))))) |
66 | 2 | recnd 11188 |
. . . . . . . . . . . . . . . . . . 19
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β β) |
67 | 66 | div1d 11928 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ / 1) = π₯) |
68 | 67 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (π
β(π₯ / 1)) = (π
βπ₯)) |
69 | 18 | pntrf 26927 |
. . . . . . . . . . . . . . . . . . 19
β’ π
:β+βΆβ |
70 | 69 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β+
β (π
βπ₯) β
β) |
71 | 10, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (π
βπ₯) β β) |
72 | 68, 71 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (π
β(π₯ / 1)) β β) |
73 | 72 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (π
β(π₯ / 1)) β β) |
74 | 73 | abscld 15327 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(π
β(π₯ / 1))) β β) |
75 | 74 | recnd 11188 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(π
β(π₯ / 1))) β β) |
76 | 75 | mul01d 11359 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ(π
β(π₯ / 1))) Β· 0) = 0) |
77 | 65, 76 | oveq12d 7376 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
β(π₯ / ((ββπ₯) + 1)))) Β· ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β 1))))) β
((absβ(π
β(π₯ / 1))) Β· 0)) = (((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) β 0)) |
78 | 47 | pntsf 26937 |
. . . . . . . . . . . . . . . . 17
β’ π:ββΆβ |
79 | 78 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β (πβπ₯) β β) |
80 | 2, 79 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (πβπ₯) β β) |
81 | | pntrlog2bnd.t |
. . . . . . . . . . . . . . . . . . 19
β’ π = (π β β β¦ if(π β β+, (π Β· (logβπ)), 0)) |
82 | | relogcl 25947 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β+
β (logβπ) β
β) |
83 | | remulcl 11141 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§
(logβπ) β
β) β (π Β·
(logβπ)) β
β) |
84 | 82, 83 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β+)
β (π Β·
(logβπ)) β
β) |
85 | | 0red 11163 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ Β¬
π β
β+) β 0 β β) |
86 | 84, 85 | ifclda 4522 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β if(π β β+,
(π Β·
(logβπ)), 0) β
β) |
87 | 81, 86 | fmpti 7061 |
. . . . . . . . . . . . . . . . . 18
β’ π:ββΆβ |
88 | 87 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . 17
β’
((ββπ₯)
β β β (πβ(ββπ₯)) β β) |
89 | 46, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (πβ(ββπ₯)) β β) |
90 | 23, 89 | remulcld 11190 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· (πβ(ββπ₯))) β β) |
91 | 80, 90 | resubcld 11588 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β ((πβπ₯) β (2 Β· (πβ(ββπ₯)))) β β) |
92 | 21, 91 | remulcld 11190 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β ((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) β β) |
93 | 92 | recnd 11188 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β ((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) β β) |
94 | 93 | subid1d 11506 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) β 0) = ((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯)))))) |
95 | 77, 94 | eqtrd 2773 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
β(π₯ / ((ββπ₯) + 1)))) Β· ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β 1))))) β
((absβ(π
β(π₯ / 1))) Β· 0)) = ((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯)))))) |
96 | 2 | flcld 13709 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (ββπ₯) β β€) |
97 | | fzval3 13647 |
. . . . . . . . . . . . . 14
β’
((ββπ₯)
β β€ β (1...(ββπ₯)) = (1..^((ββπ₯) + 1))) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β (1...(ββπ₯)) = (1..^((ββπ₯) + 1))) |
99 | 98 | eqcomd 2739 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β (1..^((ββπ₯) + 1)) = (1...(ββπ₯))) |
100 | 10 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π₯ β β+) |
101 | | elfznn 13476 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(1...(ββπ₯))
β π β
β) |
102 | 101 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
103 | 102 | nnrpd 12960 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β+) |
104 | 100, 103 | rpdivcld 12979 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π₯ / π) β
β+) |
105 | 69 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ / π) β β+ β (π
β(π₯ / π)) β β) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π
β(π₯ / π)) β β) |
107 | 106 | recnd 11188 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π
β(π₯ / π)) β β) |
108 | 107 | abscld 15327 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (absβ(π
β(π₯ / π))) β β) |
109 | 108 | recnd 11188 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (absβ(π
β(π₯ / π))) β β) |
110 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 1 β
β+) |
111 | 103, 110 | rpaddcld 12977 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π + 1) β
β+) |
112 | 100, 111 | rpdivcld 12979 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π₯ / (π + 1)) β
β+) |
113 | 69 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ / (π + 1)) β β+ β
(π
β(π₯ / (π + 1))) β β) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π
β(π₯ / (π + 1))) β β) |
115 | 114 | recnd 11188 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π
β(π₯ / (π + 1))) β β) |
116 | 115 | abscld 15327 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (absβ(π
β(π₯ / (π + 1)))) β β) |
117 | 116 | recnd 11188 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (absβ(π
β(π₯ / (π + 1)))) β β) |
118 | 109, 117 | negsubdi2d 11533 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β -((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) = ((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π))))) |
119 | 118 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π)))) = -((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1)))))) |
120 | 102 | nncnd 12174 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
121 | | 1cnd 11155 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 1 β
β) |
122 | 120, 121 | pncand 11518 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((π + 1) β 1) = π) |
123 | 122 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ((π + 1) β 1)) = (πβπ)) |
124 | 122 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ((π + 1) β 1)) = (πβπ)) |
125 | | rpre 12928 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β+
β π β
β) |
126 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (π β β+ β π β
β+)) |
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β π = π) |
128 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (logβπ) = (logβπ)) |
129 | 127, 128 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (π Β· (logβπ)) = (π Β· (logβπ))) |
130 | 126, 129 | ifbieq1d 4511 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β if(π β β+, (π Β· (logβπ)), 0) = if(π β β+, (π Β· (logβπ)), 0)) |
131 | | ovex 7391 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π Β· (logβπ)) β V |
132 | | c0ex 11154 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
V |
133 | 131, 132 | ifex 4537 |
. . . . . . . . . . . . . . . . . . . . 21
β’ if(π β β+,
(π Β·
(logβπ)), 0) β
V |
134 | 130, 81, 133 | fvmpt 6949 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (πβπ) = if(π β β+, (π Β· (logβπ)), 0)) |
135 | 125, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β (πβπ) = if(π β β+, (π Β· (logβπ)), 0)) |
136 | | iftrue 4493 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β if(π β
β+, (π
Β· (logβπ)), 0)
= (π Β·
(logβπ))) |
137 | 135, 136 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β+
β (πβπ) = (π Β· (logβπ))) |
138 | 103, 137 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) = (π Β· (logβπ))) |
139 | 124, 138 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ((π + 1) β 1)) = (π Β· (logβπ))) |
140 | 139 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· (πβ((π + 1) β 1))) = (2 Β· (π Β· (logβπ)))) |
141 | 123, 140 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))) = ((πβπ) β (2 Β· (π Β· (logβπ))))) |
142 | 119, 141 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π)))) Β· ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1))))) = (-((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) |
143 | 108, 116 | resubcld 11588 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) β β) |
144 | 143 | recnd 11188 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) β β) |
145 | 102 | nnred 12173 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β π β β) |
146 | 78 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (πβπ) β β) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) β β) |
148 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 2 β
β) |
149 | 103 | relogcld 25994 |
. . . . . . . . . . . . . . . . . 18
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (logβπ) β
β) |
150 | 145, 149 | remulcld 11190 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π Β· (logβπ)) β β) |
151 | 148, 150 | remulcld 11190 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· (π Β· (logβπ))) β
β) |
152 | 147, 151 | resubcld 11588 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (2 Β· (π Β· (logβπ)))) β β) |
153 | 152 | recnd 11188 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (2 Β· (π Β· (logβπ)))) β β) |
154 | 144, 153 | mulneg1d 11613 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (-((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) = -(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) |
155 | 142, 154 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π)))) Β· ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1))))) = -(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) |
156 | 99, 155 | sumeq12rdv 15597 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1..^((ββπ₯) + 1))(((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π)))) Β· ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1))))) = Ξ£π β
(1...(ββπ₯))-(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) |
157 | | fzfid 13884 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β (1...(ββπ₯)) β Fin) |
158 | 143, 152 | remulcld 11190 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) β β) |
159 | 158 | recnd 11188 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) β β) |
160 | 157, 159 | fsumneg 15677 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))-(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) = -Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) |
161 | 156, 160 | eqtrd 2773 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1..^((ββπ₯) + 1))(((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π)))) Β· ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1))))) = -Ξ£π β
(1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) |
162 | 95, 161 | oveq12d 7376 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((((absβ(π
β(π₯ / ((ββπ₯) + 1)))) Β· ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β 1))))) β
((absβ(π
β(π₯ / 1))) Β· 0)) β
Ξ£π β
(1..^((ββπ₯) +
1))(((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π)))) Β· ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))))) = (((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) β -Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))))) |
163 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π = π β (π₯ / π) = (π₯ / π)) |
164 | 163 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (π
β(π₯ / π)) = (π
β(π₯ / π))) |
165 | 164 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = π β (absβ(π
β(π₯ / π))) = (absβ(π
β(π₯ / π)))) |
166 | | fvoveq1 7381 |
. . . . . . . . . . . . 13
β’ (π = π β (πβ(π β 1)) = (πβ(π β 1))) |
167 | | fvoveq1 7381 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβ(π β 1)) = (πβ(π β 1))) |
168 | 167 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π = π β (2 Β· (πβ(π β 1))) = (2 Β· (πβ(π β 1)))) |
169 | 166, 168 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π = π β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = ((πβ(π β 1)) β (2 Β· (πβ(π β 1))))) |
170 | 165, 169 | jca 513 |
. . . . . . . . . . 11
β’ (π = π β ((absβ(π
β(π₯ / π))) = (absβ(π
β(π₯ / π))) β§ ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))))) |
171 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (π₯ / π) = (π₯ / (π + 1))) |
172 | 171 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (π
β(π₯ / π)) = (π
β(π₯ / (π + 1)))) |
173 | 172 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β (absβ(π
β(π₯ / π))) = (absβ(π
β(π₯ / (π + 1))))) |
174 | | fvoveq1 7381 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (πβ(π β 1)) = (πβ((π + 1) β 1))) |
175 | | fvoveq1 7381 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (πβ(π β 1)) = (πβ((π + 1) β 1))) |
176 | 175 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (2 Β· (πβ(π β 1))) = (2 Β· (πβ((π + 1) β 1)))) |
177 | 174, 176 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π = (π + 1) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1))))) |
178 | 173, 177 | jca 513 |
. . . . . . . . . . 11
β’ (π = (π + 1) β ((absβ(π
β(π₯ / π))) = (absβ(π
β(π₯ / (π + 1)))) β§ ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))))) |
179 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (π₯ / π) = (π₯ / 1)) |
180 | 179 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π
β(π₯ / π)) = (π
β(π₯ / 1))) |
181 | 180 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = 1 β (absβ(π
β(π₯ / π))) = (absβ(π
β(π₯ / 1)))) |
182 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β (π β 1) = (1 β 1)) |
183 | | 1m1e0 12230 |
. . . . . . . . . . . . . . . . 17
β’ (1
β 1) = 0 |
184 | 182, 183 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β (π β 1) = 0) |
185 | 184 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (πβ(π β 1)) = (πβ0)) |
186 | | 0re 11162 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
187 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 0 β (ββπ) =
(ββ0)) |
188 | | 0z 12515 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 β
β€ |
189 | | flid 13719 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0 β
β€ β (ββ0) = 0) |
190 | 188, 189 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(ββ0) = 0 |
191 | 187, 190 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 0 β (ββπ) = 0) |
192 | 191 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β
(1...(ββπ)) =
(1...0)) |
193 | | fz10 13468 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1...0) =
β
|
194 | 192, 193 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β
(1...(ββπ)) =
β
) |
195 | 194 | sumeq1d 15591 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β Ξ£π β
(1...(ββπ))((Ξβπ) Β· ((logβπ) + (Οβ(π / π)))) = Ξ£π β β
((Ξβπ) Β· ((logβπ) + (Οβ(π / π))))) |
196 | | sum0 15611 |
. . . . . . . . . . . . . . . . . 18
β’
Ξ£π β
β
((Ξβπ)
Β· ((logβπ) +
(Οβ(π / π)))) = 0 |
197 | 195, 196 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β Ξ£π β
(1...(ββπ))((Ξβπ) Β· ((logβπ) + (Οβ(π / π)))) = 0) |
198 | 197, 47, 132 | fvmpt 6949 |
. . . . . . . . . . . . . . . 16
β’ (0 β
β β (πβ0)
= 0) |
199 | 186, 198 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (πβ0) = 0 |
200 | 185, 199 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (πβ(π β 1)) = 0) |
201 | 184 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = 1 β (πβ(π β 1)) = (πβ0)) |
202 | | rpne0 12936 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β+
β π β
0) |
203 | 202 | necon2bi 2971 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β Β¬ π β
β+) |
204 | 203 | iffalsed 4498 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β if(π β β+,
(π Β·
(logβπ)), 0) =
0) |
205 | 204, 81, 132 | fvmpt 6949 |
. . . . . . . . . . . . . . . . . 18
β’ (0 β
β β (πβ0)
= 0) |
206 | 186, 205 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (πβ0) = 0 |
207 | 201, 206 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β (πβ(π β 1)) = 0) |
208 | 207 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (2 Β· (πβ(π β 1))) = (2 Β·
0)) |
209 | | 2t0e0 12327 |
. . . . . . . . . . . . . . 15
β’ (2
Β· 0) = 0 |
210 | 208, 209 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (2 Β· (πβ(π β 1))) = 0) |
211 | 200, 210 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (π = 1 β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = (0 β
0)) |
212 | | 0m0e0 12278 |
. . . . . . . . . . . . 13
β’ (0
β 0) = 0 |
213 | 211, 212 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (π = 1 β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = 0) |
214 | 181, 213 | jca 513 |
. . . . . . . . . . 11
β’ (π = 1 β ((absβ(π
β(π₯ / π))) = (absβ(π
β(π₯ / 1))) β§ ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = 0)) |
215 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π = ((ββπ₯) + 1) β (π₯ / π) = (π₯ / ((ββπ₯) + 1))) |
216 | 215 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π = ((ββπ₯) + 1) β (π
β(π₯ / π)) = (π
β(π₯ / ((ββπ₯) + 1)))) |
217 | 216 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = ((ββπ₯) + 1) β (absβ(π
β(π₯ / π))) = (absβ(π
β(π₯ / ((ββπ₯) + 1))))) |
218 | | fvoveq1 7381 |
. . . . . . . . . . . . 13
β’ (π = ((ββπ₯) + 1) β (πβ(π β 1)) = (πβ(((ββπ₯) + 1) β 1))) |
219 | | fvoveq1 7381 |
. . . . . . . . . . . . . 14
β’ (π = ((ββπ₯) + 1) β (πβ(π β 1)) = (πβ(((ββπ₯) + 1) β 1))) |
220 | 219 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’ (π = ((ββπ₯) + 1) β (2 Β· (πβ(π β 1))) = (2 Β· (πβ(((ββπ₯) + 1) β
1)))) |
221 | 218, 220 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ (π = ((ββπ₯) + 1) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β
1))))) |
222 | 217, 221 | jca 513 |
. . . . . . . . . . 11
β’ (π = ((ββπ₯) + 1) β ((absβ(π
β(π₯ / π))) = (absβ(π
β(π₯ / ((ββπ₯) + 1)))) β§ ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) = ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β
1)))))) |
223 | | nnuz 12811 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
224 | 15, 223 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β ((ββπ₯) + 1) β
(β€β₯β1)) |
225 | 10 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β π₯ β
β+) |
226 | | elfznn 13476 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(1...((ββπ₯) +
1)) β π β
β) |
227 | 226 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β π β
β) |
228 | 227 | nnrpd 12960 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β π β
β+) |
229 | 225, 228 | rpdivcld 12979 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β (π₯ / π) β
β+) |
230 | 69 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . 15
β’ ((π₯ / π) β β+ β (π
β(π₯ / π)) β β) |
231 | 229, 230 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β (π
β(π₯ / π)) β β) |
232 | 231 | recnd 11188 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β (π
β(π₯ / π)) β β) |
233 | 232 | abscld 15327 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β
(absβ(π
β(π₯ / π))) β β) |
234 | 233 | recnd 11188 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β
(absβ(π
β(π₯ / π))) β β) |
235 | 227 | nnred 12173 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β π β
β) |
236 | | 1red 11161 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β 1 β
β) |
237 | 235, 236 | resubcld 11588 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β (π β 1) β
β) |
238 | 78 | ffvelcdmi 7035 |
. . . . . . . . . . . . . 14
β’ ((π β 1) β β
β (πβ(π β 1)) β
β) |
239 | 237, 238 | syl 17 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β (πβ(π β 1)) β β) |
240 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β 2 β
β) |
241 | 87 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . 15
β’ ((π β 1) β β
β (πβ(π β 1)) β
β) |
242 | 237, 241 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β (πβ(π β 1)) β β) |
243 | 240, 242 | remulcld 11190 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β (2 Β·
(πβ(π β 1))) β
β) |
244 | 239, 243 | resubcld 11588 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) β
β) |
245 | 244 | recnd 11188 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...((ββπ₯) + 1))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))) β
β) |
246 | 170, 178,
214, 222, 224, 234, 245 | fsumparts 15696 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1..^((ββπ₯) + 1))((absβ(π
β(π₯ / π))) Β· (((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))))) = ((((absβ(π
β(π₯ / ((ββπ₯) + 1)))) Β· ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β 1))))) β
((absβ(π
β(π₯ / 1))) Β· 0)) β
Ξ£π β
(1..^((ββπ₯) +
1))(((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π)))) Β· ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1))))))) |
247 | 147 | recnd 11188 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) β β) |
248 | 87 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (πβπ) β β) |
249 | 145, 248 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) β β) |
250 | 148, 249 | remulcld 11190 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· (πβπ)) β β) |
251 | 250 | recnd 11188 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· (πβπ)) β β) |
252 | | 1red 11161 |
. . . . . . . . . . . . . . . . 17
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 1 β
β) |
253 | 145, 252 | resubcld 11588 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (π β 1) β β) |
254 | 78 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . 16
β’ ((π β 1) β β
β (πβ(π β 1)) β
β) |
255 | 253, 254 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ(π β 1)) β β) |
256 | 255 | recnd 11188 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ(π β 1)) β β) |
257 | 87 | ffvelcdmi 7035 |
. . . . . . . . . . . . . . . . 17
β’ ((π β 1) β β
β (πβ(π β 1)) β
β) |
258 | 253, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ(π β 1)) β β) |
259 | 148, 258 | remulcld 11190 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· (πβ(π β 1))) β
β) |
260 | 259 | recnd 11188 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· (πβ(π β 1))) β
β) |
261 | 247, 251,
256, 260 | sub4d 11566 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((πβπ) β (2 Β· (πβπ))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1))))) = (((πβπ) β (πβ(π β 1))) β ((2 Β· (πβπ)) β (2 Β· (πβ(π β 1)))))) |
262 | 124 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· (πβ((π + 1) β 1))) = (2 Β· (πβπ))) |
263 | 123, 262 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))) = ((πβπ) β (2 Β· (πβπ)))) |
264 | 263 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1))))) = (((πβπ) β (2 Β· (πβπ))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))))) |
265 | | 2cnd 12236 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β 2 β
β) |
266 | 249 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβπ) β β) |
267 | 258 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (πβ(π β 1)) β β) |
268 | 265, 266,
267 | subdid 11616 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· ((πβπ) β (πβ(π β 1)))) = ((2 Β· (πβπ)) β (2 Β· (πβ(π β 1))))) |
269 | 268 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))) = (((πβπ) β (πβ(π β 1))) β ((2 Β· (πβπ)) β (2 Β· (πβ(π β 1)))))) |
270 | 261, 264,
269 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1))))) = (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) |
271 | 270 | oveq2d 7374 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))))) = ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) |
272 | 99, 271 | sumeq12rdv 15597 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1..^((ββπ₯) + 1))((absβ(π
β(π₯ / π))) Β· (((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))) β ((πβ(π β 1)) β (2 Β· (πβ(π β 1)))))) = Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) |
273 | 246, 272 | eqtr3d 2775 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((((absβ(π
β(π₯ / ((ββπ₯) + 1)))) Β· ((πβ(((ββπ₯) + 1) β 1)) β (2 Β· (πβ(((ββπ₯) + 1) β 1))))) β
((absβ(π
β(π₯ / 1))) Β· 0)) β
Ξ£π β
(1..^((ββπ₯) +
1))(((absβ(π
β(π₯ / (π + 1)))) β (absβ(π
β(π₯ / π)))) Β· ((πβ((π + 1) β 1)) β (2 Β· (πβ((π + 1) β 1)))))) = Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) |
274 | 157, 159 | fsumcl 15623 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) β β) |
275 | 93, 274 | subnegd 11524 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) β -Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) = (((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))))) |
276 | 162, 273,
275 | 3eqtr3rd 2782 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) = Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) |
277 | 10 | relogcld 25994 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
278 | 277 | recnd 11188 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β β) |
279 | 66, 278 | mulcomd 11181 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ Β· (logβπ₯)) = ((logβπ₯) Β· π₯)) |
280 | 276, 279 | oveq12d 7376 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯))) = (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / ((logβπ₯) Β· π₯))) |
281 | 147, 255 | resubcld 11588 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (πβ(π β 1))) β
β) |
282 | 249, 258 | resubcld 11588 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (πβ(π β 1))) β
β) |
283 | 148, 282 | remulcld 11190 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· ((πβπ) β (πβ(π β 1)))) β
β) |
284 | 281, 283 | resubcld 11588 |
. . . . . . . . . . 11
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))) β
β) |
285 | 108, 284 | remulcld 11190 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) β
β) |
286 | 157, 285 | fsumrecl 15624 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) β
β) |
287 | 286 | recnd 11188 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) β
β) |
288 | 2, 8 | rplogcld 26000 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β
β+) |
289 | 288 | rpne0d 12967 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (logβπ₯) β 0) |
290 | 10 | rpne0d 12967 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β π₯ β 0) |
291 | 287, 278,
66, 289, 290 | divdiv1d 11967 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)) / π₯) = (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / ((logβπ₯) Β· π₯))) |
292 | 280, 291 | eqtr4d 2776 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯))) = ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)) / π₯)) |
293 | 292 | oveq2d 7374 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) + ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯)))) = (((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) + ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)) / π₯))) |
294 | 71 | recnd 11188 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (π
βπ₯) β β) |
295 | 294 | abscld 15327 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (absβ(π
βπ₯)) β β) |
296 | 295, 277 | remulcld 11190 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ(π
βπ₯)) Β· (logβπ₯)) β β) |
297 | 108, 281 | remulcld 11190 |
. . . . . . . . . 10
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
298 | 157, 297 | fsumrecl 15624 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
299 | 298, 288 | rerpdivcld 12993 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯)) β
β) |
300 | 296, 299 | resubcld 11588 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) β
β) |
301 | 300 | recnd 11188 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) β
β) |
302 | 287, 278,
289 | divcld 11936 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)) β
β) |
303 | 301, 302,
66, 290 | divdird 11974 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) + (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯))) / π₯) = (((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) + ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)) / π₯))) |
304 | 296 | recnd 11188 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((absβ(π
βπ₯)) Β· (logβπ₯)) β β) |
305 | 299 | recnd 11188 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯)) β
β) |
306 | 304, 305,
302 | subsubd 11545 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯)) β (Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)))) = ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) + (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)))) |
307 | | 2cnd 12236 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 2 β β) |
308 | 266, 267 | subcld 11517 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (πβ(π β 1))) β
β) |
309 | 109, 308 | mulcld 11180 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
310 | 157, 307,
309 | fsummulc2 15674 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))) = Ξ£π β (1...(ββπ₯))(2 Β· ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) |
311 | 281 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((πβπ) β (πβ(π β 1))) β
β) |
312 | 265, 308 | mulcld 11180 |
. . . . . . . . . . . . . . 15
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (2 Β· ((πβπ) β (πβ(π β 1)))) β
β) |
313 | 311, 312 | nncand 11522 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((πβπ) β (πβ(π β 1))) β (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) = (2 Β· ((πβπ) β (πβ(π β 1))))) |
314 | 313 | oveq2d 7374 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) = ((absβ(π
β(π₯ / π))) Β· (2 Β· ((πβπ) β (πβ(π β 1)))))) |
315 | 284 | recnd 11188 |
. . . . . . . . . . . . . 14
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))) β
β) |
316 | 109, 311,
315 | subdid 11616 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) = (((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))))) |
317 | 109, 265,
308 | mul12d 11369 |
. . . . . . . . . . . . 13
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (2 Β· ((πβπ) β (πβ(π β 1))))) = (2 Β·
((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) |
318 | 314, 316,
317 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β (((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) = (2 Β·
((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) |
319 | 318 | sumeq2dv 15593 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) = Ξ£π β (1...(ββπ₯))(2 Β· ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) |
320 | 297 | recnd 11188 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
321 | 285 | recnd 11188 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) β
β) |
322 | 157, 320,
321 | fsumsub 15678 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β ((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) = (Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))))) |
323 | 310, 319,
322 | 3eqtr2rd 2780 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) = (2 Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) |
324 | 323 | oveq1d 7373 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) / (logβπ₯)) = ((2 Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))) / (logβπ₯))) |
325 | 298 | recnd 11188 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
326 | 325, 287,
278, 289 | divsubdird 11975 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1))))))) / (logβπ₯)) = ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯)) β (Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)))) |
327 | 108, 282 | remulcld 11190 |
. . . . . . . . . . . 12
β’
(((β€ β§ π₯
β (1(,)+β)) β§ π β (1...(ββπ₯))) β ((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
328 | 157, 327 | fsumrecl 15624 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
329 | 328 | recnd 11188 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) β
β) |
330 | 307, 329,
278, 289 | div23d 11973 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))) / (logβπ₯)) = ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) |
331 | 324, 326,
330 | 3eqtr3d 2781 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯)) β (Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯))) = ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) |
332 | 331 | oveq2d 7374 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯)) β (Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯)))) = (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))))) |
333 | 306, 332 | eqtr3d 2775 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) + (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯))) = (((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1))))))) |
334 | 333 | oveq1d 7373 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) + (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· (((πβπ) β (πβ(π β 1))) β (2 Β· ((πβπ) β (πβ(π β 1)))))) / (logβπ₯))) / π₯) = ((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) / π₯)) |
335 | 293, 303,
334 | 3eqtr2d 2779 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β (((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) + ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯)))) = ((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) / π₯)) |
336 | 335 | mpteq2dva 5206 |
. . 3
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) + ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯))))) = (π₯ β (1(,)+β) β¦
((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) / π₯))) |
337 | 300, 10 | rerpdivcld 12993 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) β β) |
338 | 157, 158 | fsumrecl 15624 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) β β) |
339 | 92, 338 | readdcld 11189 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) β β) |
340 | 10, 288 | rpmulcld 12978 |
. . . . 5
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ Β· (logβπ₯)) β
β+) |
341 | 339, 340 | rerpdivcld 12993 |
. . . 4
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯))) β β) |
342 | 47, 18 | pntrlog2bndlem1 26941 |
. . . . 5
β’ (π₯ β (1(,)+β) β¦
((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯)) β β€π(1) |
343 | 342 | a1i 11 |
. . . 4
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯)) β β€π(1)) |
344 | 340 | rpcnd 12964 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ Β· (logβπ₯)) β β) |
345 | 340 | rpne0d 12967 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ Β· (logβπ₯)) β 0) |
346 | 93, 274, 344, 345 | divdird 11974 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯))) = ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) / (π₯ Β· (logβπ₯))) + (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯))))) |
347 | 91 | recnd 11188 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β ((πβπ₯) β (2 Β· (πβ(ββπ₯)))) β β) |
348 | 43, 347, 344, 345 | divassd 11971 |
. . . . . . . 8
β’
((β€ β§ π₯
β (1(,)+β)) β (((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) / (π₯ Β· (logβπ₯))) = ((π₯ / ((ββπ₯) + 1)) Β· (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯))))) |
349 | 348 | oveq1d 7373 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) / (π₯ Β· (logβπ₯))) + (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯)))) = (((π₯ / ((ββπ₯) + 1)) Β· (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯)))) + (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯))))) |
350 | 346, 349 | eqtrd 2773 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯))) = (((π₯ / ((ββπ₯) + 1)) Β· (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯)))) + (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯))))) |
351 | 350 | mpteq2dva 5206 |
. . . . 5
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯)))) = (π₯ β (1(,)+β) β¦ (((π₯ / ((ββπ₯) + 1)) Β· (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯)))) + (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯)))))) |
352 | 91, 340 | rerpdivcld 12993 |
. . . . . . 7
β’
((β€ β§ π₯
β (1(,)+β)) β (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯))) β β) |
353 | 21, 352 | remulcld 11190 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β ((π₯ / ((ββπ₯) + 1)) Β· (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯)))) β β) |
354 | 338, 340 | rerpdivcld 12993 |
. . . . . 6
β’
((β€ β§ π₯
β (1(,)+β)) β (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯))) β β) |
355 | | ioossre 13331 |
. . . . . . . . 9
β’
(1(,)+β) β β |
356 | 355 | a1i 11 |
. . . . . . . 8
β’ (β€
β (1(,)+β) β β) |
357 | | 1red 11161 |
. . . . . . . 8
β’ (β€
β 1 β β) |
358 | 21, 5, 30 | ltled 11308 |
. . . . . . . . 9
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ / ((ββπ₯) + 1)) β€ 1) |
359 | 358 | adantrr 716 |
. . . . . . . 8
β’
((β€ β§ (π₯
β (1(,)+β) β§ 1 β€ π₯)) β (π₯ / ((ββπ₯) + 1)) β€ 1) |
360 | 356, 21, 357, 357, 359 | ello1d 15411 |
. . . . . . 7
β’ (β€
β (π₯ β
(1(,)+β) β¦ (π₯ /
((ββπ₯) + 1)))
β β€π(1)) |
361 | 80 | recnd 11188 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (πβπ₯) β β) |
362 | 90 | recnd 11188 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· (πβ(ββπ₯))) β β) |
363 | 361, 362,
344, 345 | divsubdird 11975 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯))) = (((πβπ₯) / (π₯ Β· (logβπ₯))) β ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯))))) |
364 | 363 | mpteq2dva 5206 |
. . . . . . . . 9
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯)))) = (π₯ β (1(,)+β) β¦ (((πβπ₯) / (π₯ Β· (logβπ₯))) β ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯)))))) |
365 | 80, 340 | rerpdivcld 12993 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β ((πβπ₯) / (π₯ Β· (logβπ₯))) β β) |
366 | 90, 340 | rerpdivcld 12993 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯))) β β) |
367 | | 2cnd 12236 |
. . . . . . . . . . . 12
β’ (β€
β 2 β β) |
368 | | o1const 15508 |
. . . . . . . . . . . 12
β’
(((1(,)+β) β β β§ 2 β β) β (π₯ β (1(,)+β) β¦
2) β π(1)) |
369 | 355, 367,
368 | sylancr 588 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β
(1(,)+β) β¦ 2) β π(1)) |
370 | 365 | recnd 11188 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β ((πβπ₯) / (π₯ Β· (logβπ₯))) β β) |
371 | 80, 10 | rerpdivcld 12993 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β ((πβπ₯) / π₯) β β) |
372 | 371 | recnd 11188 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β ((πβπ₯) / π₯) β β) |
373 | 307, 278 | mulcld 11180 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· (logβπ₯)) β β) |
374 | 372, 373,
278, 289 | divsubdird 11975 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β ((((πβπ₯) / π₯) β (2 Β· (logβπ₯))) / (logβπ₯)) = ((((πβπ₯) / π₯) / (logβπ₯)) β ((2 Β· (logβπ₯)) / (logβπ₯)))) |
375 | 23, 277 | remulcld 11190 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· (logβπ₯)) β β) |
376 | 371, 375 | resubcld 11588 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (((πβπ₯) / π₯) β (2 Β· (logβπ₯))) β
β) |
377 | 376 | recnd 11188 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (((πβπ₯) / π₯) β (2 Β· (logβπ₯))) β
β) |
378 | 377, 278,
289 | divrecd 11939 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β ((((πβπ₯) / π₯) β (2 Β· (logβπ₯))) / (logβπ₯)) = ((((πβπ₯) / π₯) β (2 Β· (logβπ₯))) Β· (1 /
(logβπ₯)))) |
379 | 361, 66, 278, 290, 289 | divdiv1d 11967 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (((πβπ₯) / π₯) / (logβπ₯)) = ((πβπ₯) / (π₯ Β· (logβπ₯)))) |
380 | 307, 278,
289 | divcan4d 11942 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· (logβπ₯)) / (logβπ₯)) = 2) |
381 | 379, 380 | oveq12d 7376 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β ((((πβπ₯) / π₯) / (logβπ₯)) β ((2 Β· (logβπ₯)) / (logβπ₯))) = (((πβπ₯) / (π₯ Β· (logβπ₯))) β 2)) |
382 | 374, 378,
381 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (((πβπ₯) / (π₯ Β· (logβπ₯))) β 2) = ((((πβπ₯) / π₯) β (2 Β· (logβπ₯))) Β· (1 /
(logβπ₯)))) |
383 | 382 | mpteq2dva 5206 |
. . . . . . . . . . . . 13
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((πβπ₯) / (π₯ Β· (logβπ₯))) β 2)) = (π₯ β (1(,)+β) β¦ ((((πβπ₯) / π₯) β (2 Β· (logβπ₯))) Β· (1 /
(logβπ₯))))) |
384 | 5, 288 | rerpdivcld 12993 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (1 / (logβπ₯)) β β) |
385 | 10 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (β€
β (π₯ β
(1(,)+β) β π₯
β β+)) |
386 | 385 | ssrdv 3951 |
. . . . . . . . . . . . . . 15
β’ (β€
β (1(,)+β) β β+) |
387 | 47 | selbergs 26938 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β¦ (((πβπ₯) / π₯) β (2 Β· (logβπ₯)))) β
π(1) |
388 | 387 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (β€
β (π₯ β
β+ β¦ (((πβπ₯) / π₯) β (2 Β· (logβπ₯)))) β
π(1)) |
389 | 386, 388 | o1res2 15451 |
. . . . . . . . . . . . . 14
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((πβπ₯) / π₯) β (2 Β· (logβπ₯)))) β
π(1)) |
390 | | divlogrlim 26006 |
. . . . . . . . . . . . . . 15
β’ (π₯ β (1(,)+β) β¦
(1 / (logβπ₯)))
βπ 0 |
391 | | rlimo1 15505 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (1(,)+β) β¦
(1 / (logβπ₯)))
βπ 0 β (π₯ β (1(,)+β) β¦ (1 /
(logβπ₯))) β
π(1)) |
392 | 390, 391 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ (β€
β (π₯ β
(1(,)+β) β¦ (1 / (logβπ₯))) β π(1)) |
393 | 376, 384,
389, 392 | o1mul2 15513 |
. . . . . . . . . . . . 13
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((πβπ₯) / π₯) β (2 Β· (logβπ₯))) Β· (1 /
(logβπ₯)))) β
π(1)) |
394 | 383, 393 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((πβπ₯) / (π₯ Β· (logβπ₯))) β 2)) β
π(1)) |
395 | 370, 307,
394 | o1dif 15518 |
. . . . . . . . . . 11
β’ (β€
β ((π₯ β
(1(,)+β) β¦ ((πβπ₯) / (π₯ Β· (logβπ₯)))) β π(1) β (π₯ β (1(,)+β) β¦
2) β π(1))) |
396 | 369, 395 | mpbird 257 |
. . . . . . . . . 10
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((πβπ₯) / (π₯ Β· (logβπ₯)))) β π(1)) |
397 | 22 | a1i 11 |
. . . . . . . . . . . 12
β’ (β€
β 2 β β) |
398 | 2, 277 | remulcld 11190 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (π₯ Β· (logβπ₯)) β β) |
399 | | 2rp 12925 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β+ |
400 | 399 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β 2 β β+) |
401 | 400 | rpge0d 12966 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ 2) |
402 | | flge1nn 13732 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β β β§ 1 β€
π₯) β
(ββπ₯) β
β) |
403 | 2, 9, 402 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β (ββπ₯) β β) |
404 | 403 | nnrpd 12960 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (ββπ₯) β
β+) |
405 | | rpre 12928 |
. . . . . . . . . . . . . . . . . . 19
β’
((ββπ₯)
β β+ β (ββπ₯) β β) |
406 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (ββπ₯) β (π β β+ β
(ββπ₯) β
β+)) |
407 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (ββπ₯) β π = (ββπ₯)) |
408 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (ββπ₯) β (logβπ) =
(logβ(ββπ₯))) |
409 | 407, 408 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (ββπ₯) β (π Β· (logβπ)) = ((ββπ₯) Β· (logβ(ββπ₯)))) |
410 | 406, 409 | ifbieq1d 4511 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (ββπ₯) β if(π β β+, (π Β· (logβπ)), 0) = if((ββπ₯) β β+,
((ββπ₯) Β·
(logβ(ββπ₯))), 0)) |
411 | | ovex 7391 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((ββπ₯)
Β· (logβ(ββπ₯))) β V |
412 | 411, 132 | ifex 4537 |
. . . . . . . . . . . . . . . . . . . 20
β’
if((ββπ₯)
β β+, ((ββπ₯) Β· (logβ(ββπ₯))), 0) β
V |
413 | 410, 81, 412 | fvmpt 6949 |
. . . . . . . . . . . . . . . . . . 19
β’
((ββπ₯)
β β β (πβ(ββπ₯)) = if((ββπ₯) β β+,
((ββπ₯) Β·
(logβ(ββπ₯))), 0)) |
414 | 405, 413 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((ββπ₯)
β β+ β (πβ(ββπ₯)) = if((ββπ₯) β β+,
((ββπ₯) Β·
(logβ(ββπ₯))), 0)) |
415 | | iftrue 4493 |
. . . . . . . . . . . . . . . . . 18
β’
((ββπ₯)
β β+ β if((ββπ₯) β β+,
((ββπ₯) Β·
(logβ(ββπ₯))), 0) = ((ββπ₯) Β· (logβ(ββπ₯)))) |
416 | 414, 415 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’
((ββπ₯)
β β+ β (πβ(ββπ₯)) = ((ββπ₯) Β· (logβ(ββπ₯)))) |
417 | 404, 416 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β (πβ(ββπ₯)) = ((ββπ₯) Β· (logβ(ββπ₯)))) |
418 | 404 | relogcld 25994 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (logβ(ββπ₯)) β β) |
419 | 13 | nn0ge0d 12481 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ (ββπ₯)) |
420 | 403 | nnge1d 12206 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β 1 β€ (ββπ₯)) |
421 | 46, 420 | logge0d 26001 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ (logβ(ββπ₯))) |
422 | | flle 13710 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β
(ββπ₯) β€
π₯) |
423 | 2, 422 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (ββπ₯) β€ π₯) |
424 | 404, 10 | logled 25998 |
. . . . . . . . . . . . . . . . . 18
β’
((β€ β§ π₯
β (1(,)+β)) β ((ββπ₯) β€ π₯ β (logβ(ββπ₯)) β€ (logβπ₯))) |
425 | 423, 424 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’
((β€ β§ π₯
β (1(,)+β)) β (logβ(ββπ₯)) β€ (logβπ₯)) |
426 | 46, 2, 418, 277, 419, 421, 423, 425 | lemul12ad 12102 |
. . . . . . . . . . . . . . . 16
β’
((β€ β§ π₯
β (1(,)+β)) β ((ββπ₯) Β· (logβ(ββπ₯))) β€ (π₯ Β· (logβπ₯))) |
427 | 417, 426 | eqbrtrd 5128 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β (πβ(ββπ₯)) β€ (π₯ Β· (logβπ₯))) |
428 | 89, 398, 23, 401, 427 | lemul2ad 12100 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (2 Β· (πβ(ββπ₯))) β€ (2 Β· (π₯ Β· (logβπ₯)))) |
429 | 90, 23, 340 | ledivmul2d 13016 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β (((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯))) β€ 2 β (2 Β· (πβ(ββπ₯))) β€ (2 Β· (π₯ Β· (logβπ₯))))) |
430 | 428, 429 | mpbird 257 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯))) β€ 2) |
431 | 430 | adantrr 716 |
. . . . . . . . . . . 12
β’
((β€ β§ (π₯
β (1(,)+β) β§ 1 β€ π₯)) β ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯))) β€ 2) |
432 | 356, 366,
357, 397, 431 | ello1d 15411 |
. . . . . . . . . . 11
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯)))) β
β€π(1)) |
433 | | 0red 11163 |
. . . . . . . . . . . 12
β’ (β€
β 0 β β) |
434 | 46, 418, 419, 421 | mulge0d 11737 |
. . . . . . . . . . . . . . 15
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ ((ββπ₯) Β· (logβ(ββπ₯)))) |
435 | 434, 417 | breqtrrd 5134 |
. . . . . . . . . . . . . 14
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ (πβ(ββπ₯))) |
436 | 23, 89, 401, 435 | mulge0d 11737 |
. . . . . . . . . . . . 13
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ (2 Β· (πβ(ββπ₯)))) |
437 | 90, 340, 436 | divge0d 13002 |
. . . . . . . . . . . 12
β’
((β€ β§ π₯
β (1(,)+β)) β 0 β€ ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯)))) |
438 | 366, 433,
437 | o1lo12 15426 |
. . . . . . . . . . 11
β’ (β€
β ((π₯ β
(1(,)+β) β¦ ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯)))) β π(1) β (π₯ β (1(,)+β) β¦
((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯)))) β
β€π(1))) |
439 | 432, 438 | mpbird 257 |
. . . . . . . . . 10
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯)))) β π(1)) |
440 | 365, 366,
396, 439 | o1sub2 15514 |
. . . . . . . . 9
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((πβπ₯) / (π₯ Β· (logβπ₯))) β ((2 Β· (πβ(ββπ₯))) / (π₯ Β· (logβπ₯))))) β π(1)) |
441 | 364, 440 | eqeltrd 2834 |
. . . . . . . 8
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯)))) β π(1)) |
442 | 352, 441 | o1lo1d 15427 |
. . . . . . 7
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯)))) β
β€π(1)) |
443 | 21, 352, 360, 442, 41 | lo1mul 15516 |
. . . . . 6
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((π₯
/ ((ββπ₯) + 1))
Β· (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯))))) β
β€π(1)) |
444 | 47 | selbergsb 26939 |
. . . . . . . 8
β’
βπ β
β+ βπ¦ β (1[,)+β)(absβ(((πβπ¦) / π¦) β (2 Β· (logβπ¦)))) β€ π |
445 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β β+
β§ βπ¦ β
(1[,)+β)(absβ(((πβπ¦) / π¦) β (2 Β· (logβπ¦)))) β€ π) β π β β+) |
446 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β β+
β§ βπ¦ β
(1[,)+β)(absβ(((πβπ¦) / π¦) β (2 Β· (logβπ¦)))) β€ π) β βπ¦ β (1[,)+β)(absβ(((πβπ¦) / π¦) β (2 Β· (logβπ¦)))) β€ π) |
447 | 47, 18, 445, 446 | pntrlog2bndlem3 26943 |
. . . . . . . . 9
β’ ((π β β+
β§ βπ¦ β
(1[,)+β)(absβ(((πβπ¦) / π¦) β (2 Β· (logβπ¦)))) β€ π) β (π₯ β (1(,)+β) β¦ (Ξ£π β
(1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯)))) β π(1)) |
448 | 447 | rexlimiva 3141 |
. . . . . . . 8
β’
(βπ β
β+ βπ¦ β (1[,)+β)(absβ(((πβπ¦) / π¦) β (2 Β· (logβπ¦)))) β€ π β (π₯ β (1(,)+β) β¦ (Ξ£π β
(1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯)))) β π(1)) |
449 | 444, 448 | mp1i 13 |
. . . . . . 7
β’ (β€
β (π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯)))) β π(1)) |
450 | 354, 449 | o1lo1d 15427 |
. . . . . 6
β’ (β€
β (π₯ β
(1(,)+β) β¦ (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯)))) β
β€π(1)) |
451 | 353, 354,
443, 450 | lo1add 15515 |
. . . . 5
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((π₯
/ ((ββπ₯) + 1))
Β· (((πβπ₯) β (2 Β· (πβ(ββπ₯)))) / (π₯ Β· (logβπ₯)))) + (Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ))))) / (π₯ Β· (logβπ₯))))) β
β€π(1)) |
452 | 351, 451 | eqeltrd 2834 |
. . . 4
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯)))) β
β€π(1)) |
453 | 337, 341,
343, 452 | lo1add 15515 |
. . 3
β’ (β€
β (π₯ β
(1(,)+β) β¦ (((((absβ(π
βπ₯)) Β· (logβπ₯)) β (Ξ£π β (1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))) / (logβπ₯))) / π₯) + ((((π₯ / ((ββπ₯) + 1)) Β· ((πβπ₯) β (2 Β· (πβ(ββπ₯))))) + Ξ£π β (1...(ββπ₯))(((absβ(π
β(π₯ / π))) β (absβ(π
β(π₯ / (π + 1))))) Β· ((πβπ) β (2 Β· (π Β· (logβπ)))))) / (π₯ Β· (logβπ₯))))) β
β€π(1)) |
454 | 336, 453 | eqeltrrd 2835 |
. 2
β’ (β€
β (π₯ β
(1(,)+β) β¦ ((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) / π₯)) β β€π(1)) |
455 | 454 | mptru 1549 |
1
β’ (π₯ β (1(,)+β) β¦
((((absβ(π
βπ₯)) Β· (logβπ₯)) β ((2 / (logβπ₯)) Β· Ξ£π β
(1...(ββπ₯))((absβ(π
β(π₯ / π))) Β· ((πβπ) β (πβ(π β 1)))))) / π₯)) β β€π(1) |