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 | | oveq2 7370 |
. . 3
β’ (π = π₯ β (1 / π) = (1 / π₯)) |
10 | | 1nn 12171 |
. . . 4
β’ 1 β
β |
11 | 10 | a1i 11 |
. . 3
β’ (π β 1 β
β) |
12 | | rpreccl 12948 |
. . . . 5
β’ (π β β+
β (1 / π) β
β+) |
13 | 12 | adantl 483 |
. . . 4
β’ ((π β§ π β β+) β (1 /
π) β
β+) |
14 | 13 | rpred 12964 |
. . 3
β’ ((π β§ π β β+) β (1 /
π) β
β) |
15 | | simp3r 1203 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β π β€ π₯) |
16 | | rpregt0 12936 |
. . . . . 6
β’ (π β β+
β (π β β
β§ 0 < π)) |
17 | | rpregt0 12936 |
. . . . . 6
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
18 | | lerec 12045 |
. . . . . 6
β’ (((π β β β§ 0 <
π) β§ (π₯ β β β§ 0 <
π₯)) β (π β€ π₯ β (1 / π₯) β€ (1 / π))) |
19 | 16, 17, 18 | syl2an 597 |
. . . . 5
β’ ((π β β+
β§ π₯ β
β+) β (π β€ π₯ β (1 / π₯) β€ (1 / π))) |
20 | 19 | 3ad2ant2 1135 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (π β€ π₯ β (1 / π₯) β€ (1 / π))) |
21 | 15, 20 | mpbid 231 |
. . 3
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (1 / π₯) β€ (1 / π)) |
22 | | ax-1cn 11116 |
. . . 4
β’ 1 β
β |
23 | | divrcnv 15744 |
. . . 4
β’ (1 β
β β (π β
β+ β¦ (1 / π)) βπ
0) |
24 | 22, 23 | mp1i 13 |
. . 3
β’ (π β (π β β+ β¦ (1 /
π))
βπ 0) |
25 | | 2fveq3 6852 |
. . . . 5
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
26 | | oveq2 7370 |
. . . . 5
β’ (π = π β (1 / π) = (1 / π)) |
27 | 25, 26 | oveq12d 7380 |
. . . 4
β’ (π = π β ((πβ(πΏβπ)) Β· (1 / π)) = ((πβ(πΏβπ)) Β· (1 / π))) |
28 | 27 | cbvmptv 5223 |
. . 3
β’ (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))) = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))) |
29 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 11,
14, 21, 24, 28 | dchrisum 26856 |
. 2
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯)))) |
30 | 7 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β π·) |
31 | | nnz 12527 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
32 | 31 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β€) |
33 | 4, 1, 5, 2, 30, 32 | dchrzrhcl 26609 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
34 | | nncn 12168 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
35 | 34 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β) |
36 | | nnne0 12194 |
. . . . . . . . . . . 12
β’ (π β β β π β 0) |
37 | 36 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β 0) |
38 | 33, 35, 37 | divrecd 11941 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) Β· (1 / π))) |
39 | 38 | mpteq2dva 5210 |
. . . . . . . . 9
β’ (π β (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) |
40 | | dchrisumn0.f |
. . . . . . . . . 10
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
41 | | id 22 |
. . . . . . . . . . . 12
β’ (π = π β π = π) |
42 | 25, 41 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) / π)) |
43 | 42 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) / π)) |
44 | 40, 43 | eqtri 2765 |
. . . . . . . . 9
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
45 | 39, 44, 28 | 3eqtr4g 2802 |
. . . . . . . 8
β’ (π β πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) |
46 | 45 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0[,)+β)) β πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) |
47 | 46 | seqeq3d 13921 |
. . . . . 6
β’ ((π β§ π β (0[,)+β)) β seq1( + ,
πΉ) = seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))) |
48 | 47 | breq1d 5120 |
. . . . 5
β’ ((π β§ π β (0[,)+β)) β (seq1( + ,
πΉ) β π‘ β seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘)) |
49 | | 2fveq3 6852 |
. . . . . . . . 9
β’ (π¦ = π₯ β (seq1( + , πΉ)β(ββπ¦)) = (seq1( + , πΉ)β(ββπ₯))) |
50 | 49 | fvoveq1d 7384 |
. . . . . . . 8
β’ (π¦ = π₯ β (absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) = (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘))) |
51 | | oveq2 7370 |
. . . . . . . 8
β’ (π¦ = π₯ β (π / π¦) = (π / π₯)) |
52 | 50, 51 | breq12d 5123 |
. . . . . . 7
β’ (π¦ = π₯ β ((absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦) β (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π / π₯))) |
53 | 52 | cbvralvw 3228 |
. . . . . 6
β’
(βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦) β βπ₯ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ₯)) β π‘)) β€ (π / π₯)) |
54 | 45 | seqeq3d 13921 |
. . . . . . . . . . 11
β’ (π β seq1( + , πΉ) = seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))) |
55 | 54 | fveq1d 6849 |
. . . . . . . . . 10
β’ (π β (seq1( + , πΉ)β(ββπ₯)) = (seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯))) |
56 | 55 | fvoveq1d 7384 |
. . . . . . . . 9
β’ (π β (absβ((seq1( + ,
πΉ)β(ββπ₯)) β π‘)) = (absβ((seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘))) |
57 | 56 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) = (absβ((seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘))) |
58 | | elrege0 13378 |
. . . . . . . . . . . 12
β’ (π β (0[,)+β) β
(π β β β§ 0
β€ π)) |
59 | 58 | simplbi 499 |
. . . . . . . . . . 11
β’ (π β (0[,)+β) β
π β
β) |
60 | 59 | recnd 11190 |
. . . . . . . . . 10
β’ (π β (0[,)+β) β
π β
β) |
61 | 60 | ad2antlr 726 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π β
β) |
62 | | 1re 11162 |
. . . . . . . . . . . . 13
β’ 1 β
β |
63 | | elicopnf 13369 |
. . . . . . . . . . . . 13
β’ (1 β
β β (π₯ β
(1[,)+β) β (π₯
β β β§ 1 β€ π₯))) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (π₯ β (1[,)+β) β
(π₯ β β β§ 1
β€ π₯)) |
65 | 64 | simplbi 499 |
. . . . . . . . . . 11
β’ (π₯ β (1[,)+β) β
π₯ β
β) |
66 | 65 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π₯ β
β) |
67 | 66 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π₯ β
β) |
68 | | 0red 11165 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
β β) |
69 | | 1red 11163 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 1
β β) |
70 | | 0lt1 11684 |
. . . . . . . . . . . 12
β’ 0 <
1 |
71 | 70 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
< 1) |
72 | 64 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π₯ β (1[,)+β) β 1
β€ π₯) |
73 | 72 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 1
β€ π₯) |
74 | 68, 69, 66, 71, 73 | ltletrd 11322 |
. . . . . . . . . 10
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
< π₯) |
75 | 74 | gt0ne0d 11726 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π₯ β 0) |
76 | 61, 67, 75 | divrecd 11941 |
. . . . . . . 8
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(π / π₯) = (π Β· (1 / π₯))) |
77 | 57, 76 | breq12d 5123 |
. . . . . . 7
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
((absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π / π₯) β (absβ((seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯)))) |
78 | 77 | ralbidva 3173 |
. . . . . 6
β’ ((π β§ π β (0[,)+β)) β (βπ₯ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π / π₯) β βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯)))) |
79 | 53, 78 | bitrid 283 |
. . . . 5
β’ ((π β§ π β (0[,)+β)) β (βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦) β βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯)))) |
80 | 48, 79 | anbi12d 632 |
. . . 4
β’ ((π β§ π β (0[,)+β)) β ((seq1( + ,
πΉ) β π‘ β§ βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦)) β (seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯))))) |
81 | 80 | rexbidva 3174 |
. . 3
β’ (π β (βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦)) β βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯))))) |
82 | 81 | exbidv 1925 |
. 2
β’ (π β (βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦)) β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯))))) |
83 | 29, 82 | mpbird 257 |
1
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦))) |