Step | Hyp | Ref
| Expression |
1 | | rpvmasum.z |
. 2
β’ π =
(β€/nβ€βπ) |
2 | | rpvmasum.l |
. 2
β’ πΏ = (β€RHomβπ) |
3 | | rpvmasum.a |
. 2
β’ (π β π β β) |
4 | | rpvmasum.g |
. 2
β’ πΊ = (DChrβπ) |
5 | | rpvmasum.d |
. 2
β’ π· = (BaseβπΊ) |
6 | | rpvmasum.1 |
. 2
β’ 1 =
(0gβπΊ) |
7 | | dchrisum.b |
. 2
β’ (π β π β π·) |
8 | | dchrisum.n1 |
. 2
β’ (π β π β 1 ) |
9 | | fzfid 13885 |
. . 3
β’ ((π β§ π β β+) β
(1...(ββπ))
β Fin) |
10 | | simpl 484 |
. . . . 5
β’ ((π β§ π β β+) β π) |
11 | | elfznn 13477 |
. . . . 5
β’ (π β
(1...(ββπ))
β π β
β) |
12 | 7 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β) β π β π·) |
13 | | nnz 12527 |
. . . . . . 7
β’ (π β β β π β
β€) |
14 | 13 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β) β π β β€) |
15 | 4, 1, 5, 2, 12, 14 | dchrzrhcl 26609 |
. . . . 5
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
16 | 10, 11, 15 | syl2an 597 |
. . . 4
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β (πβ(πΏβπ)) β β) |
17 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β+) β π β
β+) |
18 | 11 | nnrpd 12962 |
. . . . . . . 8
β’ (π β
(1...(ββπ))
β π β
β+) |
19 | | ifcl 4536 |
. . . . . . . 8
β’ ((π β β+
β§ π β
β+) β if(π = 0, π, π) β
β+) |
20 | 17, 18, 19 | syl2an 597 |
. . . . . . 7
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β if(π = 0, π, π) β
β+) |
21 | 20 | relogcld 25994 |
. . . . . 6
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β (logβif(π = 0,
π, π)) β β) |
22 | 11 | adantl 483 |
. . . . . 6
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β π β
β) |
23 | 21, 22 | nndivred 12214 |
. . . . 5
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β ((logβif(π =
0, π, π)) / π) β β) |
24 | 23 | recnd 11190 |
. . . 4
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β ((logβif(π =
0, π, π)) / π) β β) |
25 | 16, 24 | mulcld 11182 |
. . 3
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β β) |
26 | 9, 25 | fsumcl 15625 |
. 2
β’ ((π β§ π β β+) β
Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β β) |
27 | | fveq2 6847 |
. . . 4
β’ (π = (π₯ / π) β (ββπ) = (ββ(π₯ / π))) |
28 | 27 | oveq2d 7378 |
. . 3
β’ (π = (π₯ / π) β (1...(ββπ)) = (1...(ββ(π₯ / π)))) |
29 | | ifeq1 4495 |
. . . . . . 7
β’ (π = (π₯ / π) β if(π = 0, π, π) = if(π = 0, (π₯ / π), π)) |
30 | 29 | fveq2d 6851 |
. . . . . 6
β’ (π = (π₯ / π) β (logβif(π = 0, π, π)) = (logβif(π = 0, (π₯ / π), π))) |
31 | 30 | oveq1d 7377 |
. . . . 5
β’ (π = (π₯ / π) β ((logβif(π = 0, π, π)) / π) = ((logβif(π = 0, (π₯ / π), π)) / π)) |
32 | 31 | oveq2d 7378 |
. . . 4
β’ (π = (π₯ / π) β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = ((πβ(πΏβπ)) Β· ((logβif(π = 0, (π₯ / π), π)) / π))) |
33 | 32 | adantr 482 |
. . 3
β’ ((π = (π₯ / π) β§ π β (1...(ββ(π₯ / π)))) β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = ((πβ(πΏβπ)) Β· ((logβif(π = 0, (π₯ / π), π)) / π))) |
34 | 28, 33 | sumeq12rdv 15599 |
. 2
β’ (π = (π₯ / π) β Ξ£π β (1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = Ξ£π β (1...(ββ(π₯ / π)))((πβ(πΏβπ)) Β· ((logβif(π = 0, (π₯ / π), π)) / π))) |
35 | | dchrvmasumif.c |
. . 3
β’ (π β πΆ β (0[,)+β)) |
36 | | dchrvmasumif.e |
. . 3
β’ (π β πΈ β (0[,)+β)) |
37 | 35, 36 | ifcld 4537 |
. 2
β’ (π β if(π = 0, πΆ, πΈ) β (0[,)+β)) |
38 | | 0cn 11154 |
. . 3
β’ 0 β
β |
39 | | dchrvmasumif.t |
. . . 4
β’ (π β seq1( + , πΎ) β π) |
40 | | climcl 15388 |
. . . 4
β’ (seq1( +
, πΎ) β π β π β β) |
41 | 39, 40 | syl 17 |
. . 3
β’ (π β π β β) |
42 | | ifcl 4536 |
. . 3
β’ ((0
β β β§ π
β β) β if(π
= 0, 0, π) β
β) |
43 | 38, 41, 42 | sylancr 588 |
. 2
β’ (π β if(π = 0, 0, π) β β) |
44 | | nnuz 12813 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
45 | | 1zzd 12541 |
. . . . . . . . 9
β’ (π β 1 β
β€) |
46 | | nncn 12168 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
47 | 46 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
48 | | nnne0 12194 |
. . . . . . . . . . . . 13
β’ (π β β β π β 0) |
49 | 48 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β 0) |
50 | 15, 47, 49 | divcld 11938 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πβ(πΏβπ)) / π) β β) |
51 | | dchrvmasumif.f |
. . . . . . . . . . . 12
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
52 | | 2fveq3 6852 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
53 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = π β π = π) |
54 | 52, 53 | oveq12d 7380 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) / π)) |
55 | 54 | cbvmptv 5223 |
. . . . . . . . . . . 12
β’ (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) / π)) |
56 | 51, 55 | eqtri 2765 |
. . . . . . . . . . 11
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
57 | 50, 56 | fmptd 7067 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
58 | | ffvelcdm 7037 |
. . . . . . . . . 10
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β) |
59 | 57, 58 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβπ) β β) |
60 | 44, 45, 59 | serf 13943 |
. . . . . . . 8
β’ (π β seq1( + , πΉ):ββΆβ) |
61 | 60 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β seq1( + , πΉ):ββΆβ) |
62 | | 3re 12240 |
. . . . . . . . . . 11
β’ 3 β
β |
63 | | elicopnf 13369 |
. . . . . . . . . . 11
β’ (3 β
β β (π β
(3[,)+β) β (π
β β β§ 3 β€ π))) |
64 | 62, 63 | mp1i 13 |
. . . . . . . . . 10
β’ (π β (π β (3[,)+β) β (π β β β§ 3 β€
π))) |
65 | 64 | simprbda 500 |
. . . . . . . . 9
β’ ((π β§ π β (3[,)+β)) β π β
β) |
66 | | 1red 11163 |
. . . . . . . . . 10
β’ ((π β§ π β (3[,)+β)) β 1 β
β) |
67 | 62 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (3[,)+β)) β 3 β
β) |
68 | | 1le3 12372 |
. . . . . . . . . . 11
β’ 1 β€
3 |
69 | 68 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (3[,)+β)) β 1 β€
3) |
70 | 64 | simplbda 501 |
. . . . . . . . . 10
β’ ((π β§ π β (3[,)+β)) β 3 β€ π) |
71 | 66, 67, 65, 69, 70 | letrd 11319 |
. . . . . . . . 9
β’ ((π β§ π β (3[,)+β)) β 1 β€ π) |
72 | | flge1nn 13733 |
. . . . . . . . 9
β’ ((π β β β§ 1 β€
π) β
(ββπ) β
β) |
73 | 65, 71, 72 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β (3[,)+β)) β
(ββπ) β
β) |
74 | 73 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β
(ββπ) β
β) |
75 | 61, 74 | ffvelcdmd 7041 |
. . . . . 6
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (seq1( + , πΉ)β(ββπ)) β
β) |
76 | 75 | abscld 15328 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (absβ(seq1( +
, πΉ)β(ββπ))) β β) |
77 | | simpl 484 |
. . . . . . . 8
β’ ((π β§ π β (3[,)+β)) β π) |
78 | | 0red 11165 |
. . . . . . . . . 10
β’ ((π β§ π β (3[,)+β)) β 0 β
β) |
79 | | 3pos 12265 |
. . . . . . . . . . 11
β’ 0 <
3 |
80 | 79 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (3[,)+β)) β 0 <
3) |
81 | 78, 67, 65, 80, 70 | ltletrd 11322 |
. . . . . . . . 9
β’ ((π β§ π β (3[,)+β)) β 0 < π) |
82 | 65, 81 | elrpd 12961 |
. . . . . . . 8
β’ ((π β§ π β (3[,)+β)) β π β
β+) |
83 | 77, 82 | jca 513 |
. . . . . . 7
β’ ((π β§ π β (3[,)+β)) β (π β§ π β
β+)) |
84 | | elrege0 13378 |
. . . . . . . . . 10
β’ (πΆ β (0[,)+β) β
(πΆ β β β§ 0
β€ πΆ)) |
85 | 84 | simplbi 499 |
. . . . . . . . 9
β’ (πΆ β (0[,)+β) β
πΆ β
β) |
86 | 35, 85 | syl 17 |
. . . . . . . 8
β’ (π β πΆ β β) |
87 | | rerpdivcl 12952 |
. . . . . . . 8
β’ ((πΆ β β β§ π β β+)
β (πΆ / π) β
β) |
88 | 86, 87 | sylan 581 |
. . . . . . 7
β’ ((π β§ π β β+) β (πΆ / π) β β) |
89 | 83, 88 | syl 17 |
. . . . . 6
β’ ((π β§ π β (3[,)+β)) β (πΆ / π) β β) |
90 | 89 | adantr 482 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (πΆ / π) β β) |
91 | 82 | relogcld 25994 |
. . . . . . 7
β’ ((π β§ π β (3[,)+β)) β
(logβπ) β
β) |
92 | 65, 71 | logge0d 26001 |
. . . . . . 7
β’ ((π β§ π β (3[,)+β)) β 0 β€
(logβπ)) |
93 | 91, 92 | jca 513 |
. . . . . 6
β’ ((π β§ π β (3[,)+β)) β
((logβπ) β
β β§ 0 β€ (logβπ))) |
94 | 93 | adantr 482 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β ((logβπ) β β β§ 0 β€
(logβπ))) |
95 | | oveq2 7370 |
. . . . . . . 8
β’ (π = 0 β ((seq1( + , πΉ)β(ββπ)) β π) = ((seq1( + , πΉ)β(ββπ)) β 0)) |
96 | 60 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (3[,)+β)) β seq1( + ,
πΉ):ββΆβ) |
97 | 96, 73 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (3[,)+β)) β (seq1( + ,
πΉ)β(ββπ)) β β) |
98 | 97 | subid1d 11508 |
. . . . . . . 8
β’ ((π β§ π β (3[,)+β)) β ((seq1( + ,
πΉ)β(ββπ)) β 0) = (seq1( + , πΉ)β(ββπ))) |
99 | 95, 98 | sylan9eqr 2799 |
. . . . . . 7
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β ((seq1( + , πΉ)β(ββπ)) β π) = (seq1( + , πΉ)β(ββπ))) |
100 | 99 | fveq2d 6851 |
. . . . . 6
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (absβ((seq1(
+ , πΉ)β(ββπ)) β π)) = (absβ(seq1( + , πΉ)β(ββπ)))) |
101 | | 2fveq3 6852 |
. . . . . . . . . 10
β’ (π¦ = π β (seq1( + , πΉ)β(ββπ¦)) = (seq1( + , πΉ)β(ββπ))) |
102 | 101 | fvoveq1d 7384 |
. . . . . . . . 9
β’ (π¦ = π β (absβ((seq1( + , πΉ)β(ββπ¦)) β π)) = (absβ((seq1( + , πΉ)β(ββπ)) β π))) |
103 | | oveq2 7370 |
. . . . . . . . 9
β’ (π¦ = π β (πΆ / π¦) = (πΆ / π)) |
104 | 102, 103 | breq12d 5123 |
. . . . . . . 8
β’ (π¦ = π β ((absβ((seq1( + , πΉ)β(ββπ¦)) β π)) β€ (πΆ / π¦) β (absβ((seq1( + , πΉ)β(ββπ)) β π)) β€ (πΆ / π))) |
105 | | dchrvmasumif.1 |
. . . . . . . . 9
β’ (π β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π)) β€ (πΆ / π¦)) |
106 | 105 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (3[,)+β)) β βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π)) β€ (πΆ / π¦)) |
107 | | 1re 11162 |
. . . . . . . . . 10
β’ 1 β
β |
108 | | elicopnf 13369 |
. . . . . . . . . 10
β’ (1 β
β β (π β
(1[,)+β) β (π
β β β§ 1 β€ π))) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . 9
β’ (π β (1[,)+β) β
(π β β β§ 1
β€ π)) |
110 | 65, 71, 109 | sylanbrc 584 |
. . . . . . . 8
β’ ((π β§ π β (3[,)+β)) β π β
(1[,)+β)) |
111 | 104, 106,
110 | rspcdva 3585 |
. . . . . . 7
β’ ((π β§ π β (3[,)+β)) β
(absβ((seq1( + , πΉ)β(ββπ)) β π)) β€ (πΆ / π)) |
112 | 111 | adantr 482 |
. . . . . 6
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (absβ((seq1(
+ , πΉ)β(ββπ)) β π)) β€ (πΆ / π)) |
113 | 100, 112 | eqbrtrrd 5134 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (absβ(seq1( +
, πΉ)β(ββπ))) β€ (πΆ / π)) |
114 | | lemul2a 12017 |
. . . . 5
β’
((((absβ(seq1( + , πΉ)β(ββπ))) β β β§ (πΆ / π) β β β§ ((logβπ) β β β§ 0 β€
(logβπ))) β§
(absβ(seq1( + , πΉ)β(ββπ))) β€ (πΆ / π)) β ((logβπ) Β· (absβ(seq1( + , πΉ)β(ββπ)))) β€ ((logβπ) Β· (πΆ / π))) |
115 | 76, 90, 94, 113, 114 | syl31anc 1374 |
. . . 4
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β ((logβπ) Β· (absβ(seq1( + ,
πΉ)β(ββπ)))) β€ ((logβπ) Β· (πΆ / π))) |
116 | | iftrue 4497 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β if(π = 0, π, π) = π) |
117 | 116 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (logβif(π = 0, π, π)) = (logβπ)) |
118 | 117 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (π = 0 β ((logβif(π = 0, π, π)) / π) = ((logβπ) / π)) |
119 | 118 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β ((logβif(π = 0, π, π)) / π) = ((logβπ) / π)) |
120 | 119 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
121 | 16 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β (πβ(πΏβπ)) β β) |
122 | | relogcl 25947 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β (logβπ) β
β) |
123 | 122 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β+) β
(logβπ) β
β) |
124 | 123 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β+) β
(logβπ) β
β) |
125 | 124 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β (logβπ) β
β) |
126 | 11 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β π β β) |
127 | 126 | nncnd 12176 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β π β β) |
128 | 126 | nnne0d 12210 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β π β 0) |
129 | 121, 125,
127, 128 | div12d 11974 |
. . . . . . . . . . 11
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β ((πβ(πΏβπ)) Β· ((logβπ) / π)) = ((logβπ) Β· ((πβ(πΏβπ)) / π))) |
130 | 120, 129 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((((π β§ π β β+) β§ π = 0) β§ π β (1...(ββπ))) β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = ((logβπ) Β· ((πβ(πΏβπ)) / π))) |
131 | 130 | sumeq2dv 15595 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π = 0) β Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = Ξ£π β (1...(ββπ))((logβπ) Β· ((πβ(πΏβπ)) / π))) |
132 | | iftrue 4497 |
. . . . . . . . . . 11
β’ (π = 0 β if(π = 0, 0, π) = 0) |
133 | 132 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = 0 β (Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π)) = (Ξ£π β (1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β 0)) |
134 | 26 | subid1d 11508 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β
(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β 0) = Ξ£π β (1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) |
135 | 133, 134 | sylan9eqr 2799 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π = 0) β (Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π)) = Ξ£π β (1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) |
136 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ ((πβ(πΏβπ)) / π) β V |
137 | 54, 51, 136 | fvmpt 6953 |
. . . . . . . . . . . . 13
β’ (π β β β (πΉβπ) = ((πβ(πΏβπ)) / π)) |
138 | 22, 137 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β (πΉβπ) = ((πβ(πΏβπ)) / π)) |
139 | 57 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β+) β πΉ:ββΆβ) |
140 | 139, 11, 58 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β (πΉβπ) β
β) |
141 | 138, 140 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β ((πβ(πΏβπ)) / π) β β) |
142 | 9, 124, 141 | fsummulc2 15676 |
. . . . . . . . . 10
β’ ((π β§ π β β+) β
((logβπ) Β·
Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) / π)) = Ξ£π β (1...(ββπ))((logβπ) Β· ((πβ(πΏβπ)) / π))) |
143 | 142 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π = 0) β ((logβπ) Β· Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) / π)) = Ξ£π β (1...(ββπ))((logβπ) Β· ((πβ(πΏβπ)) / π))) |
144 | 131, 135,
143 | 3eqtr4d 2787 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π = 0) β (Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π)) = ((logβπ) Β· Ξ£π β (1...(ββπ))((πβ(πΏβπ)) / π))) |
145 | 83, 144 | sylan 581 |
. . . . . . 7
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π)) = ((logβπ) Β· Ξ£π β (1...(ββπ))((πβ(πΏβπ)) / π))) |
146 | 83, 138 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ π β (3[,)+β)) β§ π β
(1...(ββπ)))
β (πΉβπ) = ((πβ(πΏβπ)) / π)) |
147 | 73, 44 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ ((π β§ π β (3[,)+β)) β
(ββπ) β
(β€β₯β1)) |
148 | 77, 11, 50 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π β (3[,)+β)) β§ π β
(1...(ββπ)))
β ((πβ(πΏβπ)) / π) β β) |
149 | 146, 147,
148 | fsumser 15622 |
. . . . . . . . 9
β’ ((π β§ π β (3[,)+β)) β Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) / π) = (seq1( + , πΉ)β(ββπ))) |
150 | 149 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) / π) = (seq1( + , πΉ)β(ββπ))) |
151 | 150 | oveq2d 7378 |
. . . . . . 7
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β ((logβπ) Β· Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) / π)) = ((logβπ) Β· (seq1( + , πΉ)β(ββπ)))) |
152 | 145, 151 | eqtrd 2777 |
. . . . . 6
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π)) = ((logβπ) Β· (seq1( + , πΉ)β(ββπ)))) |
153 | 152 | fveq2d 6851 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) = (absβ((logβπ) Β· (seq1( + , πΉ)β(ββπ))))) |
154 | 122 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π = 0) β (logβπ) β
β) |
155 | 154 | recnd 11190 |
. . . . . . 7
β’ (((π β§ π β β+) β§ π = 0) β (logβπ) β
β) |
156 | 83, 155 | sylan 581 |
. . . . . 6
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (logβπ) β
β) |
157 | 156, 75 | absmuld 15346 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β
(absβ((logβπ)
Β· (seq1( + , πΉ)β(ββπ)))) = ((absβ(logβπ)) Β· (absβ(seq1( +
, πΉ)β(ββπ))))) |
158 | 91, 92 | absidd 15314 |
. . . . . . 7
β’ ((π β§ π β (3[,)+β)) β
(absβ(logβπ)) =
(logβπ)) |
159 | 158 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π β (3[,)+β)) β
((absβ(logβπ))
Β· (absβ(seq1( + , πΉ)β(ββπ)))) = ((logβπ) Β· (absβ(seq1( + , πΉ)β(ββπ))))) |
160 | 159 | adantr 482 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β
((absβ(logβπ))
Β· (absβ(seq1( + , πΉ)β(ββπ)))) = ((logβπ) Β· (absβ(seq1( + , πΉ)β(ββπ))))) |
161 | 153, 157,
160 | 3eqtrd 2781 |
. . . 4
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) = ((logβπ) Β· (absβ(seq1( + , πΉ)β(ββπ))))) |
162 | | iftrue 4497 |
. . . . . . . 8
β’ (π = 0 β if(π = 0, πΆ, πΈ) = πΆ) |
163 | 162 | adantl 483 |
. . . . . . 7
β’ (((π β§ π β β+) β§ π = 0) β if(π = 0, πΆ, πΈ) = πΆ) |
164 | 163 | oveq1d 7377 |
. . . . . 6
β’ (((π β§ π β β+) β§ π = 0) β (if(π = 0, πΆ, πΈ) Β· ((logβπ) / π)) = (πΆ Β· ((logβπ) / π))) |
165 | 86 | recnd 11190 |
. . . . . . . 8
β’ (π β πΆ β β) |
166 | 165 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β+) β§ π = 0) β πΆ β β) |
167 | | rpcnne0 12940 |
. . . . . . . 8
β’ (π β β+
β (π β β
β§ π β
0)) |
168 | 167 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ π β β+) β§ π = 0) β (π β β β§ π β 0)) |
169 | | div12 11842 |
. . . . . . 7
β’ ((πΆ β β β§
(logβπ) β
β β§ (π β
β β§ π β 0))
β (πΆ Β·
((logβπ) / π)) = ((logβπ) Β· (πΆ / π))) |
170 | 166, 155,
168, 169 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π β β+) β§ π = 0) β (πΆ Β· ((logβπ) / π)) = ((logβπ) Β· (πΆ / π))) |
171 | 164, 170 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π β β+) β§ π = 0) β (if(π = 0, πΆ, πΈ) Β· ((logβπ) / π)) = ((logβπ) Β· (πΆ / π))) |
172 | 83, 171 | sylan 581 |
. . . 4
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β (if(π = 0, πΆ, πΈ) Β· ((logβπ) / π)) = ((logβπ) Β· (πΆ / π))) |
173 | 115, 161,
172 | 3brtr4d 5142 |
. . 3
β’ (((π β§ π β (3[,)+β)) β§ π = 0) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) β€ (if(π = 0, πΆ, πΈ) Β· ((logβπ) / π))) |
174 | | dchrvmasumif.2 |
. . . . . 6
β’ (π β βπ¦ β (3[,)+β)(absβ((seq1( + ,
πΎ)β(ββπ¦)) β π)) β€ (πΈ Β· ((logβπ¦) / π¦))) |
175 | | 2fveq3 6852 |
. . . . . . . . 9
β’ (π¦ = π β (seq1( + , πΎ)β(ββπ¦)) = (seq1( + , πΎ)β(ββπ))) |
176 | 175 | fvoveq1d 7384 |
. . . . . . . 8
β’ (π¦ = π β (absβ((seq1( + , πΎ)β(ββπ¦)) β π)) = (absβ((seq1( + , πΎ)β(ββπ)) β π))) |
177 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π¦ = π β (logβπ¦) = (logβπ)) |
178 | | id 22 |
. . . . . . . . . 10
β’ (π¦ = π β π¦ = π) |
179 | 177, 178 | oveq12d 7380 |
. . . . . . . . 9
β’ (π¦ = π β ((logβπ¦) / π¦) = ((logβπ) / π)) |
180 | 179 | oveq2d 7378 |
. . . . . . . 8
β’ (π¦ = π β (πΈ Β· ((logβπ¦) / π¦)) = (πΈ Β· ((logβπ) / π))) |
181 | 176, 180 | breq12d 5123 |
. . . . . . 7
β’ (π¦ = π β ((absβ((seq1( + , πΎ)β(ββπ¦)) β π)) β€ (πΈ Β· ((logβπ¦) / π¦)) β (absβ((seq1( + , πΎ)β(ββπ)) β π)) β€ (πΈ Β· ((logβπ) / π)))) |
182 | 181 | rspccva 3583 |
. . . . . 6
β’
((βπ¦ β
(3[,)+β)(absβ((seq1( + , πΎ)β(ββπ¦)) β π)) β€ (πΈ Β· ((logβπ¦) / π¦)) β§ π β (3[,)+β)) β
(absβ((seq1( + , πΎ)β(ββπ)) β π)) β€ (πΈ Β· ((logβπ) / π))) |
183 | 174, 182 | sylan 581 |
. . . . 5
β’ ((π β§ π β (3[,)+β)) β
(absβ((seq1( + , πΎ)β(ββπ)) β π)) β€ (πΈ Β· ((logβπ) / π))) |
184 | 183 | adantr 482 |
. . . 4
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β
(absβ((seq1( + , πΎ)β(ββπ)) β π)) β€ (πΈ Β· ((logβπ) / π))) |
185 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (logβπ) = (logβπ)) |
186 | 185, 53 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((logβπ) / π) = ((logβπ) / π)) |
187 | 52, 186 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β ((πβ(πΏβπ)) Β· ((logβπ) / π)) = ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
188 | | dchrvmasumif.g |
. . . . . . . . . 10
β’ πΎ = (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
189 | | ovex 7395 |
. . . . . . . . . 10
β’ ((πβ(πΏβπ)) Β· ((logβπ) / π)) β V |
190 | 187, 188,
189 | fvmpt 6953 |
. . . . . . . . 9
β’ (π β β β (πΎβπ) = ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
191 | 11, 190 | syl 17 |
. . . . . . . 8
β’ (π β
(1...(ββπ))
β (πΎβπ) = ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
192 | | ifnefalse 4503 |
. . . . . . . . . . . . 13
β’ (π β 0 β if(π = 0, π, π) = π) |
193 | 192 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π β 0 β
(logβif(π = 0, π, π)) = (logβπ)) |
194 | 193 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π β 0 β
((logβif(π = 0, π, π)) / π) = ((logβπ) / π)) |
195 | 194 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β 0 β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
196 | 195 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
197 | 196 | eqcomd 2743 |
. . . . . . . 8
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β ((πβ(πΏβπ)) Β· ((logβπ) / π)) = ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) |
198 | 191, 197 | sylan9eqr 2799 |
. . . . . . 7
β’ ((((π β§ π β (3[,)+β)) β§ π β 0) β§ π β
(1...(ββπ)))
β (πΎβπ) = ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) |
199 | 147 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β
(ββπ) β
(β€β₯β1)) |
200 | | nnrp 12933 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β+) |
201 | 200 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β+) |
202 | 201 | relogcld 25994 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (logβπ) β
β) |
203 | 202 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (logβπ) β
β) |
204 | 203, 47, 49 | divcld 11938 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((logβπ) / π) β β) |
205 | 15, 204 | mulcld 11182 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πβ(πΏβπ)) Β· ((logβπ) / π)) β β) |
206 | 187 | cbvmptv 5223 |
. . . . . . . . . . . 12
β’ (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) = (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
207 | 188, 206 | eqtri 2765 |
. . . . . . . . . . 11
β’ πΎ = (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
208 | 205, 207 | fmptd 7067 |
. . . . . . . . . 10
β’ (π β πΎ:ββΆβ) |
209 | 208 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β πΎ:ββΆβ) |
210 | | ffvelcdm 7037 |
. . . . . . . . 9
β’ ((πΎ:ββΆβ β§
π β β) β
(πΎβπ) β β) |
211 | 209, 11, 210 | syl2an 597 |
. . . . . . . 8
β’ ((((π β§ π β (3[,)+β)) β§ π β 0) β§ π β
(1...(ββπ)))
β (πΎβπ) β
β) |
212 | 198, 211 | eqeltrrd 2839 |
. . . . . . 7
β’ ((((π β§ π β (3[,)+β)) β§ π β 0) β§ π β
(1...(ββπ)))
β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β β) |
213 | 198, 199,
212 | fsumser 15622 |
. . . . . 6
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) = (seq1( + , πΎ)β(ββπ))) |
214 | | ifnefalse 4503 |
. . . . . . 7
β’ (π β 0 β if(π = 0, 0, π) = π) |
215 | 214 | adantl 483 |
. . . . . 6
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β if(π = 0, 0, π) = π) |
216 | 213, 215 | oveq12d 7380 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β (Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π)) = ((seq1( + , πΎ)β(ββπ)) β π)) |
217 | 216 | fveq2d 6851 |
. . . 4
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) = (absβ((seq1( + , πΎ)β(ββπ)) β π))) |
218 | | ifnefalse 4503 |
. . . . . 6
β’ (π β 0 β if(π = 0, πΆ, πΈ) = πΈ) |
219 | 218 | adantl 483 |
. . . . 5
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β if(π = 0, πΆ, πΈ) = πΈ) |
220 | 219 | oveq1d 7377 |
. . . 4
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β (if(π = 0, πΆ, πΈ) Β· ((logβπ) / π)) = (πΈ Β· ((logβπ) / π))) |
221 | 184, 217,
220 | 3brtr4d 5142 |
. . 3
β’ (((π β§ π β (3[,)+β)) β§ π β 0) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) β€ (if(π = 0, πΆ, πΈ) Β· ((logβπ) / π))) |
222 | 173, 221 | pm2.61dane 3033 |
. 2
β’ ((π β§ π β (3[,)+β)) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) β€ (if(π = 0, πΆ, πΈ) Β· ((logβπ) / π))) |
223 | | fzfid 13885 |
. . . 4
β’ (π β (1...2) β
Fin) |
224 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (1...2)) β π β π·) |
225 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β (1...2) β π β
β€) |
226 | 225 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (1...2)) β π β β€) |
227 | 4, 1, 5, 2, 224, 226 | dchrzrhcl 26609 |
. . . . . 6
β’ ((π β§ π β (1...2)) β (πβ(πΏβπ)) β β) |
228 | 227 | abscld 15328 |
. . . . 5
β’ ((π β§ π β (1...2)) β (absβ(πβ(πΏβπ))) β β) |
229 | | 3rp 12928 |
. . . . . . 7
β’ 3 β
β+ |
230 | | relogcl 25947 |
. . . . . . 7
β’ (3 β
β+ β (logβ3) β β) |
231 | 229, 230 | ax-mp 5 |
. . . . . 6
β’
(logβ3) β β |
232 | | elfznn 13477 |
. . . . . . 7
β’ (π β (1...2) β π β
β) |
233 | 232 | adantl 483 |
. . . . . 6
β’ ((π β§ π β (1...2)) β π β β) |
234 | | nndivre 12201 |
. . . . . 6
β’
(((logβ3) β β β§ π β β) β ((logβ3) /
π) β
β) |
235 | 231, 233,
234 | sylancr 588 |
. . . . 5
β’ ((π β§ π β (1...2)) β ((logβ3) /
π) β
β) |
236 | 228, 235 | remulcld 11192 |
. . . 4
β’ ((π β§ π β (1...2)) β ((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) β
β) |
237 | 223, 236 | fsumrecl 15626 |
. . 3
β’ (π β Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) β
β) |
238 | 43 | abscld 15328 |
. . 3
β’ (π β (absβif(π = 0, 0, π)) β β) |
239 | 237, 238 | readdcld 11191 |
. 2
β’ (π β (Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) + (absβif(π = 0, 0, π))) β β) |
240 | | simpl 484 |
. . . . . . 7
β’ ((π β§ π β (1[,)3)) β π) |
241 | 62 | rexri 11220 |
. . . . . . . . . . 11
β’ 3 β
β* |
242 | | elico2 13335 |
. . . . . . . . . . 11
β’ ((1
β β β§ 3 β β*) β (π β (1[,)3) β (π β β β§ 1 β€ π β§ π < 3))) |
243 | 107, 241,
242 | mp2an 691 |
. . . . . . . . . 10
β’ (π β (1[,)3) β (π β β β§ 1 β€
π β§ π < 3)) |
244 | 243 | simp1bi 1146 |
. . . . . . . . 9
β’ (π β (1[,)3) β π β
β) |
245 | 244 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (1[,)3)) β π β β) |
246 | | 0red 11165 |
. . . . . . . . 9
β’ ((π β§ π β (1[,)3)) β 0 β
β) |
247 | | 1red 11163 |
. . . . . . . . 9
β’ ((π β§ π β (1[,)3)) β 1 β
β) |
248 | | 0lt1 11684 |
. . . . . . . . . 10
β’ 0 <
1 |
249 | 248 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (1[,)3)) β 0 <
1) |
250 | 243 | simp2bi 1147 |
. . . . . . . . . 10
β’ (π β (1[,)3) β 1 β€
π) |
251 | 250 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1[,)3)) β 1 β€ π) |
252 | 246, 247,
245, 249, 251 | ltletrd 11322 |
. . . . . . . 8
β’ ((π β§ π β (1[,)3)) β 0 < π) |
253 | 245, 252 | elrpd 12961 |
. . . . . . 7
β’ ((π β§ π β (1[,)3)) β π β β+) |
254 | 240, 253 | jca 513 |
. . . . . 6
β’ ((π β§ π β (1[,)3)) β (π β§ π β
β+)) |
255 | 43 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β+) β if(π = 0, 0, π) β β) |
256 | 26, 255 | subcld 11519 |
. . . . . 6
β’ ((π β§ π β β+) β
(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π)) β β) |
257 | 254, 256 | syl 17 |
. . . . 5
β’ ((π β§ π β (1[,)3)) β (Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π)) β β) |
258 | 257 | abscld 15328 |
. . . 4
β’ ((π β§ π β (1[,)3)) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) β β) |
259 | 254, 26 | syl 17 |
. . . . . 6
β’ ((π β§ π β (1[,)3)) β Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β β) |
260 | 259 | abscld 15328 |
. . . . 5
β’ ((π β§ π β (1[,)3)) β
(absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
261 | 238 | adantr 482 |
. . . . 5
β’ ((π β§ π β (1[,)3)) β (absβif(π = 0, 0, π)) β β) |
262 | 260, 261 | readdcld 11191 |
. . . 4
β’ ((π β§ π β (1[,)3)) β
((absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) + (absβif(π = 0, 0, π))) β β) |
263 | 237 | adantr 482 |
. . . . 5
β’ ((π β§ π β (1[,)3)) β Ξ£π β
(1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) β
β) |
264 | 263, 261 | readdcld 11191 |
. . . 4
β’ ((π β§ π β (1[,)3)) β (Ξ£π β
(1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) + (absβif(π = 0, 0, π))) β β) |
265 | 26, 255 | abs2dif2d 15350 |
. . . . 5
β’ ((π β§ π β β+) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) β€ ((absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) + (absβif(π = 0, 0, π)))) |
266 | 254, 265 | syl 17 |
. . . 4
β’ ((π β§ π β (1[,)3)) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) β€ ((absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) + (absβif(π = 0, 0, π)))) |
267 | 25 | abscld 15328 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π β
(1...(ββπ)))
β (absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
268 | 9, 267 | fsumrecl 15626 |
. . . . . . 7
β’ ((π β§ π β β+) β
Ξ£π β
(1...(ββπ))(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
269 | 254, 268 | syl 17 |
. . . . . 6
β’ ((π β§ π β (1[,)3)) β Ξ£π β
(1...(ββπ))(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
270 | 9, 25 | fsumabs 15693 |
. . . . . . 7
β’ ((π β§ π β β+) β
(absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ Ξ£π β (1...(ββπ))(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)))) |
271 | 254, 270 | syl 17 |
. . . . . 6
β’ ((π β§ π β (1[,)3)) β
(absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ Ξ£π β (1...(ββπ))(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)))) |
272 | | fzfid 13885 |
. . . . . . . . 9
β’ ((π β§ π β β+) β (1...2)
β Fin) |
273 | 227 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β (1...2)) β (πβ(πΏβπ)) β β) |
274 | 17 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π β (1...2)) β π β
β+) |
275 | 232 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π β (1...2)) β π β
β) |
276 | 275 | nnrpd 12962 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π β (1...2)) β π β
β+) |
277 | 274, 276 | ifcld 4537 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π β (1...2)) β if(π = 0, π, π) β
β+) |
278 | 277 | relogcld 25994 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β (1...2)) β
(logβif(π = 0, π, π)) β β) |
279 | 278, 275 | nndivred 12214 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β (1...2)) β
((logβif(π = 0, π, π)) / π) β β) |
280 | 279 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β (1...2)) β
((logβif(π = 0, π, π)) / π) β β) |
281 | 273, 280 | mulcld 11182 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β (1...2)) β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β β) |
282 | 281 | abscld 15328 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β (1...2)) β
(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
283 | 272, 282 | fsumrecl 15626 |
. . . . . . . 8
β’ ((π β§ π β β+) β
Ξ£π β
(1...2)(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
284 | 254, 283 | syl 17 |
. . . . . . 7
β’ ((π β§ π β (1[,)3)) β Ξ£π β
(1...2)(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
285 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ π β (1[,)3)) β (1...2) β
Fin) |
286 | 254, 281 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β β) |
287 | 286 | abscld 15328 |
. . . . . . . 8
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
288 | 286 | absge0d 15336 |
. . . . . . . 8
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β 0 β€
(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)))) |
289 | 245 | flcld 13710 |
. . . . . . . . . 10
β’ ((π β§ π β (1[,)3)) β (ββπ) β
β€) |
290 | | 2z 12542 |
. . . . . . . . . . 11
β’ 2 β
β€ |
291 | 290 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π β (1[,)3)) β 2 β
β€) |
292 | 243 | simp3bi 1148 |
. . . . . . . . . . . . . 14
β’ (π β (1[,)3) β π < 3) |
293 | 292 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1[,)3)) β π < 3) |
294 | | 3z 12543 |
. . . . . . . . . . . . . 14
β’ 3 β
β€ |
295 | | fllt 13718 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ 3 β
β€) β (π < 3
β (ββπ)
< 3)) |
296 | 245, 294,
295 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1[,)3)) β (π < 3 β (ββπ) < 3)) |
297 | 293, 296 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1[,)3)) β (ββπ) < 3) |
298 | | df-3 12224 |
. . . . . . . . . . . 12
β’ 3 = (2 +
1) |
299 | 297, 298 | breqtrdi 5151 |
. . . . . . . . . . 11
β’ ((π β§ π β (1[,)3)) β (ββπ) < (2 + 1)) |
300 | | rpre 12930 |
. . . . . . . . . . . . . . 15
β’ (π β β+
β π β
β) |
301 | 300 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β+) β π β
β) |
302 | 301 | flcld 13710 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β+) β
(ββπ) β
β€) |
303 | | zleltp1 12561 |
. . . . . . . . . . . . 13
β’
(((ββπ)
β β€ β§ 2 β β€) β ((ββπ) β€ 2 β
(ββπ) < (2 +
1))) |
304 | 302, 290,
303 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ π β β+) β
((ββπ) β€ 2
β (ββπ)
< (2 + 1))) |
305 | 254, 304 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (1[,)3)) β ((ββπ) β€ 2 β
(ββπ) < (2 +
1))) |
306 | 299, 305 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ π β (1[,)3)) β (ββπ) β€ 2) |
307 | | eluz2 12776 |
. . . . . . . . . 10
β’ (2 β
(β€β₯β(ββπ)) β ((ββπ) β β€ β§ 2 β β€ β§
(ββπ) β€
2)) |
308 | 289, 291,
306, 307 | syl3anbrc 1344 |
. . . . . . . . 9
β’ ((π β§ π β (1[,)3)) β 2 β
(β€β₯β(ββπ))) |
309 | | fzss2 13488 |
. . . . . . . . 9
β’ (2 β
(β€β₯β(ββπ)) β (1...(ββπ)) β
(1...2)) |
310 | 308, 309 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (1[,)3)) β
(1...(ββπ))
β (1...2)) |
311 | 285, 287,
288, 310 | fsumless 15688 |
. . . . . . 7
β’ ((π β§ π β (1[,)3)) β Ξ£π β
(1...(ββπ))(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ Ξ£π β (1...2)(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)))) |
312 | 236 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β ((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) β
β) |
313 | 273, 280 | absmuld 15346 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β (1...2)) β
(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) = ((absβ(πβ(πΏβπ))) Β· (absβ((logβif(π = 0, π, π)) / π)))) |
314 | 254, 313 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) = ((absβ(πβ(πΏβπ))) Β· (absβ((logβif(π = 0, π, π)) / π)))) |
315 | 254, 279 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β ((logβif(π = 0, π, π)) / π) β β) |
316 | 254, 278 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (logβif(π = 0, π, π)) β β) |
317 | | log1 25957 |
. . . . . . . . . . . . . 14
β’
(logβ1) = 0 |
318 | | elfzle1 13451 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...2) β 1 β€
π) |
319 | | breq2 5114 |
. . . . . . . . . . . . . . . . 17
β’ (π = if(π = 0, π, π) β (1 β€ π β 1 β€ if(π = 0, π, π))) |
320 | | breq2 5114 |
. . . . . . . . . . . . . . . . 17
β’ (π = if(π = 0, π, π) β (1 β€ π β 1 β€ if(π = 0, π, π))) |
321 | 319, 320 | ifboth 4530 |
. . . . . . . . . . . . . . . 16
β’ ((1 β€
π β§ 1 β€ π) β 1 β€ if(π = 0, π, π)) |
322 | 251, 318,
321 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β 1 β€ if(π = 0, π, π)) |
323 | | 1rp 12926 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β+ |
324 | | logleb 25974 |
. . . . . . . . . . . . . . . . 17
β’ ((1
β β+ β§ if(π = 0, π, π) β β+) β (1 β€
if(π = 0, π, π) β (logβ1) β€
(logβif(π = 0, π, π)))) |
325 | 323, 277,
324 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π β (1...2)) β (1 β€
if(π = 0, π, π) β (logβ1) β€
(logβif(π = 0, π, π)))) |
326 | 254, 325 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (1 β€ if(π = 0, π, π) β (logβ1) β€
(logβif(π = 0, π, π)))) |
327 | 322, 326 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (logβ1) β€
(logβif(π = 0, π, π))) |
328 | 317, 327 | eqbrtrrid 5146 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β 0 β€
(logβif(π = 0, π, π))) |
329 | 276 | rpregt0d 12970 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π β (1...2)) β (π β β β§ 0 <
π)) |
330 | 254, 329 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (π β β β§ 0 < π)) |
331 | | divge0 12031 |
. . . . . . . . . . . . 13
β’
((((logβif(π =
0, π, π)) β β β§ 0 β€
(logβif(π = 0, π, π))) β§ (π β β β§ 0 < π)) β 0 β€
((logβif(π = 0, π, π)) / π)) |
332 | 316, 328,
330, 331 | syl21anc 837 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β 0 β€
((logβif(π = 0, π, π)) / π)) |
333 | 315, 332 | absidd 15314 |
. . . . . . . . . . 11
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β
(absβ((logβif(π
= 0, π, π)) / π)) = ((logβif(π = 0, π, π)) / π)) |
334 | 333, 315 | eqeltrd 2838 |
. . . . . . . . . 10
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β
(absβ((logβif(π
= 0, π, π)) / π)) β β) |
335 | 235 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β ((logβ3) /
π) β
β) |
336 | 228 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β (1...2)) β
(absβ(πβ(πΏβπ))) β β) |
337 | 273 | absge0d 15336 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β (1...2)) β 0 β€
(absβ(πβ(πΏβπ)))) |
338 | 336, 337 | jca 513 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β (1...2)) β
((absβ(πβ(πΏβπ))) β β β§ 0 β€
(absβ(πβ(πΏβπ))))) |
339 | 254, 338 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β ((absβ(πβ(πΏβπ))) β β β§ 0 β€
(absβ(πβ(πΏβπ))))) |
340 | 292 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β π < 3) |
341 | 275 | nnred 12175 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β (1...2)) β π β
β) |
342 | | 2re 12234 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β |
343 | 342 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β (1...2)) β 2 β
β) |
344 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β (1...2)) β 3 β
β) |
345 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...2) β π β€ 2) |
346 | 345 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β (1...2)) β π β€ 2) |
347 | | 2lt3 12332 |
. . . . . . . . . . . . . . . . . 18
β’ 2 <
3 |
348 | 347 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β (1...2)) β 2 <
3) |
349 | 341, 343,
344, 346, 348 | lelttrd 11320 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π β (1...2)) β π < 3) |
350 | 254, 349 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β π < 3) |
351 | | breq1 5113 |
. . . . . . . . . . . . . . . 16
β’ (π = if(π = 0, π, π) β (π < 3 β if(π = 0, π, π) < 3)) |
352 | | breq1 5113 |
. . . . . . . . . . . . . . . 16
β’ (π = if(π = 0, π, π) β (π < 3 β if(π = 0, π, π) < 3)) |
353 | 351, 352 | ifboth 4530 |
. . . . . . . . . . . . . . 15
β’ ((π < 3 β§ π < 3) β if(π = 0, π, π) < 3) |
354 | 340, 350,
353 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β if(π = 0, π, π) < 3) |
355 | 277 | rpred 12964 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π β (1...2)) β if(π = 0, π, π) β β) |
356 | | ltle 11250 |
. . . . . . . . . . . . . . . 16
β’
((if(π = 0, π, π) β β β§ 3 β β)
β (if(π = 0, π, π) < 3 β if(π = 0, π, π) β€ 3)) |
357 | 355, 62, 356 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π β (1...2)) β
(if(π = 0, π, π) < 3 β if(π = 0, π, π) β€ 3)) |
358 | 254, 357 | sylan 581 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (if(π = 0, π, π) < 3 β if(π = 0, π, π) β€ 3)) |
359 | 354, 358 | mpd 15 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β if(π = 0, π, π) β€ 3) |
360 | | logleb 25974 |
. . . . . . . . . . . . . . 15
β’
((if(π = 0, π, π) β β+ β§ 3 β
β+) β (if(π = 0, π, π) β€ 3 β (logβif(π = 0, π, π)) β€ (logβ3))) |
361 | 277, 229,
360 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π β (1...2)) β
(if(π = 0, π, π) β€ 3 β (logβif(π = 0, π, π)) β€ (logβ3))) |
362 | 254, 361 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (if(π = 0, π, π) β€ 3 β (logβif(π = 0, π, π)) β€ (logβ3))) |
363 | 359, 362 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (logβif(π = 0, π, π)) β€ (logβ3)) |
364 | 231 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π β (1...2)) β
(logβ3) β β) |
365 | 278, 364,
276 | lediv1d 13010 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β (1...2)) β
((logβif(π = 0, π, π)) β€ (logβ3) β
((logβif(π = 0, π, π)) / π) β€ ((logβ3) / π))) |
366 | 254, 365 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β ((logβif(π = 0, π, π)) β€ (logβ3) β
((logβif(π = 0, π, π)) / π) β€ ((logβ3) / π))) |
367 | 363, 366 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β ((logβif(π = 0, π, π)) / π) β€ ((logβ3) / π)) |
368 | 333, 367 | eqbrtrd 5132 |
. . . . . . . . . 10
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β
(absβ((logβif(π
= 0, π, π)) / π)) β€ ((logβ3) / π)) |
369 | | lemul2a 12017 |
. . . . . . . . . 10
β’
((((absβ((logβif(π = 0, π, π)) / π)) β β β§ ((logβ3) /
π) β β β§
((absβ(πβ(πΏβπ))) β β β§ 0 β€
(absβ(πβ(πΏβπ))))) β§ (absβ((logβif(π = 0, π, π)) / π)) β€ ((logβ3) / π)) β ((absβ(πβ(πΏβπ))) Β· (absβ((logβif(π = 0, π, π)) / π))) β€ ((absβ(πβ(πΏβπ))) Β· ((logβ3) / π))) |
370 | 334, 335,
339, 368, 369 | syl31anc 1374 |
. . . . . . . . 9
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β ((absβ(πβ(πΏβπ))) Β· (absβ((logβif(π = 0, π, π)) / π))) β€ ((absβ(πβ(πΏβπ))) Β· ((logβ3) / π))) |
371 | 314, 370 | eqbrtrd 5132 |
. . . . . . . 8
β’ (((π β§ π β (1[,)3)) β§ π β (1...2)) β (absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ ((absβ(πβ(πΏβπ))) Β· ((logβ3) / π))) |
372 | 285, 287,
312, 371 | fsumle 15691 |
. . . . . . 7
β’ ((π β§ π β (1[,)3)) β Ξ£π β
(1...2)(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π))) |
373 | 269, 284,
263, 311, 372 | letrd 11319 |
. . . . . 6
β’ ((π β§ π β (1[,)3)) β Ξ£π β
(1...(ββπ))(absβ((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π))) |
374 | 260, 269,
263, 271, 373 | letrd 11319 |
. . . . 5
β’ ((π β§ π β (1[,)3)) β
(absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π))) |
375 | 26 | abscld 15328 |
. . . . . . 7
β’ ((π β§ π β β+) β
(absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β β) |
376 | 237 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β+) β
Ξ£π β
(1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) β
β) |
377 | 255 | abscld 15328 |
. . . . . . 7
β’ ((π β§ π β β+) β
(absβif(π = 0, 0,
π)) β
β) |
378 | 375, 376,
377 | leadd1d 11756 |
. . . . . 6
β’ ((π β§ π β β+) β
((absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) β
((absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) + (absβif(π = 0, 0, π))) β€ (Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) + (absβif(π = 0, 0, π))))) |
379 | 254, 378 | syl 17 |
. . . . 5
β’ ((π β§ π β (1[,)3)) β
((absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) β€ Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) β
((absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) + (absβif(π = 0, 0, π))) β€ (Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) + (absβif(π = 0, 0, π))))) |
380 | 374, 379 | mpbid 231 |
. . . 4
β’ ((π β§ π β (1[,)3)) β
((absβΞ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π))) + (absβif(π = 0, 0, π))) β€ (Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) + (absβif(π = 0, 0, π)))) |
381 | 258, 262,
264, 266, 380 | letrd 11319 |
. . 3
β’ ((π β§ π β (1[,)3)) β
(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) β€ (Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) + (absβif(π = 0, 0, π)))) |
382 | 381 | ralrimiva 3144 |
. 2
β’ (π β βπ β (1[,)3)(absβ(Ξ£π β
(1...(ββπ))((πβ(πΏβπ)) Β· ((logβif(π = 0, π, π)) / π)) β if(π = 0, 0, π))) β€ (Ξ£π β (1...2)((absβ(πβ(πΏβπ))) Β· ((logβ3) / π)) + (absβif(π = 0, 0, π)))) |
383 | 1, 2, 3, 4, 5, 6, 7, 8, 26, 34, 37, 43, 222, 239, 382 | dchrvmasumlem3 26863 |
1
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (Ξ£π β (1...(ββ(π₯ / π)))((πβ(πΏβπ)) Β· ((logβif(π = 0, (π₯ / π), π)) / π)) β if(π = 0, 0, π)))) β π(1)) |