Step | Hyp | Ref
| Expression |
1 | | isumsplit.1 |
. 2
β’ π =
(β€β₯βπ) |
2 | | isumsplit.3 |
. . . 4
β’ (π β π β π) |
3 | 2, 1 | eleqtrdi 2848 |
. . 3
β’ (π β π β (β€β₯βπ)) |
4 | | eluzel2 12775 |
. . 3
β’ (π β
(β€β₯βπ) β π β β€) |
5 | 3, 4 | syl 17 |
. 2
β’ (π β π β β€) |
6 | | isumsplit.4 |
. 2
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
7 | | isumsplit.5 |
. 2
β’ ((π β§ π β π) β π΄ β β) |
8 | | isumsplit.2 |
. . 3
β’ π =
(β€β₯βπ) |
9 | | eluzelz 12780 |
. . . 4
β’ (π β
(β€β₯βπ) β π β β€) |
10 | 3, 9 | syl 17 |
. . 3
β’ (π β π β β€) |
11 | | uzss 12793 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
12 | 3, 11 | syl 17 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β
(β€β₯βπ)) |
13 | 12, 8, 1 | 3sstr4g 3994 |
. . . . . 6
β’ (π β π β π) |
14 | 13 | sselda 3949 |
. . . . 5
β’ ((π β§ π β π) β π β π) |
15 | 14, 6 | syldan 592 |
. . . 4
β’ ((π β§ π β π) β (πΉβπ) = π΄) |
16 | 14, 7 | syldan 592 |
. . . 4
β’ ((π β§ π β π) β π΄ β β) |
17 | | isumsplit.6 |
. . . . 5
β’ (π β seqπ( + , πΉ) β dom β ) |
18 | 6, 7 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
19 | 1, 2, 18 | iserex 15548 |
. . . . 5
β’ (π β (seqπ( + , πΉ) β dom β β seqπ( + , πΉ) β dom β )) |
20 | 17, 19 | mpbid 231 |
. . . 4
β’ (π β seqπ( + , πΉ) β dom β ) |
21 | 8, 10, 15, 16, 20 | isumclim2 15650 |
. . 3
β’ (π β seqπ( + , πΉ) β Ξ£π β π π΄) |
22 | | fzfid 13885 |
. . . 4
β’ (π β (π...(π β 1)) β Fin) |
23 | | elfzuz 13444 |
. . . . . 6
β’ (π β (π...(π β 1)) β π β (β€β₯βπ)) |
24 | 23, 1 | eleqtrrdi 2849 |
. . . . 5
β’ (π β (π...(π β 1)) β π β π) |
25 | 24, 7 | sylan2 594 |
. . . 4
β’ ((π β§ π β (π...(π β 1))) β π΄ β β) |
26 | 22, 25 | fsumcl 15625 |
. . 3
β’ (π β Ξ£π β (π...(π β 1))π΄ β β) |
27 | 14, 18 | syldan 592 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
28 | 8, 10, 27 | serf 13943 |
. . . 4
β’ (π β seqπ( + , πΉ):πβΆβ) |
29 | 28 | ffvelcdmda 7040 |
. . 3
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
30 | 5 | zred 12614 |
. . . . . . . . . . . 12
β’ (π β π β β) |
31 | 30 | ltm1d 12094 |
. . . . . . . . . . 11
β’ (π β (π β 1) < π) |
32 | | peano2zm 12553 |
. . . . . . . . . . . 12
β’ (π β β€ β (π β 1) β
β€) |
33 | | fzn 13464 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ (π β 1) β β€)
β ((π β 1) <
π β (π...(π β 1)) = β
)) |
34 | 5, 32, 33 | syl2anc2 586 |
. . . . . . . . . . 11
β’ (π β ((π β 1) < π β (π...(π β 1)) = β
)) |
35 | 31, 34 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (π...(π β 1)) = β
) |
36 | 35 | sumeq1d 15593 |
. . . . . . . . 9
β’ (π β Ξ£π β (π...(π β 1))π΄ = Ξ£π β β
π΄) |
37 | 36 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β Ξ£π β (π...(π β 1))π΄ = Ξ£π β β
π΄) |
38 | | sum0 15613 |
. . . . . . . 8
β’
Ξ£π β
β
π΄ =
0 |
39 | 37, 38 | eqtrdi 2793 |
. . . . . . 7
β’ ((π β§ π β π) β Ξ£π β (π...(π β 1))π΄ = 0) |
40 | 39 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π β π) β (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)) = (0 + (seqπ( + , πΉ)βπ))) |
41 | 13 | sselda 3949 |
. . . . . . . 8
β’ ((π β§ π β π) β π β π) |
42 | 1, 5, 18 | serf 13943 |
. . . . . . . . 9
β’ (π β seqπ( + , πΉ):πβΆβ) |
43 | 42 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
44 | 41, 43 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
45 | 44 | addid2d 11363 |
. . . . . 6
β’ ((π β§ π β π) β (0 + (seqπ( + , πΉ)βπ)) = (seqπ( + , πΉ)βπ)) |
46 | 40, 45 | eqtr2d 2778 |
. . . . 5
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ))) |
47 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π β (π β 1) = (π β 1)) |
48 | 47 | oveq2d 7378 |
. . . . . . . 8
β’ (π = π β (π...(π β 1)) = (π...(π β 1))) |
49 | 48 | sumeq1d 15593 |
. . . . . . 7
β’ (π = π β Ξ£π β (π...(π β 1))π΄ = Ξ£π β (π...(π β 1))π΄) |
50 | | seqeq1 13916 |
. . . . . . . 8
β’ (π = π β seqπ( + , πΉ) = seqπ( + , πΉ)) |
51 | 50 | fveq1d 6849 |
. . . . . . 7
β’ (π = π β (seqπ( + , πΉ)βπ) = (seqπ( + , πΉ)βπ)) |
52 | 49, 51 | oveq12d 7380 |
. . . . . 6
β’ (π = π β (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ))) |
53 | 52 | eqeq2d 2748 |
. . . . 5
β’ (π = π β ((seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)))) |
54 | 46, 53 | syl5ibrcom 247 |
. . . 4
β’ ((π β§ π β π) β (π = π β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)))) |
55 | | addcl 11140 |
. . . . . . . 8
β’ ((π β β β§ π β β) β (π + π) β β) |
56 | 55 | adantl 483 |
. . . . . . 7
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π β β)) β (π + π) β β) |
57 | | addass 11145 |
. . . . . . . 8
β’ ((π β β β§ π β β β§ π₯ β β) β ((π + π) + π₯) = (π + (π + π₯))) |
58 | 57 | adantl 483 |
. . . . . . 7
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ (π β β β§ π β β β§ π₯ β β)) β ((π + π) + π₯) = (π + (π + π₯))) |
59 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π β π) |
60 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π) |
61 | 10 | zcnd 12615 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
62 | | ax-1cn 11116 |
. . . . . . . . . . . . 13
β’ 1 β
β |
63 | | npcan 11417 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
64 | 61, 62, 63 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β ((π β 1) + 1) = π) |
65 | 64 | eqcomd 2743 |
. . . . . . . . . . 11
β’ (π β π = ((π β 1) + 1)) |
66 | 60, 65 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π = ((π β 1) + 1)) |
67 | 66 | fveq2d 6851 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β
(β€β₯βπ) = (β€β₯β((π β 1) +
1))) |
68 | 8, 67 | eqtrid 2789 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π = (β€β₯β((π β 1) +
1))) |
69 | 59, 68 | eleqtrd 2840 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β((π β 1) + 1))) |
70 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β π β β€) |
71 | | eluzp1m1 12796 |
. . . . . . . 8
β’ ((π β β€ β§ π β
(β€β₯β(π + 1))) β (π β 1) β
(β€β₯βπ)) |
72 | 70, 71 | sylan 581 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (π β 1) β
(β€β₯βπ)) |
73 | | elfzuz 13444 |
. . . . . . . . 9
β’ (π β (π...π) β π β (β€β₯βπ)) |
74 | 73, 1 | eleqtrrdi 2849 |
. . . . . . . 8
β’ (π β (π...π) β π β π) |
75 | 60, 74, 18 | syl2an 597 |
. . . . . . 7
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ π β (π...π)) β (πΉβπ) β β) |
76 | 56, 58, 69, 72, 75 | seqsplit 13948 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = ((seqπ( + , πΉ)β(π β 1)) + (seq((π β 1) + 1)( + , πΉ)βπ))) |
77 | 60, 24, 6 | syl2an 597 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ π β (π...(π β 1))) β (πΉβπ) = π΄) |
78 | 60, 24, 7 | syl2an 597 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ π β (β€β₯β(π + 1))) β§ π β (π...(π β 1))) β π΄ β β) |
79 | 77, 72, 78 | fsumser 15622 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β Ξ£π β (π...(π β 1))π΄ = (seqπ( + , πΉ)β(π β 1))) |
80 | 66 | seqeq1d 13919 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β seqπ( + , πΉ) = seq((π β 1) + 1)( + , πΉ)) |
81 | 80 | fveq1d 6849 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = (seq((π β 1) + 1)( + , πΉ)βπ)) |
82 | 79, 81 | oveq12d 7380 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)) = ((seqπ( + , πΉ)β(π β 1)) + (seq((π β 1) + 1)( + , πΉ)βπ))) |
83 | 76, 82 | eqtr4d 2780 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯β(π + 1))) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ))) |
84 | 83 | ex 414 |
. . . 4
β’ ((π β§ π β π) β (π β (β€β₯β(π + 1)) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ)))) |
85 | | uzp1 12811 |
. . . . . 6
β’ (π β
(β€β₯βπ) β (π = π β¨ π β (β€β₯β(π + 1)))) |
86 | 3, 85 | syl 17 |
. . . . 5
β’ (π β (π = π β¨ π β (β€β₯β(π + 1)))) |
87 | 86 | adantr 482 |
. . . 4
β’ ((π β§ π β π) β (π = π β¨ π β (β€β₯β(π + 1)))) |
88 | 54, 84, 87 | mpjaod 859 |
. . 3
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) = (Ξ£π β (π...(π β 1))π΄ + (seqπ( + , πΉ)βπ))) |
89 | 8, 10, 21, 26, 17, 29, 88 | climaddc2 15525 |
. 2
β’ (π β seqπ( + , πΉ) β (Ξ£π β (π...(π β 1))π΄ + Ξ£π β π π΄)) |
90 | 1, 5, 6, 7, 89 | isumclim 15649 |
1
β’ (π β Ξ£π β π π΄ = (Ξ£π β (π...(π β 1))π΄ + Ξ£π β π π΄)) |