HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem clim2serz 7145
Description: Limit of an infinite series with an initial segment removed.
Hypotheses
Ref Expression
clim2serz.1 |- F e. V
clim2serz.2 |- A e. V
clim2serz.3 |- (<.M, + >. seq F) ~~> A
clim2serz.4 |- F:(ZZ>` M)-->CC
Assertion
Ref Expression
clim2serz |- (N e. (ZZ>` M) -> (<.(N + 1), + >. seq F) ~~> (A - ((<.M, + >. seq F)` N)))
Proof of Theorem clim2serz
StepHypRef Expression
1 clim2serz.3 . . . 4 |- (<.M, + >. seq F) ~~> A
2 oprex 3983 . . . . 5 |- (<.M, + >. seq F) e. V
3 oprex 3983 . . . . 5 |- (<.(N + 1), + >. seq F) e. V
4 clim2serz.2 . . . . 5 |- A e. V
5 negex 5365 . . . . 5 |- -u((<.M, + >. seq F)` N) e. V
62, 3, 4, 5climaddc1 7118 . . . 4 |- ((((<.M, + >. seq F) ~~> A /\ -u((<.M, + >. seq F)` N) e. CC) /\ ((N + 1) e. ZZ /\ A.k e. (ZZ>` (N + 1))(((<.M, + >. seq F)` k) e. CC /\ ((<.(N + 1), + >. seq F)` k) = (((<.M, + >. seq F)` k) + -u((<.M, + >. seq F)` N))))) -> (<.(N + 1), + >. seq F) ~~> (A + -u((<.M, + >. seq F)` N)))
71, 6mpanl1 706 . . 3 |- ((-u((<.M, + >. seq F)` N) e. CC /\ ((N + 1) e. ZZ /\ A.k e. (ZZ>` (N + 1))(((<.M, + >. seq F)` k) e. CC /\ ((<.(N + 1), + >. seq F)` k) = (((<.M, + >. seq F)` k) + -u((<.M, + >. seq F)` N))))) -> (<.(N + 1), + >. seq F) ~~> (A + -u((<.M, + >. seq F)` N)))
8 elfzuzt 6488 . . . . . . 7 |- (j e. (M...N) -> j e. (ZZ>` M))
9 clim2serz.4 . . . . . . . 8 |- F:(ZZ>` M)-->CC
109ffvelrni 3815 . . . . . . 7 |- (j e. (ZZ>` M) -> (F` j) e. CC)
118, 10syl 10 . . . . . 6 |- (j e. (M...N) -> (F` j) e. CC)
1211rgen 1698 . . . . 5 |- A.j e. (M...N)(F` j) e. CC
13 clim2serz.1 . . . . . 6 |- F e. V
1413serzclt 7045 . . . . 5 |- ((N e. (ZZ>` M) /\ A.j e. (M...N)(F` j) e. CC) -> ((<.M, + >. seq F)` N) e. CC)
1512, 14mpan2 696 . . . 4 |- (N e. (ZZ>` M) -> ((<.M, + >. seq F)` N) e. CC)
16 negclt 5368 . . . 4 |- (((<.M, + >. seq F)` N) e. CC -> -u((<.M, + >. seq F)` N) e. CC)
1715, 16syl 10 . . 3 |- (N e. (ZZ>` M) -> -u((<.M, + >. seq F)` N) e. CC)
18 eluzelz 6423 . . . . 5 |- (N e. (ZZ>` M) -> N e. ZZ)
1918peano2zd 6167 . . . 4 |- (N e. (ZZ>` M) -> (N + 1) e. ZZ)
20 uztrn 6428 . . . . . . . . 9 |- ((k e. (ZZ>` (N + 1)) /\ (N + 1) e. (ZZ>` M)) -> k e. (ZZ>` M))
21 peano2uz 6447 . . . . . . . . 9 |- (N e. (ZZ>` M) -> (N + 1) e. (ZZ>` M))
2220, 21sylan2 451 . . . . . . . 8 |- ((k e. (ZZ>` (N + 1)) /\ N e. (ZZ>` M)) -> k e. (ZZ>` M))
2322ancoms 436 . . . . . . 7 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> k e. (ZZ>` M))
24 elfzuzt 6488 . . . . . . . . . 10 |- (j e. (M...k) -> j e. (ZZ>` M))
2524, 10syl 10 . . . . . . . . 9 |- (j e. (M...k) -> (F` j) e. CC)
2625rgen 1698 . . . . . . . 8 |- A.j e. (M...k)(F` j) e. CC
2713serzclt 7045 . . . . . . . 8 |- ((k e. (ZZ>` M) /\ A.j e. (M...k)(F` j) e. CC) -> ((<.M, + >. seq F)` k) e. CC)
2826, 27mpan2 696 . . . . . . 7 |- (k e. (ZZ>` M) -> ((<.M, + >. seq F)` k) e. CC)
2923, 28syl 10 . . . . . 6 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> ((<.M, + >. seq F)` k) e. CC)
30 negsubt 5382 . . . . . . . 8 |- ((((<.M, + >. seq F)` k) e. CC /\ ((<.M, + >. seq F)` N) e. CC) -> (((<.M, + >. seq F)` k) + -u((<.M, + >. seq F)` N)) = (((<.M, + >. seq F)` k) - ((<.M, + >. seq F)` N)))
3115adantr 389 . . . . . . . 8 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> ((<.M, + >. seq F)` N) e. CC)
3230, 29, 31sylanc 471 . . . . . . 7 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> (((<.M, + >. seq F)` k) + -u((<.M, + >. seq F)` N)) = (((<.M, + >. seq F)` k) - ((<.M, + >. seq F)` N)))
3313serzsplit 7056 . . . . . . . . . 10 |- ((k e. ZZ /\ N e. (M...(k - 1)) /\ A.j e. (M...k)(F` j) e. CC) -> ((<.M, + >. seq F)` k) = (((<.M, + >. seq F)` N) + ((<.(N + 1), + >. seq F)` k)))
34 eluzelz 6423 . . . . . . . . . . 11 |- (k e. (ZZ>` (N + 1)) -> k e. ZZ)
3534adantl 388 . . . . . . . . . 10 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> k e. ZZ)
36 eluzp1m1t 6433 . . . . . . . . . . . 12 |- ((N e. ZZ /\ k e. (ZZ>` (N + 1))) -> (k - 1) e. (ZZ>` N))
3736, 18sylan 448 . . . . . . . . . . 11 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> (k - 1) e. (ZZ>` N))
38 eluzfzt 6477 . . . . . . . . . . 11 |- ((N e. (ZZ>` M) /\ (k - 1) e. (ZZ>` N)) -> N e. (M...(k - 1)))
3937, 38syldan 467 . . . . . . . . . 10 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> N e. (M...(k - 1)))
4026a1i 8 . . . . . . . . . 10 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> A.j e. (M...k)(F` j) e. CC)
4133, 35, 39, 40syl3anc 858 . . . . . . . . 9 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> ((<.M, + >. seq F)` k) = (((<.M, + >. seq F)` N) + ((<.(N + 1), + >. seq F)` k)))
4241eqcomd 1480 . . . . . . . 8 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> (((<.M, + >. seq F)` N) + ((<.(N + 1), + >. seq F)` k)) = ((<.M, + >. seq F)` k))
43 subaddt 5375 . . . . . . . . 9 |- ((((<.M, + >. seq F)` k) e. CC /\ ((<.M, + >. seq F)` N) e. CC /\ ((<.(N + 1), + >. seq F)` k) e. CC) -> ((((<.M, + >. seq F)` k) - ((<.M, + >. seq F)` N)) = ((<.(N + 1), + >. seq F)` k) <-> (((<.M, + >. seq F)` N) + ((<.(N + 1), + >. seq F)` k)) = ((<.M, + >. seq F)` k)))
44 resexg 3394 . . . . . . . . . . . . 13 |- (F e. V -> (F |` (ZZ>` (N + 1))) e. V)
4513, 44ax-mp 7 . . . . . . . . . . . 12 |- (F |` (ZZ>` (N + 1))) e. V
4645serzclt 7045 . . . . . . . . . . 11 |- ((k e. (ZZ>` (N + 1)) /\ A.j e. ((N + 1)...k)((F |` (ZZ>` (N + 1)))` j) e. CC) -> ((<.(N + 1), + >. seq (F |` (ZZ>` (N + 1))))` k) e. CC)
47 pm3.27 323 . . . . . . . . . . 11 |- ((N e. (ZZ>` M) /\ k e. (ZZ>` (N + 1))) -> k e. (ZZ>` (N + 1)))
48 uztrn 6428 . . . . . . . . . . . . . . . . 17 |- ((j e. (ZZ>` (N + 1)) /\ (N + 1) e. (ZZ>` M)) -> j e. (ZZ>` M))
49 elfzuzt 6488 . . . . . . . . . . . . . . . . 17 |- (j e. ((N + 1)...k) -> j e. (ZZ>` (N + 1)))
5048, 49, 21syl2an 454 . . . . . . . . . . . . . . . 16 |- ((j e. ((N + 1)...k) /\ N e. (ZZ>` M)) -> j e. (ZZ>` M