Step | Hyp | Ref
| Expression |
1 | | isumshft.5 |
. . . . . . . . 9
β’ (π β π β β€) |
2 | | isumshft.4 |
. . . . . . . . 9
β’ (π β πΎ β β€) |
3 | 1, 2 | zaddcld 9379 |
. . . . . . . 8
β’ (π β (π + πΎ) β β€) |
4 | | isumshft.2 |
. . . . . . . . . . . . 13
β’ π =
(β€β₯β(π + πΎ)) |
5 | 4 | eleq2i 2244 |
. . . . . . . . . . . 12
β’ (π₯ β π β π₯ β (β€β₯β(π + πΎ))) |
6 | 5 | biimpri 133 |
. . . . . . . . . . 11
β’ (π₯ β
(β€β₯β(π + πΎ)) β π₯ β π) |
7 | 6 | adantl 277 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (β€β₯β(π + πΎ))) β π₯ β π) |
8 | | isumshft.6 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π΄ β β) |
9 | 8 | ralrimiva 2550 |
. . . . . . . . . . . 12
β’ (π β βπ β π π΄ β β) |
10 | 9 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (β€β₯β(π + πΎ))) β βπ β π π΄ β β) |
11 | | nfcsb1v 3091 |
. . . . . . . . . . . . 13
β’
β²πβ¦π₯ / πβ¦π΄ |
12 | 11 | nfel1 2330 |
. . . . . . . . . . . 12
β’
β²πβ¦π₯ / πβ¦π΄ β β |
13 | | csbeq1a 3067 |
. . . . . . . . . . . . 13
β’ (π = π₯ β π΄ = β¦π₯ / πβ¦π΄) |
14 | 13 | eleq1d 2246 |
. . . . . . . . . . . 12
β’ (π = π₯ β (π΄ β β β β¦π₯ / πβ¦π΄ β β)) |
15 | 12, 14 | rspc 2836 |
. . . . . . . . . . 11
β’ (π₯ β π β (βπ β π π΄ β β β β¦π₯ / πβ¦π΄ β β)) |
16 | 7, 10, 15 | sylc 62 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (β€β₯β(π + πΎ))) β β¦π₯ / πβ¦π΄ β β) |
17 | | eqid 2177 |
. . . . . . . . . . 11
β’ (π β π β¦ π΄) = (π β π β¦ π΄) |
18 | 17 | fvmpts 5595 |
. . . . . . . . . 10
β’ ((π₯ β π β§ β¦π₯ / πβ¦π΄ β β) β ((π β π β¦ π΄)βπ₯) = β¦π₯ / πβ¦π΄) |
19 | 7, 16, 18 | syl2anc 411 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β€β₯β(π + πΎ))) β ((π β π β¦ π΄)βπ₯) = β¦π₯ / πβ¦π΄) |
20 | 19, 16 | eqeltrd 2254 |
. . . . . . . 8
β’ ((π β§ π₯ β (β€β₯β(π + πΎ))) β ((π β π β¦ π΄)βπ₯) β β) |
21 | 4 | eleq2i 2244 |
. . . . . . . . 9
β’ (π β π β π β (β€β₯β(π + πΎ))) |
22 | 2 | zcnd 9376 |
. . . . . . . . . . 11
β’ (π β πΎ β β) |
23 | | eluzelcn 9539 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β(π + πΎ)) β π β β) |
24 | 23, 4 | eleq2s 2272 |
. . . . . . . . . . 11
β’ (π β π β π β β) |
25 | | zex 9262 |
. . . . . . . . . . . . . 14
β’ β€
β V |
26 | | isumshft.1 |
. . . . . . . . . . . . . . 15
β’ π =
(β€β₯βπ) |
27 | | uzssz 9547 |
. . . . . . . . . . . . . . 15
β’
(β€β₯βπ) β β€ |
28 | 26, 27 | eqsstri 3188 |
. . . . . . . . . . . . . 14
β’ π β
β€ |
29 | 25, 28 | ssexi 4142 |
. . . . . . . . . . . . 13
β’ π β V |
30 | 29 | mptex 5743 |
. . . . . . . . . . . 12
β’ (π β π β¦ π΅) β V |
31 | 30 | shftval 10834 |
. . . . . . . . . . 11
β’ ((πΎ β β β§ π β β) β (((π β π β¦ π΅) shift πΎ)βπ) = ((π β π β¦ π΅)β(π β πΎ))) |
32 | 22, 24, 31 | syl2an 289 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (((π β π β¦ π΅) shift πΎ)βπ) = ((π β π β¦ π΅)β(π β πΎ))) |
33 | | eqidd 2178 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β π β¦ π΅) = (π β π β¦ π΅)) |
34 | | isumshft.3 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πΎ + π) β π΄ = π΅) |
35 | 34 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πΎ + π) β (π΄ β β β π΅ β β)) |
36 | 9 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β βπ β π π΄ β β) |
37 | 1 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β π β β€) |
38 | 2 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β πΎ β β€) |
39 | 37, 38 | zaddcld 9379 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β (π + πΎ) β β€) |
40 | | eluzelz 9537 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯βπ) β π β β€) |
41 | 40, 26 | eleq2s 2272 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β π β β€) |
42 | 41 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β π β β€) |
43 | 38, 42 | zaddcld 9379 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β (πΎ + π) β β€) |
44 | 37 | zred 9375 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π) β π β β) |
45 | 42 | zred 9375 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π) β π β β) |
46 | 38 | zred 9375 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π) β πΎ β β) |
47 | 26 | eleq2i 2244 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β π β (β€β₯βπ)) |
48 | 47 | biimpi 120 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β π β (β€β₯βπ)) |
49 | 48 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
50 | | eluzle 9540 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β
(β€β₯βπ) β π β€ π) |
51 | 49, 50 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π) β π β€ π) |
52 | 44, 45, 46, 51 | leadd1dd 8516 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β (π + πΎ) β€ (π + πΎ)) |
53 | 42 | zcnd 9376 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π) β π β β) |
54 | 38 | zcnd 9376 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π) β πΎ β β) |
55 | 53, 54 | addcomd 8108 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β (π + πΎ) = (πΎ + π)) |
56 | 52, 55 | breqtrd 4030 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β (π + πΎ) β€ (πΎ + π)) |
57 | | eluz2 9534 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΎ + π) β (β€β₯β(π + πΎ)) β ((π + πΎ) β β€ β§ (πΎ + π) β β€ β§ (π + πΎ) β€ (πΎ + π))) |
58 | 39, 43, 56, 57 | syl3anbrc 1181 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β (πΎ + π) β (β€β₯β(π + πΎ))) |
59 | 58, 4 | eleqtrrdi 2271 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β (πΎ + π) β π) |
60 | 35, 36, 59 | rspcdva 2847 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β π΅ β β) |
61 | 33, 60 | fvmpt2d 5603 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = π΅) |
62 | | eqidd 2178 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (π β π β¦ π΄) = (π β π β¦ π΄)) |
63 | 34 | adantl 277 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β π) β§ π = (πΎ + π)) β π΄ = π΅) |
64 | 62, 63, 59, 60 | fvmptd 5598 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β ((π β π β¦ π΄)β(πΎ + π)) = π΅) |
65 | 61, 64 | eqtr4d 2213 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
66 | 65 | ralrimiva 2550 |
. . . . . . . . . . . . . 14
β’ (π β βπ β π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
67 | | nffvmpt1 5527 |
. . . . . . . . . . . . . . . 16
β’
β²π((π β π β¦ π΅)βπ) |
68 | 67 | nfeq1 2329 |
. . . . . . . . . . . . . . 15
β’
β²π((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) |
69 | | fveq2 5516 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΅)βπ)) |
70 | | oveq2 5883 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΎ + π) = (πΎ + π)) |
71 | 70 | fveq2d 5520 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((π β π β¦ π΄)β(πΎ + π)) = ((π β π β¦ π΄)β(πΎ + π))) |
72 | 69, 71 | eqeq12d 2192 |
. . . . . . . . . . . . . . 15
β’ (π = π β (((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)))) |
73 | 68, 72 | rspc 2836 |
. . . . . . . . . . . . . 14
β’ (π β π β (βπ β π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)))) |
74 | 66, 73 | mpan9 281 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
75 | 74 | ralrimiva 2550 |
. . . . . . . . . . . 12
β’ (π β βπ β π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
76 | 75 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β βπ β π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
77 | 1 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β β€) |
78 | 2 | adantr 276 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β πΎ β β€) |
79 | | simpr 110 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β π) |
80 | 79, 4 | eleqtrdi 2270 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β (β€β₯β(π + πΎ))) |
81 | | eluzsub 9557 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ πΎ β β€ β§ π β
(β€β₯β(π + πΎ))) β (π β πΎ) β (β€β₯βπ)) |
82 | 77, 78, 80, 81 | syl3anc 1238 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π β πΎ) β (β€β₯βπ)) |
83 | 82, 26 | eleqtrrdi 2271 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π β πΎ) β π) |
84 | | fveq2 5516 |
. . . . . . . . . . . . 13
β’ (π = (π β πΎ) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΅)β(π β πΎ))) |
85 | | oveq2 5883 |
. . . . . . . . . . . . . 14
β’ (π = (π β πΎ) β (πΎ + π) = (πΎ + (π β πΎ))) |
86 | 85 | fveq2d 5520 |
. . . . . . . . . . . . 13
β’ (π = (π β πΎ) β ((π β π β¦ π΄)β(πΎ + π)) = ((π β π β¦ π΄)β(πΎ + (π β πΎ)))) |
87 | 84, 86 | eqeq12d 2192 |
. . . . . . . . . . . 12
β’ (π = (π β πΎ) β (((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) β ((π β π β¦ π΅)β(π β πΎ)) = ((π β π β¦ π΄)β(πΎ + (π β πΎ))))) |
88 | 87 | rspccva 2841 |
. . . . . . . . . . 11
β’
((βπ β
π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) β§ (π β πΎ) β π) β ((π β π β¦ π΅)β(π β πΎ)) = ((π β π β¦ π΄)β(πΎ + (π β πΎ)))) |
89 | 76, 83, 88 | syl2anc 411 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((π β π β¦ π΅)β(π β πΎ)) = ((π β π β¦ π΄)β(πΎ + (π β πΎ)))) |
90 | | pncan3 8165 |
. . . . . . . . . . . 12
β’ ((πΎ β β β§ π β β) β (πΎ + (π β πΎ)) = π) |
91 | 22, 24, 90 | syl2an 289 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΎ + (π β πΎ)) = π) |
92 | 91 | fveq2d 5520 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((π β π β¦ π΄)β(πΎ + (π β πΎ))) = ((π β π β¦ π΄)βπ)) |
93 | 32, 89, 92 | 3eqtrrd 2215 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) = (((π β π β¦ π΅) shift πΎ)βπ)) |
94 | 21, 93 | sylan2br 288 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β(π + πΎ))) β ((π β π β¦ π΄)βπ) = (((π β π β¦ π΅) shift πΎ)βπ)) |
95 | | addcl 7936 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯ + π¦) β β) |
96 | 95 | adantl 277 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ + π¦) β β) |
97 | 3, 20, 94, 96 | seq3feq 10472 |
. . . . . . 7
β’ (π β seq(π + πΎ)( + , (π β π β¦ π΄)) = seq(π + πΎ)( + , ((π β π β¦ π΅) shift πΎ))) |
98 | 97 | breq1d 4014 |
. . . . . 6
β’ (π β (seq(π + πΎ)( + , (π β π β¦ π΄)) β π₯ β seq(π + πΎ)( + , ((π β π β¦ π΅) shift πΎ)) β π₯)) |
99 | 30 | a1i 9 |
. . . . . . 7
β’ (π β (π β π β¦ π΅) β V) |
100 | 26 | eleq2i 2244 |
. . . . . . . . . . 11
β’ (π₯ β π β π₯ β (β€β₯βπ)) |
101 | 100 | biimpri 133 |
. . . . . . . . . 10
β’ (π₯ β
(β€β₯βπ) β π₯ β π) |
102 | 101 | adantl 277 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β€β₯βπ)) β π₯ β π) |
103 | 60 | ralrimiva 2550 |
. . . . . . . . . . 11
β’ (π β βπ β π π΅ β β) |
104 | 103 | adantr 276 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (β€β₯βπ)) β βπ β π π΅ β β) |
105 | | nfcsb1v 3091 |
. . . . . . . . . . . 12
β’
β²πβ¦π₯ / πβ¦π΅ |
106 | 105 | nfel1 2330 |
. . . . . . . . . . 11
β’
β²πβ¦π₯ / πβ¦π΅ β β |
107 | | csbeq1a 3067 |
. . . . . . . . . . . 12
β’ (π = π₯ β π΅ = β¦π₯ / πβ¦π΅) |
108 | 107 | eleq1d 2246 |
. . . . . . . . . . 11
β’ (π = π₯ β (π΅ β β β β¦π₯ / πβ¦π΅ β β)) |
109 | 106, 108 | rspc 2836 |
. . . . . . . . . 10
β’ (π₯ β π β (βπ β π π΅ β β β β¦π₯ / πβ¦π΅ β β)) |
110 | 102, 104,
109 | sylc 62 |
. . . . . . . . 9
β’ ((π β§ π₯ β (β€β₯βπ)) β β¦π₯ / πβ¦π΅ β β) |
111 | | eqid 2177 |
. . . . . . . . . 10
β’ (π β π β¦ π΅) = (π β π β¦ π΅) |
112 | 111 | fvmpts 5595 |
. . . . . . . . 9
β’ ((π₯ β π β§ β¦π₯ / πβ¦π΅ β β) β ((π β π β¦ π΅)βπ₯) = β¦π₯ / πβ¦π΅) |
113 | 102, 110,
112 | syl2anc 411 |
. . . . . . . 8
β’ ((π β§ π₯ β (β€β₯βπ)) β ((π β π β¦ π΅)βπ₯) = β¦π₯ / πβ¦π΅) |
114 | 113, 110 | eqeltrd 2254 |
. . . . . . 7
β’ ((π β§ π₯ β (β€β₯βπ)) β ((π β π β¦ π΅)βπ₯) β β) |
115 | 99, 1, 2, 114, 96 | iser3shft 11354 |
. . . . . 6
β’ (π β (seqπ( + , (π β π β¦ π΅)) β π₯ β seq(π + πΎ)( + , ((π β π β¦ π΅) shift πΎ)) β π₯)) |
116 | 98, 115 | bitr4d 191 |
. . . . 5
β’ (π β (seq(π + πΎ)( + , (π β π β¦ π΄)) β π₯ β seqπ( + , (π β π β¦ π΅)) β π₯)) |
117 | 116 | iotabidv 5200 |
. . . 4
β’ (π β (β©π₯seq(π + πΎ)( + , (π β π β¦ π΄)) β π₯) = (β©π₯seqπ( + , (π β π β¦ π΅)) β π₯)) |
118 | | df-fv 5225 |
. . . 4
β’ ( β
βseq(π + πΎ)( + , (π β π β¦ π΄))) = (β©π₯seq(π + πΎ)( + , (π β π β¦ π΄)) β π₯) |
119 | | df-fv 5225 |
. . . 4
β’ ( β
βseqπ( + , (π β π β¦ π΅))) = (β©π₯seqπ( + , (π β π β¦ π΅)) β π₯) |
120 | 117, 118,
119 | 3eqtr4g 2235 |
. . 3
β’ (π β ( β βseq(π + πΎ)( + , (π β π β¦ π΄))) = ( β βseqπ( + , (π β π β¦ π΅)))) |
121 | | eqidd 2178 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) = ((π β π β¦ π΄)βπ)) |
122 | 8 | fmpttd 5672 |
. . . . 5
β’ (π β (π β π β¦ π΄):πβΆβ) |
123 | 122 | ffvelcdmda 5652 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) β β) |
124 | 4, 3, 121, 123 | isum 11393 |
. . 3
β’ (π β Ξ£π β π ((π β π β¦ π΄)βπ) = ( β βseq(π + πΎ)( + , (π β π β¦ π΄)))) |
125 | | eqidd 2178 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΅)βπ)) |
126 | 122 | adantr 276 |
. . . . . 6
β’ ((π β§ π β π) β (π β π β¦ π΄):πβΆβ) |
127 | | eluzelcn 9539 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β π β β) |
128 | 127, 26 | eleq2s 2272 |
. . . . . . . . . . 11
β’ (π β π β π β β) |
129 | | addcom 8094 |
. . . . . . . . . . 11
β’ ((πΎ β β β§ π β β) β (πΎ + π) = (π + πΎ)) |
130 | 22, 128, 129 | syl2an 289 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πΎ + π) = (π + πΎ)) |
131 | | id 19 |
. . . . . . . . . . . 12
β’ (π β π β π β π) |
132 | 131, 26 | eleqtrdi 2270 |
. . . . . . . . . . 11
β’ (π β π β π β (β€β₯βπ)) |
133 | | eluzadd 9556 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯βπ) β§ πΎ β β€) β (π + πΎ) β
(β€β₯β(π + πΎ))) |
134 | 132, 2, 133 | syl2anr 290 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (π + πΎ) β
(β€β₯β(π + πΎ))) |
135 | 130, 134 | eqeltrd 2254 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΎ + π) β (β€β₯β(π + πΎ))) |
136 | 135, 4 | eleqtrrdi 2271 |
. . . . . . . 8
β’ ((π β§ π β π) β (πΎ + π) β π) |
137 | 136 | ralrimiva 2550 |
. . . . . . 7
β’ (π β βπ β π (πΎ + π) β π) |
138 | 70 | eleq1d 2246 |
. . . . . . . 8
β’ (π = π β ((πΎ + π) β π β (πΎ + π) β π)) |
139 | 138 | rspccva 2841 |
. . . . . . 7
β’
((βπ β
π (πΎ + π) β π β§ π β π) β (πΎ + π) β π) |
140 | 137, 139 | sylan 283 |
. . . . . 6
β’ ((π β§ π β π) β (πΎ + π) β π) |
141 | 126, 140 | ffvelcdmd 5653 |
. . . . 5
β’ ((π β§ π β π) β ((π β π β¦ π΄)β(πΎ + π)) β β) |
142 | 74, 141 | eqeltrd 2254 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) β β) |
143 | 26, 1, 125, 142 | isum 11393 |
. . 3
β’ (π β Ξ£π β π ((π β π β¦ π΅)βπ) = ( β βseqπ( + , (π β π β¦ π΅)))) |
144 | 120, 124,
143 | 3eqtr4d 2220 |
. 2
β’ (π β Ξ£π β π ((π β π β¦ π΄)βπ) = Ξ£π β π ((π β π β¦ π΅)βπ)) |
145 | | sumfct 11382 |
. . 3
β’
(βπ β
π π΄ β β β Ξ£π β π ((π β π β¦ π΄)βπ) = Ξ£π β π π΄) |
146 | 9, 145 | syl 14 |
. 2
β’ (π β Ξ£π β π ((π β π β¦ π΄)βπ) = Ξ£π β π π΄) |
147 | | sumfct 11382 |
. . 3
β’
(βπ β
π π΅ β β β Ξ£π β π ((π β π β¦ π΅)βπ) = Ξ£π β π π΅) |
148 | 103, 147 | syl 14 |
. 2
β’ (π β Ξ£π β π ((π β π β¦ π΅)βπ) = Ξ£π β π π΅) |
149 | 144, 146,
148 | 3eqtr3d 2218 |
1
β’ (π β Ξ£π β π π΄ = Ξ£π β π π΅) |