Step | Hyp | Ref
| Expression |
1 | | fzodisj 13613 |
. . . . . . . . 9
β’
((1..^(πΌ + 1)) β©
((πΌ + 1)..^(π½ + 1))) =
β
|
2 | 1 | a1i 11 |
. . . . . . . 8
β’ (π β ((1..^(πΌ + 1)) β© ((πΌ + 1)..^(π½ + 1))) = β
) |
3 | | dchrisumlem2.4 |
. . . . . . . . . . . 12
β’ (π β πΌ β β) |
4 | 3 | peano2nnd 12177 |
. . . . . . . . . . 11
β’ (π β (πΌ + 1) β β) |
5 | | nnuz 12813 |
. . . . . . . . . . 11
β’ β =
(β€β₯β1) |
6 | 4, 5 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ (π β (πΌ + 1) β
(β€β₯β1)) |
7 | | dchrisumlem2.5 |
. . . . . . . . . . 11
β’ (π β π½ β (β€β₯βπΌ)) |
8 | | eluzp1p1 12798 |
. . . . . . . . . . 11
β’ (π½ β
(β€β₯βπΌ) β (π½ + 1) β
(β€β₯β(πΌ + 1))) |
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
β’ (π β (π½ + 1) β
(β€β₯β(πΌ + 1))) |
10 | | elfzuzb 13442 |
. . . . . . . . . 10
β’ ((πΌ + 1) β (1...(π½ + 1)) β ((πΌ + 1) β
(β€β₯β1) β§ (π½ + 1) β
(β€β₯β(πΌ + 1)))) |
11 | 6, 9, 10 | sylanbrc 584 |
. . . . . . . . 9
β’ (π β (πΌ + 1) β (1...(π½ + 1))) |
12 | | fzosplit 13612 |
. . . . . . . . 9
β’ ((πΌ + 1) β (1...(π½ + 1)) β (1..^(π½ + 1)) = ((1..^(πΌ + 1)) βͺ ((πΌ + 1)..^(π½ + 1)))) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
β’ (π β (1..^(π½ + 1)) = ((1..^(πΌ + 1)) βͺ ((πΌ + 1)..^(π½ + 1)))) |
14 | | fzofi 13886 |
. . . . . . . . 9
β’
(1..^(π½ + 1)) β
Fin |
15 | 14 | a1i 11 |
. . . . . . . 8
β’ (π β (1..^(π½ + 1)) β Fin) |
16 | | elfzouz 13583 |
. . . . . . . . . 10
β’ (π β (1..^(π½ + 1)) β π β
(β€β₯β1)) |
17 | 16, 5 | eleqtrrdi 2849 |
. . . . . . . . 9
β’ (π β (1..^(π½ + 1)) β π β β) |
18 | | rpvmasum.g |
. . . . . . . . . . 11
β’ πΊ = (DChrβπ) |
19 | | rpvmasum.z |
. . . . . . . . . . 11
β’ π =
(β€/nβ€βπ) |
20 | | rpvmasum.d |
. . . . . . . . . . 11
β’ π· = (BaseβπΊ) |
21 | | rpvmasum.l |
. . . . . . . . . . 11
β’ πΏ = (β€RHomβπ) |
22 | | dchrisum.b |
. . . . . . . . . . . 12
β’ (π β π β π·) |
23 | 22 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β π·) |
24 | | nnz 12527 |
. . . . . . . . . . . 12
β’ (π β β β π β
β€) |
25 | 24 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β€) |
26 | 18, 19, 20, 21, 23, 25 | dchrzrhcl 26609 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
27 | | rpvmasum.a |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
28 | | rpvmasum.1 |
. . . . . . . . . . . . . 14
β’ 1 =
(0gβπΊ) |
29 | | dchrisum.n1 |
. . . . . . . . . . . . . 14
β’ (π β π β 1 ) |
30 | | dchrisum.2 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β π΄ = π΅) |
31 | | dchrisum.3 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
32 | | dchrisum.4 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β+) β π΄ β
β) |
33 | | dchrisum.5 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
34 | | dchrisum.6 |
. . . . . . . . . . . . . 14
β’ (π β (π β β+ β¦ π΄) βπ
0) |
35 | | dchrisum.7 |
. . . . . . . . . . . . . 14
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· π΄)) |
36 | 19, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35 | dchrisumlema 26852 |
. . . . . . . . . . . . 13
β’ (π β ((π β β+ β
β¦π / πβ¦π΄ β β) β§ (π β (π[,)+β) β 0 β€
β¦π / πβ¦π΄))) |
37 | 36 | simpld 496 |
. . . . . . . . . . . 12
β’ (π β (π β β+ β
β¦π / πβ¦π΄ β β)) |
38 | | nnrp 12933 |
. . . . . . . . . . . 12
β’ (π β β β π β
β+) |
39 | 37, 38 | impel 507 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β β¦π / πβ¦π΄ β β) |
40 | 39 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π β β) β β¦π / πβ¦π΄ β β) |
41 | 26, 40 | mulcld 11182 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) |
42 | 17, 41 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π β (1..^(π½ + 1))) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) |
43 | 2, 13, 15, 42 | fsumsplit 15633 |
. . . . . . 7
β’ (π β Ξ£π β (1..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = (Ξ£π β (1..^(πΌ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) + Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄))) |
44 | | eluzelz 12780 |
. . . . . . . . 9
β’ (π½ β
(β€β₯βπΌ) β π½ β β€) |
45 | | fzval3 13648 |
. . . . . . . . 9
β’ (π½ β β€ β
(1...π½) = (1..^(π½ + 1))) |
46 | 7, 44, 45 | 3syl 18 |
. . . . . . . 8
β’ (π β (1...π½) = (1..^(π½ + 1))) |
47 | 46 | sumeq1d 15593 |
. . . . . . 7
β’ (π β Ξ£π β (1...π½)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = Ξ£π β (1..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
48 | 3 | nnzd 12533 |
. . . . . . . . . 10
β’ (π β πΌ β β€) |
49 | | fzval3 13648 |
. . . . . . . . . 10
β’ (πΌ β β€ β
(1...πΌ) = (1..^(πΌ + 1))) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
β’ (π β (1...πΌ) = (1..^(πΌ + 1))) |
51 | 50 | sumeq1d 15593 |
. . . . . . . 8
β’ (π β Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = Ξ£π β (1..^(πΌ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
52 | 51 | oveq1d 7377 |
. . . . . . 7
β’ (π β (Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) + Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) = (Ξ£π β (1..^(πΌ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) + Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄))) |
53 | 43, 47, 52 | 3eqtr4d 2787 |
. . . . . 6
β’ (π β Ξ£π β (1...π½)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = (Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) + Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄))) |
54 | | elfznn 13477 |
. . . . . . . 8
β’ (π β (1...π½) β π β β) |
55 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β β) |
56 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²ππ |
57 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π(πβ(πΏβπ)) |
58 | | nfcv 2908 |
. . . . . . . . . . 11
β’
β²π
Β· |
59 | | nfcsb1v 3885 |
. . . . . . . . . . 11
β’
β²πβ¦π / πβ¦π΄ |
60 | 57, 58, 59 | nfov 7392 |
. . . . . . . . . 10
β’
β²π((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) |
61 | | 2fveq3 6852 |
. . . . . . . . . . 11
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
62 | | csbeq1a 3874 |
. . . . . . . . . . 11
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
63 | 61, 62 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = π β ((πβ(πΏβπ)) Β· π΄) = ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
64 | 56, 60, 63, 35 | fvmptf 6974 |
. . . . . . . . 9
β’ ((π β β β§ ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) β (πΉβπ) = ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
65 | 55, 41, 64 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβπ) = ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
66 | 54, 65 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (1...π½)) β (πΉβπ) = ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
67 | 3, 5 | eleqtrdi 2848 |
. . . . . . . 8
β’ (π β πΌ β
(β€β₯β1)) |
68 | | uztrn 12788 |
. . . . . . . 8
β’ ((π½ β
(β€β₯βπΌ) β§ πΌ β (β€β₯β1))
β π½ β
(β€β₯β1)) |
69 | 7, 67, 68 | syl2anc 585 |
. . . . . . 7
β’ (π β π½ β
(β€β₯β1)) |
70 | 54, 41 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (1...π½)) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) |
71 | 66, 69, 70 | fsumser 15622 |
. . . . . 6
β’ (π β Ξ£π β (1...π½)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = (seq1( + , πΉ)βπ½)) |
72 | 53, 71 | eqtr3d 2779 |
. . . . 5
β’ (π β (Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) + Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) = (seq1( + , πΉ)βπ½)) |
73 | | elfznn 13477 |
. . . . . . 7
β’ (π β (1...πΌ) β π β β) |
74 | 73, 65 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (1...πΌ)) β (πΉβπ) = ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
75 | 73, 41 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (1...πΌ)) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) |
76 | 74, 67, 75 | fsumser 15622 |
. . . . 5
β’ (π β Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = (seq1( + , πΉ)βπΌ)) |
77 | 72, 76 | oveq12d 7380 |
. . . 4
β’ (π β ((Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) + Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) β Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) = ((seq1( + , πΉ)βπ½) β (seq1( + , πΉ)βπΌ))) |
78 | | fzfid 13885 |
. . . . . 6
β’ (π β (1...πΌ) β Fin) |
79 | 78, 75 | fsumcl 15625 |
. . . . 5
β’ (π β Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) |
80 | | fzofi 13886 |
. . . . . . 7
β’ ((πΌ + 1)..^(π½ + 1)) β Fin |
81 | 80 | a1i 11 |
. . . . . 6
β’ (π β ((πΌ + 1)..^(π½ + 1)) β Fin) |
82 | | ssun2 4138 |
. . . . . . . . 9
β’ ((πΌ + 1)..^(π½ + 1)) β ((1..^(πΌ + 1)) βͺ ((πΌ + 1)..^(π½ + 1))) |
83 | 82, 13 | sseqtrrid 4002 |
. . . . . . . 8
β’ (π β ((πΌ + 1)..^(π½ + 1)) β (1..^(π½ + 1))) |
84 | 83 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β π β (1..^(π½ + 1))) |
85 | 84, 42 | syldan 592 |
. . . . . 6
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) |
86 | 81, 85 | fsumcl 15625 |
. . . . 5
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) |
87 | 79, 86 | pncan2d 11521 |
. . . 4
β’ (π β ((Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) + Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) β Ξ£π β (1...πΌ)((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) = Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
88 | 77, 87 | eqtr3d 2779 |
. . 3
β’ (π β ((seq1( + , πΉ)βπ½) β (seq1( + , πΉ)βπΌ)) = Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
89 | 88 | fveq2d 6851 |
. 2
β’ (π β (absβ((seq1( + ,
πΉ)βπ½) β (seq1( + , πΉ)βπΌ))) = (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄))) |
90 | 86 | abscld 15328 |
. . 3
β’ (π β (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) β β) |
91 | | 2re 12234 |
. . . . . 6
β’ 2 β
β |
92 | 91 | a1i 11 |
. . . . 5
β’ (π β 2 β
β) |
93 | | dchrisum.9 |
. . . . 5
β’ (π β π
β β) |
94 | 92, 93 | remulcld 11192 |
. . . 4
β’ (π β (2 Β· π
) β
β) |
95 | 39 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β β β¦π / πβ¦π΄ β β) |
96 | | csbeq1 3863 |
. . . . . . 7
β’ (π = (πΌ + 1) β β¦π / πβ¦π΄ = β¦(πΌ + 1) / πβ¦π΄) |
97 | 96 | eleq1d 2823 |
. . . . . 6
β’ (π = (πΌ + 1) β (β¦π / πβ¦π΄ β β β β¦(πΌ + 1) / πβ¦π΄ β β)) |
98 | 97 | rspcv 3580 |
. . . . 5
β’ ((πΌ + 1) β β β
(βπ β β
β¦π / πβ¦π΄ β β β β¦(πΌ + 1) / πβ¦π΄ β β)) |
99 | 4, 95, 98 | sylc 65 |
. . . 4
β’ (π β β¦(πΌ + 1) / πβ¦π΄ β β) |
100 | 94, 99 | remulcld 11192 |
. . 3
β’ (π β ((2 Β· π
) Β· β¦(πΌ + 1) / πβ¦π΄) β β) |
101 | | dchrisumlem2.1 |
. . . . 5
β’ (π β π β
β+) |
102 | 32 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β β+ π΄ β β) |
103 | | nfcsb1v 3885 |
. . . . . . 7
β’
β²πβ¦π / πβ¦π΄ |
104 | 103 | nfel1 2924 |
. . . . . 6
β’
β²πβ¦π / πβ¦π΄ β β |
105 | | csbeq1a 3874 |
. . . . . . 7
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
106 | 105 | eleq1d 2823 |
. . . . . 6
β’ (π = π β (π΄ β β β β¦π / πβ¦π΄ β β)) |
107 | 104, 106 | rspc 3572 |
. . . . 5
β’ (π β β+
β (βπ β
β+ π΄
β β β β¦π / πβ¦π΄ β β)) |
108 | 101, 102,
107 | sylc 65 |
. . . 4
β’ (π β β¦π / πβ¦π΄ β β) |
109 | 94, 108 | remulcld 11192 |
. . 3
β’ (π β ((2 Β· π
) Β· β¦π / πβ¦π΄) β β) |
110 | 69, 5 | eleqtrrdi 2849 |
. . . . . . . . . . . 12
β’ (π β π½ β β) |
111 | 110 | peano2nnd 12177 |
. . . . . . . . . . 11
β’ (π β (π½ + 1) β β) |
112 | 111 | nnrpd 12962 |
. . . . . . . . . 10
β’ (π β (π½ + 1) β
β+) |
113 | 19, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35 | dchrisumlema 26852 |
. . . . . . . . . . 11
β’ (π β (((π½ + 1) β β+ β
β¦(π½ + 1) /
πβ¦π΄ β β) β§ ((π½ + 1) β (π[,)+β) β 0 β€
β¦(π½ + 1) /
πβ¦π΄))) |
114 | 113 | simpld 496 |
. . . . . . . . . 10
β’ (π β ((π½ + 1) β β+ β
β¦(π½ + 1) /
πβ¦π΄ β
β)) |
115 | 112, 114 | mpd 15 |
. . . . . . . . 9
β’ (π β β¦(π½ + 1) / πβ¦π΄ β β) |
116 | 115 | recnd 11190 |
. . . . . . . 8
β’ (π β β¦(π½ + 1) / πβ¦π΄ β β) |
117 | | fzofi 13886 |
. . . . . . . . . 10
β’
(0..^(π½ + 1)) β
Fin |
118 | 117 | a1i 11 |
. . . . . . . . 9
β’ (π β (0..^(π½ + 1)) β Fin) |
119 | | elfzoelz 13579 |
. . . . . . . . . 10
β’ (π β (0..^(π½ + 1)) β π β β€) |
120 | 22 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β€) β π β π·) |
121 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β β€) β π β β€) |
122 | 18, 19, 20, 21, 120, 121 | dchrzrhcl 26609 |
. . . . . . . . . 10
β’ ((π β§ π β β€) β (πβ(πΏβπ)) β β) |
123 | 119, 122 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π β (0..^(π½ + 1))) β (πβ(πΏβπ)) β β) |
124 | 118, 123 | fsumcl 15625 |
. . . . . . . 8
β’ (π β Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)) β β) |
125 | 116, 124 | mulcld 11182 |
. . . . . . 7
β’ (π β (β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β β) |
126 | 99 | recnd 11190 |
. . . . . . . 8
β’ (π β β¦(πΌ + 1) / πβ¦π΄ β β) |
127 | | fzofi 13886 |
. . . . . . . . . 10
β’
(0..^(πΌ + 1)) β
Fin |
128 | 127 | a1i 11 |
. . . . . . . . 9
β’ (π β (0..^(πΌ + 1)) β Fin) |
129 | | elfzoelz 13579 |
. . . . . . . . . 10
β’ (π β (0..^(πΌ + 1)) β π β β€) |
130 | 129, 122 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π β (0..^(πΌ + 1))) β (πβ(πΏβπ)) β β) |
131 | 128, 130 | fsumcl 15625 |
. . . . . . . 8
β’ (π β Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)) β β) |
132 | 126, 131 | mulcld 11182 |
. . . . . . 7
β’ (π β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))) β β) |
133 | 125, 132 | subcld 11519 |
. . . . . 6
β’ (π β ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) β β) |
134 | 133 | abscld 15328 |
. . . . 5
β’ (π β
(absβ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) β β) |
135 | 84, 17 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β π β β) |
136 | | peano2nn 12172 |
. . . . . . . . . . . . 13
β’ (π β β β (π + 1) β
β) |
137 | 136 | nnrpd 12962 |
. . . . . . . . . . . 12
β’ (π β β β (π + 1) β
β+) |
138 | | nfcsb1v 3885 |
. . . . . . . . . . . . . . 15
β’
β²πβ¦(π + 1) / πβ¦π΄ |
139 | 138 | nfel1 2924 |
. . . . . . . . . . . . . 14
β’
β²πβ¦(π + 1) / πβ¦π΄ β β |
140 | | csbeq1a 3874 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β π΄ = β¦(π + 1) / πβ¦π΄) |
141 | 140 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (π΄ β β β β¦(π + 1) / πβ¦π΄ β β)) |
142 | 139, 141 | rspc 3572 |
. . . . . . . . . . . . 13
β’ ((π + 1) β β+
β (βπ β
β+ π΄
β β β β¦(π + 1) / πβ¦π΄ β β)) |
143 | 142 | impcom 409 |
. . . . . . . . . . . 12
β’
((βπ β
β+ π΄
β β β§ (π +
1) β β+) β β¦(π + 1) / πβ¦π΄ β β) |
144 | 102, 137,
143 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β β¦(π + 1) / πβ¦π΄ β β) |
145 | 144, 39 | resubcld 11590 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
(β¦(π + 1) /
πβ¦π΄ β β¦π / πβ¦π΄) β β) |
146 | 145 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π β β) β
(β¦(π + 1) /
πβ¦π΄ β β¦π / πβ¦π΄) β β) |
147 | | fzofi 13886 |
. . . . . . . . . . . 12
β’
(0..^(π + 1)) β
Fin |
148 | 147 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (0..^(π + 1)) β Fin) |
149 | | elfzoelz 13579 |
. . . . . . . . . . . 12
β’ (π β (0..^(π + 1)) β π β β€) |
150 | 149, 122 | sylan2 594 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^(π + 1))) β (πβ(πΏβπ)) β β) |
151 | 148, 150 | fsumcl 15625 |
. . . . . . . . . 10
β’ (π β Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β β) |
152 | 151 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β β) |
153 | 146, 152 | mulcld 11182 |
. . . . . . . 8
β’ ((π β§ π β β) β
((β¦(π + 1) /
πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))) β β) |
154 | 135, 153 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))) β β) |
155 | 81, 154 | fsumcl 15625 |
. . . . . 6
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))) β β) |
156 | 155 | abscld 15328 |
. . . . 5
β’ (π β (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) β β) |
157 | 134, 156 | readdcld 11191 |
. . . 4
β’ (π β
((absβ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) + (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))))) β β) |
158 | 26, 40 | mulcomd 11183 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = (β¦π / πβ¦π΄ Β· (πβ(πΏβπ)))) |
159 | | nnnn0 12427 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β0) |
160 | 159 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β0) |
161 | | nn0uz 12812 |
. . . . . . . . . . . . . . 15
β’
β0 = (β€β₯β0) |
162 | 160, 161 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π β
(β€β₯β0)) |
163 | | elfzelz 13448 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β π β β€) |
164 | 122 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β β€) β (πβ(πΏβπ)) β β) |
165 | 163, 164 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (0...π)) β (πβ(πΏβπ)) β β) |
166 | 162, 165,
61 | fzosump1 15644 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) = (Ξ£π β (0..^π)(πβ(πΏβπ)) + (πβ(πΏβπ)))) |
167 | 166 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β Ξ£π β (0..^π)(πβ(πΏβπ))) = ((Ξ£π β (0..^π)(πβ(πΏβπ)) + (πβ(πΏβπ))) β Ξ£π β (0..^π)(πβ(πΏβπ)))) |
168 | | fzofi 13886 |
. . . . . . . . . . . . . . 15
β’
(0..^π) β
Fin |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (0..^π) β Fin) |
170 | | elfzoelz 13579 |
. . . . . . . . . . . . . . 15
β’ (π β (0..^π) β π β β€) |
171 | 170, 164 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (0..^π)) β (πβ(πΏβπ)) β β) |
172 | 169, 171 | fsumcl 15625 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β Ξ£π β (0..^π)(πβ(πΏβπ)) β β) |
173 | 172, 26 | pncan2d 11521 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((Ξ£π β (0..^π)(πβ(πΏβπ)) + (πβ(πΏβπ))) β Ξ£π β (0..^π)(πβ(πΏβπ))) = (πβ(πΏβπ))) |
174 | 167, 173 | eqtr2d 2778 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (πβ(πΏβπ)) = (Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β Ξ£π β (0..^π)(πβ(πΏβπ)))) |
175 | 174 | oveq2d 7378 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (β¦π / πβ¦π΄ Β· (πβ(πΏβπ))) = (β¦π / πβ¦π΄ Β· (Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β Ξ£π β (0..^π)(πβ(πΏβπ))))) |
176 | 158, 175 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = (β¦π / πβ¦π΄ Β· (Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β Ξ£π β (0..^π)(πβ(πΏβπ))))) |
177 | 135, 176 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = (β¦π / πβ¦π΄ Β· (Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β Ξ£π β (0..^π)(πβ(πΏβπ))))) |
178 | 177 | sumeq2dv 15595 |
. . . . . . 7
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = Ξ£π β ((πΌ + 1)..^(π½ + 1))(β¦π / πβ¦π΄ Β· (Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β Ξ£π β (0..^π)(πβ(πΏβπ))))) |
179 | | csbeq1 3863 |
. . . . . . . . 9
β’ (π = π β β¦π / πβ¦π΄ = β¦π / πβ¦π΄) |
180 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = π β (0..^π) = (0..^π)) |
181 | 180 | sumeq1d 15593 |
. . . . . . . . 9
β’ (π = π β Ξ£π β (0..^π)(πβ(πΏβπ)) = Ξ£π β (0..^π)(πβ(πΏβπ))) |
182 | 179, 181 | jca 513 |
. . . . . . . 8
β’ (π = π β (β¦π / πβ¦π΄ = β¦π / πβ¦π΄ β§ Ξ£π β (0..^π)(πβ(πΏβπ)) = Ξ£π β (0..^π)(πβ(πΏβπ)))) |
183 | | csbeq1 3863 |
. . . . . . . . 9
β’ (π = (π + 1) β β¦π / πβ¦π΄ = β¦(π + 1) / πβ¦π΄) |
184 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = (π + 1) β (0..^π) = (0..^(π + 1))) |
185 | 184 | sumeq1d 15593 |
. . . . . . . . 9
β’ (π = (π + 1) β Ξ£π β (0..^π)(πβ(πΏβπ)) = Ξ£π β (0..^(π + 1))(πβ(πΏβπ))) |
186 | 183, 185 | jca 513 |
. . . . . . . 8
β’ (π = (π + 1) β (β¦π / πβ¦π΄ = β¦(π + 1) / πβ¦π΄ β§ Ξ£π β (0..^π)(πβ(πΏβπ)) = Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) |
187 | | csbeq1 3863 |
. . . . . . . . 9
β’ (π = (πΌ + 1) β β¦π / πβ¦π΄ = β¦(πΌ + 1) / πβ¦π΄) |
188 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = (πΌ + 1) β (0..^π) = (0..^(πΌ + 1))) |
189 | 188 | sumeq1d 15593 |
. . . . . . . . 9
β’ (π = (πΌ + 1) β Ξ£π β (0..^π)(πβ(πΏβπ)) = Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))) |
190 | 187, 189 | jca 513 |
. . . . . . . 8
β’ (π = (πΌ + 1) β (β¦π / πβ¦π΄ = β¦(πΌ + 1) / πβ¦π΄ β§ Ξ£π β (0..^π)(πβ(πΏβπ)) = Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) |
191 | | csbeq1 3863 |
. . . . . . . . 9
β’ (π = (π½ + 1) β β¦π / πβ¦π΄ = β¦(π½ + 1) / πβ¦π΄) |
192 | | oveq2 7370 |
. . . . . . . . . 10
β’ (π = (π½ + 1) β (0..^π) = (0..^(π½ + 1))) |
193 | 192 | sumeq1d 15593 |
. . . . . . . . 9
β’ (π = (π½ + 1) β Ξ£π β (0..^π)(πβ(πΏβπ)) = Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) |
194 | 191, 193 | jca 513 |
. . . . . . . 8
β’ (π = (π½ + 1) β (β¦π / πβ¦π΄ = β¦(π½ + 1) / πβ¦π΄ β§ Ξ£π β (0..^π)(πβ(πΏβπ)) = Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) |
195 | 40 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β β β¦π / πβ¦π΄ β β) |
196 | | elfzuz 13444 |
. . . . . . . . . 10
β’ (π β ((πΌ + 1)...(π½ + 1)) β π β (β€β₯β(πΌ + 1))) |
197 | | eluznn 12850 |
. . . . . . . . . 10
β’ (((πΌ + 1) β β β§ π β
(β€β₯β(πΌ + 1))) β π β β) |
198 | 4, 196, 197 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ π β ((πΌ + 1)...(π½ + 1))) β π β β) |
199 | | csbeq1 3863 |
. . . . . . . . . . 11
β’ (π = π β β¦π / πβ¦π΄ = β¦π / πβ¦π΄) |
200 | 199 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π = π β (β¦π / πβ¦π΄ β β β β¦π / πβ¦π΄ β β)) |
201 | 200 | rspccva 3583 |
. . . . . . . . 9
β’
((βπ β
β β¦π /
πβ¦π΄ β β β§ π β β) β
β¦π / πβ¦π΄ β β) |
202 | 195, 198,
201 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ π β ((πΌ + 1)...(π½ + 1))) β β¦π / πβ¦π΄ β β) |
203 | | fzofi 13886 |
. . . . . . . . . . 11
β’
(0..^π) β
Fin |
204 | 203 | a1i 11 |
. . . . . . . . . 10
β’ (π β (0..^π) β Fin) |
205 | | elfzoelz 13579 |
. . . . . . . . . . 11
β’ (π β (0..^π) β π β β€) |
206 | 205, 122 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβ(πΏβπ)) β β) |
207 | 204, 206 | fsumcl 15625 |
. . . . . . . . 9
β’ (π β Ξ£π β (0..^π)(πβ(πΏβπ)) β β) |
208 | 207 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((πΌ + 1)...(π½ + 1))) β Ξ£π β (0..^π)(πβ(πΏβπ)) β β) |
209 | 182, 186,
190, 194, 9, 202, 208 | fsumparts 15698 |
. . . . . . 7
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))(β¦π / πβ¦π΄ Β· (Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β Ξ£π β (0..^π)(πβ(πΏβπ)))) = (((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) β Ξ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))))) |
210 | 178, 209 | eqtrd 2777 |
. . . . . 6
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) = (((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) β Ξ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))))) |
211 | 210 | fveq2d 6851 |
. . . . 5
β’ (π β (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) = (absβ(((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) β Ξ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))))) |
212 | 133, 155 | abs2dif2d 15350 |
. . . . 5
β’ (π β
(absβ(((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) β Ξ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))))) β€
((absβ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) + (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))))) |
213 | 211, 212 | eqbrtrd 5132 |
. . . 4
β’ (π β (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) β€ ((absβ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) + (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))))) |
214 | 115, 99 | readdcld 11191 |
. . . . . . 7
β’ (π β (β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) β β) |
215 | 214, 93 | remulcld 11192 |
. . . . . 6
β’ (π β ((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) Β· π
) β β) |
216 | 179, 183,
187, 191, 9, 202 | telfsumo 15694 |
. . . . . . . 8
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))(β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) = (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄)) |
217 | 135, 39 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β β¦π / πβ¦π΄ β β) |
218 | 135, 144 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β β¦(π + 1) / πβ¦π΄ β β) |
219 | 217, 218 | resubcld 11590 |
. . . . . . . . 9
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β (β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) β β) |
220 | 81, 219 | fsumrecl 15626 |
. . . . . . . 8
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))(β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) β β) |
221 | 216, 220 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) β β) |
222 | 221, 93 | remulcld 11192 |
. . . . . 6
β’ (π β ((β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) Β· π
) β β) |
223 | 125 | abscld 15328 |
. . . . . . . 8
β’ (π β
(absβ(β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) β β) |
224 | 132 | abscld 15328 |
. . . . . . . 8
β’ (π β
(absβ(β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) β β) |
225 | 223, 224 | readdcld 11191 |
. . . . . . 7
β’ (π β
((absβ(β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) + (absβ(β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) β β) |
226 | 125, 132 | abs2dif2d 15350 |
. . . . . . 7
β’ (π β
(absβ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) β€ ((absβ(β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) + (absβ(β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))))) |
227 | 115, 93 | remulcld 11192 |
. . . . . . . . 9
β’ (π β (β¦(π½ + 1) / πβ¦π΄ Β· π
) β β) |
228 | 99, 93 | remulcld 11192 |
. . . . . . . . 9
β’ (π β (β¦(πΌ + 1) / πβ¦π΄ Β· π
) β β) |
229 | 116, 124 | absmuld 15346 |
. . . . . . . . . . 11
β’ (π β
(absβ(β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) = ((absββ¦(π½ + 1) / πβ¦π΄) Β· (absβΞ£π β (0..^(π½ + 1))(πβ(πΏβπ))))) |
230 | | eluzelre 12781 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯βπ) β π β β) |
231 | 230 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (β€β₯βπ)) β π β β) |
232 | | eluzle 12783 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯βπ) β π β€ π) |
233 | 232 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (β€β₯βπ)) β π β€ π) |
234 | 31 | nnred 12175 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β) |
235 | 234 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (β€β₯βπ)) β π β β) |
236 | | elicopnf 13369 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (π β (π[,)+β) β (π β β β§ π β€ π))) |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (β€β₯βπ)) β (π β (π[,)+β) β (π β β β§ π β€ π))) |
238 | 231, 233,
237 | mpbir2and 712 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯βπ)) β π β (π[,)+β)) |
239 | 238 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (β€β₯βπ) β π β (π[,)+β))) |
240 | 239 | ssrdv 3955 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (π[,)+β)) |
241 | 31 | nnzd 12533 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β€) |
242 | 48 | peano2zd 12617 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΌ + 1) β β€) |
243 | 101 | rpred 12964 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β) |
244 | 4 | nnred 12175 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΌ + 1) β β) |
245 | | dchrisumlem2.2 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β€ π) |
246 | | dchrisumlem2.3 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β€ (πΌ + 1)) |
247 | 234, 243,
244, 245, 246 | letrd 11319 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β€ (πΌ + 1)) |
248 | | eluz2 12776 |
. . . . . . . . . . . . . . . . 17
β’ ((πΌ + 1) β
(β€β₯βπ) β (π β β€ β§ (πΌ + 1) β β€ β§ π β€ (πΌ + 1))) |
249 | 241, 242,
247, 248 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΌ + 1) β
(β€β₯βπ)) |
250 | | uztrn 12788 |
. . . . . . . . . . . . . . . 16
β’ (((π½ + 1) β
(β€β₯β(πΌ + 1)) β§ (πΌ + 1) β
(β€β₯βπ)) β (π½ + 1) β
(β€β₯βπ)) |
251 | 9, 249, 250 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (π½ + 1) β
(β€β₯βπ)) |
252 | 240, 251 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’ (π β (π½ + 1) β (π[,)+β)) |
253 | 113 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β ((π½ + 1) β (π[,)+β) β 0 β€
β¦(π½ + 1) /
πβ¦π΄)) |
254 | 252, 253 | mpd 15 |
. . . . . . . . . . . . 13
β’ (π β 0 β€
β¦(π½ + 1) /
πβ¦π΄) |
255 | 115, 254 | absidd 15314 |
. . . . . . . . . . . 12
β’ (π β
(absββ¦(π½ + 1) / πβ¦π΄) = β¦(π½ + 1) / πβ¦π΄) |
256 | 255 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π β
((absββ¦(π½ + 1) / πβ¦π΄) Β· (absβΞ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) = (β¦(π½ + 1) / πβ¦π΄ Β· (absβΞ£π β (0..^(π½ + 1))(πβ(πΏβπ))))) |
257 | 229, 256 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π β
(absβ(β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) = (β¦(π½ + 1) / πβ¦π΄ Β· (absβΞ£π β (0..^(π½ + 1))(πβ(πΏβπ))))) |
258 | 124 | abscld 15328 |
. . . . . . . . . . 11
β’ (π β (absβΞ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β β) |
259 | 111 | nnnn0d 12480 |
. . . . . . . . . . . 12
β’ (π β (π½ + 1) β
β0) |
260 | | dchrisum.10 |
. . . . . . . . . . . . 13
β’ (π β βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π
) |
261 | 19, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260 | dchrisumlem1 26853 |
. . . . . . . . . . . 12
β’ ((π β§ (π½ + 1) β β0) β
(absβΞ£π β
(0..^(π½ + 1))(πβ(πΏβπ))) β€ π
) |
262 | 259, 261 | mpdan 686 |
. . . . . . . . . . 11
β’ (π β (absβΞ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β€ π
) |
263 | 258, 93, 115, 254, 262 | lemul2ad 12102 |
. . . . . . . . . 10
β’ (π β (β¦(π½ + 1) / πβ¦π΄ Β· (absβΞ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) β€ (β¦(π½ + 1) / πβ¦π΄ Β· π
)) |
264 | 257, 263 | eqbrtrd 5132 |
. . . . . . . . 9
β’ (π β
(absβ(β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) β€ (β¦(π½ + 1) / πβ¦π΄ Β· π
)) |
265 | 126, 131 | absmuld 15346 |
. . . . . . . . . . 11
β’ (π β
(absβ(β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) = ((absββ¦(πΌ + 1) / πβ¦π΄) Β· (absβΞ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) |
266 | 240, 249 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’ (π β (πΌ + 1) β (π[,)+β)) |
267 | 19, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35 | dchrisumlema 26852 |
. . . . . . . . . . . . . . 15
β’ (π β (((πΌ + 1) β β+ β
β¦(πΌ + 1) /
πβ¦π΄ β β) β§ ((πΌ + 1) β (π[,)+β) β 0 β€
β¦(πΌ + 1) /
πβ¦π΄))) |
268 | 267 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β ((πΌ + 1) β (π[,)+β) β 0 β€
β¦(πΌ + 1) /
πβ¦π΄)) |
269 | 266, 268 | mpd 15 |
. . . . . . . . . . . . 13
β’ (π β 0 β€
β¦(πΌ + 1) /
πβ¦π΄) |
270 | 99, 269 | absidd 15314 |
. . . . . . . . . . . 12
β’ (π β
(absββ¦(πΌ + 1) / πβ¦π΄) = β¦(πΌ + 1) / πβ¦π΄) |
271 | 270 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π β
((absββ¦(πΌ + 1) / πβ¦π΄) Β· (absβΞ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) = (β¦(πΌ + 1) / πβ¦π΄ Β· (absβΞ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) |
272 | 265, 271 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π β
(absβ(β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) = (β¦(πΌ + 1) / πβ¦π΄ Β· (absβΞ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) |
273 | 131 | abscld 15328 |
. . . . . . . . . . 11
β’ (π β (absβΞ£π β (0..^(πΌ + 1))(πβ(πΏβπ))) β β) |
274 | 4 | nnnn0d 12480 |
. . . . . . . . . . . 12
β’ (π β (πΌ + 1) β
β0) |
275 | 19, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260 | dchrisumlem1 26853 |
. . . . . . . . . . . 12
β’ ((π β§ (πΌ + 1) β β0) β
(absβΞ£π β
(0..^(πΌ + 1))(πβ(πΏβπ))) β€ π
) |
276 | 274, 275 | mpdan 686 |
. . . . . . . . . . 11
β’ (π β (absβΞ£π β (0..^(πΌ + 1))(πβ(πΏβπ))) β€ π
) |
277 | 273, 93, 99, 269, 276 | lemul2ad 12102 |
. . . . . . . . . 10
β’ (π β (β¦(πΌ + 1) / πβ¦π΄ Β· (absβΞ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) β€ (β¦(πΌ + 1) / πβ¦π΄ Β· π
)) |
278 | 272, 277 | eqbrtrd 5132 |
. . . . . . . . 9
β’ (π β
(absβ(β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ)))) β€ (β¦(πΌ + 1) / πβ¦π΄ Β· π
)) |
279 | 223, 224,
227, 228, 264, 278 | le2addd 11781 |
. . . . . . . 8
β’ (π β
((absβ(β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) + (absβ(β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) β€ ((β¦(π½ + 1) / πβ¦π΄ Β· π
) + (β¦(πΌ + 1) / πβ¦π΄ Β· π
))) |
280 | 93 | recnd 11190 |
. . . . . . . . 9
β’ (π β π
β β) |
281 | 116, 126,
280 | adddird 11187 |
. . . . . . . 8
β’ (π β ((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) Β· π
) = ((β¦(π½ + 1) / πβ¦π΄ Β· π
) + (β¦(πΌ + 1) / πβ¦π΄ Β· π
))) |
282 | 279, 281 | breqtrrd 5138 |
. . . . . . 7
β’ (π β
((absβ(β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ)))) + (absβ(β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) β€ ((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) Β· π
)) |
283 | 134, 225,
215, 226, 282 | letrd 11319 |
. . . . . 6
β’ (π β
(absβ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) β€ ((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) Β· π
)) |
284 | 154 | abscld 15328 |
. . . . . . . 8
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β
(absβ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) β β) |
285 | 81, 284 | fsumrecl 15626 |
. . . . . . 7
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))(absβ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) β β) |
286 | 81, 154 | fsumabs 15693 |
. . . . . . 7
β’ (π β (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) β€ Ξ£π β ((πΌ + 1)..^(π½ + 1))(absβ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))))) |
287 | 93 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β π
β β) |
288 | 219, 287 | remulcld 11192 |
. . . . . . . . 9
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β ((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· π
) β β) |
289 | 135, 146 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β (β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) β β) |
290 | 151 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β Ξ£π β (0..^(π + 1))(πβ(πΏβπ)) β β) |
291 | 289, 290 | absmuld 15346 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β
(absβ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) = ((absβ(β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄)) Β· (absβΞ£π β (0..^(π + 1))(πβ(πΏβπ))))) |
292 | | elfzouz 13583 |
. . . . . . . . . . . . . . 15
β’ (π β ((πΌ + 1)..^(π½ + 1)) β π β (β€β₯β(πΌ + 1))) |
293 | | uztrn 12788 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β(πΌ + 1)) β§ (πΌ + 1) β
(β€β₯βπ)) β π β (β€β₯βπ)) |
294 | 292, 249,
293 | syl2anr 598 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β π β (β€β₯βπ)) |
295 | | eluznn 12850 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β
(β€β₯βπ)) β π β β) |
296 | 31, 295 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β π β β) |
297 | 296, 137 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β (π + 1) β
β+) |
298 | 296 | nnrpd 12962 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β π β β+) |
299 | 33 | 3expia 1122 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β β+ β§ π₯ β β+))
β ((π β€ π β§ π β€ π₯) β π΅ β€ π΄)) |
300 | 299 | ralrimivva 3198 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ β β+ βπ₯ β β+
((π β€ π β§ π β€ π₯) β π΅ β€ π΄)) |
301 | 300 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β βπ β β+
βπ₯ β
β+ ((π
β€ π β§ π β€ π₯) β π΅ β€ π΄)) |
302 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . 18
β’
β²πβ+ |
303 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(π β€ π β§ π β€ π₯) |
304 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²ππ΅ |
305 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π
β€ |
306 | 304, 305,
59 | nfbr 5157 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π π΅ β€ β¦π / πβ¦π΄ |
307 | 303, 306 | nfim 1900 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄) |
308 | 302, 307 | nfralw 3297 |
. . . . . . . . . . . . . . . . 17
β’
β²πβπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄) |
309 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π β€ π β π β€ π)) |
310 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (π β€ π₯ β π β€ π₯)) |
311 | 309, 310 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((π β€ π β§ π β€ π₯) β (π β€ π β§ π β€ π₯))) |
312 | 62 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π΅ β€ π΄ β π΅ β€ β¦π / πβ¦π΄)) |
313 | 311, 312 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄))) |
314 | 313 | ralbidv 3175 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄))) |
315 | 308, 314 | rspc 3572 |
. . . . . . . . . . . . . . . 16
β’ (π β β+
β (βπ β
β+ βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄))) |
316 | 298, 301,
315 | sylc 65 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β βπ₯ β β+
((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄)) |
317 | 231 | lep1d 12093 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β π β€ (π + 1)) |
318 | 233, 317 | jca 513 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β€β₯βπ)) β (π β€ π β§ π β€ (π + 1))) |
319 | | breq2 5114 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = (π + 1) β (π β€ π₯ β π β€ (π + 1))) |
320 | 319 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = (π + 1) β ((π β€ π β§ π β€ π₯) β (π β€ π β§ π β€ (π + 1)))) |
321 | | eqvisset 3465 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = (π + 1) β (π + 1) β V) |
322 | | eqtr3 2763 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ = (π + 1) β§ π = (π + 1)) β π₯ = π) |
323 | 30 | equcoms 2024 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β π΄ = π΅) |
324 | 322, 323 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ = (π + 1) β§ π = (π + 1)) β π΄ = π΅) |
325 | 321, 324 | csbied 3898 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = (π + 1) β β¦(π + 1) / πβ¦π΄ = π΅) |
326 | 325 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = (π + 1) β π΅ = β¦(π + 1) / πβ¦π΄) |
327 | 326 | breq1d 5120 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = (π + 1) β (π΅ β€ β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄)) |
328 | 320, 327 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (π + 1) β (((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄) β ((π β€ π β§ π β€ (π + 1)) β β¦(π + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄))) |
329 | 328 | rspcv 3580 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) β β+
β (βπ₯ β
β+ ((π
β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄) β ((π β€ π β§ π β€ (π + 1)) β β¦(π + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄))) |
330 | 297, 316,
318, 329 | syl3c 66 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β€β₯βπ)) β β¦(π + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄) |
331 | 294, 330 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β β¦(π + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄) |
332 | 218, 217,
331 | abssuble0d 15324 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β
(absβ(β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄)) = (β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄)) |
333 | 332 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β
((absβ(β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄)) Β· (absβΞ£π β (0..^(π + 1))(πβ(πΏβπ)))) = ((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· (absβΞ£π β (0..^(π + 1))(πβ(πΏβπ))))) |
334 | 291, 333 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β
(absβ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) = ((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· (absβΞ£π β (0..^(π + 1))(πβ(πΏβπ))))) |
335 | 290 | abscld 15328 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β (absβΞ£π β (0..^(π + 1))(πβ(πΏβπ))) β β) |
336 | 217, 218 | subge0d 11752 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β (0 β€ (β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) β β¦(π + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄)) |
337 | 331, 336 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β 0 β€ (β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄)) |
338 | 135 | peano2nnd 12177 |
. . . . . . . . . . . . 13
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β (π + 1) β β) |
339 | 338 | nnnn0d 12480 |
. . . . . . . . . . . 12
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β (π + 1) β
β0) |
340 | 19, 21, 27, 18, 20, 28, 22, 29, 30, 31, 32, 33, 34, 35, 93, 260 | dchrisumlem1 26853 |
. . . . . . . . . . . 12
β’ ((π β§ (π + 1) β β0) β
(absβΞ£π β
(0..^(π + 1))(πβ(πΏβπ))) β€ π
) |
341 | 339, 340 | syldan 592 |
. . . . . . . . . . 11
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β (absβΞ£π β (0..^(π + 1))(πβ(πΏβπ))) β€ π
) |
342 | 335, 287,
219, 337, 341 | lemul2ad 12102 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β ((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· (absβΞ£π β (0..^(π + 1))(πβ(πΏβπ)))) β€ ((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· π
)) |
343 | 334, 342 | eqbrtrd 5132 |
. . . . . . . . 9
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β
(absβ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) β€ ((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· π
)) |
344 | 81, 284, 288, 343 | fsumle 15691 |
. . . . . . . 8
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))(absβ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) β€ Ξ£π β ((πΌ + 1)..^(π½ + 1))((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· π
)) |
345 | 219 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΌ + 1)..^(π½ + 1))) β (β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) β β) |
346 | 81, 280, 345 | fsummulc1 15677 |
. . . . . . . . 9
β’ (π β (Ξ£π β ((πΌ + 1)..^(π½ + 1))(β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· π
) = Ξ£π β ((πΌ + 1)..^(π½ + 1))((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· π
)) |
347 | 216 | oveq1d 7377 |
. . . . . . . . 9
β’ (π β (Ξ£π β ((πΌ + 1)..^(π½ + 1))(β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· π
) = ((β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) Β· π
)) |
348 | 346, 347 | eqtr3d 2779 |
. . . . . . . 8
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))((β¦π / πβ¦π΄ β β¦(π + 1) / πβ¦π΄) Β· π
) = ((β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) Β· π
)) |
349 | 344, 348 | breqtrd 5136 |
. . . . . . 7
β’ (π β Ξ£π β ((πΌ + 1)..^(π½ + 1))(absβ((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) β€ ((β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) Β· π
)) |
350 | 156, 285,
222, 286, 349 | letrd 11319 |
. . . . . 6
β’ (π β (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ)))) β€ ((β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) Β· π
)) |
351 | 134, 156,
215, 222, 283, 350 | le2addd 11781 |
. . . . 5
β’ (π β
((absβ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) + (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))))) β€ (((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) Β· π
) + ((β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) Β· π
))) |
352 | 126 | 2timesd 12403 |
. . . . . . . 8
β’ (π β (2 Β·
β¦(πΌ + 1) /
πβ¦π΄) = (β¦(πΌ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄)) |
353 | 126, 116,
126 | ppncand 11559 |
. . . . . . . 8
β’ (π β ((β¦(πΌ + 1) / πβ¦π΄ + β¦(π½ + 1) / πβ¦π΄) + (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄)) = (β¦(πΌ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄)) |
354 | 126, 116 | addcomd 11364 |
. . . . . . . . 9
β’ (π β (β¦(πΌ + 1) / πβ¦π΄ + β¦(π½ + 1) / πβ¦π΄) = (β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄)) |
355 | 354 | oveq1d 7377 |
. . . . . . . 8
β’ (π β ((β¦(πΌ + 1) / πβ¦π΄ + β¦(π½ + 1) / πβ¦π΄) + (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄)) = ((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) + (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄))) |
356 | 352, 353,
355 | 3eqtr2d 2783 |
. . . . . . 7
β’ (π β (2 Β·
β¦(πΌ + 1) /
πβ¦π΄) = ((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) + (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄))) |
357 | 356 | oveq1d 7377 |
. . . . . 6
β’ (π β ((2 Β·
β¦(πΌ + 1) /
πβ¦π΄) Β· π
) = (((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) + (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄)) Β· π
)) |
358 | | 2cnd 12238 |
. . . . . . 7
β’ (π β 2 β
β) |
359 | 358, 126,
280 | mul32d 11372 |
. . . . . 6
β’ (π β ((2 Β·
β¦(πΌ + 1) /
πβ¦π΄) Β· π
) = ((2 Β· π
) Β· β¦(πΌ + 1) / πβ¦π΄)) |
360 | 214 | recnd 11190 |
. . . . . . 7
β’ (π β (β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) β β) |
361 | 221 | recnd 11190 |
. . . . . . 7
β’ (π β (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) β β) |
362 | 360, 361,
280 | adddird 11187 |
. . . . . 6
β’ (π β (((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) + (β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄)) Β· π
) = (((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) Β· π
) + ((β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) Β· π
))) |
363 | 357, 359,
362 | 3eqtr3d 2785 |
. . . . 5
β’ (π β ((2 Β· π
) Β· β¦(πΌ + 1) / πβ¦π΄) = (((β¦(π½ + 1) / πβ¦π΄ + β¦(πΌ + 1) / πβ¦π΄) Β· π
) + ((β¦(πΌ + 1) / πβ¦π΄ β β¦(π½ + 1) / πβ¦π΄) Β· π
))) |
364 | 351, 363 | breqtrrd 5138 |
. . . 4
β’ (π β
((absβ((β¦(π½ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(π½ + 1))(πβ(πΏβπ))) β (β¦(πΌ + 1) / πβ¦π΄ Β· Ξ£π β (0..^(πΌ + 1))(πβ(πΏβπ))))) + (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((β¦(π + 1) / πβ¦π΄ β β¦π / πβ¦π΄) Β· Ξ£π β (0..^(π + 1))(πβ(πΏβπ))))) β€ ((2 Β· π
) Β· β¦(πΌ + 1) / πβ¦π΄)) |
365 | 90, 157, 100, 213, 364 | letrd 11319 |
. . 3
β’ (π β (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) β€ ((2 Β· π
) Β· β¦(πΌ + 1) / πβ¦π΄)) |
366 | | 2nn0 12437 |
. . . . . 6
β’ 2 β
β0 |
367 | | nn0ge0 12445 |
. . . . . 6
β’ (2 β
β0 β 0 β€ 2) |
368 | 366, 367 | mp1i 13 |
. . . . 5
β’ (π β 0 β€ 2) |
369 | | 0red 11165 |
. . . . . 6
β’ (π β 0 β
β) |
370 | 124 | absge0d 15336 |
. . . . . 6
β’ (π β 0 β€
(absβΞ£π β
(0..^(π½ + 1))(πβ(πΏβπ)))) |
371 | 369, 258,
93, 370, 262 | letrd 11319 |
. . . . 5
β’ (π β 0 β€ π
) |
372 | 92, 93, 368, 371 | mulge0d 11739 |
. . . 4
β’ (π β 0 β€ (2 Β· π
)) |
373 | 4 | nnrpd 12962 |
. . . . 5
β’ (π β (πΌ + 1) β
β+) |
374 | | nfv 1918 |
. . . . . . . . 9
β’
β²π(π β€ π β§ π β€ π₯) |
375 | 304, 305,
103 | nfbr 5157 |
. . . . . . . . 9
β’
β²π π΅ β€ β¦π / πβ¦π΄ |
376 | 374, 375 | nfim 1900 |
. . . . . . . 8
β’
β²π((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄) |
377 | 302, 376 | nfralw 3297 |
. . . . . . 7
β’
β²πβπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄) |
378 | | breq2 5114 |
. . . . . . . . . 10
β’ (π = π β (π β€ π β π β€ π)) |
379 | | breq1 5113 |
. . . . . . . . . 10
β’ (π = π β (π β€ π₯ β π β€ π₯)) |
380 | 378, 379 | anbi12d 632 |
. . . . . . . . 9
β’ (π = π β ((π β€ π β§ π β€ π₯) β (π β€ π β§ π β€ π₯))) |
381 | 105 | breq2d 5122 |
. . . . . . . . 9
β’ (π = π β (π΅ β€ π΄ β π΅ β€ β¦π / πβ¦π΄)) |
382 | 380, 381 | imbi12d 345 |
. . . . . . . 8
β’ (π = π β (((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄))) |
383 | 382 | ralbidv 3175 |
. . . . . . 7
β’ (π = π β (βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄))) |
384 | 377, 383 | rspc 3572 |
. . . . . 6
β’ (π β β+
β (βπ β
β+ βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ π΄) β βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄))) |
385 | 101, 300,
384 | sylc 65 |
. . . . 5
β’ (π β βπ₯ β β+ ((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄)) |
386 | 245, 246 | jca 513 |
. . . . 5
β’ (π β (π β€ π β§ π β€ (πΌ + 1))) |
387 | | breq2 5114 |
. . . . . . . 8
β’ (π₯ = (πΌ + 1) β (π β€ π₯ β π β€ (πΌ + 1))) |
388 | 387 | anbi2d 630 |
. . . . . . 7
β’ (π₯ = (πΌ + 1) β ((π β€ π β§ π β€ π₯) β (π β€ π β§ π β€ (πΌ + 1)))) |
389 | | eqvisset 3465 |
. . . . . . . . . 10
β’ (π₯ = (πΌ + 1) β (πΌ + 1) β V) |
390 | | eqtr3 2763 |
. . . . . . . . . . 11
β’ ((π₯ = (πΌ + 1) β§ π = (πΌ + 1)) β π₯ = π) |
391 | 390, 323 | syl 17 |
. . . . . . . . . 10
β’ ((π₯ = (πΌ + 1) β§ π = (πΌ + 1)) β π΄ = π΅) |
392 | 389, 391 | csbied 3898 |
. . . . . . . . 9
β’ (π₯ = (πΌ + 1) β β¦(πΌ + 1) / πβ¦π΄ = π΅) |
393 | 392 | eqcomd 2743 |
. . . . . . . 8
β’ (π₯ = (πΌ + 1) β π΅ = β¦(πΌ + 1) / πβ¦π΄) |
394 | 393 | breq1d 5120 |
. . . . . . 7
β’ (π₯ = (πΌ + 1) β (π΅ β€ β¦π / πβ¦π΄ β β¦(πΌ + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄)) |
395 | 388, 394 | imbi12d 345 |
. . . . . 6
β’ (π₯ = (πΌ + 1) β (((π β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄) β ((π β€ π β§ π β€ (πΌ + 1)) β β¦(πΌ + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄))) |
396 | 395 | rspcv 3580 |
. . . . 5
β’ ((πΌ + 1) β β+
β (βπ₯ β
β+ ((π
β€ π β§ π β€ π₯) β π΅ β€ β¦π / πβ¦π΄) β ((π β€ π β§ π β€ (πΌ + 1)) β β¦(πΌ + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄))) |
397 | 373, 385,
386, 396 | syl3c 66 |
. . . 4
β’ (π β β¦(πΌ + 1) / πβ¦π΄ β€ β¦π / πβ¦π΄) |
398 | 99, 108, 94, 372, 397 | lemul2ad 12102 |
. . 3
β’ (π β ((2 Β· π
) Β· β¦(πΌ + 1) / πβ¦π΄) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
399 | 90, 100, 109, 365, 398 | letrd 11319 |
. 2
β’ (π β (absβΞ£π β ((πΌ + 1)..^(π½ + 1))((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
400 | 89, 399 | eqbrtrd 5132 |
1
β’ (π β (absβ((seq1( + ,
πΉ)βπ½) β (seq1( + , πΉ)βπΌ))) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄)) |