Step | Hyp | Ref
| Expression |
1 | | rpvmasum.z |
. . 3
β’ π =
(β€/nβ€βπ) |
2 | | rpvmasum.l |
. . 3
β’ πΏ = (β€RHomβπ) |
3 | | rpvmasum.a |
. . 3
β’ (π β π β β) |
4 | | rpvmasum.g |
. . 3
β’ πΊ = (DChrβπ) |
5 | | rpvmasum.d |
. . 3
β’ π· = (BaseβπΊ) |
6 | | rpvmasum.1 |
. . 3
β’ 1 =
(0gβπΊ) |
7 | | dchrisum.b |
. . 3
β’ (π β π β π·) |
8 | | dchrisum.n1 |
. . 3
β’ (π β π β 1 ) |
9 | | eqid 2737 |
. . 3
β’ (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) = (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | dchrvmasumlema 26864 |
. 2
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦)))) |
11 | 3 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β π β β) |
12 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β π β π·) |
13 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β π β 1 ) |
14 | | dchrvmasumif.f |
. . . . 5
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
15 | | dchrvmasumif.c |
. . . . . 6
β’ (π β πΆ β (0[,)+β)) |
16 | 15 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β πΆ β (0[,)+β)) |
17 | | dchrvmasumif.s |
. . . . . 6
β’ (π β seq1( + , πΉ) β π) |
18 | 17 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β seq1( + , πΉ) β π) |
19 | | dchrvmasumif.1 |
. . . . . 6
β’ (π β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π)) β€ (πΆ / π¦)) |
20 | 19 | adantr 482 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π)) β€ (πΆ / π¦)) |
21 | | simprl 770 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β π β (0[,)+β)) |
22 | | simprrl 780 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘) |
23 | | simprrr 781 |
. . . . 5
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))) |
24 | 1, 2, 11, 4, 5, 6,
12, 13, 14, 16, 18, 20, 9, 21, 22, 23 | dchrvmasumiflem2 26866 |
. . . 4
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))))) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π = 0, (logβπ₯), 0))) β π(1)) |
25 | 24 | rexlimdvaa 3154 |
. . 3
β’ (π β (βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π = 0, (logβπ₯), 0))) β
π(1))) |
26 | 25 | exlimdv 1937 |
. 2
β’ (π β (βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π)))) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· ((logβπ) / π))))β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π = 0, (logβπ₯), 0))) β
π(1))) |
27 | 10, 26 | mpd 15 |
1
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π = 0, (logβπ₯), 0))) β π(1)) |