Step | Hyp | Ref
| Expression |
1 | | rpssre 12929 |
. . . 4
β’
β+ β β |
2 | | ax-1cn 11116 |
. . . 4
β’ 1 β
β |
3 | | o1const 15509 |
. . . 4
β’
((β+ β β β§ 1 β β) β
(π₯ β
β+ β¦ 1) β π(1)) |
4 | 1, 2, 3 | mp2an 691 |
. . 3
β’ (π₯ β β+
β¦ 1) β π(1) |
5 | 4 | a1i 11 |
. 2
β’ (π β (π₯ β β+ β¦ 1) β
π(1)) |
6 | 2 | a1i 11 |
. . 3
β’ ((π β§ π₯ β β+) β 1 β
β) |
7 | | fzfid 13885 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
8 | | rpvmasum.g |
. . . . . . 7
β’ πΊ = (DChrβπ) |
9 | | rpvmasum.z |
. . . . . . 7
β’ π =
(β€/nβ€βπ) |
10 | | rpvmasum.d |
. . . . . . 7
β’ π· = (BaseβπΊ) |
11 | | rpvmasum.l |
. . . . . . 7
β’ πΏ = (β€RHomβπ) |
12 | | dchrisum.b |
. . . . . . . 8
β’ (π β π β π·) |
13 | 12 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β π·) |
14 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β
(1...(ββπ₯))
β π β
β€) |
15 | 14 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β€) |
16 | 8, 9, 10, 11, 13, 15 | dchrzrhcl 26609 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πβ(πΏβπ)) β β) |
17 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ₯))
β π β
β) |
18 | 17 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
19 | | mucl 26506 |
. . . . . . . . . 10
β’ (π β β β
(ΞΌβπ) β
β€) |
20 | 19 | zred 12614 |
. . . . . . . . 9
β’ (π β β β
(ΞΌβπ) β
β) |
21 | | nndivre 12201 |
. . . . . . . . 9
β’
(((ΞΌβπ)
β β β§ π
β β) β ((ΞΌβπ) / π) β β) |
22 | 20, 21 | mpancom 687 |
. . . . . . . 8
β’ (π β β β
((ΞΌβπ) / π) β
β) |
23 | 18, 22 | syl 17 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
24 | 23 | recnd 11190 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
25 | 16, 24 | mulcld 11182 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) β β) |
26 | 7, 25 | fsumcl 15625 |
. . . 4
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) β β) |
27 | | dchrisumn0.t |
. . . . . 6
β’ (π β seq1( + , πΉ) β π) |
28 | | climcl 15388 |
. . . . . 6
β’ (seq1( +
, πΉ) β π β π β β) |
29 | 27, 28 | syl 17 |
. . . . 5
β’ (π β π β β) |
30 | 29 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β β+) β π β
β) |
31 | 26, 30 | mulcld 11182 |
. . 3
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π) β β) |
32 | 1 | a1i 11 |
. . . 4
β’ (π β β+
β β) |
33 | | subcl 11407 |
. . . . 5
β’ ((1
β β β§ (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π) β β) β (1 β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π)) β β) |
34 | 2, 31, 33 | sylancr 588 |
. . . 4
β’ ((π β§ π₯ β β+) β (1
β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π)) β β) |
35 | | 1red 11163 |
. . . 4
β’ (π β 1 β
β) |
36 | | dchrisumn0.c |
. . . . . 6
β’ (π β πΆ β (0[,)+β)) |
37 | | elrege0 13378 |
. . . . . 6
β’ (πΆ β (0[,)+β) β
(πΆ β β β§ 0
β€ πΆ)) |
38 | 36, 37 | sylib 217 |
. . . . 5
β’ (π β (πΆ β β β§ 0 β€ πΆ)) |
39 | 38 | simpld 496 |
. . . 4
β’ (π β πΆ β β) |
40 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(1...(ββπ₯))
β Fin) |
41 | 25 | adantlrr 720 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) β β) |
42 | | nnuz 12813 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
43 | | 1zzd 12541 |
. . . . . . . . . . . 12
β’ (π β 1 β
β€) |
44 | 12 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β π·) |
45 | | nnz 12527 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β€) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β β€) |
47 | 8, 9, 10, 11, 44, 46 | dchrzrhcl 26609 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
48 | | nncn 12168 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
49 | 48 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β) |
50 | | nnne0 12194 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β 0) |
51 | 50 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β 0) |
52 | 47, 49, 51 | divcld 11938 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πβ(πΏβπ)) / π) β β) |
53 | | dchrisumn0.f |
. . . . . . . . . . . . . . 15
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
54 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
55 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β π = π) |
56 | 54, 55 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) / π)) |
57 | 56 | cbvmptv 5223 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) / π)) |
58 | 53, 57 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
59 | 52, 58 | fmptd 7067 |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆβ) |
60 | 59 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΉβπ) β β) |
61 | 42, 43, 60 | serf 13943 |
. . . . . . . . . . 11
β’ (π β seq1( + , πΉ):ββΆβ) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β seq1( + , πΉ):ββΆβ) |
63 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β
β+) |
64 | 63 | rpred 12964 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β
β) |
65 | | nndivre 12201 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β (π₯ / π) β β) |
66 | 64, 17, 65 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
67 | 17 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
β) |
68 | 67 | nncnd 12176 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
β) |
69 | 68 | mulid2d 11180 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (1 Β· π) =
π) |
70 | | fznnfl 13774 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (π β
(1...(ββπ₯))
β (π β β
β§ π β€ π₯))) |
71 | 64, 70 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π β
(1...(ββπ₯))
β (π β β
β§ π β€ π₯))) |
72 | 71 | simplbda 501 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β€ π₯) |
73 | 69, 72 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (1 Β· π) β€
π₯) |
74 | | 1red 11163 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β 1 β β) |
75 | 64 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π₯ β
β) |
76 | 67 | nnrpd 12962 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
β+) |
77 | 74, 75, 76 | lemuldivd 13013 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((1 Β· π) β€
π₯ β 1 β€ (π₯ / π))) |
78 | 73, 77 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β 1 β€ (π₯ / π)) |
79 | | flge1nn 13733 |
. . . . . . . . . . 11
β’ (((π₯ / π) β β β§ 1 β€ (π₯ / π)) β (ββ(π₯ / π)) β β) |
80 | 66, 78, 79 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (ββ(π₯ /
π)) β
β) |
81 | 62, 80 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (seq1( + , πΉ)β(ββ(π₯ / π))) β β) |
82 | 41, 81 | mulcld 11182 |
. . . . . . . 8
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) β β) |
83 | 29 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
β) |
84 | 41, 83 | mulcld 11182 |
. . . . . . . 8
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π) β β) |
85 | 40, 82, 84 | fsumsub 15680 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))((((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π)) = (Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) β Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π))) |
86 | 41, 81, 83 | subdid 11618 |
. . . . . . . 8
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)) = ((((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π))) |
87 | 86 | sumeq2dv 15595 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)) = Ξ£π β (1...(ββπ₯))((((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π))) |
88 | 12 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β π·) |
89 | 14 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β€) |
90 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(1...(ββ(π₯ /
π))) β π β
β€) |
91 | 90 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β€) |
92 | 8, 9, 10, 11, 88, 89, 91 | dchrzrhmul 26610 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (πβ(πΏβ(π Β· π))) = ((πβ(πΏβπ)) Β· (πβ(πΏβπ)))) |
93 | 92 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β ((πβ(πΏβ(π Β· π))) / (π Β· π)) = (((πβ(πΏβπ)) Β· (πβ(πΏβπ))) / (π Β· π))) |
94 | 16 | adantlrr 720 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πβ(πΏβπ)) β β) |
95 | 94 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (πβ(πΏβπ)) β β) |
96 | 68 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
97 | 8, 9, 10, 11, 88, 91 | dchrzrhcl 26609 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (πβ(πΏβπ)) β β) |
98 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(1...(ββ(π₯ /
π))) β π β
β) |
99 | 98 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
100 | 99 | nncnd 12176 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β
β) |
101 | 67 | nnne0d 12210 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
0) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β 0) |
103 | 99 | nnne0d 12210 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β π β 0) |
104 | 95, 96, 97, 100, 102, 103 | divmuldivd 11979 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)) = (((πβ(πΏβπ)) Β· (πβ(πΏβπ))) / (π Β· π))) |
105 | 93, 104 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β ((πβ(πΏβ(π Β· π))) / (π Β· π)) = (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π))) |
106 | 105 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((ΞΌβπ) Β·
((πβ(πΏβ(π Β· π))) / (π Β· π))) = ((ΞΌβπ) Β· (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)))) |
107 | 67, 19 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β€) |
108 | 107 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(ΞΌβπ) β
β) |
110 | 95, 96, 102 | divcld 11938 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β ((πβ(πΏβπ)) / π) β β) |
111 | 97, 100, 103 | divcld 11938 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β ((πβ(πΏβπ)) / π) β β) |
112 | 109, 110,
111 | mulassd 11185 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(((ΞΌβπ) Β·
((πβ(πΏβπ)) / π)) Β· ((πβ(πΏβπ)) / π)) = ((ΞΌβπ) Β· (((πβ(πΏβπ)) / π) Β· ((πβ(πΏβπ)) / π)))) |
113 | 109, 95, 96, 102 | div12d 11974 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((ΞΌβπ) Β·
((πβ(πΏβπ)) / π)) = ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) |
114 | 113 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
(((ΞΌβπ) Β·
((πβ(πΏβπ)) / π)) Β· ((πβ(πΏβπ)) / π)) = (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) / π))) |
115 | 106, 112,
114 | 3eqtr2d 2783 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β
((ΞΌβπ) Β·
((πβ(πΏβ(π Β· π))) / (π Β· π))) = (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) / π))) |
116 | 115 | sumeq2dv 15595 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))((ΞΌβπ) Β· ((πβ(πΏβ(π Β· π))) / (π Β· π))) = Ξ£π β (1...(ββ(π₯ / π)))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) / π))) |
117 | | fzfid 13885 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (1...(ββ(π₯ / π))) β Fin) |
118 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π) |
119 | 118, 98, 52 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β ((πβ(πΏβπ)) / π) β β) |
120 | 117, 41, 119 | fsummulc2 15676 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π₯ / π)))((πβ(πΏβπ)) / π)) = Ξ£π β (1...(ββ(π₯ / π)))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((πβ(πΏβπ)) / π))) |
121 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
β’ ((πβ(πΏβπ)) / π) β V |
122 | 56, 53, 121 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
β’ (π β β β (πΉβπ) = ((πβ(πΏβπ)) / π)) |
123 | 99, 122 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ(π₯ /
π)))) β (πΉβπ) = ((πβ(πΏβπ)) / π)) |
124 | 80, 42 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (ββ(π₯ /
π)) β
(β€β₯β1)) |
125 | 123, 124,
119 | fsumser 15622 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))((πβ(πΏβπ)) / π) = (seq1( + , πΉ)β(ββ(π₯ / π)))) |
126 | 125 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· Ξ£π β (1...(ββ(π₯ / π)))((πβ(πΏβπ)) / π)) = (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π))))) |
127 | 116, 120,
126 | 3eqtr2rd 2784 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) = Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((πβ(πΏβ(π Β· π))) / (π Β· π)))) |
128 | 127 | sumeq2dv 15595 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((πβ(πΏβ(π Β· π))) / (π Β· π)))) |
129 | | 2fveq3 6852 |
. . . . . . . . . . . . 13
β’ (π = (π Β· π) β (πβ(πΏβπ)) = (πβ(πΏβ(π Β· π)))) |
130 | | id 22 |
. . . . . . . . . . . . 13
β’ (π = (π Β· π) β π = (π Β· π)) |
131 | 129, 130 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π = (π Β· π) β ((πβ(πΏβπ)) / π) = ((πβ(πΏβ(π Β· π))) / (π Β· π))) |
132 | 131 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = (π Β· π) β ((ΞΌβπ) Β· ((πβ(πΏβπ)) / π)) = ((ΞΌβπ) Β· ((πβ(πΏβ(π Β· π))) / (π Β· π)))) |
133 | | elrabi 3644 |
. . . . . . . . . . . . . . 15
β’ (π β {π¦ β β β£ π¦ β₯ π} β π β β) |
134 | 133 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
135 | 134, 19 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β€) |
136 | 135 | zcnd 12615 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β) |
137 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β π·) |
138 | | elfzelz 13448 |
. . . . . . . . . . . . . . . 16
β’ (π β
(1...(ββπ₯))
β π β
β€) |
139 | 138 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
β€) |
140 | 8, 9, 10, 11, 137, 139 | dchrzrhcl 26609 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πβ(πΏβπ)) β β) |
141 | | fz1ssnn 13479 |
. . . . . . . . . . . . . . . . 17
β’
(1...(ββπ₯)) β β |
142 | 141 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(1...(ββπ₯))
β β) |
143 | 142 | sselda 3949 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
β) |
144 | 143 | nncnd 12176 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
β) |
145 | 143 | nnne0d 12210 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
0) |
146 | 140, 144,
145 | divcld 11938 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) / π) β β) |
147 | 146 | adantrr 716 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((πβ(πΏβπ)) / π) β β) |
148 | 136, 147 | mulcld 11182 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ (π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β ((ΞΌβπ) Β· ((πβ(πΏβπ)) / π)) β β) |
149 | 132, 64, 148 | dvdsflsumcom 26553 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((πβ(πΏβπ)) / π)) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))((ΞΌβπ) Β· ((πβ(πΏβ(π Β· π))) / (π Β· π)))) |
150 | | 2fveq3 6852 |
. . . . . . . . . . . 12
β’ (π = 1 β (πβ(πΏβπ)) = (πβ(πΏβ1))) |
151 | | id 22 |
. . . . . . . . . . . 12
β’ (π = 1 β π = 1) |
152 | 150, 151 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = 1 β ((πβ(πΏβπ)) / π) = ((πβ(πΏβ1)) / 1)) |
153 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β€ π₯) |
154 | | flge1nn 13733 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ 1 β€
π₯) β
(ββπ₯) β
β) |
155 | 64, 153, 154 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
β) |
156 | 155, 42 | eleqtrdi 2848 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
(β€β₯β1)) |
157 | | eluzfz1 13455 |
. . . . . . . . . . . 12
β’
((ββπ₯)
β (β€β₯β1) β 1 β
(1...(ββπ₯))) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β
(1...(ββπ₯))) |
159 | 152, 40, 142, 158, 146 | musumsum 26557 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· ((πβ(πΏβπ)) / π)) = ((πβ(πΏβ1)) / 1)) |
160 | 128, 149,
159 | 3eqtr2d 2783 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) = ((πβ(πΏβ1)) / 1)) |
161 | 8, 9, 10, 11, 12 | dchrzrh1 26608 |
. . . . . . . . . . . 12
β’ (π β (πβ(πΏβ1)) = 1) |
162 | 161 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (πβ(πΏβ1)) = 1) |
163 | 162 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β ((πβ(πΏβ1)) / 1) = (1 / 1)) |
164 | | 1div1e1 11852 |
. . . . . . . . . 10
β’ (1 / 1) =
1 |
165 | 163, 164 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β ((πβ(πΏβ1)) / 1) = 1) |
166 | 160, 165 | eqtr2d 2778 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 = Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π))))) |
167 | 29 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π β
β) |
168 | 40, 167, 41 | fsummulc1 15677 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π) = Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π)) |
169 | 166, 168 | oveq12d 7380 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (1 β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π)) = (Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (seq1( + , πΉ)β(ββ(π₯ / π)))) β Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π))) |
170 | 85, 87, 169 | 3eqtr4rd 2788 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (1 β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π)) = Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) |
171 | 170 | fveq2d 6851 |
. . . . 5
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (absβ(1
β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π))) = (absβΞ£π β (1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)))) |
172 | 81, 83 | subcld 11519 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((seq1( + , πΉ)β(ββ(π₯ / π))) β π) β β) |
173 | 41, 172 | mulcld 11182 |
. . . . . . . 8
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)) β β) |
174 | 40, 173 | fsumcl 15625 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)) β β) |
175 | 174 | abscld 15328 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β β) |
176 | 173 | abscld 15328 |
. . . . . . 7
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β β) |
177 | 40, 176 | fsumrecl 15626 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β β) |
178 | 39 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β πΆ β
β) |
179 | 40, 173 | fsumabs 15693 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β€ Ξ£π β (1...(ββπ₯))(absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)))) |
180 | | reflcl 13708 |
. . . . . . . . . 10
β’ (π₯ β β β
(ββπ₯) β
β) |
181 | 64, 180 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
β) |
182 | 181, 178 | remulcld 11192 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
((ββπ₯) Β·
πΆ) β
β) |
183 | 182, 63 | rerpdivcld 12995 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(((ββπ₯)
Β· πΆ) / π₯) β
β) |
184 | 178, 63 | rerpdivcld 12995 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (πΆ / π₯) β β) |
185 | 184 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πΆ / π₯) β
β) |
186 | 41 | abscld 15328 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) β β) |
187 | 67 | nnrecred 12211 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
188 | 172 | abscld 15328 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)) β β) |
189 | 76 | rpred 12964 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β
β) |
190 | 185, 189 | remulcld 11192 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((πΆ / π₯) Β· π) β β) |
191 | 41 | absge0d 15336 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)))) |
192 | 172 | absge0d 15336 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) |
193 | 94 | abscld 15328 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ(πβ(πΏβπ))) β β) |
194 | 24 | adantlrr 720 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
195 | 194 | abscld 15328 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) β β) |
196 | 94 | absge0d 15336 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ(πβ(πΏβπ)))) |
197 | 194 | absge0d 15336 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ((ΞΌβπ) / π))) |
198 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(Baseβπ) =
(Baseβπ) |
199 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β π β π·) |
200 | | rpvmasum.a |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
201 | 200 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β
β0) |
202 | 9, 198, 11 | znzrhfo 20970 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β πΏ:β€βontoβ(Baseβπ)) |
203 | | fof 6761 |
. . . . . . . . . . . . . . . . 17
β’ (πΏ:β€βontoβ(Baseβπ) β πΏ:β€βΆ(Baseβπ)) |
204 | 201, 202,
203 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β πΏ:β€βΆ(Baseβπ)) |
205 | 204 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β πΏ:β€βΆ(Baseβπ)) |
206 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . 15
β’ ((πΏ:β€βΆ(Baseβπ) β§ π β β€) β (πΏβπ) β (Baseβπ)) |
207 | 205, 14, 206 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πΏβπ) β (Baseβπ)) |
208 | 8, 10, 9, 198, 199, 207 | dchrabs2 26626 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ(πβ(πΏβπ))) β€ 1) |
209 | 108, 68, 101 | absdivd 15347 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) = ((absβ(ΞΌβπ)) / (absβπ))) |
210 | 76 | rprege0d 12971 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (π β β
β§ 0 β€ π)) |
211 | | absid 15188 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ 0 β€
π) β (absβπ) = π) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβπ) =
π) |
213 | 212 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((absβ(ΞΌβπ)) / (absβπ)) = ((absβ(ΞΌβπ)) / π)) |
214 | 209, 213 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) = ((absβ(ΞΌβπ)) / π)) |
215 | 108 | abscld 15328 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β β) |
216 | | mule1 26513 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(absβ(ΞΌβπ))
β€ 1) |
217 | 67, 216 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β€ 1) |
218 | 215, 74, 76, 217 | lediv1dd 13022 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((absβ(ΞΌβπ)) / π) β€ (1 / π)) |
219 | 214, 218 | eqbrtrd 5132 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) β€ (1 / π)) |
220 | 193, 74, 195, 187, 196, 197, 208, 219 | lemul12ad 12104 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((absβ(πβ(πΏβπ))) Β· (absβ((ΞΌβπ) / π))) β€ (1 Β· (1 / π))) |
221 | 94, 194 | absmuld 15346 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) = ((absβ(πβ(πΏβπ))) Β· (absβ((ΞΌβπ) / π)))) |
222 | 187 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
223 | 222 | mulid2d 11180 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (1 Β· (1 / π))
= (1 / π)) |
224 | 223 | eqcomd 2743 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (1 / π) = (1
Β· (1 / π))) |
225 | 220, 221,
224 | 3brtr4d 5142 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) β€ (1 / π)) |
226 | | 2fveq3 6852 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π₯ / π) β (seq1( + , πΉ)β(ββπ¦)) = (seq1( + , πΉ)β(ββ(π₯ / π)))) |
227 | 226 | fvoveq1d 7384 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π₯ / π) β (absβ((seq1( + , πΉ)β(ββπ¦)) β π)) = (absβ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) |
228 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π₯ / π) β (πΆ / π¦) = (πΆ / (π₯ / π))) |
229 | 227, 228 | breq12d 5123 |
. . . . . . . . . . . . 13
β’ (π¦ = (π₯ / π) β ((absβ((seq1( + , πΉ)β(ββπ¦)) β π)) β€ (πΆ / π¦) β (absβ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)) β€ (πΆ / (π₯ / π)))) |
230 | | dchrisumn0.1 |
. . . . . . . . . . . . . 14
β’ (π β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π)) β€ (πΆ / π¦)) |
231 | 230 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β βπ¦ β
(1[,)+β)(absβ((seq1( + , πΉ)β(ββπ¦)) β π)) β€ (πΆ / π¦)) |
232 | | 1re 11162 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
233 | | elicopnf 13369 |
. . . . . . . . . . . . . . 15
β’ (1 β
β β ((π₯ / π) β (1[,)+β) β
((π₯ / π) β β β§ 1 β€ (π₯ / π)))) |
234 | 232, 233 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ((π₯ / π) β (1[,)+β) β ((π₯ / π) β β β§ 1 β€ (π₯ / π))) |
235 | 66, 78, 234 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
(1[,)+β)) |
236 | 229, 231,
235 | rspcdva 3585 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)) β€ (πΆ / (π₯ / π))) |
237 | 178 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β πΆ β
β) |
238 | 237 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β πΆ β
β) |
239 | | rpcnne0 12940 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β (π₯ β β
β§ π₯ β
0)) |
240 | 239 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯ β β β§ π₯ β 0)) |
241 | 240 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ π₯ β
0)) |
242 | | divdiv2 11874 |
. . . . . . . . . . . . . 14
β’ ((πΆ β β β§ (π₯ β β β§ π₯ β 0) β§ (π β β β§ π β 0)) β (πΆ / (π₯ / π)) = ((πΆ Β· π) / π₯)) |
243 | 238, 241,
68, 101, 242 | syl112anc 1375 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πΆ / (π₯ / π)) = ((πΆ Β· π) / π₯)) |
244 | | div23 11839 |
. . . . . . . . . . . . . 14
β’ ((πΆ β β β§ π β β β§ (π₯ β β β§ π₯ β 0)) β ((πΆ Β· π) / π₯) = ((πΆ / π₯) Β· π)) |
245 | 238, 68, 241, 244 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((πΆ Β· π) / π₯) = ((πΆ / π₯) Β· π)) |
246 | 243, 245 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πΆ / (π₯ / π)) = ((πΆ / π₯) Β· π)) |
247 | 236, 246 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)) β€ ((πΆ / π₯) Β· π)) |
248 | 186, 187,
188, 190, 191, 192, 225, 247 | lemul12ad 12104 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) Β· (absβ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β€ ((1 / π) Β· ((πΆ / π₯) Β· π))) |
249 | 41, 172 | absmuld 15346 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) = ((absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) Β· (absβ((seq1( + , πΉ)β(ββ(π₯ / π))) β π)))) |
250 | 184 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (πΆ / π₯) β β) |
251 | 250 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πΆ / π₯) β
β) |
252 | 251, 68, 101 | divcan4d 11944 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πΆ / π₯) Β· π) / π) = (πΆ / π₯)) |
253 | 251, 68 | mulcld 11182 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((πΆ / π₯) Β· π) β β) |
254 | 253, 68, 101 | divrec2d 11942 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (((πΆ / π₯) Β· π) / π) = ((1 / π) Β· ((πΆ / π₯) Β· π))) |
255 | 252, 254 | eqtr3d 2779 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πΆ / π₯) = ((1 / π) Β· ((πΆ / π₯) Β· π))) |
256 | 248, 249,
255 | 3brtr4d 5142 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β€ (πΆ / π₯)) |
257 | 40, 176, 185, 256 | fsumle 15691 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β€ Ξ£π β (1...(ββπ₯))(πΆ / π₯)) |
258 | 155 | nnnn0d 12480 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
β0) |
259 | | hashfz1 14253 |
. . . . . . . . . . 11
β’
((ββπ₯)
β β0 β (β―β(1...(ββπ₯))) = (ββπ₯)) |
260 | 258, 259 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(β―β(1...(ββπ₯))) = (ββπ₯)) |
261 | 260 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
((β―β(1...(ββπ₯))) Β· (πΆ / π₯)) = ((ββπ₯) Β· (πΆ / π₯))) |
262 | | fsumconst 15682 |
. . . . . . . . . 10
β’
(((1...(ββπ₯)) β Fin β§ (πΆ / π₯) β β) β Ξ£π β
(1...(ββπ₯))(πΆ / π₯) = ((β―β(1...(ββπ₯))) Β· (πΆ / π₯))) |
263 | 40, 250, 262 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(πΆ / π₯) = ((β―β(1...(ββπ₯))) Β· (πΆ / π₯))) |
264 | 155 | nncnd 12176 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
β) |
265 | | divass 11838 |
. . . . . . . . . 10
β’
(((ββπ₯)
β β β§ πΆ
β β β§ (π₯
β β β§ π₯ β
0)) β (((ββπ₯) Β· πΆ) / π₯) = ((ββπ₯) Β· (πΆ / π₯))) |
266 | 264, 237,
240, 265 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(((ββπ₯)
Β· πΆ) / π₯) = ((ββπ₯) Β· (πΆ / π₯))) |
267 | 261, 263,
266 | 3eqtr4d 2787 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(πΆ / π₯) = (((ββπ₯) Β· πΆ) / π₯)) |
268 | 257, 267 | breqtrd 5136 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β€ (((ββπ₯) Β· πΆ) / π₯)) |
269 | 38 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (πΆ β β β§ 0 β€
πΆ)) |
270 | | flle 13711 |
. . . . . . . . . 10
β’ (π₯ β β β
(ββπ₯) β€
π₯) |
271 | 64, 270 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β€
π₯) |
272 | | lemul1a 12016 |
. . . . . . . . 9
β’
((((ββπ₯)
β β β§ π₯
β β β§ (πΆ
β β β§ 0 β€ πΆ)) β§ (ββπ₯) β€ π₯) β ((ββπ₯) Β· πΆ) β€ (π₯ Β· πΆ)) |
273 | 181, 64, 269, 271, 272 | syl31anc 1374 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
((ββπ₯) Β·
πΆ) β€ (π₯ Β· πΆ)) |
274 | 182, 178,
63 | ledivmuld 13017 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
((((ββπ₯)
Β· πΆ) / π₯) β€ πΆ β ((ββπ₯) Β· πΆ) β€ (π₯ Β· πΆ))) |
275 | 273, 274 | mpbird 257 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(((ββπ₯)
Β· πΆ) / π₯) β€ πΆ) |
276 | 177, 183,
178, 268, 275 | letrd 11319 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β€ πΆ) |
277 | 175, 177,
178, 179, 276 | letrd 11319 |
. . . . 5
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· ((seq1( + , πΉ)β(ββ(π₯ / π))) β π))) β€ πΆ) |
278 | 171, 277 | eqbrtrd 5132 |
. . . 4
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (absβ(1
β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π))) β€ πΆ) |
279 | 32, 34, 35, 39, 278 | elo1d 15425 |
. . 3
β’ (π β (π₯ β β+ β¦ (1
β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π))) β π(1)) |
280 | 6, 31, 279 | o1dif 15519 |
. 2
β’ (π β ((π₯ β β+ β¦ 1) β
π(1) β (π₯
β β+ β¦ (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π)) β π(1))) |
281 | 5, 280 | mpbid 231 |
1
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· π)) β π(1)) |