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 7420 |
. . 3
β’ (π = π₯ β (1 / π) = (1 / π₯)) |
10 | | 1nn 12228 |
. . . 4
β’ 1 β
β |
11 | 10 | a1i 11 |
. . 3
β’ (π β 1 β
β) |
12 | | rpreccl 13005 |
. . . . 5
β’ (π β β+
β (1 / π) β
β+) |
13 | 12 | adantl 481 |
. . . 4
β’ ((π β§ π β β+) β (1 /
π) β
β+) |
14 | 13 | rpred 13021 |
. . 3
β’ ((π β§ π β β+) β (1 /
π) β
β) |
15 | | simp3r 1201 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β π β€ π₯) |
16 | | rpregt0 12993 |
. . . . . 6
β’ (π β β+
β (π β β
β§ 0 < π)) |
17 | | rpregt0 12993 |
. . . . . 6
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
18 | | lerec 12102 |
. . . . . 6
β’ (((π β β β§ 0 <
π) β§ (π₯ β β β§ 0 <
π₯)) β (π β€ π₯ β (1 / π₯) β€ (1 / π))) |
19 | 16, 17, 18 | syl2an 595 |
. . . . 5
β’ ((π β β+
β§ π₯ β
β+) β (π β€ π₯ β (1 / π₯) β€ (1 / π))) |
20 | 19 | 3ad2ant2 1133 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (π β€ π₯ β (1 / π₯) β€ (1 / π))) |
21 | 15, 20 | mpbid 231 |
. . 3
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (1 β€ π β§ π β€ π₯)) β (1 / π₯) β€ (1 / π)) |
22 | | ax-1cn 11172 |
. . . 4
β’ 1 β
β |
23 | | divrcnv 15803 |
. . . 4
β’ (1 β
β β (π β
β+ β¦ (1 / π)) βπ
0) |
24 | 22, 23 | mp1i 13 |
. . 3
β’ (π β (π β β+ β¦ (1 /
π))
βπ 0) |
25 | | 2fveq3 6896 |
. . . . 5
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
26 | | oveq2 7420 |
. . . . 5
β’ (π = π β (1 / π) = (1 / π)) |
27 | 25, 26 | oveq12d 7430 |
. . . 4
β’ (π = π β ((πβ(πΏβπ)) Β· (1 / π)) = ((πβ(πΏβπ)) Β· (1 / π))) |
28 | 27 | cbvmptv 5261 |
. . 3
β’ (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))) = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))) |
29 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 11,
14, 21, 24, 28 | dchrisum 27232 |
. 2
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯)))) |
30 | 7 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β π·) |
31 | | nnz 12584 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
32 | 31 | adantl 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β€) |
33 | 4, 1, 5, 2, 30, 32 | dchrzrhcl 26985 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
34 | | nncn 12225 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
35 | 34 | adantl 481 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β) |
36 | | nnne0 12251 |
. . . . . . . . . . . 12
β’ (π β β β π β 0) |
37 | 36 | adantl 481 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β 0) |
38 | 33, 35, 37 | divrecd 11998 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) Β· (1 / π))) |
39 | 38 | mpteq2dva 5248 |
. . . . . . . . 9
β’ (π β (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) |
40 | | dchrisumn0.f |
. . . . . . . . . 10
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
41 | | id 22 |
. . . . . . . . . . . 12
β’ (π = π β π = π) |
42 | 25, 41 | oveq12d 7430 |
. . . . . . . . . . 11
β’ (π = π β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) / π)) |
43 | 42 | cbvmptv 5261 |
. . . . . . . . . 10
β’ (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) / π)) |
44 | 40, 43 | eqtri 2759 |
. . . . . . . . 9
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
45 | 39, 44, 28 | 3eqtr4g 2796 |
. . . . . . . 8
β’ (π β πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) |
46 | 45 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β (0[,)+β)) β πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) |
47 | 46 | seqeq3d 13979 |
. . . . . 6
β’ ((π β§ π β (0[,)+β)) β seq1( + ,
πΉ) = seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))) |
48 | 47 | breq1d 5158 |
. . . . 5
β’ ((π β§ π β (0[,)+β)) β (seq1( + ,
πΉ) β π‘ β seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘)) |
49 | | 2fveq3 6896 |
. . . . . . . . 9
β’ (π¦ = π₯ β (seq1( + , πΉ)β(ββπ¦)) = (seq1( + , πΉ)β(ββπ₯))) |
50 | 49 | fvoveq1d 7434 |
. . . . . . . 8
β’ (π¦ = π₯ β (absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) = (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘))) |
51 | | oveq2 7420 |
. . . . . . . 8
β’ (π¦ = π₯ β (π / π¦) = (π / π₯)) |
52 | 50, 51 | breq12d 5161 |
. . . . . . 7
β’ (π¦ = π₯ β ((absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦) β (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π / π₯))) |
53 | 52 | cbvralvw 3233 |
. . . . . 6
β’
(βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦) β βπ₯ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ₯)) β π‘)) β€ (π / π₯)) |
54 | 45 | seqeq3d 13979 |
. . . . . . . . . . 11
β’ (π β seq1( + , πΉ) = seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))) |
55 | 54 | fveq1d 6893 |
. . . . . . . . . 10
β’ (π β (seq1( + , πΉ)β(ββπ₯)) = (seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯))) |
56 | 55 | fvoveq1d 7434 |
. . . . . . . . 9
β’ (π β (absβ((seq1( + ,
πΉ)β(ββπ₯)) β π‘)) = (absβ((seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘))) |
57 | 56 | ad2antrr 723 |
. . . . . . . 8
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) = (absβ((seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘))) |
58 | | elrege0 13436 |
. . . . . . . . . . . 12
β’ (π β (0[,)+β) β
(π β β β§ 0
β€ π)) |
59 | 58 | simplbi 497 |
. . . . . . . . . . 11
β’ (π β (0[,)+β) β
π β
β) |
60 | 59 | recnd 11247 |
. . . . . . . . . 10
β’ (π β (0[,)+β) β
π β
β) |
61 | 60 | ad2antlr 724 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π β
β) |
62 | | 1re 11219 |
. . . . . . . . . . . . 13
β’ 1 β
β |
63 | | elicopnf 13427 |
. . . . . . . . . . . . 13
β’ (1 β
β β (π₯ β
(1[,)+β) β (π₯
β β β§ 1 β€ π₯))) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (π₯ β (1[,)+β) β
(π₯ β β β§ 1
β€ π₯)) |
65 | 64 | simplbi 497 |
. . . . . . . . . . 11
β’ (π₯ β (1[,)+β) β
π₯ β
β) |
66 | 65 | adantl 481 |
. . . . . . . . . 10
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π₯ β
β) |
67 | 66 | recnd 11247 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π₯ β
β) |
68 | | 0red 11222 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
β β) |
69 | | 1red 11220 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 1
β β) |
70 | | 0lt1 11741 |
. . . . . . . . . . . 12
β’ 0 <
1 |
71 | 70 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
< 1) |
72 | 64 | simprbi 496 |
. . . . . . . . . . . 12
β’ (π₯ β (1[,)+β) β 1
β€ π₯) |
73 | 72 | adantl 481 |
. . . . . . . . . . 11
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 1
β€ π₯) |
74 | 68, 69, 66, 71, 73 | ltletrd 11379 |
. . . . . . . . . 10
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β 0
< π₯) |
75 | 74 | gt0ne0d 11783 |
. . . . . . . . 9
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
π₯ β 0) |
76 | 61, 67, 75 | divrecd 11998 |
. . . . . . . 8
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
(π / π₯) = (π Β· (1 / π₯))) |
77 | 57, 76 | breq12d 5161 |
. . . . . . 7
β’ (((π β§ π β (0[,)+β)) β§ π₯ β (1[,)+β)) β
((absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π / π₯) β (absβ((seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯)))) |
78 | 77 | ralbidva 3174 |
. . . . . 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 630 |
. . . 4
β’ ((π β§ π β (0[,)+β)) β ((seq1( + ,
πΉ) β π‘ β§ βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦)) β (seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯))))) |
81 | 80 | rexbidva 3175 |
. . 3
β’ (π β (βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦)) β βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) Β· (1 / π)))) β π‘ β§ βπ₯ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) Β· (1 / π))))β(ββπ₯)) β π‘)) β€ (π Β· (1 / π₯))))) |
82 | 81 | exbidv 1923 |
. 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( + ,
πΉ)β(ββπ¦)) β π‘)) β€ (π / π¦))) |