Step | Hyp | Ref
| Expression |
1 | | abelthlem6.1 |
. . . 4
β’ (π β π β (π β {1})) |
2 | 1 | eldifad 3960 |
. . 3
β’ (π β π β π) |
3 | | oveq1 7413 |
. . . . . 6
β’ (π₯ = π β (π₯βπ) = (πβπ)) |
4 | 3 | oveq2d 7422 |
. . . . 5
β’ (π₯ = π β ((π΄βπ) Β· (π₯βπ)) = ((π΄βπ) Β· (πβπ))) |
5 | 4 | sumeq2sdv 15647 |
. . . 4
β’ (π₯ = π β Ξ£π β β0 ((π΄βπ) Β· (π₯βπ)) = Ξ£π β β0 ((π΄βπ) Β· (πβπ))) |
6 | | abelth.6 |
. . . 4
β’ πΉ = (π₯ β π β¦ Ξ£π β β0 ((π΄βπ) Β· (π₯βπ))) |
7 | | sumex 15631 |
. . . 4
β’
Ξ£π β
β0 ((π΄βπ) Β· (πβπ)) β V |
8 | 5, 6, 7 | fvmpt 6996 |
. . 3
β’ (π β π β (πΉβπ) = Ξ£π β β0 ((π΄βπ) Β· (πβπ))) |
9 | 2, 8 | syl 17 |
. 2
β’ (π β (πΉβπ) = Ξ£π β β0 ((π΄βπ) Β· (πβπ))) |
10 | | nn0uz 12861 |
. . 3
β’
β0 = (β€β₯β0) |
11 | | 0zd 12567 |
. . 3
β’ (π β 0 β
β€) |
12 | | fveq2 6889 |
. . . . . 6
β’ (π = π β (π΄βπ) = (π΄βπ)) |
13 | | oveq2 7414 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
14 | 12, 13 | oveq12d 7424 |
. . . . 5
β’ (π = π β ((π΄βπ) Β· (πβπ)) = ((π΄βπ) Β· (πβπ))) |
15 | | eqid 2733 |
. . . . 5
β’ (π β β0
β¦ ((π΄βπ) Β· (πβπ))) = (π β β0 β¦ ((π΄βπ) Β· (πβπ))) |
16 | | ovex 7439 |
. . . . 5
β’ ((π΄βπ) Β· (πβπ)) β V |
17 | 14, 15, 16 | fvmpt 6996 |
. . . 4
β’ (π β β0
β ((π β
β0 β¦ ((π΄βπ) Β· (πβπ)))βπ) = ((π΄βπ) Β· (πβπ))) |
18 | 17 | adantl 483 |
. . 3
β’ ((π β§ π β β0) β ((π β β0
β¦ ((π΄βπ) Β· (πβπ)))βπ) = ((π΄βπ) Β· (πβπ))) |
19 | | abelth.1 |
. . . . 5
β’ (π β π΄:β0βΆβ) |
20 | 19 | ffvelcdmda 7084 |
. . . 4
β’ ((π β§ π β β0) β (π΄βπ) β β) |
21 | | abelth.5 |
. . . . . . 7
β’ π = {π§ β β β£ (absβ(1 β
π§)) β€ (π Β· (1 β (absβπ§)))} |
22 | 21 | ssrab3 4080 |
. . . . . 6
β’ π β
β |
23 | 22, 2 | sselid 3980 |
. . . . 5
β’ (π β π β β) |
24 | | expcl 14042 |
. . . . 5
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
25 | 23, 24 | sylan 581 |
. . . 4
β’ ((π β§ π β β0) β (πβπ) β β) |
26 | 20, 25 | mulcld 11231 |
. . 3
β’ ((π β§ π β β0) β ((π΄βπ) Β· (πβπ)) β β) |
27 | | fveq2 6889 |
. . . . . . . . 9
β’ (π = π β (seq0( + , π΄)βπ) = (seq0( + , π΄)βπ)) |
28 | 27, 13 | oveq12d 7424 |
. . . . . . . 8
β’ (π = π β ((seq0( + , π΄)βπ) Β· (πβπ)) = ((seq0( + , π΄)βπ) Β· (πβπ))) |
29 | | eqid 2733 |
. . . . . . . 8
β’ (π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ))) = (π β β0 β¦ ((seq0( +
, π΄)βπ) Β· (πβπ))) |
30 | | ovex 7439 |
. . . . . . . 8
β’ ((seq0( +
, π΄)βπ) Β· (πβπ)) β V |
31 | 28, 29, 30 | fvmpt 6996 |
. . . . . . 7
β’ (π β β0
β ((π β
β0 β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))βπ) = ((seq0( + , π΄)βπ) Β· (πβπ))) |
32 | 31 | adantl 483 |
. . . . . 6
β’ ((π β§ π β β0) β ((π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))βπ) = ((seq0( + , π΄)βπ) Β· (πβπ))) |
33 | 10, 11, 20 | serf 13993 |
. . . . . . . 8
β’ (π β seq0( + , π΄):β0βΆβ) |
34 | 33 | ffvelcdmda 7084 |
. . . . . . 7
β’ ((π β§ π β β0) β (seq0( +
, π΄)βπ) β
β) |
35 | 34, 25 | mulcld 11231 |
. . . . . 6
β’ ((π β§ π β β0) β ((seq0( +
, π΄)βπ) Β· (πβπ)) β β) |
36 | | abelth.2 |
. . . . . . . . . 10
β’ (π β seq0( + , π΄) β dom β
) |
37 | | abelth.3 |
. . . . . . . . . 10
β’ (π β π β β) |
38 | | abelth.4 |
. . . . . . . . . 10
β’ (π β 0 β€ π) |
39 | 19, 36, 37, 38, 21 | abelthlem2 25936 |
. . . . . . . . 9
β’ (π β (1 β π β§ (π β {1}) β (0(ballβ(abs
β β ))1))) |
40 | 39 | simprd 497 |
. . . . . . . 8
β’ (π β (π β {1}) β (0(ballβ(abs
β β ))1)) |
41 | 40, 1 | sseldd 3983 |
. . . . . . 7
β’ (π β π β (0(ballβ(abs β β
))1)) |
42 | | abelth.7 |
. . . . . . . 8
β’ (π β seq0( + , π΄) β 0) |
43 | 19, 36, 37, 38, 21, 6, 42 | abelthlem5 25939 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β seq0( + , (π
β β0 β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))) β dom β ) |
44 | 41, 43 | mpdan 686 |
. . . . . 6
β’ (π β seq0( + , (π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))) β dom β ) |
45 | 10, 11, 32, 35, 44 | isumclim2 15701 |
. . . . 5
β’ (π β seq0( + , (π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))) β Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) |
46 | | seqex 13965 |
. . . . . 6
β’ seq0( + ,
(π β
β0 β¦ ((π΄βπ) Β· (πβπ)))) β V |
47 | 46 | a1i 11 |
. . . . 5
β’ (π β seq0( + , (π β β0
β¦ ((π΄βπ) Β· (πβπ)))) β V) |
48 | | 0nn0 12484 |
. . . . . . . 8
β’ 0 β
β0 |
49 | 48 | a1i 11 |
. . . . . . 7
β’ (π β 0 β
β0) |
50 | | oveq1 7413 |
. . . . . . . . . . . . 13
β’ (π = π β (π β 1) = (π β 1)) |
51 | 50 | oveq2d 7422 |
. . . . . . . . . . . 12
β’ (π = π β (0...(π β 1)) = (0...(π β 1))) |
52 | 51 | sumeq1d 15644 |
. . . . . . . . . . 11
β’ (π = π β Ξ£π β (0...(π β 1))(π΄βπ) = Ξ£π β (0...(π β 1))(π΄βπ)) |
53 | | oveq2 7414 |
. . . . . . . . . . 11
β’ (π = π β (πβπ) = (πβπ)) |
54 | 52, 53 | oveq12d 7424 |
. . . . . . . . . 10
β’ (π = π β (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)) = (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))) |
55 | | eqid 2733 |
. . . . . . . . . 10
β’ (π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))) = (π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))) |
56 | | ovex 7439 |
. . . . . . . . . 10
β’
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)) β V |
57 | 54, 55, 56 | fvmpt 6996 |
. . . . . . . . 9
β’ (π β β0
β ((π β
β0 β¦ (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) = (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))) |
58 | 57 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) = (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))) |
59 | | fzfid 13935 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β
(0...(π β 1)) β
Fin) |
60 | 19 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π΄:β0βΆβ) |
61 | | elfznn0 13591 |
. . . . . . . . . . 11
β’ (π β (0...(π β 1)) β π β β0) |
62 | | ffvelcdm 7081 |
. . . . . . . . . . 11
β’ ((π΄:β0βΆβ β§
π β
β0) β (π΄βπ) β β) |
63 | 60, 61, 62 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β (0...(π β 1))) β (π΄βπ) β β) |
64 | 59, 63 | fsumcl 15676 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
Ξ£π β (0...(π β 1))(π΄βπ) β β) |
65 | | expcl 14042 |
. . . . . . . . . 10
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
66 | 23, 65 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (πβπ) β β) |
67 | 64, 66 | mulcld 11231 |
. . . . . . . 8
β’ ((π β§ π β β0) β
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)) β β) |
68 | 58, 67 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) β β) |
69 | 11 | peano2zd 12666 |
. . . . . . . . 9
β’ (π β (0 + 1) β
β€) |
70 | | nnuz 12862 |
. . . . . . . . . . . 12
β’ β =
(β€β₯β1) |
71 | | 1e0p1 12716 |
. . . . . . . . . . . . 13
β’ 1 = (0 +
1) |
72 | 71 | fveq2i 6892 |
. . . . . . . . . . . 12
β’
(β€β₯β1) = (β€β₯β(0 +
1)) |
73 | 70, 72 | eqtri 2761 |
. . . . . . . . . . 11
β’ β =
(β€β₯β(0 + 1)) |
74 | 73 | eleq2i 2826 |
. . . . . . . . . 10
β’ (π β β β π β
(β€β₯β(0 + 1))) |
75 | | nnm1nn0 12510 |
. . . . . . . . . . . . 13
β’ (π β β β (π β 1) β
β0) |
76 | 75 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π β 1) β
β0) |
77 | | fveq2 6889 |
. . . . . . . . . . . . . . 15
β’ (π = (π β 1) β (seq0( + , π΄)βπ) = (seq0( + , π΄)β(π β 1))) |
78 | | oveq2 7414 |
. . . . . . . . . . . . . . 15
β’ (π = (π β 1) β (πβπ) = (πβ(π β 1))) |
79 | 77, 78 | oveq12d 7424 |
. . . . . . . . . . . . . 14
β’ (π = (π β 1) β ((seq0( + , π΄)βπ) Β· (πβπ)) = ((seq0( + , π΄)β(π β 1)) Β· (πβ(π β 1)))) |
80 | 79 | oveq2d 7422 |
. . . . . . . . . . . . 13
β’ (π = (π β 1) β (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))) = (π Β· ((seq0( + , π΄)β(π β 1)) Β· (πβ(π β 1))))) |
81 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ)))) = (π β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) |
82 | | ovex 7439 |
. . . . . . . . . . . . 13
β’ (π Β· ((seq0( + , π΄)β(π β 1)) Β· (πβ(π β 1)))) β V |
83 | 80, 81, 82 | fvmpt 6996 |
. . . . . . . . . . . 12
β’ ((π β 1) β
β0 β ((π β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))))β(π β 1)) = (π Β· ((seq0( + , π΄)β(π β 1)) Β· (πβ(π β 1))))) |
84 | 76, 83 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))))β(π β 1)) = (π Β· ((seq0( + , π΄)β(π β 1)) Β· (πβ(π β 1))))) |
85 | | ax-1cn 11165 |
. . . . . . . . . . . 12
β’ 1 β
β |
86 | | nncn 12217 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
87 | 86 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
88 | | nn0ex 12475 |
. . . . . . . . . . . . . 14
β’
β0 β V |
89 | 88 | mptex 7222 |
. . . . . . . . . . . . 13
β’ (π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ)))) β V |
90 | 89 | shftval 15018 |
. . . . . . . . . . . 12
β’ ((1
β β β§ π
β β) β (((π
β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) shift 1)βπ) = ((π β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))))β(π β 1))) |
91 | 85, 87, 90 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((π β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) shift 1)βπ) = ((π β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))))β(π β 1))) |
92 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (0...(π β 1))) β (π΄βπ) = (π΄βπ)) |
93 | 76, 10 | eleqtrdi 2844 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π β 1) β
(β€β₯β0)) |
94 | 19 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π΄:β0βΆβ) |
95 | | elfznn0 13591 |
. . . . . . . . . . . . . . 15
β’ (π β (0...(π β 1)) β π β β0) |
96 | 94, 95, 62 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (0...(π β 1))) β (π΄βπ) β β) |
97 | 92, 93, 96 | fsumser 15673 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β Ξ£π β (0...(π β 1))(π΄βπ) = (seq0( + , π΄)β(π β 1))) |
98 | | expm1t 14053 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β (πβπ) = ((πβ(π β 1)) Β· π)) |
99 | 23, 98 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβπ) = ((πβ(π β 1)) Β· π)) |
100 | 23 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β) |
101 | | expcl 14042 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π β 1) β
β0) β (πβ(π β 1)) β β) |
102 | 23, 75, 101 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πβ(π β 1)) β β) |
103 | 100, 102 | mulcomd 11232 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (π Β· (πβ(π β 1))) = ((πβ(π β 1)) Β· π)) |
104 | 99, 103 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβπ) = (π Β· (πβ(π β 1)))) |
105 | 97, 104 | oveq12d 7424 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)) = ((seq0( + , π΄)β(π β 1)) Β· (π Β· (πβ(π β 1))))) |
106 | | nnnn0 12476 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β0) |
107 | 106 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β0) |
108 | | oveq1 7413 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (π β 1) = (π β 1)) |
109 | 108 | oveq2d 7422 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (0...(π β 1)) = (0...(π β 1))) |
110 | 109 | sumeq1d 15644 |
. . . . . . . . . . . . . . 15
β’ (π = π β Ξ£π β (0...(π β 1))(π΄βπ) = Ξ£π β (0...(π β 1))(π΄βπ)) |
111 | 110, 13 | oveq12d 7424 |
. . . . . . . . . . . . . 14
β’ (π = π β (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)) = (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))) |
112 | | ovex 7439 |
. . . . . . . . . . . . . 14
β’
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)) β V |
113 | 111, 55, 112 | fvmpt 6996 |
. . . . . . . . . . . . 13
β’ (π β β0
β ((π β
β0 β¦ (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) = (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))) |
114 | 107, 113 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) = (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))) |
115 | | ffvelcdm 7081 |
. . . . . . . . . . . . . 14
β’ ((seq0( +
, π΄):β0βΆβ β§
(π β 1) β
β0) β (seq0( + , π΄)β(π β 1)) β β) |
116 | 33, 75, 115 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (seq0( + , π΄)β(π β 1)) β β) |
117 | 100, 116,
102 | mul12d 11420 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π Β· ((seq0( + , π΄)β(π β 1)) Β· (πβ(π β 1)))) = ((seq0( + , π΄)β(π β 1)) Β· (π Β· (πβ(π β 1))))) |
118 | 105, 114,
117 | 3eqtr4d 2783 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) = (π Β· ((seq0( + , π΄)β(π β 1)) Β· (πβ(π β 1))))) |
119 | 84, 91, 118 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (((π β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) shift 1)βπ) = ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ)) |
120 | 74, 119 | sylan2br 596 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯β(0 +
1))) β (((π β
β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) shift 1)βπ) = ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ)) |
121 | 69, 120 | seqfeq 13990 |
. . . . . . . 8
β’ (π β seq(0 + 1)( + , ((π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ)))) shift 1)) = seq(0 + 1)( + , (π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))))) |
122 | | fveq2 6889 |
. . . . . . . . . . . . . 14
β’ (π = π β (seq0( + , π΄)βπ) = (seq0( + , π΄)βπ)) |
123 | 122, 53 | oveq12d 7424 |
. . . . . . . . . . . . 13
β’ (π = π β ((seq0( + , π΄)βπ) Β· (πβπ)) = ((seq0( + , π΄)βπ) Β· (πβπ))) |
124 | | ovex 7439 |
. . . . . . . . . . . . 13
β’ ((seq0( +
, π΄)βπ) Β· (πβπ)) β V |
125 | 123, 29, 124 | fvmpt 6996 |
. . . . . . . . . . . 12
β’ (π β β0
β ((π β
β0 β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))βπ) = ((seq0( + , π΄)βπ) Β· (πβπ))) |
126 | 125 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))βπ) = ((seq0( + , π΄)βπ) Β· (πβπ))) |
127 | 33 | ffvelcdmda 7084 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (seq0( +
, π΄)βπ) β
β) |
128 | 127, 66 | mulcld 11231 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((seq0( +
, π΄)βπ) Β· (πβπ)) β β) |
129 | 126, 128 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))βπ) β β) |
130 | 123 | oveq2d 7422 |
. . . . . . . . . . . . 13
β’ (π = π β (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))) = (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) |
131 | | ovex 7439 |
. . . . . . . . . . . . 13
β’ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))) β V |
132 | 130, 81, 131 | fvmpt 6996 |
. . . . . . . . . . . 12
β’ (π β β0
β ((π β
β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))))βπ) = (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) |
133 | 132 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ))))βπ) = (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) |
134 | 126 | oveq2d 7422 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β (π Β· ((π β β0 β¦ ((seq0( +
, π΄)βπ) Β· (πβπ)))βπ)) = (π Β· ((seq0( + , π΄)βπ) Β· (πβπ)))) |
135 | 133, 134 | eqtr4d 2776 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β ((π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ))))βπ) = (π Β· ((π β β0 β¦ ((seq0( +
, π΄)βπ) Β· (πβπ)))βπ))) |
136 | 10, 11, 23, 45, 129, 135 | isermulc2 15601 |
. . . . . . . . 9
β’ (π β seq0( + , (π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ))))) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
137 | | 0z 12566 |
. . . . . . . . . 10
β’ 0 β
β€ |
138 | | 1z 12589 |
. . . . . . . . . 10
β’ 1 β
β€ |
139 | 89 | isershft 15607 |
. . . . . . . . . 10
β’ ((0
β β€ β§ 1 β β€) β (seq0( + , (π β β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))))) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) β seq(0 + 1)( + , ((π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ)))) shift 1)) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))))) |
140 | 137, 138,
139 | mp2an 691 |
. . . . . . . . 9
β’ (seq0( +
, (π β
β0 β¦ (π Β· ((seq0( + , π΄)βπ) Β· (πβπ))))) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) β seq(0 + 1)( + , ((π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ)))) shift 1)) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
141 | 136, 140 | sylib 217 |
. . . . . . . 8
β’ (π β seq(0 + 1)( + , ((π β β0
β¦ (π Β· ((seq0(
+ , π΄)βπ) Β· (πβπ)))) shift 1)) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
142 | 121, 141 | eqbrtrrd 5172 |
. . . . . . 7
β’ (π β seq(0 + 1)( + , (π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
143 | 10, 49, 68, 142 | clim2ser2 15599 |
. . . . . 6
β’ (π β seq0( + , (π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))) β ((π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) + (seq0( + , (π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))))β0))) |
144 | | seq1 13976 |
. . . . . . . . . . 11
β’ (0 β
β€ β (seq0( + , (π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))))β0) = ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))β0)) |
145 | 137, 144 | ax-mp 5 |
. . . . . . . . . 10
β’ (seq0( +
, (π β
β0 β¦ (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))))β0) = ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))β0) |
146 | | oveq1 7413 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β (π β 1) = (0 β 1)) |
147 | 146 | oveq2d 7422 |
. . . . . . . . . . . . . . . 16
β’ (π = 0 β (0...(π β 1)) = (0...(0 β
1))) |
148 | | risefall0lem 15967 |
. . . . . . . . . . . . . . . 16
β’ (0...(0
β 1)) = β
|
149 | 147, 148 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’ (π = 0 β (0...(π β 1)) =
β
) |
150 | 149 | sumeq1d 15644 |
. . . . . . . . . . . . . 14
β’ (π = 0 β Ξ£π β (0...(π β 1))(π΄βπ) = Ξ£π β β
(π΄βπ)) |
151 | | sum0 15664 |
. . . . . . . . . . . . . 14
β’
Ξ£π β
β
(π΄βπ) = 0 |
152 | 150, 151 | eqtrdi 2789 |
. . . . . . . . . . . . 13
β’ (π = 0 β Ξ£π β (0...(π β 1))(π΄βπ) = 0) |
153 | | oveq2 7414 |
. . . . . . . . . . . . 13
β’ (π = 0 β (πβπ) = (πβ0)) |
154 | 152, 153 | oveq12d 7424 |
. . . . . . . . . . . 12
β’ (π = 0 β (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)) = (0 Β· (πβ0))) |
155 | | ovex 7439 |
. . . . . . . . . . . 12
β’ (0
Β· (πβ0)) β
V |
156 | 154, 55, 155 | fvmpt 6996 |
. . . . . . . . . . 11
β’ (0 β
β0 β ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))β0) = (0 Β· (πβ0))) |
157 | 48, 156 | ax-mp 5 |
. . . . . . . . . 10
β’ ((π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))β0) = (0 Β· (πβ0)) |
158 | 145, 157 | eqtri 2761 |
. . . . . . . . 9
β’ (seq0( +
, (π β
β0 β¦ (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))))β0) = (0 Β· (πβ0)) |
159 | | expcl 14042 |
. . . . . . . . . . 11
β’ ((π β β β§ 0 β
β0) β (πβ0) β β) |
160 | 23, 48, 159 | sylancl 587 |
. . . . . . . . . 10
β’ (π β (πβ0) β β) |
161 | 160 | mul02d 11409 |
. . . . . . . . 9
β’ (π β (0 Β· (πβ0)) = 0) |
162 | 158, 161 | eqtrid 2785 |
. . . . . . . 8
β’ (π β (seq0( + , (π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))))β0) = 0) |
163 | 162 | oveq2d 7422 |
. . . . . . 7
β’ (π β ((π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) + (seq0( + , (π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))))β0)) = ((π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) + 0)) |
164 | 10, 11, 32, 35, 44 | isumcl 15704 |
. . . . . . . . 9
β’ (π β Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)) β β) |
165 | 23, 164 | mulcld 11231 |
. . . . . . . 8
β’ (π β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) β β) |
166 | 165 | addridd 11411 |
. . . . . . 7
β’ (π β ((π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) + 0) = (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
167 | 163, 166 | eqtrd 2773 |
. . . . . 6
β’ (π β ((π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) + (seq0( + , (π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))))β0)) = (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
168 | 143, 167 | breqtrd 5174 |
. . . . 5
β’ (π β seq0( + , (π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
169 | 10, 11, 129 | serf 13993 |
. . . . . 6
β’ (π β seq0( + , (π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))):β0βΆβ) |
170 | 169 | ffvelcdmda 7084 |
. . . . 5
β’ ((π β§ π β β0) β (seq0( +
, (π β
β0 β¦ ((seq0( + , π΄)βπ) Β· (πβπ))))βπ) β β) |
171 | 10, 11, 68 | serf 13993 |
. . . . . 6
β’ (π β seq0( + , (π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))):β0βΆβ) |
172 | 171 | ffvelcdmda 7084 |
. . . . 5
β’ ((π β§ π β β0) β (seq0( +
, (π β
β0 β¦ (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))))βπ) β β) |
173 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β β0) β π β
β0) |
174 | 173, 10 | eleqtrdi 2844 |
. . . . . 6
β’ ((π β§ π β β0) β π β
(β€β₯β0)) |
175 | | simpl 484 |
. . . . . . 7
β’ ((π β§ π β β0) β π) |
176 | | elfznn0 13591 |
. . . . . . 7
β’ (π β (0...π) β π β β0) |
177 | 32, 35 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))βπ) β β) |
178 | 175, 176,
177 | syl2an 597 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β (0...π)) β ((π β β0 β¦ ((seq0( +
, π΄)βπ) Β· (πβπ)))βπ) β β) |
179 | 113 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) = (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ))) |
180 | | fzfid 13935 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β
(0...(π β 1)) β
Fin) |
181 | 19 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β π΄:β0βΆβ) |
182 | 181, 95, 62 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β (0...(π β 1))) β (π΄βπ) β β) |
183 | 180, 182 | fsumcl 15676 |
. . . . . . . . 9
β’ ((π β§ π β β0) β
Ξ£π β (0...(π β 1))(π΄βπ) β β) |
184 | 183, 25 | mulcld 11231 |
. . . . . . . 8
β’ ((π β§ π β β0) β
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)) β β) |
185 | 179, 184 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π β β0
β¦ (Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) β β) |
186 | 175, 176,
185 | syl2an 597 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β (0...π)) β ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ) β β) |
187 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β (π΄βπ) = (π΄βπ)) |
188 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β π β
β0) |
189 | 188, 10 | eleqtrdi 2844 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β π β
(β€β₯β0)) |
190 | | elfznn0 13591 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β π β β0) |
191 | 181, 190,
62 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ π β (0...π)) β (π΄βπ) β β) |
192 | 187, 189,
191 | fsumser 15673 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β
Ξ£π β (0...π)(π΄βπ) = (seq0( + , π΄)βπ)) |
193 | | fveq2 6889 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ) = (π΄βπ)) |
194 | 189, 191,
193 | fsumm1 15694 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β
Ξ£π β (0...π)(π΄βπ) = (Ξ£π β (0...(π β 1))(π΄βπ) + (π΄βπ))) |
195 | 192, 194 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ ((π β§ π β β0) β (seq0( +
, π΄)βπ) = (Ξ£π β (0...(π β 1))(π΄βπ) + (π΄βπ))) |
196 | 195 | oveq1d 7421 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β ((seq0( +
, π΄)βπ) β Ξ£π β (0...(π β 1))(π΄βπ)) = ((Ξ£π β (0...(π β 1))(π΄βπ) + (π΄βπ)) β Ξ£π β (0...(π β 1))(π΄βπ))) |
197 | 183, 20 | pncan2d 11570 |
. . . . . . . . . . 11
β’ ((π β§ π β β0) β
((Ξ£π β
(0...(π β 1))(π΄βπ) + (π΄βπ)) β Ξ£π β (0...(π β 1))(π΄βπ)) = (π΄βπ)) |
198 | 196, 197 | eqtr2d 2774 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β (π΄βπ) = ((seq0( + , π΄)βπ) β Ξ£π β (0...(π β 1))(π΄βπ))) |
199 | 198 | oveq1d 7421 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((π΄βπ) Β· (πβπ)) = (((seq0( + , π΄)βπ) β Ξ£π β (0...(π β 1))(π΄βπ)) Β· (πβπ))) |
200 | 34, 183, 25 | subdird 11668 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (((seq0(
+ , π΄)βπ) β Ξ£π β (0...(π β 1))(π΄βπ)) Β· (πβπ)) = (((seq0( + , π΄)βπ) Β· (πβπ)) β (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)))) |
201 | 199, 200 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π΄βπ) Β· (πβπ)) = (((seq0( + , π΄)βπ) Β· (πβπ)) β (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)))) |
202 | 32, 179 | oveq12d 7424 |
. . . . . . . 8
β’ ((π β§ π β β0) β (((π β β0
β¦ ((seq0( + , π΄)βπ) Β· (πβπ)))βπ) β ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ)) = (((seq0( + , π΄)βπ) Β· (πβπ)) β (Ξ£π β (0...(π β 1))(π΄βπ) Β· (πβπ)))) |
203 | 201, 18, 202 | 3eqtr4d 2783 |
. . . . . . 7
β’ ((π β§ π β β0) β ((π β β0
β¦ ((π΄βπ) Β· (πβπ)))βπ) = (((π β β0 β¦ ((seq0( +
, π΄)βπ) Β· (πβπ)))βπ) β ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ))) |
204 | 175, 176,
203 | syl2an 597 |
. . . . . 6
β’ (((π β§ π β β0) β§ π β (0...π)) β ((π β β0 β¦ ((π΄βπ) Β· (πβπ)))βπ) = (((π β β0 β¦ ((seq0( +
, π΄)βπ) Β· (πβπ)))βπ) β ((π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ)))βπ))) |
205 | 174, 178,
186, 204 | sersub 14008 |
. . . . 5
β’ ((π β§ π β β0) β (seq0( +
, (π β
β0 β¦ ((π΄βπ) Β· (πβπ))))βπ) = ((seq0( + , (π β β0 β¦ ((seq0( +
, π΄)βπ) Β· (πβπ))))βπ) β (seq0( + , (π β β0 β¦
(Ξ£π β
(0...(π β 1))(π΄βπ) Β· (πβπ))))βπ))) |
206 | 10, 11, 45, 47, 168, 170, 172, 205 | climsub 15575 |
. . . 4
β’ (π β seq0( + , (π β β0
β¦ ((π΄βπ) Β· (πβπ)))) β (Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))))) |
207 | | 1cnd 11206 |
. . . . . 6
β’ (π β 1 β
β) |
208 | 207, 23, 164 | subdird 11668 |
. . . . 5
β’ (π β ((1 β π) Β· Ξ£π β β0
((seq0( + , π΄)βπ) Β· (πβπ))) = ((1 Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))))) |
209 | 164 | mullidd 11229 |
. . . . . 6
β’ (π β (1 Β· Ξ£π β β0
((seq0( + , π΄)βπ) Β· (πβπ))) = Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))) |
210 | 209 | oveq1d 7421 |
. . . . 5
β’ (π β ((1 Β· Ξ£π β β0
((seq0( + , π΄)βπ) Β· (πβπ))) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) = (Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))))) |
211 | 208, 210 | eqtrd 2773 |
. . . 4
β’ (π β ((1 β π) Β· Ξ£π β β0
((seq0( + , π΄)βπ) Β· (πβπ))) = (Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)) β (π Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ))))) |
212 | 206, 211 | breqtrrd 5176 |
. . 3
β’ (π β seq0( + , (π β β0
β¦ ((π΄βπ) Β· (πβπ)))) β ((1 β π) Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
213 | 10, 11, 18, 26, 212 | isumclim 15700 |
. 2
β’ (π β Ξ£π β β0 ((π΄βπ) Β· (πβπ)) = ((1 β π) Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |
214 | 9, 213 | eqtrd 2773 |
1
β’ (π β (πΉβπ) = ((1 β π) Β· Ξ£π β β0 ((seq0( + , π΄)βπ) Β· (πβπ)))) |