Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. 2
β’ (π β 1 β
β) |
2 | | sumex 15579 |
. . . 4
β’
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β V |
3 | 2 | a1i 11 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β V) |
4 | | sumex 15579 |
. . . 4
β’
Ξ£π β
(((ββπ₯) +
1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β V |
5 | 4 | a1i 11 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(((ββπ₯) +
1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β V) |
6 | | rpvmasum.z |
. . . . 5
β’ π =
(β€/nβ€βπ) |
7 | | rpvmasum.l |
. . . . 5
β’ πΏ = (β€RHomβπ) |
8 | | rpvmasum.a |
. . . . 5
β’ (π β π β β) |
9 | | rpvmasum2.g |
. . . . 5
β’ πΊ = (DChrβπ) |
10 | | rpvmasum2.d |
. . . . 5
β’ π· = (BaseβπΊ) |
11 | | rpvmasum2.1 |
. . . . 5
β’ 1 =
(0gβπΊ) |
12 | | rpvmasum2.w |
. . . . . . . 8
β’ π = {π¦ β (π· β { 1 }) β£ Ξ£π β β ((π¦β(πΏβπ)) / π) = 0} |
13 | 12 | ssrab3 4045 |
. . . . . . 7
β’ π β (π· β { 1 }) |
14 | | difss 4096 |
. . . . . . 7
β’ (π· β { 1 }) β π· |
15 | 13, 14 | sstri 3958 |
. . . . . 6
β’ π β π· |
16 | | dchrisum0.b |
. . . . . 6
β’ (π β π β π) |
17 | 15, 16 | sselid 3947 |
. . . . 5
β’ (π β π β π·) |
18 | 13, 16 | sselid 3947 |
. . . . . 6
β’ (π β π β (π· β { 1 })) |
19 | | eldifsni 4755 |
. . . . . 6
β’ (π β (π· β { 1 }) β π β 1 ) |
20 | 18, 19 | syl 17 |
. . . . 5
β’ (π β π β 1 ) |
21 | | eqid 2737 |
. . . . 5
β’ (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) / π)) |
22 | 6, 7, 8, 9, 10, 11, 17, 20, 21 | dchrmusumlema 26857 |
. . . 4
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦))) |
23 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β β) |
24 | 16 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β π) |
25 | | dchrisum0lem1.f |
. . . . . . 7
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
26 | | dchrisum0.c |
. . . . . . . 8
β’ (π β πΆ β (0[,)+β)) |
27 | 26 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β πΆ β (0[,)+β)) |
28 | | dchrisum0.s |
. . . . . . . 8
β’ (π β seq1( + , πΉ) β π) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β seq1( + , πΉ) β π) |
30 | | dchrisum0.1 |
. . . . . . . 8
β’ (π β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π)) β€ (πΆ / (ββπ¦))) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π)) β€ (πΆ / (ββπ¦))) |
32 | | eqid 2737 |
. . . . . . 7
β’ (π¦ β β+
β¦ (Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))) = (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))) |
33 | 32 | divsqrsum 26347 |
. . . . . . . . 9
β’ (π¦ β β+
β¦ (Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))) β dom
βπ |
34 | 32 | divsqrsumf 26346 |
. . . . . . . . . . . 12
β’ (π¦ β β+
β¦ (Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))):β+βΆβ |
35 | | ax-resscn 11115 |
. . . . . . . . . . . 12
β’ β
β β |
36 | | fss 6690 |
. . . . . . . . . . . 12
β’ (((π¦ β β+
β¦ (Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))):β+βΆβ β§
β β β) β (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))):β+βΆβ) |
37 | 34, 35, 36 | mp2an 691 |
. . . . . . . . . . 11
β’ (π¦ β β+
β¦ (Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))):β+βΆβ |
38 | 37 | a1i 11 |
. . . . . . . . . 10
β’ (π β (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))):β+βΆβ) |
39 | | rpsup 13778 |
. . . . . . . . . . 11
β’
sup(β+, β*, < ) =
+β |
40 | 39 | a1i 11 |
. . . . . . . . . 10
β’ (π β sup(β+,
β*, < ) = +β) |
41 | 38, 40 | rlimdm 15440 |
. . . . . . . . 9
β’ (π β ((π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))) β dom βπ
β (π¦ β
β+ β¦ (Ξ£π β (1...(ββπ¦))(1 / (ββπ)) β (2 Β·
(ββπ¦))))
βπ ( βπ β(π¦ β β+
β¦ (Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦))))))) |
42 | 33, 41 | mpbii 232 |
. . . . . . . 8
β’ (π β (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))) βπ (
βπ β(π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))))) |
43 | 42 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))) βπ (
βπ β(π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))))) |
44 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β (0[,)+β)) |
45 | | simprrl 780 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘) |
46 | | simprrr 781 |
. . . . . . 7
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) |
47 | 6, 7, 23, 9, 10, 11, 12, 24, 25, 27, 29, 31, 32, 43, 21, 44, 45, 46 | dchrisum0lem2 26882 |
. . . . . 6
β’ ((π β§ (π β (0[,)+β) β§ (seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1)) |
48 | 47 | rexlimdvaa 3154 |
. . . . 5
β’ (π β (βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1))) |
49 | 48 | exlimdv 1937 |
. . . 4
β’ (π β (βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1))) |
50 | 22, 49 | mpd 15 |
. . 3
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1)) |
51 | 6, 7, 8, 9, 10, 11, 12, 16, 25, 26, 28, 30 | dchrisum0lem1 26880 |
. . 3
β’ (π β (π₯ β β+ β¦
Ξ£π β
(((ββπ₯) +
1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1)) |
52 | 3, 5, 50, 51 | o1add2 15513 |
. 2
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) + Ξ£π β (((ββπ₯) + 1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)))) β π(1)) |
53 | | ovexd 7397 |
. 2
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) + Ξ£π β (((ββπ₯) + 1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β V) |
54 | | fzfid 13885 |
. . 3
β’ ((π β§ π₯ β β+) β
(1...(ββ(π₯β2))) β Fin) |
55 | | fzfid 13885 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β
(1...(ββ((π₯β2) / π))) β Fin) |
56 | 17 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β π β π·) |
57 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β
(1...(ββ(π₯β2))) β π β β€) |
58 | 57 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β π β β€) |
59 | 9, 6, 10, 7, 56, 58 | dchrzrhcl 26609 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β (πβ(πΏβπ)) β β) |
60 | 59 | adantr 482 |
. . . . 5
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (πβ(πΏβπ)) β β) |
61 | | elfznn 13477 |
. . . . . . . . . 10
β’ (π β
(1...(ββ(π₯β2))) β π β β) |
62 | 61 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β π β β) |
63 | 62 | nnrpd 12962 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β π β β+) |
64 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββ((π₯β2) / π))) β π β β) |
65 | 64 | nnrpd 12962 |
. . . . . . . 8
β’ (π β
(1...(ββ((π₯β2) / π))) β π β β+) |
66 | | rpmulcl 12945 |
. . . . . . . 8
β’ ((π β β+
β§ π β
β+) β (π Β· π) β
β+) |
67 | 63, 65, 66 | syl2an 597 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (π Β· π) β
β+) |
68 | 67 | rpsqrtcld 15303 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (ββ(π Β· π)) β
β+) |
69 | 68 | rpcnd 12966 |
. . . . 5
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (ββ(π Β· π)) β β) |
70 | 68 | rpne0d 12969 |
. . . . 5
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (ββ(π Β· π)) β 0) |
71 | 60, 69, 70 | divcld 11938 |
. . . 4
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β ((πβ(πΏβπ)) / (ββ(π Β· π))) β β) |
72 | 55, 71 | fsumcl 15625 |
. . 3
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π))) β β) |
73 | 54, 72 | fsumcl 15625 |
. 2
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π))) β β) |
74 | 73 | abscld 15328 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π)))) β β) |
75 | 74 | adantrr 716 |
. . 3
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π)))) β β) |
76 | 62 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β π β β) |
77 | 76 | nnrpd 12962 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β π β β+) |
78 | 77 | rprege0d 12971 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (π β β β§ 0 β€ π)) |
79 | 64 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β π β β) |
80 | 79 | nnrpd 12962 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β π β β+) |
81 | 80 | rprege0d 12971 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (π β β β§ 0 β€ π)) |
82 | | sqrtmul 15151 |
. . . . . . . . . . 11
β’ (((π β β β§ 0 β€
π) β§ (π β β β§ 0 β€
π)) β
(ββ(π Β·
π)) = ((ββπ) Β· (ββπ))) |
83 | 78, 81, 82 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (ββ(π Β· π)) = ((ββπ) Β· (ββπ))) |
84 | 83 | oveq2d 7378 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β ((πβ(πΏβπ)) / (ββ(π Β· π))) = ((πβ(πΏβπ)) / ((ββπ) Β· (ββπ)))) |
85 | 77 | rpsqrtcld 15303 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (ββπ) β
β+) |
86 | 85 | rpcnne0d 12973 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β ((ββπ) β β β§
(ββπ) β
0)) |
87 | 80 | rpsqrtcld 15303 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (ββπ) β
β+) |
88 | 87 | rpcnne0d 12973 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β ((ββπ) β β β§
(ββπ) β
0)) |
89 | | divdiv1 11873 |
. . . . . . . . . 10
β’ (((πβ(πΏβπ)) β β β§ ((ββπ) β β β§
(ββπ) β 0)
β§ ((ββπ)
β β β§ (ββπ) β 0)) β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = ((πβ(πΏβπ)) / ((ββπ) Β· (ββπ)))) |
90 | 60, 86, 88, 89 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = ((πβ(πΏβπ)) / ((ββπ) Β· (ββπ)))) |
91 | 84, 90 | eqtr4d 2780 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β§ π β (1...(ββ((π₯β2) / π)))) β ((πβ(πΏβπ)) / (ββ(π Β· π))) = (((πβ(πΏβπ)) / (ββπ)) / (ββπ))) |
92 | 91 | sumeq2dv 15595 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π))) = Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) |
93 | 92 | sumeq2dv 15595 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π))) = Ξ£π β (1...(ββ(π₯β2)))Ξ£π β
(1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) |
94 | 93 | adantrr 716 |
. . . . 5
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π))) = Ξ£π β (1...(ββ(π₯β2)))Ξ£π β
(1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) |
95 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
96 | 95 | rpred 12964 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β π₯ β
β) |
97 | | reflcl 13708 |
. . . . . . . . . 10
β’ (π₯ β β β
(ββπ₯) β
β) |
98 | 96, 97 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β) |
99 | 98 | ltp1d 12092 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
(ββπ₯) <
((ββπ₯) +
1)) |
100 | | fzdisj 13475 |
. . . . . . . 8
β’
((ββπ₯)
< ((ββπ₯) +
1) β ((1...(ββπ₯)) β© (((ββπ₯) + 1)...(ββ(π₯β2)))) = β
) |
101 | 99, 100 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β© (((ββπ₯) +
1)...(ββ(π₯β2)))) = β
) |
102 | 101 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
((1...(ββπ₯))
β© (((ββπ₯) +
1)...(ββ(π₯β2)))) = β
) |
103 | 95 | rprege0d 12971 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (π₯ β β β§ 0 β€
π₯)) |
104 | | flge0nn0 13732 |
. . . . . . . . . 10
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββπ₯) β
β0) |
105 | | nn0p1nn 12459 |
. . . . . . . . . 10
β’
((ββπ₯)
β β0 β ((ββπ₯) + 1) β β) |
106 | 103, 104,
105 | 3syl 18 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
((ββπ₯) + 1)
β β) |
107 | | nnuz 12813 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
108 | 106, 107 | eleqtrdi 2848 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((ββπ₯) + 1)
β (β€β₯β1)) |
109 | 108 | adantrr 716 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
((ββπ₯) + 1)
β (β€β₯β1)) |
110 | 96 | adantrr 716 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β
β) |
111 | | 2z 12542 |
. . . . . . . . . . 11
β’ 2 β
β€ |
112 | | rpexpcl 13993 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 2 β β€) β (π₯β2) β
β+) |
113 | 95, 111, 112 | sylancl 587 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (π₯β2) β
β+) |
114 | 113 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯β2) β
β+) |
115 | 114 | rpred 12964 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯β2) β
β) |
116 | 110 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β
β) |
117 | 116 | mulid1d 11179 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯ Β· 1) = π₯) |
118 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β€ π₯) |
119 | | 1red 11163 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β
β) |
120 | | rpregt0 12936 |
. . . . . . . . . . . . 13
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
121 | 120 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯ β β β§ 0 <
π₯)) |
122 | | lemul2 12015 |
. . . . . . . . . . . 12
β’ ((1
β β β§ π₯
β β β§ (π₯
β β β§ 0 < π₯)) β (1 β€ π₯ β (π₯ Β· 1) β€ (π₯ Β· π₯))) |
123 | 119, 110,
121, 122 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (1 β€ π₯ β (π₯ Β· 1) β€ (π₯ Β· π₯))) |
124 | 118, 123 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯ Β· 1) β€ (π₯ Β· π₯)) |
125 | 117, 124 | eqbrtrrd 5134 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β€ (π₯ Β· π₯)) |
126 | 116 | sqvald 14055 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯β2) = (π₯ Β· π₯)) |
127 | 125, 126 | breqtrrd 5138 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β€ (π₯β2)) |
128 | | flword2 13725 |
. . . . . . . 8
β’ ((π₯ β β β§ (π₯β2) β β β§
π₯ β€ (π₯β2)) β (ββ(π₯β2)) β
(β€β₯β(ββπ₯))) |
129 | 110, 115,
127, 128 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββ(π₯β2))
β (β€β₯β(ββπ₯))) |
130 | | fzsplit2 13473 |
. . . . . . 7
β’
((((ββπ₯)
+ 1) β (β€β₯β1) β§ (ββ(π₯β2)) β
(β€β₯β(ββπ₯))) β (1...(ββ(π₯β2))) =
((1...(ββπ₯))
βͺ (((ββπ₯) +
1)...(ββ(π₯β2))))) |
131 | 109, 129,
130 | syl2anc 585 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(1...(ββ(π₯β2))) = ((1...(ββπ₯)) βͺ (((ββπ₯) + 1)...(ββ(π₯β2))))) |
132 | | fzfid 13885 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(1...(ββ(π₯β2))) β Fin) |
133 | 92, 72 | eqeltrrd 2839 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββ(π₯β2)))) β Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
134 | 133 | adantlrr 720 |
. . . . . 6
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββ(π₯β2)))) β Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
135 | 102, 131,
132, 134 | fsumsplit 15633 |
. . . . 5
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = (Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) + Ξ£π β (((ββπ₯) + 1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)))) |
136 | 94, 135 | eqtrd 2777 |
. . . 4
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π))) = (Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) + Ξ£π β (((ββπ₯) + 1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)))) |
137 | 136 | fveq2d 6851 |
. . 3
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π)))) = (absβ(Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) + Ξ£π β (((ββπ₯) + 1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))))) |
138 | 75, 137 | eqled 11265 |
. 2
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π)))) β€ (absβ(Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) + Ξ£π β (((ββπ₯) + 1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))))) |
139 | 1, 52, 53, 73, 138 | o1le 15544 |
1
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββ(π Β· π)))) β π(1)) |