Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
β’ (π β π) |
2 | | dvnmul.n |
. . 3
β’ (π β π β
β0) |
3 | | nn0uz 12861 |
. . . . 5
β’
β0 = (β€β₯β0) |
4 | 2, 3 | eleqtrdi 2844 |
. . . 4
β’ (π β π β
(β€β₯β0)) |
5 | | eluzfz2 13506 |
. . . 4
β’ (π β
(β€β₯β0) β π β (0...π)) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β π β (0...π)) |
7 | | eleq1 2822 |
. . . . 5
β’ (π = π β (π β (0...π) β π β (0...π))) |
8 | | fveq2 6889 |
. . . . . . 7
β’ (π = π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ)) |
9 | | oveq2 7414 |
. . . . . . . . . 10
β’ (π = π β (0...π) = (0...π)) |
10 | 9 | sumeq1d 15644 |
. . . . . . . . 9
β’ (π = π β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) |
11 | | oveq1 7413 |
. . . . . . . . . . 11
β’ (π = π β (πCπ) = (πCπ)) |
12 | | fvoveq1 7429 |
. . . . . . . . . . . . 13
β’ (π = π β (π·β(π β π)) = (π·β(π β π))) |
13 | 12 | fveq1d 6891 |
. . . . . . . . . . . 12
β’ (π = π β ((π·β(π β π))βπ₯) = ((π·β(π β π))βπ₯)) |
14 | 13 | oveq2d 7422 |
. . . . . . . . . . 11
β’ (π = π β (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)) = (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) |
15 | 11, 14 | oveq12d 7424 |
. . . . . . . . . 10
β’ (π = π β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) |
16 | 15 | sumeq2sdv 15647 |
. . . . . . . . 9
β’ (π = π β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) |
17 | 10, 16 | eqtrd 2773 |
. . . . . . . 8
β’ (π = π β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) |
18 | 17 | mpteq2dv 5250 |
. . . . . . 7
β’ (π = π β (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) |
19 | 8, 18 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β (((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) |
20 | 19 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))))) |
21 | 7, 20 | imbi12d 345 |
. . . 4
β’ (π = π β ((π β (0...π) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) β (π β (0...π) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))))) |
22 | | fveq2 6889 |
. . . . . . 7
β’ (π = 0 β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β0)) |
23 | | simpl 484 |
. . . . . . . . . 10
β’ ((π = 0 β§ π₯ β π) β π = 0) |
24 | 23 | oveq2d 7422 |
. . . . . . . . 9
β’ ((π = 0 β§ π₯ β π) β (0...π) = (0...0)) |
25 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π = 0 β§ π₯ β π) β§ π β (0...0)) β π = 0) |
26 | 25 | oveq1d 7421 |
. . . . . . . . . 10
β’ (((π = 0 β§ π₯ β π) β§ π β (0...0)) β (πCπ) = (0Cπ)) |
27 | 25 | fvoveq1d 7428 |
. . . . . . . . . . . 12
β’ (((π = 0 β§ π₯ β π) β§ π β (0...0)) β (π·β(π β π)) = (π·β(0 β π))) |
28 | 27 | fveq1d 6891 |
. . . . . . . . . . 11
β’ (((π = 0 β§ π₯ β π) β§ π β (0...0)) β ((π·β(π β π))βπ₯) = ((π·β(0 β π))βπ₯)) |
29 | 28 | oveq2d 7422 |
. . . . . . . . . 10
β’ (((π = 0 β§ π₯ β π) β§ π β (0...0)) β (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)) = (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))) |
30 | 26, 29 | oveq12d 7424 |
. . . . . . . . 9
β’ (((π = 0 β§ π₯ β π) β§ π β (0...0)) β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = ((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯)))) |
31 | 24, 30 | sumeq12rdv 15650 |
. . . . . . . 8
β’ ((π = 0 β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯)))) |
32 | 31 | mpteq2dva 5248 |
. . . . . . 7
β’ (π = 0 β (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) = (π₯ β π β¦ Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))))) |
33 | 22, 32 | eqeq12d 2749 |
. . . . . 6
β’ (π = 0 β (((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β0) = (π₯ β π β¦ Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯)))))) |
34 | 33 | imbi2d 341 |
. . . . 5
β’ (π = 0 β ((π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β0) = (π₯ β π β¦ Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))))))) |
35 | | fveq2 6889 |
. . . . . . 7
β’ (π = π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ)) |
36 | | simpl 484 |
. . . . . . . . . 10
β’ ((π = π β§ π₯ β π) β π = π) |
37 | 36 | oveq2d 7422 |
. . . . . . . . 9
β’ ((π = π β§ π₯ β π) β (0...π) = (0...π)) |
38 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β π = π) |
39 | 38 | oveq1d 7421 |
. . . . . . . . . 10
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β (πCπ) = (πCπ)) |
40 | 38 | fvoveq1d 7428 |
. . . . . . . . . . . 12
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β (π·β(π β π)) = (π·β(π β π))) |
41 | 40 | fveq1d 6891 |
. . . . . . . . . . 11
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β ((π·β(π β π))βπ₯) = ((π·β(π β π))βπ₯)) |
42 | 41 | oveq2d 7422 |
. . . . . . . . . 10
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)) = (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) |
43 | 39, 42 | oveq12d 7424 |
. . . . . . . . 9
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) |
44 | 37, 43 | sumeq12rdv 15650 |
. . . . . . . 8
β’ ((π = π β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) |
45 | 44 | mpteq2dva 5248 |
. . . . . . 7
β’ (π = π β (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) |
46 | 35, 45 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β (((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) |
47 | 46 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))))) |
48 | | fveq2 6889 |
. . . . . . 7
β’ (π = (π + 1) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1))) |
49 | | simpl 484 |
. . . . . . . . . 10
β’ ((π = (π + 1) β§ π₯ β π) β π = (π + 1)) |
50 | 49 | oveq2d 7422 |
. . . . . . . . 9
β’ ((π = (π + 1) β§ π₯ β π) β (0...π) = (0...(π + 1))) |
51 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π = (π + 1) β§ π₯ β π) β§ π β (0...(π + 1))) β π = (π + 1)) |
52 | 51 | oveq1d 7421 |
. . . . . . . . . 10
β’ (((π = (π + 1) β§ π₯ β π) β§ π β (0...(π + 1))) β (πCπ) = ((π + 1)Cπ)) |
53 | 51 | fvoveq1d 7428 |
. . . . . . . . . . . 12
β’ (((π = (π + 1) β§ π₯ β π) β§ π β (0...(π + 1))) β (π·β(π β π)) = (π·β((π + 1) β π))) |
54 | 53 | fveq1d 6891 |
. . . . . . . . . . 11
β’ (((π = (π + 1) β§ π₯ β π) β§ π β (0...(π + 1))) β ((π·β(π β π))βπ₯) = ((π·β((π + 1) β π))βπ₯)) |
55 | 54 | oveq2d 7422 |
. . . . . . . . . 10
β’ (((π = (π + 1) β§ π₯ β π) β§ π β (0...(π + 1))) β (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)) = (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) |
56 | 52, 55 | oveq12d 7424 |
. . . . . . . . 9
β’ (((π = (π + 1) β§ π₯ β π) β§ π β (0...(π + 1))) β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
57 | 50, 56 | sumeq12rdv 15650 |
. . . . . . . 8
β’ ((π = (π + 1) β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
58 | 57 | mpteq2dva 5248 |
. . . . . . 7
β’ (π = (π + 1) β (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
59 | 48, 58 | eqeq12d 2749 |
. . . . . 6
β’ (π = (π + 1) β (((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1)) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))))) |
60 | 59 | imbi2d 341 |
. . . . 5
β’ (π = (π + 1) β ((π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1)) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))))) |
61 | | fveq2 6889 |
. . . . . . 7
β’ (π = π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ)) |
62 | | simpl 484 |
. . . . . . . . . 10
β’ ((π = π β§ π₯ β π) β π = π) |
63 | 62 | oveq2d 7422 |
. . . . . . . . 9
β’ ((π = π β§ π₯ β π) β (0...π) = (0...π)) |
64 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β π = π) |
65 | 64 | oveq1d 7421 |
. . . . . . . . . 10
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β (πCπ) = (πCπ)) |
66 | 64 | fvoveq1d 7428 |
. . . . . . . . . . . 12
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β (π·β(π β π)) = (π·β(π β π))) |
67 | 66 | fveq1d 6891 |
. . . . . . . . . . 11
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β ((π·β(π β π))βπ₯) = ((π·β(π β π))βπ₯)) |
68 | 67 | oveq2d 7422 |
. . . . . . . . . 10
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)) = (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) |
69 | 65, 68 | oveq12d 7424 |
. . . . . . . . 9
β’ (((π = π β§ π₯ β π) β§ π β (0...π)) β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) |
70 | 63, 69 | sumeq12rdv 15650 |
. . . . . . . 8
β’ ((π = π β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) |
71 | 70 | mpteq2dva 5248 |
. . . . . . 7
β’ (π = π β (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) |
72 | 61, 71 | eqeq12d 2749 |
. . . . . 6
β’ (π = π β (((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) |
73 | 72 | imbi2d 341 |
. . . . 5
β’ (π = π β ((π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))))) |
74 | | dvnmul.s |
. . . . . . . . 9
β’ (π β π β {β, β}) |
75 | | recnprss 25413 |
. . . . . . . . 9
β’ (π β {β, β}
β π β
β) |
76 | 74, 75 | syl 17 |
. . . . . . . 8
β’ (π β π β β) |
77 | | dvnmul.a |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π΄ β β) |
78 | | dvnmul.cc |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π΅ β β) |
79 | 77, 78 | mulcld 11231 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (π΄ Β· π΅) β β) |
80 | | restsspw 17374 |
. . . . . . . . . . 11
β’
((TopOpenββfld) βΎt π) β π« π |
81 | | dvnmul.x |
. . . . . . . . . . 11
β’ (π β π β
((TopOpenββfld) βΎt π)) |
82 | 80, 81 | sselid 3980 |
. . . . . . . . . 10
β’ (π β π β π« π) |
83 | | elpwi 4609 |
. . . . . . . . . 10
β’ (π β π« π β π β π) |
84 | 82, 83 | syl 17 |
. . . . . . . . 9
β’ (π β π β π) |
85 | | cnex 11188 |
. . . . . . . . . 10
β’ β
β V |
86 | 85 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
V) |
87 | 79, 84, 86, 74 | mptelpm 43858 |
. . . . . . . 8
β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (β βpm π)) |
88 | | dvn0 25433 |
. . . . . . . 8
β’ ((π β β β§ (π₯ β π β¦ (π΄ Β· π΅)) β (β βpm π)) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β0) = (π₯ β π β¦ (π΄ Β· π΅))) |
89 | 76, 87, 88 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β0) = (π₯ β π β¦ (π΄ Β· π΅))) |
90 | | 0z 12566 |
. . . . . . . . . . . 12
β’ 0 β
β€ |
91 | | fzsn 13540 |
. . . . . . . . . . . 12
β’ (0 β
β€ β (0...0) = {0}) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . . 11
β’ (0...0) =
{0} |
93 | 92 | sumeq1i 15641 |
. . . . . . . . . 10
β’
Ξ£π β
(0...0)((0Cπ) Β·
(((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))) = Ξ£π β {0} ((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))) |
94 | 93 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))) = Ξ£π β {0} ((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯)))) |
95 | | nfcvd 2905 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β β²π(π΄ Β· π΅)) |
96 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π β§ π₯ β π) |
97 | | oveq2 7414 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (0Cπ) = (0C0)) |
98 | | 0nn0 12484 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β0 |
99 | | bcn0 14267 |
. . . . . . . . . . . . . . . 16
β’ (0 β
β0 β (0C0) = 1) |
100 | 98, 99 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ (0C0) =
1 |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (0C0) =
1) |
102 | 97, 101 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π = 0 β (0Cπ) = 1) |
103 | 102 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π = 0) β (0Cπ) = 1) |
104 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (πΆβπ) = (πΆβ0)) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = 0) β (πΆβπ) = (πΆβ0)) |
106 | | dvnmul.c |
. . . . . . . . . . . . . . . . . . . . 21
β’ πΆ = (π β (0...π) β¦ ((π Dπ πΉ)βπ)) |
107 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((π Dπ πΉ)βπ) = ((π Dπ πΉ)βπ)) |
108 | 107 | cbvmptv 5261 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...π) β¦ ((π Dπ πΉ)βπ)) = (π β (0...π) β¦ ((π Dπ πΉ)βπ)) |
109 | 106, 108 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . 20
β’ πΆ = (π β (0...π) β¦ ((π Dπ πΉ)βπ)) |
110 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β ((π Dπ πΉ)βπ) = ((π Dπ πΉ)β0)) |
111 | | eluzfz1 13505 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
112 | 4, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 0 β (0...π)) |
113 | | fvexd 6904 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π Dπ πΉ)β0) β V) |
114 | 109, 110,
112, 113 | fvmptd3 7019 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΆβ0) = ((π Dπ πΉ)β0)) |
115 | 114 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = 0) β (πΆβ0) = ((π Dπ πΉ)β0)) |
116 | 105, 115 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = 0) β (πΆβπ) = ((π Dπ πΉ)β0)) |
117 | | dvnmulf |
. . . . . . . . . . . . . . . . . . . 20
β’ πΉ = (π₯ β π β¦ π΄) |
118 | 77, 84, 86, 74 | mptelpm 43858 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π₯ β π β¦ π΄) β (β βpm π)) |
119 | 117, 118 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ β (β βpm π)) |
120 | | dvn0 25433 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ πΉ β (β
βpm π))
β ((π
Dπ πΉ)β0) = πΉ) |
121 | 76, 119, 120 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π Dπ πΉ)β0) = πΉ) |
122 | 121 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = 0) β ((π Dπ πΉ)β0) = πΉ) |
123 | 116, 122 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = 0) β (πΆβπ) = πΉ) |
124 | 123 | fveq1d 6891 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π = 0) β ((πΆβπ)βπ₯) = (πΉβπ₯)) |
125 | 124 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π = 0) β ((πΆβπ)βπ₯) = (πΉβπ₯)) |
126 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β π) β π₯ β π) |
127 | 117 | fvmpt2 7007 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β π β§ π΄ β β) β (πΉβπ₯) = π΄) |
128 | 126, 77, 127 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β (πΉβπ₯) = π΄) |
129 | 128 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π = 0) β (πΉβπ₯) = π΄) |
130 | 125, 129 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ π = 0) β ((πΆβπ)βπ₯) = π΄) |
131 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (0 β π) = (0 β
0)) |
132 | | 0m0e0 12329 |
. . . . . . . . . . . . . . . . . . . 20
β’ (0
β 0) = 0 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (0 β 0) =
0) |
134 | 131, 133 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (0 β π) = 0) |
135 | 134 | fveq2d 6893 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (π·β(0 β π)) = (π·β0)) |
136 | 135 | fveq1d 6891 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β ((π·β(0 β π))βπ₯) = ((π·β0)βπ₯)) |
137 | 136 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π = 0) β ((π·β(0 β π))βπ₯) = ((π·β0)βπ₯)) |
138 | 137 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π = 0) β ((π·β(0 β π))βπ₯) = ((π·β0)βπ₯)) |
139 | | dvnmul.d |
. . . . . . . . . . . . . . . . . . . 20
β’ π· = (π β (0...π) β¦ ((π Dπ πΊ)βπ)) |
140 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π Dπ πΊ)βπ) = ((π Dπ πΊ)βπ)) |
141 | 140 | cbvmptv 5261 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0...π) β¦ ((π Dπ πΊ)βπ)) = (π β (0...π) β¦ ((π Dπ πΊ)βπ)) |
142 | 139, 141 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . 19
β’ π· = (π β (0...π) β¦ ((π Dπ πΊ)βπ)) |
143 | 142 | fveq1i 6890 |
. . . . . . . . . . . . . . . . . 18
β’ (π·β0) = ((π β (0...π) β¦ ((π Dπ πΊ)βπ))β0) |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π·β0) = ((π β (0...π) β¦ ((π Dπ πΊ)βπ))β0)) |
145 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π β (0...π) β¦ ((π Dπ πΊ)βπ)) = (π β (0...π) β¦ ((π Dπ πΊ)βπ))) |
146 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β ((π Dπ πΊ)βπ) = ((π Dπ πΊ)β0)) |
147 | 146 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π = 0) β ((π Dπ πΊ)βπ) = ((π Dπ πΊ)β0)) |
148 | | dvnmul.f |
. . . . . . . . . . . . . . . . . . . . . 22
β’ πΊ = (π₯ β π β¦ π΅) |
149 | 78, 84, 86, 74 | mptelpm 43858 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π₯ β π β¦ π΅) β (β βpm π)) |
150 | 148, 149 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΊ β (β βpm π)) |
151 | | dvn0 25433 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ πΊ β (β
βpm π))
β ((π
Dπ πΊ)β0) = πΊ) |
152 | 76, 150, 151 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π Dπ πΊ)β0) = πΊ) |
153 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π = 0) β ((π Dπ πΊ)β0) = πΊ) |
154 | 147, 153 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = 0) β ((π Dπ πΊ)βπ) = πΊ) |
155 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΊ = (π₯ β π β¦ π΅)) |
156 | | mptexg 7220 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π« π β (π₯ β π β¦ π΅) β V) |
157 | 82, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π₯ β π β¦ π΅) β V) |
158 | 155, 157 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΊ β V) |
159 | 145, 154,
112, 158 | fvmptd 7003 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π β (0...π) β¦ ((π Dπ πΊ)βπ))β0) = πΊ) |
160 | 144, 159 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (π β (π·β0) = πΊ) |
161 | 160 | fveq1d 6891 |
. . . . . . . . . . . . . . 15
β’ (π β ((π·β0)βπ₯) = (πΊβπ₯)) |
162 | 161 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π = 0) β ((π·β0)βπ₯) = (πΊβπ₯)) |
163 | 155, 78 | fvmpt2d 7009 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π) β (πΊβπ₯) = π΅) |
164 | 163 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π = 0) β (πΊβπ₯) = π΅) |
165 | 138, 162,
164 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ π = 0) β ((π·β(0 β π))βπ₯) = π΅) |
166 | 130, 165 | oveq12d 7424 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ π = 0) β (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯)) = (π΄ Β· π΅)) |
167 | 103, 166 | oveq12d 7424 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π = 0) β ((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))) = (1 Β· (π΄ Β· π΅))) |
168 | 79 | mullidd 11229 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β (1 Β· (π΄ Β· π΅)) = (π΄ Β· π΅)) |
169 | 168 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ π = 0) β (1 Β· (π΄ Β· π΅)) = (π΄ Β· π΅)) |
170 | 167, 169 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ π = 0) β ((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))) = (π΄ Β· π΅)) |
171 | | 0re 11213 |
. . . . . . . . . . 11
β’ 0 β
β |
172 | 171 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β 0 β β) |
173 | 95, 96, 170, 172, 79 | sumsnd 43696 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β Ξ£π β {0} ((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))) = (π΄ Β· π΅)) |
174 | 94, 173 | eqtr2d 2774 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (π΄ Β· π΅) = Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯)))) |
175 | 174 | mpteq2dva 5248 |
. . . . . . 7
β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) = (π₯ β π β¦ Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))))) |
176 | 89, 175 | eqtrd 2773 |
. . . . . 6
β’ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β0) = (π₯ β π β¦ Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯))))) |
177 | 176 | a1i 11 |
. . . . 5
β’ (π β
(β€β₯β0) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β0) = (π₯ β π β¦ Ξ£π β (0...0)((0Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(0 β π))βπ₯)))))) |
178 | | simp3 1139 |
. . . . . . 7
β’ ((π β (0..^π) β§ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β§ π) β π) |
179 | | simp1 1137 |
. . . . . . 7
β’ ((π β (0..^π) β§ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β§ π) β π β (0..^π)) |
180 | | simp2 1138 |
. . . . . . . 8
β’ ((π β (0..^π) β§ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β§ π) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) |
181 | | pm3.35 802 |
. . . . . . . 8
β’ ((π β§ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) |
182 | 178, 180,
181 | syl2anc 585 |
. . . . . . 7
β’ ((π β (0..^π) β§ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β§ π) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) |
183 | 76 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β β) |
184 | 87 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π₯ β π β¦ (π΄ Β· π΅)) β (β βpm π)) |
185 | | elfzonn0 13674 |
. . . . . . . . . . 11
β’ (π β (0..^π) β π β β0) |
186 | 185 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β β0) |
187 | | dvnp1 25434 |
. . . . . . . . . 10
β’ ((π β β β§ (π₯ β π β¦ (π΄ Β· π΅)) β (β βpm π) β§ π β β0) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1)) = (π D ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ))) |
188 | 183, 184,
186, 187 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1)) = (π D ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ))) |
189 | 188 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1)) = (π D ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ))) |
190 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) |
191 | 190 | oveq2d 7422 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β (π D ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ)) = (π D (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) |
192 | | eqid 2733 |
. . . . . . . . . . 11
β’
((TopOpenββfld) βΎt π) =
((TopOpenββfld) βΎt π) |
193 | | eqid 2733 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
194 | 74 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π β {β, β}) |
195 | 81 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β π β
((TopOpenββfld) βΎt π)) |
196 | | fzfid 13935 |
. . . . . . . . . . 11
β’ ((π β§ π β (0..^π)) β (0...π) β Fin) |
197 | 185 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0..^π) β§ π β (0...π)) β π β β0) |
198 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β π β β€) |
199 | 198 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0..^π) β§ π β (0...π)) β π β β€) |
200 | 197, 199 | bccld 44012 |
. . . . . . . . . . . . . . 15
β’ ((π β (0..^π) β§ π β (0...π)) β (πCπ) β
β0) |
201 | 200 | nn0cnd 12531 |
. . . . . . . . . . . . . 14
β’ ((π β (0..^π) β§ π β (0...π)) β (πCπ) β β) |
202 | 201 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (πCπ) β β) |
203 | 202 | 3adant3 1133 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β (πCπ) β β) |
204 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β π) |
205 | | 0zd 12567 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (0...π)) β 0 β β€) |
206 | | elfzoel2 13628 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β π β β€) |
207 | 206 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (0...π)) β π β β€) |
208 | | elfzle1 13501 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0...π) β 0 β€ π) |
209 | 208 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (0...π)) β 0 β€ π) |
210 | 199 | zred 12663 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β π β β) |
211 | 206 | zred 12663 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^π) β π β β) |
212 | 211 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β π β β) |
213 | 185 | nn0red 12530 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β π β β) |
214 | 213 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β π β β) |
215 | | elfzle2 13502 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...π) β π β€ π) |
216 | 215 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β π β€ π) |
217 | | elfzolt2 13638 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β π < π) |
218 | 217 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β π < π) |
219 | 210, 214,
212, 216, 218 | lelttrd 11369 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β π < π) |
220 | 210, 212,
219 | ltled 11359 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (0...π)) β π β€ π) |
221 | 205, 207,
199, 209, 220 | elfzd 13489 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (0..^π) β§ π β (0...π)) β π β (0...π)) |
222 | 221 | adantll 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β π β (0...π)) |
223 | | dvnmul.dvnf |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0...π)) β ((π Dπ πΉ)βπ):πβΆβ) |
224 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΆ = (π β (0...π) β¦ ((π Dπ πΉ)βπ))) |
225 | | fvexd 6904 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π)) β ((π Dπ πΉ)βπ) β V) |
226 | 224, 225 | fvmpt2d 7009 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0...π)) β (πΆβπ) = ((π Dπ πΉ)βπ)) |
227 | 226 | feq1d 6700 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0...π)) β ((πΆβπ):πβΆβ β ((π Dπ πΉ)βπ):πβΆβ)) |
228 | 223, 227 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0...π)) β (πΆβπ):πβΆβ) |
229 | 204, 222,
228 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (πΆβπ):πβΆβ) |
230 | 229 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β (πΆβπ):πβΆβ) |
231 | | simp3 1139 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β π₯ β π) |
232 | 230, 231 | ffvelcdmd 7085 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β ((πΆβπ)βπ₯) β β) |
233 | 185 | nn0zd 12581 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β π β β€) |
234 | 233 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β π β β€) |
235 | 234, 199 | zsubcld 12668 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) β β€) |
236 | | elfzel2 13496 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π) β π β β€) |
237 | 236 | zred 12663 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...π) β π β β) |
238 | 198 | zred 12663 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...π) β π β β) |
239 | 237, 238 | subge0d 11801 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...π) β (0 β€ (π β π) β π β€ π)) |
240 | 215, 239 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0...π) β 0 β€ (π β π)) |
241 | 240 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β 0 β€ (π β π)) |
242 | 214, 210 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) β β) |
243 | 212, 210 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) β β) |
244 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...π)) β 0 β β) |
245 | 212, 244 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (0...π)) β (π β β β§ 0 β
β)) |
246 | | resubcl 11521 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ 0 β
β) β (π β
0) β β) |
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β (π β 0) β β) |
248 | 214, 212,
210, 218 | ltsub1dd 11823 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) < (π β π)) |
249 | 244, 210,
212, 209 | lesub2dd 11828 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) β€ (π β 0)) |
250 | 242, 243,
247, 248, 249 | ltletrd 11371 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) < (π β 0)) |
251 | 211 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0..^π) β π β β) |
252 | 251 | subid1d 11557 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0..^π) β (π β 0) = π) |
253 | 252 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (0...π)) β (π β 0) = π) |
254 | 250, 253 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) < π) |
255 | 242, 212,
254 | ltled 11359 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) β€ π) |
256 | 205, 207,
235, 241, 255 | elfzd 13489 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) β (0...π)) |
257 | 256 | adantll 713 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π β π) β (0...π)) |
258 | | ovex 7439 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π) β V |
259 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β π) β (π β (0...π) β (π β π) β (0...π))) |
260 | 259 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β π) β ((π β§ π β (0...π)) β (π β§ (π β π) β (0...π)))) |
261 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β π) β ((π Dπ πΊ)βπ) = ((π Dπ πΊ)β(π β π))) |
262 | 261 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β π) β (((π Dπ πΊ)βπ):πβΆβ β ((π Dπ πΊ)β(π β π)):πβΆβ)) |
263 | 260, 262 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π β π) β (((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) β ((π β§ (π β π) β (0...π)) β ((π Dπ πΊ)β(π β π)):πβΆβ))) |
264 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) |
265 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π β (0...π) β π β (0...π))) |
266 | 265 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((π β§ π β (0...π)) β (π β§ π β (0...π)))) |
267 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π Dπ πΊ)βπ) = ((π Dπ πΊ)βπ)) |
268 | 267 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((π Dπ πΊ)βπ):πβΆβ β ((π Dπ πΊ)βπ):πβΆβ)) |
269 | 266, 268 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) β ((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ))) |
270 | | dvnmul.dvng |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) |
271 | 264, 269,
270 | chvarfv 2234 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) |
272 | 258, 263,
271 | vtocl 3550 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β π) β (0...π)) β ((π Dπ πΊ)β(π β π)):πβΆβ) |
273 | 204, 257,
272 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΊ)β(π β π)):πβΆβ) |
274 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β π) β ((π Dπ πΊ)βπ) = ((π Dπ πΊ)β(π β π))) |
275 | | fvexd 6904 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β ((π Dπ πΊ)β(π β π)) β V) |
276 | 142, 274,
256, 275 | fvmptd3 7019 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (0...π)) β (π·β(π β π)) = ((π Dπ πΊ)β(π β π))) |
277 | 276 | adantll 713 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π·β(π β π)) = ((π Dπ πΊ)β(π β π))) |
278 | 277 | feq1d 6700 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π·β(π β π)):πβΆβ β ((π Dπ πΊ)β(π β π)):πβΆβ)) |
279 | 273, 278 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π·β(π β π)):πβΆβ) |
280 | 279 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β (π·β(π β π)):πβΆβ) |
281 | 280, 231 | ffvelcdmd 7085 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β ((π·β(π β π))βπ₯) β β) |
282 | 232, 281 | mulcld 11231 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)) β β) |
283 | 203, 282 | mulcld 11231 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) β β) |
284 | 203 | 3expa 1119 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (πCπ) β β) |
285 | 234 | peano2zd 12666 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β β€) |
286 | 285, 199 | zsubcld 12668 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (0...π)) β ((π + 1) β π) β β€) |
287 | | peano2re 11384 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β (π + 1) β
β) |
288 | 237, 287 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0...π) β (π + 1) β β) |
289 | | peano2re 11384 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β (π + 1) β
β) |
290 | 238, 289 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π) β (π + 1) β β) |
291 | 238 | ltp1d 12141 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π) β π < (π + 1)) |
292 | | 1red 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (0...π) β 1 β β) |
293 | 238, 237,
292, 215 | leadd1dd 11825 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π) β (π + 1) β€ (π + 1)) |
294 | 238, 290,
288, 291, 293 | ltletrd 11371 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0...π) β π < (π + 1)) |
295 | 238, 288,
294 | ltled 11359 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...π) β π β€ (π + 1)) |
296 | 295 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β π β€ (π + 1)) |
297 | 214, 287 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β β) |
298 | 297, 210 | subge0d 11801 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β (0 β€ ((π + 1) β π) β π β€ (π + 1))) |
299 | 296, 298 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (0...π)) β 0 β€ ((π + 1) β π)) |
300 | 297, 210 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β ((π + 1) β π) β β) |
301 | | elfzop1le2 13642 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0..^π) β (π + 1) β€ π) |
302 | 301 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β€ π) |
303 | 297, 212,
210, 302 | lesub1dd 11827 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β ((π + 1) β π) β€ (π β π)) |
304 | 249, 253 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β (π β π) β€ π) |
305 | 300, 243,
212, 303, 304 | letrd 11368 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (0...π)) β ((π + 1) β π) β€ π) |
306 | 205, 207,
286, 299, 305 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β ((π + 1) β π) β (0...π)) |
307 | 306 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π + 1) β π) β (0...π)) |
308 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π + 1) β π) β V |
309 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = ((π + 1) β π) β (π β (0...π) β ((π + 1) β π) β (0...π))) |
310 | 309 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = ((π + 1) β π) β ((π β§ π β (0...π)) β (π β§ ((π + 1) β π) β (0...π)))) |
311 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = ((π + 1) β π) β ((π Dπ πΊ)βπ) = ((π Dπ πΊ)β((π + 1) β π))) |
312 | 311 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = ((π + 1) β π) β (((π Dπ πΊ)βπ):πβΆβ β ((π Dπ πΊ)β((π + 1) β π)):πβΆβ)) |
313 | 310, 312 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = ((π + 1) β π) β (((π β§ π β (0...π)) β ((π Dπ πΊ)βπ):πβΆβ) β ((π β§ ((π + 1) β π) β (0...π)) β ((π Dπ πΊ)β((π + 1) β π)):πβΆβ))) |
314 | 308, 313,
271 | vtocl 3550 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ ((π + 1) β π) β (0...π)) β ((π Dπ πΊ)β((π + 1) β π)):πβΆβ) |
315 | 204, 307,
314 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΊ)β((π + 1) β π)):πβΆβ) |
316 | 142 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β π· = (π β (0...π) β¦ ((π Dπ πΊ)βπ))) |
317 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π = ((π + 1) β π)) β π = ((π + 1) β π)) |
318 | 317 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π = ((π + 1) β π)) β ((π Dπ πΊ)βπ) = ((π Dπ πΊ)β((π + 1) β π))) |
319 | | fvexd 6904 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΊ)β((π + 1) β π)) β V) |
320 | 316, 318,
307, 319 | fvmptd 7003 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π·β((π + 1) β π)) = ((π Dπ πΊ)β((π + 1) β π))) |
321 | 320 | feq1d 6700 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π·β((π + 1) β π)):πβΆβ β ((π Dπ πΊ)β((π + 1) β π)):πβΆβ)) |
322 | 315, 321 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π·β((π + 1) β π)):πβΆβ) |
323 | 322 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((π·β((π + 1) β π))βπ₯) β β) |
324 | 232 | 3expa 1119 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((πΆβπ)βπ₯) β β) |
325 | 323, 324 | mulcomd 11232 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯)) = (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) |
326 | 325 | oveq2d 7422 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))) = ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
327 | 199 | peano2zd 12666 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β β€) |
328 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...π) β 0 β β) |
329 | 328, 238,
290, 208, 291 | lelttrd 11369 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...π) β 0 < (π + 1)) |
330 | 328, 290,
329 | ltled 11359 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0...π) β 0 β€ (π + 1)) |
331 | 330 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β 0 β€ (π + 1)) |
332 | 210, 289 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β β) |
333 | 293 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β€ (π + 1)) |
334 | 332, 297,
212, 333, 302 | letrd 11368 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β€ π) |
335 | 205, 207,
327, 331, 334 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β (0...π)) |
336 | 335 | adantll 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π + 1) β (0...π)) |
337 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . 19
β’ (π + 1) β V |
338 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π + 1) β (π β (0...π) β (π + 1) β (0...π))) |
339 | 338 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π + 1) β ((π β§ π β (0...π)) β (π β§ (π + 1) β (0...π)))) |
340 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π + 1) β (πΆβπ) = (πΆβ(π + 1))) |
341 | 340 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π + 1) β ((πΆβπ):πβΆβ β (πΆβ(π + 1)):πβΆβ)) |
342 | 339, 341 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β (((π β§ π β (0...π)) β (πΆβπ):πβΆβ) β ((π β§ (π + 1) β (0...π)) β (πΆβ(π + 1)):πβΆβ))) |
343 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(π β§ π β (0...π)) |
344 | | nfmpt1 5256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(π β (0...π) β¦ ((π Dπ πΉ)βπ)) |
345 | 106, 344 | nfcxfr 2902 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²ππΆ |
346 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²ππ |
347 | 345, 346 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π(πΆβπ) |
348 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²ππ |
349 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²πβ |
350 | 347, 348,
349 | nff 6711 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(πΆβπ):πβΆβ |
351 | 343, 350 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((π β§ π β (0...π)) β (πΆβπ):πβΆβ) |
352 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (πΆβπ) = (πΆβπ)) |
353 | 352 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πΆβπ):πβΆβ β (πΆβπ):πβΆβ)) |
354 | 266, 353 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((π β§ π β (0...π)) β (πΆβπ):πβΆβ) β ((π β§ π β (0...π)) β (πΆβπ):πβΆβ))) |
355 | 351, 354,
228 | chvarfv 2234 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π)) β (πΆβπ):πβΆβ) |
356 | 337, 342,
355 | vtocl 3550 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π + 1) β (0...π)) β (πΆβ(π + 1)):πβΆβ) |
357 | 204, 336,
356 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (πΆβ(π + 1)):πβΆβ) |
358 | 357 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((πΆβ(π + 1))βπ₯) β β) |
359 | 281 | 3expa 1119 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((π·β(π β π))βπ₯) β β) |
360 | 358, 359 | mulcld 11231 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) β β) |
361 | 323, 324 | mulcld 11231 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯)) β β) |
362 | 360, 361 | addcld 11230 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))) β β) |
363 | 326, 362 | eqeltrrd 2835 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
364 | 284, 363 | mulcld 11231 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) β β) |
365 | 364 | 3impa 1111 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β (0...π) β§ π₯ β π) β ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) β β) |
366 | 204, 74 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β π β {β, β}) |
367 | 171 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β 0 β β) |
368 | 204, 81 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β π β
((TopOpenββfld) βΎt π)) |
369 | 366, 368,
202 | dvmptconst 44618 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D (π₯ β π β¦ (πCπ))) = (π₯ β π β¦ 0)) |
370 | 282 | 3expa 1119 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)) β β) |
371 | 204, 222,
226 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (πΆβπ) = ((π Dπ πΉ)βπ)) |
372 | 371 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΉ)βπ) = (πΆβπ)) |
373 | 229 | feqmptd 6958 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (πΆβπ) = (π₯ β π β¦ ((πΆβπ)βπ₯))) |
374 | 372, 373 | eqtr2d 2774 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π₯ β π β¦ ((πΆβπ)βπ₯)) = ((π Dπ πΉ)βπ)) |
375 | 374 | oveq2d 7422 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D (π₯ β π β¦ ((πΆβπ)βπ₯))) = (π D ((π Dπ πΉ)βπ))) |
376 | 366, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β π β β) |
377 | 204, 119 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β πΉ β (β βpm π)) |
378 | | elfznn0 13591 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β π β β0) |
379 | 378 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β π β β0) |
380 | | dvnp1 25434 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ πΉ β (β
βpm π)
β§ π β
β0) β ((π Dπ πΉ)β(π + 1)) = (π D ((π Dπ πΉ)βπ))) |
381 | 376, 377,
379, 380 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΉ)β(π + 1)) = (π D ((π Dπ πΉ)βπ))) |
382 | 381 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D ((π Dπ πΉ)βπ)) = ((π Dπ πΉ)β(π + 1))) |
383 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β ((π Dπ πΉ)βπ) = ((π Dπ πΉ)β(π + 1))) |
384 | | fvexd 6904 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΉ)β(π + 1)) β V) |
385 | 109, 383,
336, 384 | fvmptd3 7019 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (πΆβ(π + 1)) = ((π Dπ πΉ)β(π + 1))) |
386 | 385 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΉ)β(π + 1)) = (πΆβ(π + 1))) |
387 | 357 | feqmptd 6958 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (πΆβ(π + 1)) = (π₯ β π β¦ ((πΆβ(π + 1))βπ₯))) |
388 | 386, 387 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΉ)β(π + 1)) = (π₯ β π β¦ ((πΆβ(π + 1))βπ₯))) |
389 | 375, 382,
388 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D (π₯ β π β¦ ((πΆβπ)βπ₯))) = (π₯ β π β¦ ((πΆβ(π + 1))βπ₯))) |
390 | 277 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΊ)β(π β π)) = (π·β(π β π))) |
391 | 279 | feqmptd 6958 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π·β(π β π)) = (π₯ β π β¦ ((π·β(π β π))βπ₯))) |
392 | 390, 391 | eqtr2d 2774 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π₯ β π β¦ ((π·β(π β π))βπ₯)) = ((π Dπ πΊ)β(π β π))) |
393 | 392 | oveq2d 7422 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D (π₯ β π β¦ ((π·β(π β π))βπ₯))) = (π D ((π Dπ πΊ)β(π β π)))) |
394 | 204, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β πΊ β (β βpm π)) |
395 | | fznn0sub 13530 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0...π) β (π β π) β
β0) |
396 | 395 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π β π) β
β0) |
397 | | dvnp1 25434 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ πΊ β (β
βpm π)
β§ (π β π) β β0)
β ((π
Dπ πΊ)β((π β π) + 1)) = (π D ((π Dπ πΊ)β(π β π)))) |
398 | 376, 394,
396, 397 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΊ)β((π β π) + 1)) = (π D ((π Dπ πΊ)β(π β π)))) |
399 | 398 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D ((π Dπ πΊ)β(π β π))) = ((π Dπ πΊ)β((π β π) + 1))) |
400 | 214 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β π β β) |
401 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β 1 β β) |
402 | 210 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...π)) β π β β) |
403 | 400, 401,
402 | addsubd 11589 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (0...π)) β ((π + 1) β π) = ((π β π) + 1)) |
404 | 403 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (0...π)) β ((π β π) + 1) = ((π + 1) β π)) |
405 | 404 | fveq2d 6893 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (0..^π) β§ π β (0...π)) β ((π Dπ πΊ)β((π β π) + 1)) = ((π Dπ πΊ)β((π + 1) β π))) |
406 | 405 | adantll 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΊ)β((π β π) + 1)) = ((π Dπ πΊ)β((π + 1) β π))) |
407 | 320 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΊ)β((π + 1) β π)) = (π·β((π + 1) β π))) |
408 | 322 | feqmptd 6958 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π·β((π + 1) β π)) = (π₯ β π β¦ ((π·β((π + 1) β π))βπ₯))) |
409 | 406, 407,
408 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π Dπ πΊ)β((π β π) + 1)) = (π₯ β π β¦ ((π·β((π + 1) β π))βπ₯))) |
410 | 393, 399,
409 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D (π₯ β π β¦ ((π·β(π β π))βπ₯))) = (π₯ β π β¦ ((π·β((π + 1) β π))βπ₯))) |
411 | 366, 324,
358, 389, 359, 323, 410 | dvmptmul 25470 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D (π₯ β π β¦ (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))) = (π₯ β π β¦ ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))))) |
412 | 366, 284,
367, 369, 370, 362, 411 | dvmptmul 25470 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D (π₯ β π β¦ ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) = (π₯ β π β¦ ((0 Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) + (((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))) Β· (πCπ))))) |
413 | 370 | mul02d 11409 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (0 Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) = 0) |
414 | 326 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))) Β· (πCπ)) = (((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) Β· (πCπ))) |
415 | 363, 284 | mulcomd 11232 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) Β· (πCπ)) = ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
416 | 414, 415 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))) Β· (πCπ)) = ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
417 | 413, 416 | oveq12d 7424 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((0 Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) + (((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))) Β· (πCπ))) = (0 + ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))))) |
418 | 364 | addlidd 11412 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (0 + ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) = ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
419 | 417, 418 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((0 Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) + (((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))) Β· (πCπ))) = ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
420 | 419 | mpteq2dva 5248 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π₯ β π β¦ ((0 Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))) + (((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((π·β((π + 1) β π))βπ₯) Β· ((πΆβπ)βπ₯))) Β· (πCπ)))) = (π₯ β π β¦ ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))))) |
421 | 412, 420 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β (π D (π₯ β π β¦ ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) = (π₯ β π β¦ ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))))) |
422 | 192, 193,
194, 195, 196, 283, 365, 421 | dvmptfsum 25484 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π D (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))))) |
423 | 202 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β (πCπ) β β) |
424 | 360 | an32s 651 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) β β) |
425 | | anass 470 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((π β§ π β (0..^π)) β§ (π β (0...π) β§ π₯ β π))) |
426 | | ancom 462 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0...π) β§ π₯ β π) β (π₯ β π β§ π β (0...π))) |
427 | 426 | anbi2i 624 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ (π β (0...π) β§ π₯ β π)) β ((π β§ π β (0..^π)) β§ (π₯ β π β§ π β (0...π)))) |
428 | | anass 470 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((π β§ π β (0..^π)) β§ (π₯ β π β§ π β (0...π)))) |
429 | 428 | bicomi 223 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ (π₯ β π β§ π β (0...π))) β (((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π))) |
430 | 427, 429 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ (π β (0...π) β§ π₯ β π)) β (((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π))) |
431 | 425, 430 | bitri 275 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β (((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π))) |
432 | 431 | imbi1i 350 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((πΆβπ)βπ₯) β β) β ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((πΆβπ)βπ₯) β β)) |
433 | 324, 432 | mpbi 229 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((πΆβπ)βπ₯) β β) |
434 | 431 | imbi1i 350 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (0..^π)) β§ π β (0...π)) β§ π₯ β π) β ((π·β((π + 1) β π))βπ₯) β β) β ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((π·β((π + 1) β π))βπ₯) β β)) |
435 | 323, 434 | mpbi 229 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((π·β((π + 1) β π))βπ₯) β β) |
436 | 433, 435 | mulcld 11231 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) β β) |
437 | 423, 424,
436 | adddid 11235 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = (((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) + ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
438 | 437 | sumeq2dv 15646 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (0...π)(((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) + ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
439 | 196 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (0...π) β Fin) |
440 | 423, 424 | mulcld 11231 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) β β) |
441 | 423, 436 | mulcld 11231 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
442 | 439, 440,
441 | fsumadd 15683 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)(((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) + ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = (Ξ£π β (0...π)((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) + Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
443 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β β (πCπ) = (πCβ)) |
444 | | fvoveq1 7429 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β β (πΆβ(π + 1)) = (πΆβ(β + 1))) |
445 | 444 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β β ((πΆβ(π + 1))βπ₯) = ((πΆβ(β + 1))βπ₯)) |
446 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = β β (π β π) = (π β β)) |
447 | 446 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = β β (π·β(π β π)) = (π·β(π β β))) |
448 | 447 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β β ((π·β(π β π))βπ₯) = ((π·β(π β β))βπ₯)) |
449 | 445, 448 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β β (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) = (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) |
450 | 443, 449 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . 18
β’ (π = β β ((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) = ((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯)))) |
451 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²β(0...π) |
452 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(0...π) |
453 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²β((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) |
454 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(πCβ) |
455 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π
Β· |
456 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π(β + 1) |
457 | 345, 456 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(πΆβ(β + 1)) |
458 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²ππ₯ |
459 | 457, 458 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((πΆβ(β + 1))βπ₯) |
460 | | nfmpt1 5256 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(π β (0...π) β¦ ((π Dπ πΊ)βπ)) |
461 | 139, 460 | nfcxfr 2902 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²ππ· |
462 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π(π β β) |
463 | 461, 462 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π(π·β(π β β)) |
464 | 463, 458 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((π·β(π β β))βπ₯) |
465 | 459, 455,
464 | nfov 7436 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯)) |
466 | 454, 455,
465 | nfov 7436 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) |
467 | 450, 451,
452, 453, 466 | cbvsum 15638 |
. . . . . . . . . . . . . . . . 17
β’
Ξ£π β
(0...π)((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£β β (0...π)((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) |
468 | 467 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£β β (0...π)((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯)))) |
469 | | 1zzd 12590 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β 1 β β€) |
470 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β 0 β β€) |
471 | 233 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β π β β€) |
472 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((π β§ π β (0..^π)) β§ π₯ β π) |
473 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²πβ |
474 | 473, 452 | nfel 2918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π β β (0...π) |
475 | 472, 474 | nfan 1903 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(((π β§ π β (0..^π)) β§ π₯ β π) β§ β β (0...π)) |
476 | 466, 349 | nfel 2918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) β β |
477 | 475, 476 | nfim 1900 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((((π β§ π β (0..^π)) β§ π₯ β π) β§ β β (0...π)) β ((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) β β) |
478 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = β β (π β (0...π) β β β (0...π))) |
479 | 478 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β β ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β (((π β§ π β (0..^π)) β§ π₯ β π) β§ β β (0...π)))) |
480 | 450 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = β β (((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) β β β ((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) β β)) |
481 | 479, 480 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π = β β (((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) β β) β ((((π β§ π β (0..^π)) β§ π₯ β π) β§ β β (0...π)) β ((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) β β))) |
482 | 477, 481,
440 | chvarfv 2234 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ β β (0...π)) β ((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) β β) |
483 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . 18
β’ (β = (π β 1) β (πCβ) = (πC(π β 1))) |
484 | | fvoveq1 7429 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = (π β 1) β (πΆβ(β + 1)) = (πΆβ((π β 1) + 1))) |
485 | 484 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = (π β 1) β ((πΆβ(β + 1))βπ₯) = ((πΆβ((π β 1) + 1))βπ₯)) |
486 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β = (π β 1) β (π β β) = (π β (π β 1))) |
487 | 486 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β = (π β 1) β (π·β(π β β)) = (π·β(π β (π β 1)))) |
488 | 487 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (β = (π β 1) β ((π·β(π β β))βπ₯) = ((π·β(π β (π β 1)))βπ₯)) |
489 | 485, 488 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . 18
β’ (β = (π β 1) β (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯)) = (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯))) |
490 | 483, 489 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (β = (π β 1) β ((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) = ((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯)))) |
491 | 469, 470,
471, 482, 490 | fsumshft 15723 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£β β (0...π)((πCβ) Β· (((πΆβ(β + 1))βπ₯) Β· ((π·β(π β β))βπ₯))) = Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯)))) |
492 | 468, 491 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) = Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯)))) |
493 | | 0p1e1 12331 |
. . . . . . . . . . . . . . . . . 18
β’ (0 + 1) =
1 |
494 | 493 | oveq1i 7416 |
. . . . . . . . . . . . . . . . 17
β’ ((0 +
1)...(π + 1)) = (1...(π + 1)) |
495 | 494 | sumeq1i 15641 |
. . . . . . . . . . . . . . . 16
β’
Ξ£π β ((0
+ 1)...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯))) = Ξ£π β (1...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯))) |
496 | 495 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β ((0 + 1)...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯))) = Ξ£π β (1...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯)))) |
497 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...(π + 1)) β π β β€) |
498 | 497 | zcnd 12664 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...(π + 1)) β π β β) |
499 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...(π + 1)) β 1 β
β) |
500 | 498, 499 | npcand 11572 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...(π + 1)) β ((π β 1) + 1) = π) |
501 | 500 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...(π + 1)) β (πΆβ((π β 1) + 1)) = (πΆβπ)) |
502 | 501 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...(π + 1)) β ((πΆβ((π β 1) + 1))βπ₯) = ((πΆβπ)βπ₯)) |
503 | 502 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((πΆβ((π β 1) + 1))βπ₯) = ((πΆβπ)βπ₯)) |
504 | 213 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0..^π) β π β β) |
505 | 504 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β) |
506 | 498 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β) |
507 | 499 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β 1 β
β) |
508 | 505, 506,
507 | subsub3d 11598 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (π β (π β 1)) = ((π + 1) β π)) |
509 | 508 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (π·β(π β (π β 1))) = (π·β((π + 1) β π))) |
510 | 509 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π·β(π β (π β 1)))βπ₯) = ((π·β((π + 1) β π))βπ₯)) |
511 | 503, 510 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯)) = (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) |
512 | 511 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯))) = ((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
513 | 512 | sumeq2dv 15646 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β Ξ£π β (1...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯))) = Ξ£π β (1...(π + 1))((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
514 | 513 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯))) = Ξ£π β (1...(π + 1))((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
515 | | nfv 1918 |
. . . . . . . . . . . . . . . . 17
β’
β²π((π β§ π β (0..^π)) β§ π₯ β π) |
516 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π((πC((π + 1) β 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) |
517 | | fzfid 13935 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (1...(π + 1)) β Fin) |
518 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β0) |
519 | 497 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β€) |
520 | | 1zzd 12590 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β 1 β
β€) |
521 | 519, 520 | zsubcld 12668 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (π β 1) β β€) |
522 | 518, 521 | bccld 44012 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (πC(π β 1)) β
β0) |
523 | 522 | nn0cnd 12531 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (πC(π β 1)) β β) |
524 | 523 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π β (1...(π + 1))) β (πC(π β 1)) β β) |
525 | 524 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...(π + 1))) β (πC(π β 1)) β β) |
526 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ π β (1...(π + 1))) β π) |
527 | | 0zd 12567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β 0 β
β€) |
528 | 206 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β€) |
529 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...(π + 1)) β 0 β
β) |
530 | 497 | zred 12663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...(π + 1)) β π β β) |
531 | | 1red 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...(π + 1)) β 1 β
β) |
532 | | 0lt1 11733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 0 <
1 |
533 | 532 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...(π + 1)) β 0 < 1) |
534 | | elfzle1 13501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...(π + 1)) β 1 β€ π) |
535 | 529, 531,
530, 533, 534 | ltletrd 11371 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...(π + 1)) β 0 < π) |
536 | 529, 530,
535 | ltled 11359 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...(π + 1)) β 0 β€ π) |
537 | 536 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β 0 β€ π) |
538 | 530 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β) |
539 | 213 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β) |
540 | | 1red 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β 1 β
β) |
541 | 539, 540 | readdcld 11240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (π + 1) β β) |
542 | 211 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β) |
543 | | elfzle2 13502 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...(π + 1)) β π β€ (π + 1)) |
544 | 543 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β€ (π + 1)) |
545 | 301 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (π + 1) β€ π) |
546 | 538, 541,
542, 544, 545 | letrd 11368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β€ π) |
547 | 527, 528,
519, 537, 546 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β (0...π)) |
548 | 547 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ π β (1...(π + 1))) β π β (0...π)) |
549 | 526, 548,
355 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ π β (1...(π + 1))) β (πΆβπ):πβΆβ) |
550 | 549 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...(π + 1))) β (πΆβπ):πβΆβ) |
551 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...(π + 1))) β π₯ β π) |
552 | 550, 551 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...(π + 1))) β ((πΆβπ)βπ₯) β β) |
553 | 233 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β€) |
554 | 553 | peano2zd 12666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (π + 1) β β€) |
555 | 554, 519 | zsubcld 12668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π + 1) β π) β β€) |
556 | 541, 538 | subge0d 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β (0 β€ ((π + 1) β π) β π β€ (π + 1))) |
557 | 544, 556 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β 0 β€ ((π + 1) β π)) |
558 | 541, 538 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π + 1) β π) β β) |
559 | 558 | leidd 11777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π + 1) β π) β€ ((π + 1) β π)) |
560 | 530, 535 | elrpd 13010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (1...(π + 1)) β π β β+) |
561 | 560 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β π β β+) |
562 | 541, 561 | ltsubrpd 13045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π + 1) β π) < (π + 1)) |
563 | 558, 541,
542, 562, 545 | ltletrd 11371 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π + 1) β π) < π) |
564 | 558, 558,
542, 559, 563 | lelttrd 11369 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π + 1) β π) < π) |
565 | 558, 542,
564 | ltled 11359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π + 1) β π) β€ π) |
566 | 527, 528,
555, 557, 565 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (1...(π + 1))) β ((π + 1) β π) β (0...π)) |
567 | 566 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ π β (1...(π + 1))) β ((π + 1) β π) β (0...π)) |
568 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(π β§ ((π + 1) β π) β (0...π)) |
569 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π((π + 1) β π) |
570 | 461, 569 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π(π·β((π + 1) β π)) |
571 | 570, 348,
349 | nff 6711 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(π·β((π + 1) β π)):πβΆβ |
572 | 568, 571 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π((π β§ ((π + 1) β π) β (0...π)) β (π·β((π + 1) β π)):πβΆβ) |
573 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π + 1) β π) β V |
574 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = ((π + 1) β π) β (π β (0...π) β ((π + 1) β π) β (0...π))) |
575 | 574 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((π + 1) β π) β ((π β§ π β (0...π)) β (π β§ ((π + 1) β π) β (0...π)))) |
576 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = ((π + 1) β π) β (π·βπ) = (π·β((π + 1) β π))) |
577 | 576 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((π + 1) β π) β ((π·βπ):πβΆβ β (π·β((π + 1) β π)):πβΆβ)) |
578 | 575, 577 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((π + 1) β π) β (((π β§ π β (0...π)) β (π·βπ):πβΆβ) β ((π β§ ((π + 1) β π) β (0...π)) β (π·β((π + 1) β π)):πβΆβ))) |
579 | 139 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π· = (π β (0...π) β¦ ((π Dπ πΊ)βπ))) |
580 | | fvexd 6904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β (0...π)) β ((π Dπ πΊ)βπ) β V) |
581 | 579, 580 | fvmpt2d 7009 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (0...π)) β (π·βπ) = ((π Dπ πΊ)βπ)) |
582 | 581 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π β (0...π)) β ((π·βπ):πβΆβ β ((π Dπ πΊ)βπ):πβΆβ)) |
583 | 270, 582 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0...π)) β (π·βπ):πβΆβ) |
584 | 572, 573,
578, 583 | vtoclf 3548 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ ((π + 1) β π) β (0...π)) β (π·β((π + 1) β π)):πβΆβ) |
585 | 526, 567,
584 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ π β (1...(π + 1))) β (π·β((π + 1) β π)):πβΆβ) |
586 | 585 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...(π + 1))) β (π·β((π + 1) β π)):πβΆβ) |
587 | 586, 551 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...(π + 1))) β ((π·β((π + 1) β π))βπ₯) β β) |
588 | 552, 587 | mulcld 11231 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...(π + 1))) β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) β β) |
589 | 525, 588 | mulcld 11231 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...(π + 1))) β ((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
590 | | 1zzd 12590 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β 1 β β€) |
591 | 233 | peano2zd 12666 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β (π + 1) β β€) |
592 | 493 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 1 = (0 +
1) |
593 | 592 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0..^π) β 1 = (0 + 1)) |
594 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0..^π) β 0 β β) |
595 | | 1red 11212 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0..^π) β 1 β β) |
596 | 185 | nn0ge0d 12532 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0..^π) β 0 β€ π) |
597 | 594, 213,
595, 596 | leadd1dd 11825 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0..^π) β (0 + 1) β€ (π + 1)) |
598 | 593, 597 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β 1 β€ (π + 1)) |
599 | 590, 591,
598 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^π) β (1 β β€ β§ (π + 1) β β€ β§ 1
β€ (π +
1))) |
600 | | eluz2 12825 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π + 1) β
(β€β₯β1) β (1 β β€ β§ (π + 1) β β€ β§ 1
β€ (π +
1))) |
601 | 599, 600 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β (π + 1) β
(β€β₯β1)) |
602 | | eluzfz2 13506 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) β
(β€β₯β1) β (π + 1) β (1...(π + 1))) |
603 | 601, 602 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β (π + 1) β (1...(π + 1))) |
604 | 603 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (π + 1) β (1...(π + 1))) |
605 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β (π β 1) = ((π + 1) β 1)) |
606 | 605 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β (πC(π β 1)) = (πC((π + 1) β 1))) |
607 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π + 1) β (πΆβπ) = (πΆβ(π + 1))) |
608 | 607 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β ((πΆβπ)βπ₯) = ((πΆβ(π + 1))βπ₯)) |
609 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π + 1) β ((π + 1) β π) = ((π + 1) β (π + 1))) |
610 | 609 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π + 1) β (π·β((π + 1) β π)) = (π·β((π + 1) β (π + 1)))) |
611 | 610 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β ((π·β((π + 1) β π))βπ₯) = ((π·β((π + 1) β (π + 1)))βπ₯)) |
612 | 608, 611 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) = (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) |
613 | 606, 612 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β ((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = ((πC((π + 1) β 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯)))) |
614 | 515, 516,
517, 589, 604, 613 | fsumsplit1 15688 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...(π + 1))((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = (((πC((π + 1) β 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) + Ξ£π β ((1...(π + 1)) β {(π + 1)})((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
615 | | 1cnd 11206 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0..^π) β 1 β β) |
616 | 504, 615 | pncand 11569 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0..^π) β ((π + 1) β 1) = π) |
617 | 616 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β (πC((π + 1) β 1)) = (πCπ)) |
618 | | bcnn 14269 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β (πCπ) = 1) |
619 | 185, 618 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β (πCπ) = 1) |
620 | 617, 619 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^π) β (πC((π + 1) β 1)) = 1) |
621 | 504, 615 | addcld 11230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0..^π) β (π + 1) β β) |
622 | 621 | subidd 11556 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0..^π) β ((π + 1) β (π + 1)) = 0) |
623 | 622 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0..^π) β (π·β((π + 1) β (π + 1))) = (π·β0)) |
624 | 623 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β ((π·β((π + 1) β (π + 1)))βπ₯) = ((π·β0)βπ₯)) |
625 | 624 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^π) β (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯)) = (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯))) |
626 | 620, 625 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β ((πC((π + 1) β 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) = (1 Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)))) |
627 | 626 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((πC((π + 1) β 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) = (1 Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)))) |
628 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0..^π)) β π) |
629 | | fzofzp1 13726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0..^π) β (π + 1) β (0...π)) |
630 | 629 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
631 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(π β§ (π + 1) β (0...π)) |
632 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π(π + 1) |
633 | 345, 632 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π(πΆβ(π + 1)) |
634 | 633, 348,
349 | nff 6711 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(πΆβ(π + 1)):πβΆβ |
635 | 631, 634 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π((π β§ (π + 1) β (0...π)) β (πΆβ(π + 1)):πβΆβ) |
636 | | ovex 7439 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π + 1) β V |
637 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π + 1) β (π β (0...π) β (π + 1) β (0...π))) |
638 | 637 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π + 1) β ((π β§ π β (0...π)) β (π β§ (π + 1) β (0...π)))) |
639 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π + 1) β (πΆβπ) = (πΆβ(π + 1))) |
640 | 639 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π + 1) β ((πΆβπ):πβΆβ β (πΆβ(π + 1)):πβΆβ)) |
641 | 638, 640 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π + 1) β (((π β§ π β (0...π)) β (πΆβπ):πβΆβ) β ((π β§ (π + 1) β (0...π)) β (πΆβ(π + 1)):πβΆβ))) |
642 | 635, 636,
641, 228 | vtoclf 3548 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (π + 1) β (0...π)) β (πΆβ(π + 1)):πβΆβ) |
643 | 628, 630,
642 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0..^π)) β (πΆβ(π + 1)):πβΆβ) |
644 | 643 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((πΆβ(π + 1))βπ₯) β β) |
645 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π(π β§ 0 β (0...π)) |
646 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
β²π0 |
647 | 461, 646 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
β²π(π·β0) |
648 | 647, 348,
349 | nff 6711 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π(π·β0):πβΆβ |
649 | 645, 648 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π((π β§ 0 β (0...π)) β (π·β0):πβΆβ) |
650 | | c0ex 11205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β
V |
651 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = 0 β (π β (0...π) β 0 β (0...π))) |
652 | 651 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = 0 β ((π β§ π β (0...π)) β (π β§ 0 β (0...π)))) |
653 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = 0 β (π·βπ) = (π·β0)) |
654 | 653 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = 0 β ((π·βπ):πβΆβ β (π·β0):πβΆβ)) |
655 | 652, 654 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = 0 β (((π β§ π β (0...π)) β (π·βπ):πβΆβ) β ((π β§ 0 β (0...π)) β (π·β0):πβΆβ))) |
656 | 649, 650,
655, 583 | vtoclf 3548 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ 0 β (0...π)) β (π·β0):πβΆβ) |
657 | 1, 112, 656 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π·β0):πβΆβ) |
658 | 657 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0..^π)) β (π·β0):πβΆβ) |
659 | 658 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((π·β0)βπ₯) β β) |
660 | 644, 659 | mulcld 11231 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) β β) |
661 | 660 | mullidd 11229 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (1 Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯))) = (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯))) |
662 | 627, 661 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((πC((π + 1) β 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) = (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯))) |
663 | | 1m1e0 12281 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (1
β 1) = 0 |
664 | 663 | fveq2i 6892 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(β€β₯β(1 β 1)) =
(β€β₯β0) |
665 | 3 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(β€β₯β0) = β0 |
666 | 664, 665 | eqtr2i 2762 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β0 = (β€β₯β(1 β
1)) |
667 | 666 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0..^π) β β0 =
(β€β₯β(1 β 1))) |
668 | 185, 667 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β π β (β€β₯β(1
β 1))) |
669 | | fzdifsuc2 44007 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β(1 β 1)) β (1...π) = ((1...(π + 1)) β {(π + 1)})) |
670 | 668, 669 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^π) β (1...π) = ((1...(π + 1)) β {(π + 1)})) |
671 | 670 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β ((1...(π + 1)) β {(π + 1)}) = (1...π)) |
672 | 671 | sumeq1d 15644 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β Ξ£π β ((1...(π + 1)) β {(π + 1)})((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
673 | 672 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β ((1...(π + 1)) β {(π + 1)})((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
674 | 662, 673 | oveq12d 7424 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πC((π + 1) β 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) + Ξ£π β ((1...(π + 1)) β {(π + 1)})((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = ((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
675 | 514, 614,
674 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...(π + 1))((πC(π β 1)) Β· (((πΆβ((π β 1) + 1))βπ₯) Β· ((π·β(π β (π β 1)))βπ₯))) = ((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
676 | 492, 496,
675 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) = ((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
677 | | nfcv 2904 |
. . . . . . . . . . . . . . . . 17
β’
β²π(πC0) |
678 | 345, 646 | nffv 6899 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(πΆβ0) |
679 | 678, 458 | nffv 6899 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((πΆβ0)βπ₯) |
680 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((π + 1) β 0) |
681 | 461, 680 | nffv 6899 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(π·β((π + 1) β 0)) |
682 | 681, 458 | nffv 6899 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π·β((π + 1) β 0))βπ₯) |
683 | 679, 455,
682 | nfov 7436 |
. . . . . . . . . . . . . . . . 17
β’
β²π(((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯)) |
684 | 677, 455,
683 | nfov 7436 |
. . . . . . . . . . . . . . . 16
β’
β²π((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) |
685 | 665 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β (β€β₯β0) =
β0) |
686 | 185, 685 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β π β
(β€β₯β0)) |
687 | | eluzfz1 13505 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
688 | 686, 687 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β 0 β (0...π)) |
689 | 688 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β 0 β (0...π)) |
690 | | oveq2 7414 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (πCπ) = (πC0)) |
691 | 104 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β ((πΆβπ)βπ₯) = ((πΆβ0)βπ₯)) |
692 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β ((π + 1) β π) = ((π + 1) β 0)) |
693 | 692 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (π·β((π + 1) β π)) = (π·β((π + 1) β 0))) |
694 | 693 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β ((π·β((π + 1) β π))βπ₯) = ((π·β((π + 1) β 0))βπ₯)) |
695 | 691, 694 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) = (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) |
696 | 690, 695 | oveq12d 7424 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = ((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯)))) |
697 | 472, 684,
439, 441, 689, 696 | fsumsplit1 15688 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = (((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) + Ξ£π β ((0...π) β {0})((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
698 | 621 | subid1d 11557 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β ((π + 1) β 0) = (π + 1)) |
699 | 698 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^π) β (π·β((π + 1) β 0)) = (π·β(π + 1))) |
700 | 699 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β ((π·β((π + 1) β 0))βπ₯) = ((π·β(π + 1))βπ₯)) |
701 | 700 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯)) = (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) |
702 | 701 | oveq2d 7422 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β ((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) = ((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)))) |
703 | 702 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
β’ (π β (0..^π) β (((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) + Ξ£π β ((0...π) β {0})((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = (((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) + Ξ£π β ((0...π) β {0})((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
704 | 703 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) + Ξ£π β ((0...π) β {0})((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = (((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) + Ξ£π β ((0...π) β {0})((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
705 | | bcn0 14267 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (πC0) =
1) |
706 | 185, 705 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β (πC0) = 1) |
707 | 706 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β ((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) = (1 Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)))) |
708 | 707 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) = (1 Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)))) |
709 | 678, 348,
349 | nff 6711 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(πΆβ0):πβΆβ |
710 | 645, 709 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π((π β§ 0 β (0...π)) β (πΆβ0):πβΆβ) |
711 | 104 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = 0 β ((πΆβπ):πβΆβ β (πΆβ0):πβΆβ)) |
712 | 652, 711 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = 0 β (((π β§ π β (0...π)) β (πΆβπ):πβΆβ) β ((π β§ 0 β (0...π)) β (πΆβ0):πβΆβ))) |
713 | 710, 650,
712, 228 | vtoclf 3548 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ 0 β (0...π)) β (πΆβ0):πβΆβ) |
714 | 1, 112, 713 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (πΆβ0):πβΆβ) |
715 | 714 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0..^π)) β (πΆβ0):πβΆβ) |
716 | 715 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((πΆβ0)βπ₯) β β) |
717 | 461, 632 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(π·β(π + 1)) |
718 | 717, 348,
349 | nff 6711 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(π·β(π + 1)):πβΆβ |
719 | 631, 718 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
β²π((π β§ (π + 1) β (0...π)) β (π·β(π + 1)):πβΆβ) |
720 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π + 1) β (π·βπ) = (π·β(π + 1))) |
721 | 720 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π + 1) β ((π·βπ):πβΆβ β (π·β(π + 1)):πβΆβ)) |
722 | 638, 721 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π + 1) β (((π β§ π β (0...π)) β (π·βπ):πβΆβ) β ((π β§ (π + 1) β (0...π)) β (π·β(π + 1)):πβΆβ))) |
723 | 719, 636,
722, 583 | vtoclf 3548 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π + 1) β (0...π)) β (π·β(π + 1)):πβΆβ) |
724 | 628, 630,
723 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0..^π)) β (π·β(π + 1)):πβΆβ) |
725 | 724 | ffvelcdmda 7084 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((π·β(π + 1))βπ₯) β β) |
726 | 716, 725 | mulcld 11231 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) β β) |
727 | 726 | mullidd 11229 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (1 Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) = (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) |
728 | 708, 727 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) = (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) |
729 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π π β (0..^π) |
730 | | 1zzd 12590 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β ((0...π) β {0})) β 1 β
β€) |
731 | 233 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β ((0...π) β {0})) β π β β€) |
732 | | eldifi 4126 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((0...π) β {0}) β π β (0...π)) |
733 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π) β π β β€) |
734 | 732, 733 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β ((0...π) β {0}) β π β β€) |
735 | 734 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β ((0...π) β {0})) β π β β€) |
736 | | elfznn0 13591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0...π) β π β β0) |
737 | 732, 736 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((0...π) β {0}) β π β β0) |
738 | | eldifsni 4793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ((0...π) β {0}) β π β 0) |
739 | 737, 738 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((0...π) β {0}) β (π β β0 β§ π β 0)) |
740 | | elnnne0 12483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β (π β β0
β§ π β
0)) |
741 | 739, 740 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((0...π) β {0}) β π β β) |
742 | | nnge1 12237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β 1 β€
π) |
743 | 741, 742 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β ((0...π) β {0}) β 1 β€ π) |
744 | 743 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β ((0...π) β {0})) β 1 β€ π) |
745 | | elfzle2 13502 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...π) β π β€ π) |
746 | 732, 745 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β ((0...π) β {0}) β π β€ π) |
747 | 746 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β ((0...π) β {0})) β π β€ π) |
748 | 730, 731,
735, 744, 747 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β ((0...π) β {0})) β π β (1...π)) |
749 | 748 | ex 414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β (π β ((0...π) β {0}) β π β (1...π))) |
750 | | 0zd 12567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...π) β 0 β β€) |
751 | | elfzel2 13496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...π) β π β β€) |
752 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...π) β π β β€) |
753 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...π) β 0 β β) |
754 | 752 | zred 12663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...π) β π β β) |
755 | | 1red 11212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...π) β 1 β β) |
756 | 532 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...π) β 0 < 1) |
757 | | elfzle1 13501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (1...π) β 1 β€ π) |
758 | 753, 755,
754, 756, 757 | ltletrd 11371 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (1...π) β 0 < π) |
759 | 753, 754,
758 | ltled 11359 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...π) β 0 β€ π) |
760 | | elfzle2 13502 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...π) β π β€ π) |
761 | 750, 751,
752, 759, 760 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...π) β π β (0...π)) |
762 | 753, 758 | gtned 11346 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...π) β π β 0) |
763 | | nelsn 4668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β 0 β Β¬ π β {0}) |
764 | 762, 763 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...π) β Β¬ π β {0}) |
765 | 761, 764 | eldifd 3959 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) β π β ((0...π) β {0})) |
766 | 765 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (1...π)) β π β ((0...π) β {0})) |
767 | 766 | ex 414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β (π β (1...π) β π β ((0...π) β {0}))) |
768 | 749, 767 | impbid 211 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^π) β (π β ((0...π) β {0}) β π β (1...π))) |
769 | 729, 768 | alrimi 2207 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β βπ(π β ((0...π) β {0}) β π β (1...π))) |
770 | | dfcleq 2726 |
. . . . . . . . . . . . . . . . . . 19
β’
(((0...π) β
{0}) = (1...π) β
βπ(π β ((0...π) β {0}) β π β (1...π))) |
771 | 769, 770 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β ((0...π) β {0}) = (1...π)) |
772 | 771 | sumeq1d 15644 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β Ξ£π β ((0...π) β {0})((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
773 | 772 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β ((0...π) β {0})((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
774 | 728, 773 | oveq12d 7424 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πC0) Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) + Ξ£π β ((0...π) β {0})((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
775 | 697, 704,
774 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
776 | 676, 775 | oveq12d 7424 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (Ξ£π β (0...π)((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) + Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = (((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) + ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))))) |
777 | | fzfid 13935 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (1...π) β Fin) |
778 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...π)) β π β β0) |
779 | 766, 734 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (1...π)) β π β β€) |
780 | | 1zzd 12590 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (1...π)) β 1 β β€) |
781 | 779, 780 | zsubcld 12668 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...π)) β (π β 1) β β€) |
782 | 778, 781 | bccld 44012 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (1...π)) β (πC(π β 1)) β
β0) |
783 | 782 | nn0cnd 12531 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (1...π)) β (πC(π β 1)) β β) |
784 | 783 | adantll 713 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (πC(π β 1)) β β) |
785 | 784 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (πC(π β 1)) β β) |
786 | | simpl 484 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((π β§ π β (0..^π)) β§ π₯ β π)) |
787 | | fzelp1 13550 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β π β (1...(π + 1))) |
788 | 787 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β π β (1...(π + 1))) |
789 | 786, 788,
552 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((πΆβπ)βπ₯) β β) |
790 | 788, 587 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((π·β((π + 1) β π))βπ₯) β β) |
791 | 789, 790 | mulcld 11231 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) β β) |
792 | 785, 791 | mulcld 11231 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
793 | 777, 792 | fsumcl 15676 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
794 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...π)) β π β β0) |
795 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π) β π β β€) |
796 | 795 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...π)) β π β β€) |
797 | 794, 796 | bccld 44012 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (1...π)) β (πCπ) β
β0) |
798 | 797 | nn0cnd 12531 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (0..^π) β§ π β (1...π)) β (πCπ) β β) |
799 | 798 | adantll 713 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (πCπ) β β) |
800 | 799 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (πCπ) β β) |
801 | | simpll 766 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (π β§ π β (0..^π))) |
802 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β π₯ β π) |
803 | 761 | ssriv 3986 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1...π) β
(0...π) |
804 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β π β (1...π)) |
805 | 803, 804 | sselid 3980 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β π β (0...π)) |
806 | 805 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β π β (0...π)) |
807 | 801, 802,
806, 433 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((πΆβπ)βπ₯) β β) |
808 | 806, 435 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((π·β((π + 1) β π))βπ₯) β β) |
809 | 807, 808 | mulcld 11231 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) β β) |
810 | 800, 809 | mulcld 11231 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
811 | 777, 810 | fsumcl 15676 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
812 | 660, 793,
726, 811 | add4d 11439 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) + ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) = (((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) + (Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))))) |
813 | | oveq1 7413 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π β 1) = (π β 1)) |
814 | 813 | oveq2d 7422 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (πC(π β 1)) = (πC(π β 1))) |
815 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (πΆβπ) = (πΆβπ)) |
816 | 815 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πΆβπ)βπ₯) = ((πΆβπ)βπ₯)) |
817 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β ((π + 1) β π) = ((π + 1) β π)) |
818 | 817 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (π·β((π + 1) β π)) = (π·β((π + 1) β π))) |
819 | 818 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((π·β((π + 1) β π))βπ₯) = ((π·β((π + 1) β π))βπ₯)) |
820 | 816, 819 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) = (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) |
821 | 814, 820 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = ((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
822 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(1...π) |
823 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(1...π) |
824 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(πC(π β 1)) |
825 | 347, 458 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π((πΆβπ)βπ₯) |
826 | 570, 458 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π((π·β((π + 1) β π))βπ₯) |
827 | 825, 455,
826 | nfov 7436 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) |
828 | 824, 455,
827 | nfov 7436 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) |
829 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) |
830 | 821, 822,
823, 828, 829 | cbvsum 15638 |
. . . . . . . . . . . . . . . . . 18
β’
Ξ£π β
(1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) |
831 | 830 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
832 | 831 | oveq1d 7421 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = (Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
833 | | peano2zm 12602 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β€ β (π β 1) β
β€) |
834 | 796, 833 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (1...π)) β (π β 1) β β€) |
835 | 794, 834 | bccld 44012 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (1...π)) β (πC(π β 1)) β
β0) |
836 | 835 | nn0cnd 12531 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (1...π)) β (πC(π β 1)) β β) |
837 | 836 | adantll 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (πC(π β 1)) β β) |
838 | 837 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (πC(π β 1)) β β) |
839 | 838, 809 | mulcld 11231 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
840 | 777, 839,
810 | fsumadd 15683 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...π)(((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = (Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
841 | 840 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (1...π)(((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
842 | 836, 798 | addcomd 11413 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (1...π)) β ((πC(π β 1)) + (πCπ)) = ((πCπ) + (πC(π β 1)))) |
843 | | bcpasc 14278 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β0
β§ π β β€)
β ((πCπ) + (πC(π β 1))) = ((π + 1)Cπ)) |
844 | 794, 796,
843 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (1...π)) β ((πCπ) + (πC(π β 1))) = ((π + 1)Cπ)) |
845 | 842, 844 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (1...π)) β ((π + 1)Cπ) = ((πC(π β 1)) + (πCπ))) |
846 | 845 | oveq1d 7421 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...π)) β (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = (((πC(π β 1)) + (πCπ)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
847 | 846 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = (((πC(π β 1)) + (πCπ)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
848 | 847 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = (((πC(π β 1)) + (πCπ)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
849 | 838, 800,
809 | adddird 11236 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (((πC(π β 1)) + (πCπ)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = (((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
850 | 848, 849 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
851 | 850 | sumeq2dv 15646 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...π)(((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + ((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
852 | 832, 841,
851 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
853 | 852 | oveq2d 7422 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) + (Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) = (((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) + Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
854 | | peano2nn0 12509 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β0
β (π + 1) β
β0) |
855 | 794, 854 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (1...π)) β (π + 1) β
β0) |
856 | 855, 796 | bccld 44012 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (1...π)) β ((π + 1)Cπ) β
β0) |
857 | 856 | nn0cnd 12531 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β (0..^π) β§ π β (1...π)) β ((π + 1)Cπ) β β) |
858 | 857 | adantll 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β ((π + 1)Cπ) β β) |
859 | 858 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β ((π + 1)Cπ) β β) |
860 | 859, 809 | mulcld 11231 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (1...π)) β (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
861 | 777, 860 | fsumcl 15676 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
862 | 660, 726,
861 | addassd 11233 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) + Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = ((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))))) |
863 | 185, 854 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0..^π) β (π + 1) β
β0) |
864 | | bcn0 14267 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π + 1) β β0
β ((π + 1)C0) =
1) |
865 | 863, 864 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (0..^π) β ((π + 1)C0) = 1) |
866 | 865, 701 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (0..^π) β (((π + 1)C0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) = (1 Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)))) |
867 | 866 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((π + 1)C0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) = (1 Β· (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)))) |
868 | 867, 727 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) = (((π + 1)C0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯)))) |
869 | 771 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((0...π) β {0}) = (1...π)) |
870 | 869 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (1...π) = ((0...π) β {0})) |
871 | 870 | sumeq1d 15644 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β ((0...π) β {0})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
872 | 868, 871 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = ((((π + 1)C0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) + Ξ£π β ((0...π) β {0})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
873 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π((π + 1)C0) |
874 | 873, 455,
683 | nfov 7436 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π(((π + 1)C0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) |
875 | 197, 854 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...π)) β (π + 1) β
β0) |
876 | 875, 199 | bccld 44012 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (0...π)) β ((π + 1)Cπ) β
β0) |
877 | 876 | nn0cnd 12531 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...π)) β ((π + 1)Cπ) β β) |
878 | 877 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ π β (0...π)) β ((π + 1)Cπ) β β) |
879 | 878 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β ((π + 1)Cπ) β β) |
880 | 879, 436 | mulcld 11231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...π)) β (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
881 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = 0 β ((π + 1)Cπ) = ((π + 1)C0)) |
882 | 881, 695 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 0 β (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = (((π + 1)C0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯)))) |
883 | 472, 874,
439, 880, 689, 882 | fsumsplit1 15688 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = ((((π + 1)C0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) + Ξ£π β ((0...π) β {0})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
884 | 883 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((((π + 1)C0) Β· (((πΆβ0)βπ₯) Β· ((π·β((π + 1) β 0))βπ₯))) + Ξ£π β ((0...π) β {0})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (0...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
885 | 872, 884 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (0...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
886 | 885 | oveq2d 7422 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) = ((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + Ξ£π β (0...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
887 | | bcnn 14269 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π + 1) β β0
β ((π + 1)C(π + 1)) = 1) |
888 | 863, 887 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β ((π + 1)C(π + 1)) = 1) |
889 | 888 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((π + 1)C(π + 1)) = 1) |
890 | 889 | oveq1d 7421 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((π + 1)C(π + 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) = (1 Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯)))) |
891 | 623 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (0..^π)) β (π·β((π + 1) β (π + 1))) = (π·β0)) |
892 | 891 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0..^π)) β ((π·β((π + 1) β (π + 1))):πβΆβ β (π·β0):πβΆβ)) |
893 | 658, 892 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0..^π)) β (π·β((π + 1) β (π + 1))):πβΆβ) |
894 | 893 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (π·β((π + 1) β (π + 1))):πβΆβ) |
895 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β π₯ β π) |
896 | 894, 895 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((π·β((π + 1) β (π + 1)))βπ₯) β β) |
897 | 644, 896 | mulcld 11231 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯)) β β) |
898 | 897 | mullidd 11229 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (1 Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) = (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) |
899 | 625 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯)) = (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯))) |
900 | 890, 898,
899 | 3eqtrrd 2778 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) = (((π + 1)C(π + 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯)))) |
901 | | fzdifsuc 13558 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯β0) β (0...π) = ((0...(π + 1)) β {(π + 1)})) |
902 | 686, 901 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β (0...π) = ((0...(π + 1)) β {(π + 1)})) |
903 | 902 | sumeq1d 15644 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^π) β Ξ£π β (0...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β ((0...(π + 1)) β {(π + 1)})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
904 | 903 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = Ξ£π β ((0...(π + 1)) β {(π + 1)})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
905 | 900, 904 | oveq12d 7424 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + Ξ£π β (0...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = ((((π + 1)C(π + 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) + Ξ£π β ((0...(π + 1)) β {(π + 1)})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
906 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . 18
β’
β²π((π + 1)C(π + 1)) |
907 | 633, 458 | nffv 6899 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π((πΆβ(π + 1))βπ₯) |
908 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π((π + 1) β (π + 1)) |
909 | 461, 908 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π(π·β((π + 1) β (π + 1))) |
910 | 909, 458 | nffv 6899 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π((π·β((π + 1) β (π + 1)))βπ₯) |
911 | 907, 455,
910 | nfov 7436 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯)) |
912 | 906, 455,
911 | nfov 7436 |
. . . . . . . . . . . . . . . . 17
β’
β²π(((π + 1)C(π + 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) |
913 | | fzfid 13935 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (0...(π + 1)) β Fin) |
914 | 863 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (π + 1) β
β0) |
915 | | elfzelz 13498 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (0...(π + 1)) β π β β€) |
916 | 915 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β π β β€) |
917 | 914, 916 | bccld 44012 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β ((π + 1)Cπ) β
β0) |
918 | 917 | nn0cnd 12531 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β ((π + 1)Cπ) β β) |
919 | 918 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0..^π)) β§ π β (0...(π + 1))) β ((π + 1)Cπ) β β) |
920 | 919 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β ((π + 1)Cπ) β β) |
921 | 628 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ π β (0...(π + 1))) β π) |
922 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β 0 β
β€) |
923 | 206 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β π β β€) |
924 | | elfzle1 13501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0...(π + 1)) β 0 β€ π) |
925 | 924 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β 0 β€ π) |
926 | 916 | zred 12663 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β π β β) |
927 | 914 | nn0red 12530 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (π + 1) β β) |
928 | 211 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β π β β) |
929 | | elfzle2 13502 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (0...(π + 1)) β π β€ (π + 1)) |
930 | 929 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β π β€ (π + 1)) |
931 | 301 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (π + 1) β€ π) |
932 | 926, 927,
928, 930, 931 | letrd 11368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β π β€ π) |
933 | 922, 923,
916, 925, 932 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β π β (0...π)) |
934 | 933 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ π β (0...(π + 1))) β π β (0...π)) |
935 | 921, 934,
228 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ π β (0...(π + 1))) β (πΆβπ):πβΆβ) |
936 | 935 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β (πΆβπ):πβΆβ) |
937 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β π₯ β π) |
938 | 936, 937 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β ((πΆβπ)βπ₯) β β) |
939 | 921 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β π) |
940 | 591 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (π + 1) β β€) |
941 | 940, 916 | zsubcld 12668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β ((π + 1) β π) β β€) |
942 | 927, 926 | subge0d 11801 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (0 β€ ((π + 1) β π) β π β€ (π + 1))) |
943 | 930, 942 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β 0 β€ ((π + 1) β π)) |
944 | 927, 926 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β ((π + 1) β π) β β) |
945 | 928, 926 | resubcld 11639 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (π β π) β β) |
946 | 928, 171,
246 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (π β 0) β β) |
947 | 927, 928,
926, 931 | lesub1dd 11827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β ((π + 1) β π) β€ (π β π)) |
948 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β 0 β
β) |
949 | 948, 926,
928, 925 | lesub2dd 11828 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (π β π) β€ (π β 0)) |
950 | 944, 945,
946, 947, 949 | letrd 11368 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β ((π + 1) β π) β€ (π β 0)) |
951 | 252 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β (π β 0) = π) |
952 | 950, 951 | breqtrd 5174 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β ((π + 1) β π) β€ π) |
953 | 922, 923,
941, 943, 952 | elfzd 13489 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (0..^π) β§ π β (0...(π + 1))) β ((π + 1) β π) β (0...π)) |
954 | 953 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ π β (0...(π + 1))) β ((π + 1) β π) β (0...π)) |
955 | 954 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β ((π + 1) β π) β (0...π)) |
956 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((π + 1) β π) β (π·βπ) = (π·β((π + 1) β π))) |
957 | 956 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((π + 1) β π) β ((π·βπ):πβΆβ β (π·β((π + 1) β π)):πβΆβ)) |
958 | 310, 957 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = ((π + 1) β π) β (((π β§ π β (0...π)) β (π·βπ):πβΆβ) β ((π β§ ((π + 1) β π) β (0...π)) β (π·β((π + 1) β π)):πβΆβ))) |
959 | 461, 346 | nffv 6899 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
β²π(π·βπ) |
960 | 959, 348,
349 | nff 6711 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(π·βπ):πβΆβ |
961 | 343, 960 | nfim 1900 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π((π β§ π β (0...π)) β (π·βπ):πβΆβ) |
962 | | fveq2 6889 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (π·βπ) = (π·βπ)) |
963 | 962 | feq1d 6700 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β ((π·βπ):πβΆβ β (π·βπ):πβΆβ)) |
964 | 266, 963 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (((π β§ π β (0...π)) β (π·βπ):πβΆβ) β ((π β§ π β (0...π)) β (π·βπ):πβΆβ))) |
965 | 961, 964,
583 | chvarfv 2234 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (0...π)) β (π·βπ):πβΆβ) |
966 | 308, 958,
965 | vtocl 3550 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ ((π + 1) β π) β (0...π)) β (π·β((π + 1) β π)):πβΆβ) |
967 | 939, 955,
966 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β (π·β((π + 1) β π)):πβΆβ) |
968 | 967, 937 | ffvelcdmd 7085 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β ((π·β((π + 1) β π))βπ₯) β β) |
969 | 938, 968 | mulcld 11231 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) β β) |
970 | 920, 969 | mulcld 11231 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0..^π)) β§ π₯ β π) β§ π β (0...(π + 1))) β (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) β β) |
971 | 863, 685 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β (π + 1) β
(β€β₯β0)) |
972 | | eluzfz2 13506 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π + 1) β
(β€β₯β0) β (π + 1) β (0...(π + 1))) |
973 | 971, 972 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (0..^π) β (π + 1) β (0...(π + 1))) |
974 | 973 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (π + 1) β (0...(π + 1))) |
975 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β ((π + 1)Cπ) = ((π + 1)C(π + 1))) |
976 | 639 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β ((πΆβπ)βπ₯) = ((πΆβ(π + 1))βπ₯)) |
977 | | oveq2 7414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π + 1) β ((π + 1) β π) = ((π + 1) β (π + 1))) |
978 | 977 | fveq2d 6893 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π + 1) β (π·β((π + 1) β π)) = (π·β((π + 1) β (π + 1)))) |
979 | 978 | fveq1d 6891 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β ((π·β((π + 1) β π))βπ₯) = ((π·β((π + 1) β (π + 1)))βπ₯)) |
980 | 976, 979 | oveq12d 7424 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)) = (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) |
981 | 975, 980 | oveq12d 7424 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = (((π + 1)C(π + 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯)))) |
982 | 472, 912,
913, 970, 974, 981 | fsumsplit1 15688 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) = ((((π + 1)C(π + 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) + Ξ£π β ((0...(π + 1)) β {(π + 1)})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
983 | 982 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((((π + 1)C(π + 1)) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β((π + 1) β (π + 1)))βπ₯))) + Ξ£π β ((0...(π + 1)) β {(π + 1)})(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
984 | 886, 905,
983 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β ((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + ((((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯)) + Ξ£π β (1...π)(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) = Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
985 | 853, 862,
984 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (((((πΆβ(π + 1))βπ₯) Β· ((π·β0)βπ₯)) + (((πΆβ0)βπ₯) Β· ((π·β(π + 1))βπ₯))) + (Ξ£π β (1...π)((πC(π β 1)) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))) + Ξ£π β (1...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) = Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
986 | 776, 812,
985 | 3eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β (Ξ£π β (0...π)((πCπ) Β· (((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯))) + Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
987 | 438, 442,
986 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π₯ β π) β Ξ£π β (0...π)((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) = Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯)))) |
988 | 987 | mpteq2dva 5248 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· ((((πΆβ(π + 1))βπ₯) Β· ((π·β(π β π))βπ₯)) + (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
989 | 422, 988 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (π D (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
990 | 989 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β (π D (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
991 | 189, 191,
990 | 3eqtrd 2777 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1)) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
992 | 178, 179,
182, 991 | syl21anc 837 |
. . . . . 6
β’ ((π β (0..^π) β§ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β§ π) β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1)) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))) |
993 | 992 | 3exp 1120 |
. . . . 5
β’ (π β (0..^π) β ((π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))β(π + 1)) = (π₯ β π β¦ Ξ£π β (0...(π + 1))(((π + 1)Cπ) Β· (((πΆβπ)βπ₯) Β· ((π·β((π + 1) β π))βπ₯))))))) |
994 | 34, 47, 60, 73, 177, 993 | fzind2 13747 |
. . . 4
β’ (π β (0...π) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) |
995 | 21, 994 | vtoclg 3557 |
. . 3
β’ (π β β0
β (π β (0...π) β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))))) |
996 | 2, 6, 995 | sylc 65 |
. 2
β’ (π β (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯)))))) |
997 | 1, 996 | mpd 15 |
1
β’ (π β ((π Dπ (π₯ β π β¦ (π΄ Β· π΅)))βπ) = (π₯ β π β¦ Ξ£π β (0...π)((πCπ) Β· (((πΆβπ)βπ₯) Β· ((π·β(π β π))βπ₯))))) |