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 | | fveq2 6847 |
. . . 4
β’ (π = π₯ β (logβπ) = (logβπ₯)) |
10 | | id 22 |
. . . 4
β’ (π = π₯ β π = π₯) |
11 | 9, 10 | oveq12d 7380 |
. . 3
β’ (π = π₯ β ((logβπ) / π) = ((logβπ₯) / π₯)) |
12 | | 3nn 12239 |
. . . 4
β’ 3 β
β |
13 | 12 | a1i 11 |
. . 3
β’ (π β 3 β
β) |
14 | | relogcl 25947 |
. . . . 5
β’ (π β β+
β (logβπ) β
β) |
15 | | rerpdivcl 12952 |
. . . . 5
β’
(((logβπ)
β β β§ π
β β+) β ((logβπ) / π) β β) |
16 | 14, 15 | mpancom 687 |
. . . 4
β’ (π β β+
β ((logβπ) /
π) β
β) |
17 | 16 | adantl 483 |
. . 3
β’ ((π β§ π β β+) β
((logβπ) / π) β
β) |
18 | | simp3r 1203 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β π β€ π₯) |
19 | | simp2l 1200 |
. . . . . 6
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β π β β+) |
20 | 19 | rpred 12964 |
. . . . 5
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β π β β) |
21 | | ere 15978 |
. . . . . . 7
β’ e β
β |
22 | 21 | a1i 11 |
. . . . . 6
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β e β β) |
23 | | 3re 12240 |
. . . . . . 7
β’ 3 β
β |
24 | 23 | a1i 11 |
. . . . . 6
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β 3 β β) |
25 | | egt2lt3 16095 |
. . . . . . . . 9
β’ (2 < e
β§ e < 3) |
26 | 25 | simpri 487 |
. . . . . . . 8
β’ e <
3 |
27 | 21, 23, 26 | ltleii 11285 |
. . . . . . 7
β’ e β€
3 |
28 | 27 | a1i 11 |
. . . . . 6
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β e β€ 3) |
29 | | simp3l 1202 |
. . . . . 6
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β 3 β€ π) |
30 | 22, 24, 20, 28, 29 | letrd 11319 |
. . . . 5
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β e β€ π) |
31 | | simp2r 1201 |
. . . . . 6
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β π₯ β β+) |
32 | 31 | rpred 12964 |
. . . . 5
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β π₯ β β) |
33 | 22, 20, 32, 30, 18 | letrd 11319 |
. . . . 5
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β e β€ π₯) |
34 | | logdivle 25993 |
. . . . 5
β’ (((π β β β§ e β€
π) β§ (π₯ β β β§ e β€
π₯)) β (π β€ π₯ β ((logβπ₯) / π₯) β€ ((logβπ) / π))) |
35 | 20, 30, 32, 33, 34 | syl22anc 838 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β (π β€ π₯ β ((logβπ₯) / π₯) β€ ((logβπ) / π))) |
36 | 18, 35 | mpbid 231 |
. . 3
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (3 β€ π β§ π β€ π₯)) β ((logβπ₯) / π₯) β€ ((logβπ) / π)) |
37 | | rpcn 12932 |
. . . . . . 7
β’ (π β β+
β π β
β) |
38 | 37 | cxp1d 26077 |
. . . . . 6
β’ (π β β+
β (πβπ1) = π) |
39 | 38 | oveq2d 7378 |
. . . . 5
β’ (π β β+
β ((logβπ) /
(πβπ1)) =
((logβπ) / π)) |
40 | 39 | mpteq2ia 5213 |
. . . 4
β’ (π β β+
β¦ ((logβπ) /
(πβπ1))) = (π β β+
β¦ ((logβπ) /
π)) |
41 | | 1rp 12926 |
. . . . 5
β’ 1 β
β+ |
42 | | cxploglim 26343 |
. . . . 5
β’ (1 β
β+ β (π β β+ β¦
((logβπ) / (πβπ1)))
βπ 0) |
43 | 41, 42 | mp1i 13 |
. . . 4
β’ (π β (π β β+ β¦
((logβπ) / (πβπ1)))
βπ 0) |
44 | 40, 43 | eqbrtrrid 5146 |
. . 3
β’ (π β (π β β+ β¦
((logβπ) / π)) βπ
0) |
45 | | dchrvmasumlema.f |
. . . 4
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
46 | | 2fveq3 6852 |
. . . . . 6
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
47 | | fveq2 6847 |
. . . . . . 7
β’ (π = π β (logβπ) = (logβπ)) |
48 | | id 22 |
. . . . . . 7
β’ (π = π β π = π) |
49 | 47, 48 | oveq12d 7380 |
. . . . . 6
β’ (π = π β ((logβπ) / π) = ((logβπ) / π)) |
50 | 46, 49 | oveq12d 7380 |
. . . . 5
β’ (π = π β ((πβ(πΏβπ)) Β· ((logβπ) / π)) = ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
51 | 50 | cbvmptv 5223 |
. . . 4
β’ (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) = (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
52 | 45, 51 | eqtri 2765 |
. . 3
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· ((logβπ) / π))) |
53 | 1, 2, 3, 4, 5, 6, 7, 8, 11, 13, 17, 36, 44, 52 | dchrisum 26856 |
. 2
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ₯ β (3[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ₯)) β π‘)) β€ (π Β· ((logβπ₯) / π₯)))) |
54 | | 2fveq3 6852 |
. . . . . . . 8
β’ (π₯ = π¦ β (seq1( + , πΉ)β(ββπ₯)) = (seq1( + , πΉ)β(ββπ¦))) |
55 | 54 | fvoveq1d 7384 |
. . . . . . 7
β’ (π₯ = π¦ β (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) = (absβ((seq1( + , πΉ)β(ββπ¦)) β π‘))) |
56 | | fveq2 6847 |
. . . . . . . . 9
β’ (π₯ = π¦ β (logβπ₯) = (logβπ¦)) |
57 | | id 22 |
. . . . . . . . 9
β’ (π₯ = π¦ β π₯ = π¦) |
58 | 56, 57 | oveq12d 7380 |
. . . . . . . 8
β’ (π₯ = π¦ β ((logβπ₯) / π₯) = ((logβπ¦) / π¦)) |
59 | 58 | oveq2d 7378 |
. . . . . . 7
β’ (π₯ = π¦ β (π Β· ((logβπ₯) / π₯)) = (π Β· ((logβπ¦) / π¦))) |
60 | 55, 59 | breq12d 5123 |
. . . . . 6
β’ (π₯ = π¦ β ((absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· ((logβπ₯) / π₯)) β (absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦)))) |
61 | 60 | cbvralvw 3228 |
. . . . 5
β’
(βπ₯ β
(3[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· ((logβπ₯) / π₯)) β βπ¦ β (3[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦))) |
62 | 61 | anbi2i 624 |
. . . 4
β’ ((seq1( +
, πΉ) β π‘ β§ βπ₯ β
(3[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· ((logβπ₯) / π₯))) β (seq1( + , πΉ) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦)))) |
63 | 62 | rexbii 3098 |
. . 3
β’
(βπ β
(0[,)+β)(seq1( + , πΉ)
β π‘ β§
βπ₯ β
(3[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· ((logβπ₯) / π₯))) β βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦)))) |
64 | 63 | exbii 1851 |
. 2
β’
(βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ₯ β (3[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ₯)) β π‘)) β€ (π Β· ((logβπ₯) / π₯))) β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦)))) |
65 | 53, 64 | sylib 217 |
1
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (3[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π Β· ((logβπ¦) / π¦)))) |