Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . 4
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
2 | | simpl 484 |
. . . . 5
β’ ((π β§ π₯ β β+) β π) |
3 | | elfznn 13477 |
. . . . 5
β’ (π β
(1...(ββπ₯))
β π β
β) |
4 | | rpvmasum2.g |
. . . . . . 7
β’ πΊ = (DChrβπ) |
5 | | rpvmasum.z |
. . . . . . 7
β’ π =
(β€/nβ€βπ) |
6 | | rpvmasum2.d |
. . . . . . 7
β’ π· = (BaseβπΊ) |
7 | | rpvmasum.l |
. . . . . . 7
β’ πΏ = (β€RHomβπ) |
8 | | rpvmasum2.w |
. . . . . . . . . . 11
β’ π = {π¦ β (π· β { 1 }) β£ Ξ£π β β ((π¦β(πΏβπ)) / π) = 0} |
9 | 8 | ssrab3 4045 |
. . . . . . . . . 10
β’ π β (π· β { 1 }) |
10 | | dchrisum0.b |
. . . . . . . . . 10
β’ (π β π β π) |
11 | 9, 10 | sselid 3947 |
. . . . . . . . 9
β’ (π β π β (π· β { 1 })) |
12 | 11 | eldifad 3927 |
. . . . . . . 8
β’ (π β π β π·) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β π·) |
14 | | nnz 12527 |
. . . . . . . 8
β’ (π β β β π β
β€) |
15 | 14 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β) β π β β€) |
16 | 4, 5, 6, 7, 13, 15 | dchrzrhcl 26609 |
. . . . . 6
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
17 | | nnrp 12933 |
. . . . . . . . 9
β’ (π β β β π β
β+) |
18 | 17 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β+) |
19 | 18 | rpsqrtcld 15303 |
. . . . . . 7
β’ ((π β§ π β β) β (ββπ) β
β+) |
20 | 19 | rpcnd 12966 |
. . . . . 6
β’ ((π β§ π β β) β (ββπ) β
β) |
21 | 19 | rpne0d 12969 |
. . . . . 6
β’ ((π β§ π β β) β (ββπ) β 0) |
22 | 16, 20, 21 | divcld 11938 |
. . . . 5
β’ ((π β§ π β β) β ((πβ(πΏβπ)) / (ββπ)) β β) |
23 | 2, 3, 22 | syl2an 597 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) / (ββπ)) β β) |
24 | 1, 23 | fsumcl 15625 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) β β) |
25 | | dchrisum0lem2.u |
. . . . 5
β’ (π β π» βπ π) |
26 | | rlimcl 15392 |
. . . . 5
β’ (π» βπ
π β π β β) |
27 | 25, 26 | syl 17 |
. . . 4
β’ (π β π β β) |
28 | 27 | adantr 482 |
. . 3
β’ ((π β§ π₯ β β+) β π β
β) |
29 | | 0xr 11209 |
. . . . . . . . 9
β’ 0 β
β* |
30 | | 0lt1 11684 |
. . . . . . . . 9
β’ 0 <
1 |
31 | | df-ioo 13275 |
. . . . . . . . . 10
β’ (,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ < π§ β§ π§ < π¦)}) |
32 | | df-ico 13277 |
. . . . . . . . . 10
β’ [,) =
(π₯ β
β*, π¦
β β* β¦ {π§ β β* β£ (π₯ β€ π§ β§ π§ < π¦)}) |
33 | | xrltletr 13083 |
. . . . . . . . . 10
β’ ((0
β β* β§ 1 β β* β§ π€ β β*)
β ((0 < 1 β§ 1 β€ π€) β 0 < π€)) |
34 | 31, 32, 33 | ixxss1 13289 |
. . . . . . . . 9
β’ ((0
β β* β§ 0 < 1) β (1[,)+β) β
(0(,)+β)) |
35 | 29, 30, 34 | mp2an 691 |
. . . . . . . 8
β’
(1[,)+β) β (0(,)+β) |
36 | | ioorp 13349 |
. . . . . . . 8
β’
(0(,)+β) = β+ |
37 | 35, 36 | sseqtri 3985 |
. . . . . . 7
β’
(1[,)+β) β β+ |
38 | | resmpt 5996 |
. . . . . . 7
β’
((1[,)+β) β β+ β ((π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) βΎ (1[,)+β)) = (π₯ β (1[,)+β) β¦
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)))) |
39 | 37, 38 | ax-mp 5 |
. . . . . 6
β’ ((π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) βΎ (1[,)+β)) = (π₯ β (1[,)+β) β¦
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) |
40 | 37 | sseli 3945 |
. . . . . . . . 9
β’ (π₯ β (1[,)+β) β
π₯ β
β+) |
41 | 3 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
42 | | 2fveq3 6852 |
. . . . . . . . . . . 12
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
43 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (ββπ) = (ββπ)) |
44 | 42, 43 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π = π β ((πβ(πΏβπ)) / (ββπ)) = ((πβ(πΏβπ)) / (ββπ))) |
45 | | dchrisum0lem1.f |
. . . . . . . . . . 11
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
46 | | ovex 7395 |
. . . . . . . . . . 11
β’ ((πβ(πΏβπ)) / (ββπ)) β V |
47 | 44, 45, 46 | fvmpt3i 6958 |
. . . . . . . . . 10
β’ (π β β β (πΉβπ) = ((πβ(πΏβπ)) / (ββπ))) |
48 | 41, 47 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΉβπ) = ((πβ(πΏβπ)) / (ββπ))) |
49 | 40, 48 | sylanl2 680 |
. . . . . . . 8
β’ (((π β§ π₯ β (1[,)+β)) β§ π β
(1...(ββπ₯)))
β (πΉβπ) = ((πβ(πΏβπ)) / (ββπ))) |
50 | | 1re 11162 |
. . . . . . . . . . . 12
β’ 1 β
β |
51 | | elicopnf 13369 |
. . . . . . . . . . . 12
β’ (1 β
β β (π₯ β
(1[,)+β) β (π₯
β β β§ 1 β€ π₯))) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . 11
β’ (π₯ β (1[,)+β) β
(π₯ β β β§ 1
β€ π₯)) |
53 | | flge1nn 13733 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ 1 β€
π₯) β
(ββπ₯) β
β) |
54 | 52, 53 | sylbi 216 |
. . . . . . . . . 10
β’ (π₯ β (1[,)+β) β
(ββπ₯) β
β) |
55 | 54 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π₯ β (1[,)+β)) β
(ββπ₯) β
β) |
56 | | nnuz 12813 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
57 | 55, 56 | eleqtrdi 2848 |
. . . . . . . 8
β’ ((π β§ π₯ β (1[,)+β)) β
(ββπ₯) β
(β€β₯β1)) |
58 | 40, 23 | sylanl2 680 |
. . . . . . . 8
β’ (((π β§ π₯ β (1[,)+β)) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) / (ββπ)) β β) |
59 | 49, 57, 58 | fsumser 15622 |
. . . . . . 7
β’ ((π β§ π₯ β (1[,)+β)) β Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) = (seq1( + , πΉ)β(ββπ₯))) |
60 | 59 | mpteq2dva 5210 |
. . . . . 6
β’ (π β (π₯ β (1[,)+β) β¦ Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) = (π₯ β (1[,)+β) β¦ (seq1( + ,
πΉ)β(ββπ₯)))) |
61 | 39, 60 | eqtrid 2789 |
. . . . 5
β’ (π β ((π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) βΎ (1[,)+β)) = (π₯ β (1[,)+β) β¦
(seq1( + , πΉ)β(ββπ₯)))) |
62 | | fveq2 6847 |
. . . . . . 7
β’ (π = (ββπ₯) β (seq1( + , πΉ)βπ) = (seq1( + , πΉ)β(ββπ₯))) |
63 | | rpssre 12929 |
. . . . . . . . 9
β’
β+ β β |
64 | 63 | a1i 11 |
. . . . . . . 8
β’ (π β β+
β β) |
65 | 37, 64 | sstrid 3960 |
. . . . . . 7
β’ (π β (1[,)+β) β
β) |
66 | | 1zzd 12541 |
. . . . . . 7
β’ (π β 1 β
β€) |
67 | 44 | cbvmptv 5223 |
. . . . . . . . . . . . 13
β’ (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
68 | 45, 67 | eqtri 2765 |
. . . . . . . . . . . 12
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
69 | 22, 68 | fmptd 7067 |
. . . . . . . . . . 11
β’ (π β πΉ:ββΆβ) |
70 | 69 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβπ) β β) |
71 | 56, 66, 70 | serf 13943 |
. . . . . . . . 9
β’ (π β seq1( + , πΉ):ββΆβ) |
72 | 71 | feqmptd 6915 |
. . . . . . . 8
β’ (π β seq1( + , πΉ) = (π β β β¦ (seq1( + , πΉ)βπ))) |
73 | | dchrisum0.s |
. . . . . . . 8
β’ (π β seq1( + , πΉ) β π) |
74 | 72, 73 | eqbrtrrd 5134 |
. . . . . . 7
β’ (π β (π β β β¦ (seq1( + , πΉ)βπ)) β π) |
75 | 71 | ffvelcdmda 7040 |
. . . . . . 7
β’ ((π β§ π β β) β (seq1( + , πΉ)βπ) β β) |
76 | 52 | simprbi 498 |
. . . . . . . 8
β’ (π₯ β (1[,)+β) β 1
β€ π₯) |
77 | 76 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β (1[,)+β)) β 1 β€ π₯) |
78 | 56, 62, 65, 66, 74, 75, 77 | climrlim2 15436 |
. . . . . 6
β’ (π β (π₯ β (1[,)+β) β¦ (seq1( + ,
πΉ)β(ββπ₯))) βπ π) |
79 | | rlimo1 15506 |
. . . . . 6
β’ ((π₯ β (1[,)+β) β¦
(seq1( + , πΉ)β(ββπ₯))) βπ π β (π₯ β (1[,)+β) β¦ (seq1( + ,
πΉ)β(ββπ₯))) β π(1)) |
80 | 78, 79 | syl 17 |
. . . . 5
β’ (π β (π₯ β (1[,)+β) β¦ (seq1( + ,
πΉ)β(ββπ₯))) β π(1)) |
81 | 61, 80 | eqeltrd 2838 |
. . . 4
β’ (π β ((π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) βΎ (1[,)+β)) β
π(1)) |
82 | 24 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))):β+βΆβ) |
83 | | 1red 11163 |
. . . . 5
β’ (π β 1 β
β) |
84 | 82, 64, 83 | o1resb 15455 |
. . . 4
β’ (π β ((π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) β π(1) β ((π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) βΎ (1[,)+β)) β
π(1))) |
85 | 81, 84 | mpbird 257 |
. . 3
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ))) β π(1)) |
86 | | o1const 15509 |
. . . 4
β’
((β+ β β β§ π β β) β (π₯ β β+ β¦ π) β
π(1)) |
87 | 63, 27, 86 | sylancr 588 |
. . 3
β’ (π β (π₯ β β+ β¦ π) β
π(1)) |
88 | 24, 28, 85, 87 | o1mul2 15514 |
. 2
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) Β· π)) β π(1)) |
89 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
90 | | 2z 12542 |
. . . . . . . . 9
β’ 2 β
β€ |
91 | | rpexpcl 13993 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 2 β β€) β (π₯β2) β
β+) |
92 | 89, 90, 91 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β (π₯β2) β
β+) |
93 | 3 | nnrpd 12962 |
. . . . . . . 8
β’ (π β
(1...(ββπ₯))
β π β
β+) |
94 | | rpdivcl 12947 |
. . . . . . . 8
β’ (((π₯β2) β
β+ β§ π
β β+) β ((π₯β2) / π) β
β+) |
95 | 92, 93, 94 | syl2an 597 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((π₯β2) / π) β
β+) |
96 | | dchrisum0lem2.h |
. . . . . . . . 9
β’ π» = (π¦ β β+ β¦
(Ξ£π β
(1...(ββπ¦))(1 /
(ββπ)) β
(2 Β· (ββπ¦)))) |
97 | 96 | divsqrsumf 26346 |
. . . . . . . 8
β’ π»:β+βΆβ |
98 | 97 | ffvelcdmi 7039 |
. . . . . . 7
β’ (((π₯β2) / π) β β+ β (π»β((π₯β2) / π)) β β) |
99 | 95, 98 | syl 17 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π»β((π₯β2) / π)) β β) |
100 | 99 | recnd 11190 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π»β((π₯β2) / π)) β β) |
101 | 23, 100 | mulcld 11182 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β β) |
102 | 1, 101 | fsumcl 15625 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β β) |
103 | 24, 28 | mulcld 11182 |
. . 3
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) Β· π) β β) |
104 | 25 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π»
βπ π) |
105 | 104, 26 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
106 | 23, 105 | mulcld 11182 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· π) β β) |
107 | 1, 101, 106 | fsumsub 15680 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β (((πβ(πΏβπ)) / (ββπ)) Β· π)) = (Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· π))) |
108 | 23, 100, 105 | subdid 11618 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π)) = ((((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β (((πβ(πΏβπ)) / (ββπ)) Β· π))) |
109 | 108 | sumeq2dv 15595 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π)) = Ξ£π β (1...(ββπ₯))((((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β (((πβ(πΏβπ)) / (ββπ)) Β· π))) |
110 | 1, 28, 23 | fsummulc1 15677 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) Β· π) = Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· π)) |
111 | 110 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) Β· π)) = (Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· π))) |
112 | 107, 109,
111 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π)) = (Ξ£π β (1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) Β· π))) |
113 | 112 | mpteq2dva 5210 |
. . . 4
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) Β· π)))) |
114 | 100, 105 | subcld 11519 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((π»β((π₯β2) / π)) β π) β β) |
115 | 23, 114 | mulcld 11182 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π)) β β) |
116 | 1, 115 | fsumcl 15625 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π)) β β) |
117 | 116 | abscld 15328 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β β) |
118 | 115 | abscld 15328 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β β) |
119 | 1, 118 | fsumrecl 15626 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β β) |
120 | | 1red 11163 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β 1 β
β) |
121 | 1, 115 | fsumabs 15693 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β€ Ξ£π β (1...(ββπ₯))(absβ(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π)))) |
122 | | rprege0 12937 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β (π₯ β β
β§ 0 β€ π₯)) |
123 | 122 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (π₯ β β β§ 0 β€
π₯)) |
124 | 123 | simpld 496 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β π₯ β
β) |
125 | | reflcl 13708 |
. . . . . . . . . 10
β’ (π₯ β β β
(ββπ₯) β
β) |
126 | 124, 125 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β) |
127 | 126, 89 | rerpdivcld 12995 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((ββπ₯) / π₯) β
β) |
128 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π₯ β
β+) |
129 | 128 | rprecred 12975 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / π₯) β
β) |
130 | 23 | abscld 15328 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) / (ββπ))) β β) |
131 | 93 | rpsqrtcld 15303 |
. . . . . . . . . . . . . 14
β’ (π β
(1...(ββπ₯))
β (ββπ)
β β+) |
132 | 131 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β β+) |
133 | 132 | rprecred 12975 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / (ββπ)) β β) |
134 | 114 | abscld 15328 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((π»β((π₯β2) / π)) β π)) β β) |
135 | 132, 128 | rpdivcld 12981 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ) /
π₯) β
β+) |
136 | 63, 135 | sselid 3947 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ) /
π₯) β
β) |
137 | 23 | absge0d 15336 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ((πβ(πΏβπ)) / (ββπ)))) |
138 | 114 | absge0d 15336 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ((π»β((π₯β2) / π)) β π))) |
139 | 2, 3, 16 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πβ(πΏβπ)) β β) |
140 | 132 | rpcnd 12966 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β β) |
141 | 132 | rpne0d 12969 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β 0) |
142 | 139, 140,
141 | absdivd 15347 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) / (ββπ))) = ((absβ(πβ(πΏβπ))) / (absβ(ββπ)))) |
143 | 132 | rprege0d 12971 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ)
β β β§ 0 β€ (ββπ))) |
144 | | absid 15188 |
. . . . . . . . . . . . . . . 16
β’
(((ββπ)
β β β§ 0 β€ (ββπ)) β (absβ(ββπ)) = (ββπ)) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(ββπ)) = (ββπ)) |
146 | 145 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(πβ(πΏβπ))) / (absβ(ββπ))) = ((absβ(πβ(πΏβπ))) / (ββπ))) |
147 | 142, 146 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) / (ββπ))) = ((absβ(πβ(πΏβπ))) / (ββπ))) |
148 | 139 | abscld 15328 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(πβ(πΏβπ))) β β) |
149 | | 1red 11163 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 1 β β) |
150 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(Baseβπ) =
(Baseβπ) |
151 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β π·) |
152 | | rpvmasum.a |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
153 | 152 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β
β0) |
154 | 5, 150, 7 | znzrhfo 20970 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β πΏ:β€βontoβ(Baseβπ)) |
155 | | fof 6761 |
. . . . . . . . . . . . . . . . . 18
β’ (πΏ:β€βontoβ(Baseβπ) β πΏ:β€βΆ(Baseβπ)) |
156 | 153, 154,
155 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΏ:β€βΆ(Baseβπ)) |
157 | 156 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β β+) β πΏ:β€βΆ(Baseβπ)) |
158 | | elfzelz 13448 |
. . . . . . . . . . . . . . . 16
β’ (π β
(1...(ββπ₯))
β π β
β€) |
159 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . 16
β’ ((πΏ:β€βΆ(Baseβπ) β§ π β β€) β (πΏβπ) β (Baseβπ)) |
160 | 157, 158,
159 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΏβπ) β (Baseβπ)) |
161 | 4, 6, 5, 150, 151, 160 | dchrabs2 26626 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(πβ(πΏβπ))) β€ 1) |
162 | 148, 149,
132, 161 | lediv1dd 13022 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(πβ(πΏβπ))) / (ββπ)) β€ (1 / (ββπ))) |
163 | 147, 162 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) / (ββπ))) β€ (1 / (ββπ))) |
164 | 96, 104 | divsqrtsum2 26348 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ ((π₯β2) / π) β β+)
β (absβ((π»β((π₯β2) / π)) β π)) β€ (1 / (ββ((π₯β2) / π)))) |
165 | 95, 164 | mpdan 686 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((π»β((π₯β2) / π)) β π)) β€ (1 / (ββ((π₯β2) / π)))) |
166 | 92 | rprege0d 12971 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β β+) β ((π₯β2) β β β§ 0
β€ (π₯β2))) |
167 | | sqrtdiv 15157 |
. . . . . . . . . . . . . . . . 17
β’ ((((π₯β2) β β β§ 0
β€ (π₯β2)) β§
π β
β+) β (ββ((π₯β2) / π)) = ((ββ(π₯β2)) / (ββπ))) |
168 | 166, 93, 167 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ((π₯β2) / π)) = ((ββ(π₯β2)) / (ββπ))) |
169 | 122 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ 0 β€ π₯)) |
170 | | sqrtsq 15161 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββ(π₯β2))
= π₯) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ(π₯β2)) = π₯) |
172 | 171 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββ(π₯β2)) / (ββπ)) = (π₯ / (ββπ))) |
173 | 168, 172 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ((π₯β2) / π)) = (π₯ / (ββπ))) |
174 | 173 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / (ββ((π₯β2) / π))) = (1 / (π₯ / (ββπ)))) |
175 | | rpcnne0 12940 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β (π₯ β β
β§ π₯ β
0)) |
176 | 175 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ β β
β§ π₯ β
0)) |
177 | 132 | rpcnne0d 12973 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ)
β β β§ (ββπ) β 0)) |
178 | | recdiv 11868 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π₯ β 0) β§
((ββπ) β
β β§ (ββπ) β 0)) β (1 / (π₯ / (ββπ))) = ((ββπ) / π₯)) |
179 | 176, 177,
178 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / (π₯ /
(ββπ))) =
((ββπ) / π₯)) |
180 | 174, 179 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / (ββ((π₯β2) / π))) = ((ββπ) / π₯)) |
181 | 165, 180 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((π»β((π₯β2) / π)) β π)) β€ ((ββπ) / π₯)) |
182 | 130, 133,
134, 136, 137, 138, 163, 181 | lemul12ad 12104 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ((πβ(πΏβπ)) / (ββπ))) Β· (absβ((π»β((π₯β2) / π)) β π))) β€ ((1 / (ββπ)) Β·
((ββπ) / π₯))) |
183 | 23, 114 | absmuld 15346 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) = ((absβ((πβ(πΏβπ)) / (ββπ))) Β· (absβ((π»β((π₯β2) / π)) β π)))) |
184 | | 1cnd 11157 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 1 β β) |
185 | | dmdcan 11872 |
. . . . . . . . . . . . 13
β’
((((ββπ)
β β β§ (ββπ) β 0) β§ (π₯ β β β§ π₯ β 0) β§ 1 β β) β
(((ββπ) / π₯) Β· (1 /
(ββπ))) = (1 /
π₯)) |
186 | 177, 176,
184, 185 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ββπ)
/ π₯) Β· (1 /
(ββπ))) = (1 /
π₯)) |
187 | 135 | rpcnd 12966 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ) /
π₯) β
β) |
188 | | reccl 11827 |
. . . . . . . . . . . . . 14
β’
(((ββπ)
β β β§ (ββπ) β 0) β (1 / (ββπ)) β
β) |
189 | 177, 188 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / (ββπ)) β β) |
190 | 187, 189 | mulcomd 11183 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ββπ)
/ π₯) Β· (1 /
(ββπ))) = ((1 /
(ββπ)) Β·
((ββπ) / π₯))) |
191 | 186, 190 | eqtr3d 2779 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / π₯) = ((1 /
(ββπ)) Β·
((ββπ) / π₯))) |
192 | 182, 183,
191 | 3brtr4d 5142 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β€ (1 / π₯)) |
193 | 1, 118, 129, 192 | fsumle 15691 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β€ Ξ£π β (1...(ββπ₯))(1 / π₯)) |
194 | | flge0nn0 13732 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββπ₯) β
β0) |
195 | | hashfz1 14253 |
. . . . . . . . . . . 12
β’
((ββπ₯)
β β0 β (β―β(1...(ββπ₯))) = (ββπ₯)) |
196 | 123, 194,
195 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β
(β―β(1...(ββπ₯))) = (ββπ₯)) |
197 | 196 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
((β―β(1...(ββπ₯))) Β· (1 / π₯)) = ((ββπ₯) Β· (1 / π₯))) |
198 | 89 | rpreccld 12974 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β+) |
199 | 198 | rpcnd 12966 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β) |
200 | | fsumconst 15682 |
. . . . . . . . . . 11
β’
(((1...(ββπ₯)) β Fin β§ (1 / π₯) β β) β Ξ£π β
(1...(ββπ₯))(1 /
π₯) =
((β―β(1...(ββπ₯))) Β· (1 / π₯))) |
201 | 1, 199, 200 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(1 /
π₯) =
((β―β(1...(ββπ₯))) Β· (1 / π₯))) |
202 | 126 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β) |
203 | 175 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β (π₯ β β β§ π₯ β 0)) |
204 | 203 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β π₯ β
β) |
205 | 203 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β π₯ β 0) |
206 | 202, 204,
205 | divrecd 11941 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
((ββπ₯) / π₯) = ((ββπ₯) Β· (1 / π₯))) |
207 | 197, 201,
206 | 3eqtr4d 2787 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(1 /
π₯) = ((ββπ₯) / π₯)) |
208 | 193, 207 | breqtrd 5136 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β€ ((ββπ₯) / π₯)) |
209 | | flle 13711 |
. . . . . . . . . . 11
β’ (π₯ β β β
(ββπ₯) β€
π₯) |
210 | 124, 209 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
(ββπ₯) β€
π₯) |
211 | 124 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β π₯ β
β) |
212 | 211 | mulid1d 11179 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (π₯ Β· 1) = π₯) |
213 | 210, 212 | breqtrrd 5138 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(ββπ₯) β€
(π₯ Β·
1)) |
214 | | rpregt0 12936 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
215 | 214 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (π₯ β β β§ 0 <
π₯)) |
216 | | ledivmul 12038 |
. . . . . . . . . 10
β’
(((ββπ₯)
β β β§ 1 β β β§ (π₯ β β β§ 0 < π₯)) β (((ββπ₯) / π₯) β€ 1 β (ββπ₯) β€ (π₯ Β· 1))) |
217 | 126, 120,
215, 216 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(((ββπ₯) / π₯) β€ 1 β
(ββπ₯) β€
(π₯ Β·
1))) |
218 | 213, 217 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((ββπ₯) / π₯) β€ 1) |
219 | 119, 127,
120, 208, 218 | letrd 11319 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β€ 1) |
220 | 117, 119,
120, 121, 219 | letrd 11319 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β€ 1) |
221 | 220 | adantrr 716 |
. . . . 5
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β€ 1) |
222 | 64, 116, 83, 83, 221 | elo1d 15425 |
. . . 4
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· ((π»β((π₯β2) / π)) β π))) β π(1)) |
223 | 113, 222 | eqeltrrd 2839 |
. . 3
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π))) β (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) Β· π))) β π(1)) |
224 | 102, 103,
223 | o1dif 15519 |
. 2
β’ (π β ((π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π)))) β π(1) β (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) / (ββπ)) Β· π)) β π(1))) |
225 | 88, 224 | mpbird 257 |
1
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) / (ββπ)) Β· (π»β((π₯β2) / π)))) β π(1)) |