Step | Hyp | Ref
| Expression |
1 | | 2cnd 12238 |
. . 3
β’ ((π β§ π₯ β β+) β 2 β
β) |
2 | | rpcn 12932 |
. . . . 5
β’ (π₯ β β+
β π₯ β
β) |
3 | 2 | adantl 483 |
. . . 4
β’ ((π β§ π₯ β β+) β π₯ β
β) |
4 | | fzfid 13885 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
5 | | rpvmasum2.g |
. . . . . . 7
β’ πΊ = (DChrβπ) |
6 | | rpvmasum.z |
. . . . . . 7
β’ π =
(β€/nβ€βπ) |
7 | | rpvmasum2.d |
. . . . . . 7
β’ π· = (BaseβπΊ) |
8 | | rpvmasum.l |
. . . . . . 7
β’ πΏ = (β€RHomβπ) |
9 | | rpvmasum2.w |
. . . . . . . . . . 11
β’ π = {π¦ β (π· β { 1 }) β£ Ξ£π β β ((π¦β(πΏβπ)) / π) = 0} |
10 | 9 | ssrab3 4045 |
. . . . . . . . . 10
β’ π β (π· β { 1 }) |
11 | | dchrisum0.b |
. . . . . . . . . 10
β’ (π β π β π) |
12 | 10, 11 | sselid 3947 |
. . . . . . . . 9
β’ (π β π β (π· β { 1 })) |
13 | 12 | eldifad 3927 |
. . . . . . . 8
β’ (π β π β π·) |
14 | 13 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β π·) |
15 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β
(1...(ββπ₯))
β π β
β€) |
16 | 15 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β€) |
17 | 5, 6, 7, 8, 14, 16 | dchrzrhcl 26609 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πβ(πΏβπ)) β β) |
18 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ₯))
β π β
β) |
19 | 18 | nnrpd 12962 |
. . . . . . . 8
β’ (π β
(1...(ββπ₯))
β π β
β+) |
20 | 19 | adantl 483 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β+) |
21 | 20 | rpcnd 12966 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
22 | 20 | rpne0d 12969 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
0) |
23 | 17, 21, 22 | divcld 11938 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) / π) β β) |
24 | 4, 23 | fsumcl 15625 |
. . . 4
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π) β β) |
25 | 3, 24 | mulcld 11182 |
. . 3
β’ ((π β§ π₯ β β+) β (π₯ Β· Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)) β β) |
26 | | rpssre 12929 |
. . . . 5
β’
β+ β β |
27 | | 2cn 12235 |
. . . . 5
β’ 2 β
β |
28 | | o1const 15509 |
. . . . 5
β’
((β+ β β β§ 2 β β) β
(π₯ β
β+ β¦ 2) β π(1)) |
29 | 26, 27, 28 | mp2an 691 |
. . . 4
β’ (π₯ β β+
β¦ 2) β π(1) |
30 | 29 | a1i 11 |
. . 3
β’ (π β (π₯ β β+ β¦ 2) β
π(1)) |
31 | 26 | a1i 11 |
. . . 4
β’ (π β β+
β β) |
32 | | 1red 11163 |
. . . 4
β’ (π β 1 β
β) |
33 | | dchrisum0lem2.e |
. . . . 5
β’ (π β πΈ β (0[,)+β)) |
34 | | elrege0 13378 |
. . . . . 6
β’ (πΈ β (0[,)+β) β
(πΈ β β β§ 0
β€ πΈ)) |
35 | 34 | simplbi 499 |
. . . . 5
β’ (πΈ β (0[,)+β) β
πΈ β
β) |
36 | 33, 35 | syl 17 |
. . . 4
β’ (π β πΈ β β) |
37 | 3, 24 | absmuld 15346 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(absβ(π₯ Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) = ((absβπ₯) Β· (absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)))) |
38 | | rprege0 12937 |
. . . . . . . . . 10
β’ (π₯ β β+
β (π₯ β β
β§ 0 β€ π₯)) |
39 | 38 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β (π₯ β β β§ 0 β€
π₯)) |
40 | | absid 15188 |
. . . . . . . . 9
β’ ((π₯ β β β§ 0 β€
π₯) β (absβπ₯) = π₯) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
(absβπ₯) = π₯) |
42 | 41 | oveq1d 7377 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
((absβπ₯) Β·
(absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) = (π₯ Β· (absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)))) |
43 | 37, 42 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(absβ(π₯ Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) = (π₯ Β· (absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)))) |
44 | 43 | adantrr 716 |
. . . . 5
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ(π₯ Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) = (π₯ Β· (absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)))) |
45 | 24 | adantrr 716 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π) β β) |
46 | 45 | subid1d 11508 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π) β 0) = Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π)) |
47 | 18 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
48 | | 2fveq3 6852 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
49 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π = π β π = π) |
50 | 48, 49 | oveq12d 7380 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβ(πΏβπ)) / π) = ((πβ(πΏβπ)) / π)) |
51 | | dchrisum0lem2.k |
. . . . . . . . . . . . . 14
β’ πΎ = (π β β β¦ ((πβ(πΏβπ)) / π)) |
52 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ ((πβ(πΏβπ)) / π) β V |
53 | 50, 51, 52 | fvmpt3i 6958 |
. . . . . . . . . . . . 13
β’ (π β β β (πΎβπ) = ((πβ(πΏβπ)) / π)) |
54 | 47, 53 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΎβπ) = ((πβ(πΏβπ)) / π)) |
55 | 54 | adantlrr 720 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β (πΎβπ) = ((πβ(πΏβπ)) / π)) |
56 | | rpregt0 12936 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
57 | 56 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯ β β β§ 0 <
π₯)) |
58 | 57 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β
β) |
59 | | simprr 772 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 1 β€ π₯) |
60 | | flge1nn 13733 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ 1 β€
π₯) β
(ββπ₯) β
β) |
61 | 58, 59, 60 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
β) |
62 | | nnuz 12813 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
63 | 61, 62 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(ββπ₯) β
(β€β₯β1)) |
64 | 23 | adantlrr 720 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β+ β§ 1 β€
π₯)) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) / π) β β) |
65 | 55, 63, 64 | fsumser 15622 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π) = (seq1( + , πΎ)β(ββπ₯))) |
66 | | rpvmasum.a |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
67 | | rpvmasum2.1 |
. . . . . . . . . . . . . 14
β’ 1 =
(0gβπΊ) |
68 | | eldifsni 4755 |
. . . . . . . . . . . . . . 15
β’ (π β (π· β { 1 }) β π β 1 ) |
69 | 12, 68 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β 1 ) |
70 | | dchrisum0lem2.t |
. . . . . . . . . . . . . 14
β’ (π β seq1( + , πΎ) β π) |
71 | | dchrisum0lem2.3 |
. . . . . . . . . . . . . 14
β’ (π β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΎ)β(ββπ¦)) β π)) β€ (πΈ / π¦)) |
72 | 6, 8, 66, 5, 7, 67, 13, 69, 51, 33, 70, 71, 9 | dchrvmaeq0 26868 |
. . . . . . . . . . . . 13
β’ (π β (π β π β π = 0)) |
73 | 11, 72 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β π = 0) |
74 | 73 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π = 0) |
75 | 74 | eqcomd 2743 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β 0 = π) |
76 | 65, 75 | oveq12d 7380 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π) β 0) = ((seq1( + , πΎ)β(ββπ₯)) β π)) |
77 | 46, 76 | eqtr3d 2779 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π) = ((seq1( + , πΎ)β(ββπ₯)) β π)) |
78 | 77 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)) = (absβ((seq1( + , πΎ)β(ββπ₯)) β π))) |
79 | | 2fveq3 6852 |
. . . . . . . . . 10
β’ (π¦ = π₯ β (seq1( + , πΎ)β(ββπ¦)) = (seq1( + , πΎ)β(ββπ₯))) |
80 | 79 | fvoveq1d 7384 |
. . . . . . . . 9
β’ (π¦ = π₯ β (absβ((seq1( + , πΎ)β(ββπ¦)) β π)) = (absβ((seq1( + , πΎ)β(ββπ₯)) β π))) |
81 | | oveq2 7370 |
. . . . . . . . 9
β’ (π¦ = π₯ β (πΈ / π¦) = (πΈ / π₯)) |
82 | 80, 81 | breq12d 5123 |
. . . . . . . 8
β’ (π¦ = π₯ β ((absβ((seq1( + , πΎ)β(ββπ¦)) β π)) β€ (πΈ / π¦) β (absβ((seq1( + , πΎ)β(ββπ₯)) β π)) β€ (πΈ / π₯))) |
83 | 71 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β βπ¦ β
(1[,)+β)(absβ((seq1( + , πΎ)β(ββπ¦)) β π)) β€ (πΈ / π¦)) |
84 | | 1re 11162 |
. . . . . . . . . 10
β’ 1 β
β |
85 | | elicopnf 13369 |
. . . . . . . . . 10
β’ (1 β
β β (π₯ β
(1[,)+β) β (π₯
β β β§ 1 β€ π₯))) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . 9
β’ (π₯ β (1[,)+β) β
(π₯ β β β§ 1
β€ π₯)) |
87 | 58, 59, 86 | sylanbrc 584 |
. . . . . . . 8
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β π₯ β
(1[,)+β)) |
88 | 82, 83, 87 | rspcdva 3585 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ((seq1( + , πΎ)β(ββπ₯)) β π)) β€ (πΈ / π₯)) |
89 | 78, 88 | eqbrtrd 5132 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)) β€ (πΈ / π₯)) |
90 | 45 | abscld 15328 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)) β β) |
91 | 36 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β πΈ β
β) |
92 | | lemuldiv2 12043 |
. . . . . . 7
β’
(((absβΞ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π)) β β β§ πΈ β β β§ (π₯ β β β§ 0 < π₯)) β ((π₯ Β· (absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) β€ πΈ β (absβΞ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π)) β€ (πΈ / π₯))) |
93 | 90, 91, 57, 92 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β ((π₯ Β·
(absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) β€ πΈ β (absβΞ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π)) β€ (πΈ / π₯))) |
94 | 89, 93 | mpbird 257 |
. . . . 5
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β (π₯ Β·
(absβΞ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) β€ πΈ) |
95 | 44, 94 | eqbrtrd 5132 |
. . . 4
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβ(π₯ Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) β€ πΈ) |
96 | 31, 25, 32, 36, 95 | elo1d 15425 |
. . 3
β’ (π β (π₯ β β+ β¦ (π₯ Β· Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) β π(1)) |
97 | 1, 25, 30, 96 | o1mul2 15514 |
. 2
β’ (π β (π₯ β β+ β¦ (2
Β· (π₯ Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)))) β π(1)) |
98 | | fzfid 13885 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1...(ββ((π₯β2) / π))) β Fin) |
99 | 20 | rpsqrtcld 15303 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β β+) |
100 | 99 | rpcnd 12966 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β β) |
101 | 99 | rpne0d 12969 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β 0) |
102 | 17, 100, 101 | divcld 11938 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) / (ββπ)) β β) |
103 | 102 | adantr 482 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β ((πβ(πΏβπ)) / (ββπ)) β β) |
104 | | elfznn 13477 |
. . . . . . . . . 10
β’ (π β
(1...(ββ((π₯β2) / π))) β π β β) |
105 | 104 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β π β β) |
106 | 105 | nnrpd 12962 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β π β β+) |
107 | 106 | rpsqrtcld 15303 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (ββπ) β
β+) |
108 | 107 | rpcnd 12966 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (ββπ) β β) |
109 | 107 | rpne0d 12969 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (ββπ) β 0) |
110 | 103, 108,
109 | divcld 11938 |
. . . . 5
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
111 | 98, 110 | fsumcl 15625 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
112 | 4, 111 | fsumcl 15625 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
113 | | mulcl 11142 |
. . . 4
β’ ((2
β β β§ (π₯
Β· Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)) β β) β (2 Β· (π₯ Β· Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) β β) |
114 | 27, 25, 113 | sylancr 588 |
. . 3
β’ ((π β§ π₯ β β+) β (2
Β· (π₯ Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) β β) |
115 | | 2re 12234 |
. . . . . . . . . 10
β’ 2 β
β |
116 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
117 | | 2z 12542 |
. . . . . . . . . . . . . 14
β’ 2 β
β€ |
118 | | rpexpcl 13993 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ 2 β β€) β (π₯β2) β
β+) |
119 | 116, 117,
118 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β (π₯β2) β
β+) |
120 | | rpdivcl 12947 |
. . . . . . . . . . . . 13
β’ (((π₯β2) β
β+ β§ π
β β+) β ((π₯β2) / π) β
β+) |
121 | 119, 19, 120 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((π₯β2) / π) β
β+) |
122 | 121 | rpsqrtcld 15303 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ((π₯β2) / π)) β
β+) |
123 | 122 | rpred 12964 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ((π₯β2) / π)) β β) |
124 | | remulcl 11143 |
. . . . . . . . . 10
β’ ((2
β β β§ (ββ((π₯β2) / π)) β β) β (2 Β·
(ββ((π₯β2)
/ π))) β
β) |
125 | 115, 123,
124 | sylancr 588 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (2 Β· (ββ((π₯β2) / π))) β β) |
126 | 125 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (2 Β· (ββ((π₯β2) / π))) β β) |
127 | 102, 126 | mulcld 11182 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π)))) β
β) |
128 | 4, 111, 127 | fsumsub 15680 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π))))) = (Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π)))))) |
129 | 107 | rpcnne0d 12973 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β ((ββπ) β β β§
(ββπ) β
0)) |
130 | | reccl 11827 |
. . . . . . . . . . 11
β’
(((ββπ)
β β β§ (ββπ) β 0) β (1 / (ββπ)) β
β) |
131 | 129, 130 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (1 / (ββπ)) β
β) |
132 | 98, 131 | fsumcl 15625 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ((π₯β2) / π)))(1 / (ββπ)) β β) |
133 | 102, 132,
126 | subdid 11618 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· (Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ)) β (2 Β· (ββ((π₯β2) / π))))) = ((((πβ(πΏβπ)) / (ββπ)) Β· Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ))) β (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π)))))) |
134 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π¦ = ((π₯β2) / π) β (ββπ¦) = (ββ((π₯β2) / π))) |
135 | 134 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π¦ = ((π₯β2) / π) β (1...(ββπ¦)) = (1...(ββ((π₯β2) / π)))) |
136 | 135 | sumeq1d 15593 |
. . . . . . . . . . . 12
β’ (π¦ = ((π₯β2) / π) β Ξ£π β (1...(ββπ¦))(1 / (ββπ)) = Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ))) |
137 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π¦ = ((π₯β2) / π) β (ββπ¦) = (ββ((π₯β2) / π))) |
138 | 137 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π¦ = ((π₯β2) / π) β (2 Β· (ββπ¦)) = (2 Β·
(ββ((π₯β2)
/ π)))) |
139 | 136, 138 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π¦ = ((π₯β2) / π) β (Ξ£π β (1...(ββπ¦))(1 / (ββπ)) β (2 Β·
(ββπ¦))) =
(Ξ£π β
(1...(ββ((π₯β2) / π)))(1 / (ββπ)) β (2 Β· (ββ((π₯β2) / π))))) |
140 | | dchrisum0lem2.h |
. . . . . . . . . . 11
β’ π» = (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))) |
141 | | ovex 7395 |
. . . . . . . . . . 11
β’
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦))) β V |
142 | 139, 140,
141 | fvmpt3i 6958 |
. . . . . . . . . 10
β’ (((π₯β2) / π) β β+ β (π»β((π₯β2) / π)) = (Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ)) β (2 Β· (ββ((π₯β2) / π))))) |
143 | 121, 142 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π»β((π₯β2) / π)) = (Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ)) β (2 Β· (ββ((π₯β2) / π))))) |
144 | 143 | oveq2d 7378 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) = (((πβ(πΏβπ)) / (ββπ)) Β· (Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ)) β (2 Β· (ββ((π₯β2) / π)))))) |
145 | 103, 108,
109 | divrecd 11941 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = (((πβ(πΏβπ)) / (ββπ)) Β· (1 / (ββπ)))) |
146 | 145 | sumeq2dv 15595 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) Β· (1 / (ββπ)))) |
147 | 98, 102, 131 | fsummulc2 15676 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ))) = Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) Β· (1 / (ββπ)))) |
148 | 146, 147 | eqtr4d 2780 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = (((πβ(πΏβπ)) / (ββπ)) Β· Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ)))) |
149 | 148 | oveq1d 7377 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (Ξ£π β
(1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π))))) = ((((πβ(πΏβπ)) / (ββπ)) Β· Ξ£π β (1...(ββ((π₯β2) / π)))(1 / (ββπ))) β (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π)))))) |
150 | 133, 144,
149 | 3eqtr4d 2787 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) = (Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π)))))) |
151 | 150 | sumeq2dv 15595 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) = Ξ£π β (1...(ββπ₯))(Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π)))))) |
152 | | mulcl 11142 |
. . . . . . . . . 10
β’ ((2
β β β§ π₯
β β) β (2 Β· π₯) β β) |
153 | 27, 3, 152 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β (2
Β· π₯) β
β) |
154 | 4, 153, 23 | fsummulc2 15676 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β ((2
Β· π₯) Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)) = Ξ£π β (1...(ββπ₯))((2 Β· π₯) Β· ((πβ(πΏβπ)) / π))) |
155 | 1, 3, 24 | mulassd 11185 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β ((2
Β· π₯) Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)) = (2 Β· (π₯ Β· Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π)))) |
156 | 153 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (2 Β· π₯)
β β) |
157 | 156, 102,
100, 101 | div12d 11974 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· π₯)
Β· (((πβ(πΏβπ)) / (ββπ)) / (ββπ))) = (((πβ(πΏβπ)) / (ββπ)) Β· ((2 Β· π₯) / (ββπ)))) |
158 | 99 | rpcnne0d 12973 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ)
β β β§ (ββπ) β 0)) |
159 | | divdiv1 11873 |
. . . . . . . . . . . . 13
β’ (((πβ(πΏβπ)) β β β§ ((ββπ) β β β§
(ββπ) β 0)
β§ ((ββπ)
β β β§ (ββπ) β 0)) β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = ((πβ(πΏβπ)) / ((ββπ) Β· (ββπ)))) |
160 | 17, 158, 158, 159 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = ((πβ(πΏβπ)) / ((ββπ) Β· (ββπ)))) |
161 | 20 | rprege0d 12971 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β β
β§ 0 β€ π)) |
162 | | remsqsqrt 15148 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ 0 β€
π) β
((ββπ) Β·
(ββπ)) = π) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ)
Β· (ββπ))
= π) |
164 | 163 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) / ((ββπ) Β· (ββπ))) = ((πβ(πΏβπ)) / π)) |
165 | 160, 164 | eqtr2d 2778 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) / π) = (((πβ(πΏβπ)) / (ββπ)) / (ββπ))) |
166 | 165 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· π₯)
Β· ((πβ(πΏβπ)) / π)) = ((2 Β· π₯) Β· (((πβ(πΏβπ)) / (ββπ)) / (ββπ)))) |
167 | 119 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯β2) β
β+) |
168 | 167 | rprege0d 12971 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((π₯β2) β
β β§ 0 β€ (π₯β2))) |
169 | | sqrtdiv 15157 |
. . . . . . . . . . . . . . 15
β’ ((((π₯β2) β β β§ 0
β€ (π₯β2)) β§
π β
β+) β (ββ((π₯β2) / π)) = ((ββ(π₯β2)) / (ββπ))) |
170 | 168, 20, 169 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ((π₯β2) / π)) = ((ββ(π₯β2)) / (ββπ))) |
171 | 38 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ 0 β€ π₯)) |
172 | | sqrtsq 15161 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββ(π₯β2))
= π₯) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ(π₯β2)) = π₯) |
174 | 173 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββ(π₯β2)) / (ββπ)) = (π₯ / (ββπ))) |
175 | 170, 174 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ((π₯β2) / π)) = (π₯ / (ββπ))) |
176 | 175 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (2 Β· (ββ((π₯β2) / π))) = (2 Β· (π₯ / (ββπ)))) |
177 | | 2cnd 12238 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 2 β β) |
178 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π₯ β
β) |
179 | | divass 11838 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ π₯
β β β§ ((ββπ) β β β§ (ββπ) β 0)) β ((2 Β·
π₯) / (ββπ)) = (2 Β· (π₯ / (ββπ)))) |
180 | 177, 178,
158, 179 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· π₯) /
(ββπ)) = (2
Β· (π₯ /
(ββπ)))) |
181 | 176, 180 | eqtr4d 2780 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (2 Β· (ββ((π₯β2) / π))) = ((2 Β· π₯) / (ββπ))) |
182 | 181 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π)))) = (((πβ(πΏβπ)) / (ββπ)) Β· ((2 Β· π₯) / (ββπ)))) |
183 | 157, 166,
182 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· π₯)
Β· ((πβ(πΏβπ)) / π)) = (((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π))))) |
184 | 183 | sumeq2dv 15595 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((2
Β· π₯) Β·
((πβ(πΏβπ)) / π)) = Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π))))) |
185 | 154, 155,
184 | 3eqtr3d 2785 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (2
Β· (π₯ Β·
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π))) = Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π))))) |
186 | 185 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β (2 Β· (π₯ Β· Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π)))) = (Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (2 Β·
(ββ((π₯β2)
/ π)))))) |
187 | 128, 151,
186 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) = (Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β (2 Β· (π₯ Β· Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π))))) |
188 | 187 | mpteq2dva 5210 |
. . . 4
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π)))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β (2 Β· (π₯ Β· Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π)))))) |
189 | | dchrisum0lem1.f |
. . . . 5
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
190 | | dchrisum0.c |
. . . . 5
β’ (π β πΆ β (0[,)+β)) |
191 | | dchrisum0.s |
. . . . 5
β’ (π β seq1( + , πΉ) β π) |
192 | | dchrisum0.1 |
. . . . 5
β’ (π β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π)) β€ (πΆ / (ββπ¦))) |
193 | | dchrisum0lem2.u |
. . . . 5
β’ (π β π» βπ π) |
194 | 6, 8, 66, 5, 7, 67, 9, 11, 189, 190, 191, 192, 140, 193 | dchrisum0lem2a 26881 |
. . . 4
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π)))) β π(1)) |
195 | 188, 194 | eqeltrrd 2839 |
. . 3
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β (2 Β· (π₯ Β· Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / π))))) β π(1)) |
196 | 112, 114,
195 | o1dif 15519 |
. 2
β’ (π β ((π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1) β (π₯ β β+
β¦ (2 Β· (π₯
Β· Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / π)))) β π(1))) |
197 | 97, 196 | mpbird 257 |
1
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1)) |