Step | Hyp | Ref
| Expression |
1 | | isumsplit.1 |
. 2
β’ π =
(β€β₯βπ) |
2 | | isumsplit.3 |
. . . 4
β’ (π β π β π) |
3 | 2, 1 | eleqtrdi 2268 |
. . 3
β’ (π β π β (β€β₯βπ)) |
4 | | eluzel2 9504 |
. . 3
β’ (π β
(β€β₯βπ) β π β β€) |
5 | 3, 4 | syl 14 |
. 2
β’ (π β π β β€) |
6 | | isumsplit.4 |
. 2
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
7 | | isumsplit.5 |
. 2
β’ ((π β§ π β π) β π΄ β β) |
8 | | isumsplit.2 |
. . 3
β’ π =
(β€β₯βπ) |
9 | | eluzelz 9508 |
. . . 4
β’ (π β
(β€β₯βπ) β π β β€) |
10 | 3, 9 | syl 14 |
. . 3
β’ (π β π β β€) |
11 | | uzss 9519 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
12 | 3, 11 | syl 14 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β
(β€β₯βπ)) |
13 | 12, 8, 1 | 3sstr4g 3196 |
. . . . . 6
β’ (π β π β π) |
14 | 13 | sselda 3153 |
. . . . 5
β’ ((π β§ π β π) β π β π) |
15 | 14, 6 | syldan 282 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
16 | 14, 7 | syldan 282 |
. . . 4
β’ ((π β§ π β π) β π΄ β β) |
17 | | isumsplit.6 |
. . . . 5
β’ (π β seqπ( + , πΉ) β dom β ) |
18 | 6, 7 | eqeltrd 2252 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
19 | 1, 2, 18 | iserex 11314 |
. . . . 5
β’ (π β (seqπ( + , πΉ) β dom β β seqπ( + , πΉ) β dom β )) |
20 | 17, 19 | mpbid 147 |
. . . 4
β’ (π β seqπ( + , πΉ) β dom β ) |
21 | 8, 10, 15, 16, 20 | isumclim2 11397 |
. . 3
β’ (π β seqπ( + , πΉ) β Ξ£π β π π΄) |
22 | | peano2zm 9262 |
. . . . . 6
β’ (π β β€ β (π β 1) β
β€) |
23 | 10, 22 | syl 14 |
. . . . 5
β’ (π β (π β 1) β β€) |
24 | 5, 23 | fzfigd 10399 |
. . . 4
β’ (π β (π...(π β 1)) β Fin) |
25 | | elfzuz 9989 |
. . . . . 6
β’ (π β (π...(π β 1)) β π β (β€β₯βπ)) |
26 | 25, 1 | eleqtrrdi 2269 |
. . . . 5
β’ (π β (π...(π β 1)) β π β π) |
27 | 26, 7 | sylan2 286 |
. . . 4
β’ ((π β§ π β (π...(π β 1))) β π΄ β β) |
28 | 24, 27 | fsumcl 11375 |
. . 3
β’ (π β Ξ£π β (π...(π β 1))π΄ β β) |
29 | 14, 18 | syldan 282 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
30 | 8, 10, 29 | serf 10442 |
. . . 4
β’ (π β seqπ( + , πΉ):πβΆβ) |
31 | 30 | ffvelcdmda 5643 |
. . 3
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
32 | 5 | zred 9346 |
. . . . . . . . . . . 12
β’ (π β π β β) |
33 | 32 | ltm1d 8860 |
. . . . . . . . . . 11
β’ (π β (π β 1) < π) |
34 | | peano2zm 9262 |
. . . . . . . . . . . . 13
β’ (π β β€ β (π β 1) β
β€) |
35 | 5, 34 | syl 14 |
. . . . . . . . . . . 12
β’ (π β (π β 1) β β€) |
36 | | fzn 10010 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ (π β 1) β β€)
β ((π β 1) <
π β (π...(π β 1)) = β
)) |
37 | 5, 35, 36 | syl2anc 411 |
. . . . . . . . . . 11
β’ (π β ((π β 1) < π β (π...(π β 1)) = β
)) |
38 | 33, 37 | mpbid 147 |
. . . . . . . . . 10
β’ (π β (π...(π β 1)) = β
) |
39 | 38 | sumeq1d 11341 |
. . . . . . . . 9
β’ (π β Ξ£π β (π...(π β 1))π΄ = Ξ£π β β
π΄) |
40 | 39 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π β π) β Ξ£π β (π...(π β 1))π΄ = Ξ£π β β
π΄) |
41 | | sum0 11363 |
. . . . . . . 8
β’
Ξ£π β
β
π΄ =
0 |
42 | 40, 41 | eqtrdi 2224 |
. . . . . . 7
β’ ((π β§ π β π) β Ξ£π β (π...(π β 1))π΄ = 0) |
43 | 42 | oveq1d 5880 |
. . . . . 6
β’ ((π β§ π β π) β (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)) = (0 + (seqπ( + , πΉ)βπ))) |
44 | 13 | sselda 3153 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
45 | 1, 5, 18 | serf 10442 |
. . . . . . . . 9
β’ (π β seqπ( + , πΉ):πβΆβ) |
46 | 45 | ffvelcdmda 5643 |
. . . . . . . 8
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
47 | 44, 46 | syldan 282 |
. . . . . . 7
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
48 | 47 | addid2d 8081 |
. . . . . 6
β’ ((π β§ π β π) β (0 + (seqπ( + , πΉ)βπ)) = (seqπ( + , πΉ)βπ)) |
49 | 43, 48 | eqtr2d 2209 |
. . . . 5
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ))) |
50 | | oveq1 5872 |
. . . . . . . . 9
β’ (π = π β (π β 1) = (π β 1)) |
51 | 50 | oveq2d 5881 |
. . . . . . . 8
β’ (π = π β (π...(π β 1)) = (π...(π β 1))) |
52 | 51 | sumeq1d 11341 |
. . . . . . 7
β’ (π = π β Ξ£π β (π...(π β 1))π΄ = Ξ£π β (π...(π β 1))π΄) |
53 | | seqeq1 10416 |
. . . . . . . 8
β’ (π = π β seqπ( + , πΉ) = seqπ( + , πΉ)) |
54 | 53 | fveq1d 5509 |
. . . . . . 7
β’ (π = π β (seqπ( + , πΉ)βπ) = (seqπ( + , πΉ)βπ)) |
55 | 52, 54 | oveq12d 5883 |
. . . . . 6
β’ (π = π β (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ))) |
56 | 55 | eqeq2d 2187 |
. . . . 5
β’ (π = π β ((seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)))) |
57 | 49, 56 | syl5ibrcom 157 |
. . . 4
β’ ((π β§ π β π) β (π = π β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)))) |
58 | | addcl 7911 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π + π) β β) |
59 | 58 | adantl 277 |
. . . . . . 7
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π β β)) β (π + π) β β) |
60 | | addass 7916 |
. . . . . . . 8
β’ ((π β β β§ π β β β§ π₯ β β) β ((π + π) + π₯) = (π + (π + π₯))) |
61 | 60 | adantl 277 |
. . . . . . 7
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π β β β§ π₯ β β)) β ((π + π) + π₯) = (π + (π + π₯))) |
62 | | simplr 528 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π β π) |
63 | | simpll 527 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π) |
64 | 10 | zcnd 9347 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
65 | | ax-1cn 7879 |
. . . . . . . . . . . . 13
β’ 1 β
β |
66 | | npcan 8140 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
67 | 64, 65, 66 | sylancl 413 |
. . . . . . . . . . . 12
β’ (π β ((π β 1) + 1) = π) |
68 | 67 | eqcomd 2181 |
. . . . . . . . . . 11
β’ (π β π = ((π β 1) + 1)) |
69 | 63, 68 | syl 14 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π = ((π β 1) + 1)) |
70 | 69 | fveq2d 5511 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β
(β€β₯βπ) = (β€β₯β((π β 1) +
1))) |
71 | 8, 70 | eqtrid 2220 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π = (β€β₯β((π β 1) +
1))) |
72 | 62, 71 | eleqtrd 2254 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β((π β 1) + 1))) |
73 | 5 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π β π) β π β β€) |
74 | | eluzp1m1 9522 |
. . . . . . . 8
β’ ((π β β€ β§ π β
(β€β₯β(π + 1))) β (π β 1) β
(β€β₯βπ)) |
75 | 73, 74 | sylan 283 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (π β 1) β
(β€β₯βπ)) |
76 | 1 | eleq2i 2242 |
. . . . . . . . . 10
β’ (π β π β π β (β€β₯βπ)) |
77 | 76, 6 | sylan2br 288 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) = π΄) |
78 | 63, 77 | sylan 283 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ π β (β€β₯βπ)) β (πΉβπ) = π΄) |
79 | 76, 7 | sylan2br 288 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β π΄ β β) |
80 | 63, 79 | sylan 283 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ π β (β€β₯βπ)) β π΄ β β) |
81 | 78, 80 | eqeltrd 2252 |
. . . . . . 7
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
82 | 59, 61, 72, 75, 81 | seq3split 10447 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seqπ( + , πΉ)β(π β 1)) + (seq((π β 1) + 1)( + , πΉ)βπ))) |
83 | 78, 75, 80 | fsum3ser 11372 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β Ξ£π β (π...(π β 1))π΄ = (seqπ( + , πΉ)β(π β 1))) |
84 | 69 | seqeq1d 10419 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β seqπ( + , πΉ) = seq((π β 1) + 1)( + , πΉ)) |
85 | 84 | fveq1d 5509 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = (seq((π β 1) + 1)( + , πΉ)βπ)) |
86 | 83, 85 | oveq12d 5883 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)) = ((seqπ( + , πΉ)β(π β 1)) + (seq((π β 1) + 1)( + , πΉ)βπ))) |
87 | 82, 86 | eqtr4d 2211 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ))) |
88 | 87 | ex 115 |
. . . 4
β’ ((π β§ π β π) β (π β (β€β₯β(π + 1)) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)))) |
89 | | uzp1 9532 |
. . . . . 6
β’ (π β
(β€β₯βπ) β (π = π β¨ π β (β€β₯β(π + 1)))) |
90 | 3, 89 | syl 14 |
. . . . 5
β’ (π β (π = π β¨ π β (β€β₯β(π + 1)))) |
91 | 90 | adantr 276 |
. . . 4
β’ ((π β§ π β π) β (π = π β¨ π β (β€β₯β(π + 1)))) |
92 | 57, 88, 91 | mpjaod 718 |
. . 3
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ))) |
93 | 8, 10, 21, 28, 17, 31, 92 | climaddc2 11305 |
. 2
β’ (π β seqπ( + , πΉ) β (Ξ£π β (π...(π β 1))π΄ + Ξ£π β π π΄)) |
94 | 1, 5, 6, 7, 93 | isumclim 11396 |
1
β’ (π β Ξ£π β π π΄ = (Ξ£π β (π...(π β 1))π΄ + Ξ£π β π π΄)) |