Table of ContentsTable of Contents Mathbox for Jeff Madsen < Previous   Next >
Related theorems
Unicode version
Theorem fsumleisumi 16911
Description: A partial sum of a series with nonnegative terms is less than or equal to the infinite sum.
Hypothesis
Ref Expression
fsumleisumi.1 |- N e. (ZZ>=` M)
Assertion
Ref Expression
fsumleisumi |- ((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x) -> sum_k e. (M...N)(F` k) <_ sum_k e. (ZZ>=` M)(F` k))
Distinct variable groups:   k,M,x   k,N,x   k,F,x
Proof of Theorem fsumleisumi
StepHypRef Expression
1 fveq2 4804 . . . 4 |- (k = j -> (F` k) = (F` j))
21breq2d 3551 . . 3 |- (k = j -> (0 <_ (F` k) <-> 0 <_ (F` j)))
32cbvralv 2557 . 2 |- (A.k e. (ZZ>=` M)0 <_ (F` k) <-> A.j e. (ZZ>=` M)0 <_ (F` j))
4 fveq1 4803 . . . . 5 |- (F = if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (F` k) = (if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k))
54sumeq2sdv 8765 . . . 4 |- (F = if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> sum_k e. (M...N)(F` k) = sum_k e. (M...N)(if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k))
64sumeq2sdv 8765 . . . 4 |- (F = if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> sum_k e. (ZZ>=` M)(F` k) = sum_k e. (ZZ>=` M)(if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k))
75, 6breq12d 3552 . . 3 |- (F = if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (sum_k e. (M...N)(F` k) <_ sum_k e. (ZZ>=` M)(F` k) <-> sum_k e. (M...N)(if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k) <_ sum_k e. (ZZ>=` M)(if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)))
8 fsumleisumi.1 . . . 4 |- N e. (ZZ>=` M)
9 feq1 4685 . . . . . . . 8 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (F:(ZZ>=` M)-->RR <-> if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR))
10 ax-17 1634 . . . . . . . . . 10 |- (u e. F -> A.k u e. F)
11 ax-17 1634 . . . . . . . . . . . 12 |- (F:(ZZ>=` M)-->RR -> A.k F:(ZZ>=` M)-->RR)
12 hbra1 2428 . . . . . . . . . . . 12 |- (A.k e. (ZZ>=` M)0 <_ (F` k) -> A.kA.k e. (ZZ>=` M)0 <_ (F` k))
13 ax-17 1634 . . . . . . . . . . . 12 |- (E.x(<.M, + >. seq F) ~~> x -> A.kE.x(<.M, + >. seq F) ~~> x)
1411, 12, 13hb3an 1677 . . . . . . . . . . 11 |- ((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x) -> A.k(F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x))
15 ax-17 1634 . . . . . . . . . . 11 |- (u e. ((ZZ>=` M) X. {0}) -> A.k u e. ((ZZ>=` M) X. {0}))
1614, 10, 15hbif 3228 . . . . . . . . . 10 |- (u e. if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> A.k u e. if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})))
1710, 16hbeq 2274 . . . . . . . . 9 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> A.k F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})))
18 fveq1 4803 . . . . . . . . . 10 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (F` k) = (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k))
1918breq2d 3551 . . . . . . . . 9 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (0 <_ (F` k) <-> 0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)))
2017, 19ralbid 2401 . . . . . . . 8 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (A.k e. (ZZ>=` M)0 <_ (F` k) <-> A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)))
21 ax-17 1634 . . . . . . . . . 10 |- (u e. F -> A.x u e. F)
22 ax-17 1634 . . . . . . . . . . . 12 |- (F:(ZZ>=` M)-->RR -> A.x F:(ZZ>=` M)-->RR)
23 ax-17 1634 . . . . . . . . . . . 12 |- (A.k e. (ZZ>=` M)0 <_ (F` k) -> A.xA.k e. (ZZ>=` M)0 <_ (F` k))
24 hbe1 1681 . . . . . . . . . . . 12 |- (E.x(<.M, + >. seq F) ~~> x -> A.xE.x(<.M, + >. seq F) ~~> x)
2522, 23, 24hb3an 1677 . . . . . . . . . . 11 |- ((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x) -> A.x(F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x))
26 ax-17 1634 . . . . . . . . . . 11 |- (u e. ((ZZ>=` M) X. {0}) -> A.x u e. ((ZZ>=` M) X. {0}))
2725, 21, 26hbif 3228 . . . . . . . . . 10 |- (u e. if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> A.x u e. if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})))
2821, 27hbeq 2274 . . . . . . . . 9 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> A.x F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})))
29 opreq2 5026 . . . . . . . . . 10 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (<.M, + >. seq F) = (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))))
3029breq1d 3549 . . . . . . . . 9 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> ((<.M, + >. seq F) ~~> x <-> (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x))
3128, 30exbid 1772 . . . . . . . 8 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (E.x(<.M, + >. seq F) ~~> x <-> E.x(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x))
329, 20, 313anbi123d 1469 . . . . . . 7 |- (F = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> ((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x) <-> (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k) /\ E.x(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x)))
33 feq1 4685 . . . . . . . 8 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (((ZZ>=` M) X. {0}):(ZZ>=` M)-->RR <-> if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR))
3415, 16hbeq 2274 . . . . . . . . 9 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> A.k((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})))
35 fveq1 4803 . . . . . . . . . 10 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (((ZZ>=` M) X. {0})` k) = (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k))
3635breq2d 3551 . . . . . . . . 9 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (0 <_ (((ZZ>=` M) X. {0})` k) <-> 0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)))
3734, 36ralbid 2401 . . . . . . . 8 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (A.k e. (ZZ>=` M)0 <_ (((ZZ>=` M) X. {0})` k) <-> A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)))
3826, 27hbeq 2274 . . . . . . . . 9 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> A.x((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})))
39 opreq2 5026 . . . . . . . . . 10 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (<.M, + >. seq ((ZZ>=` M) X. {0})) = (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))))
4039breq1d 3549 . . . . . . . . 9 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> ((<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x <-> (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x))
4138, 40exbid 1772 . . . . . . . 8 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> (E.x(<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x <-> E.x(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x))
4233, 37, 413anbi123d 1469 . . . . . . 7 |- (((ZZ>=` M) X. {0}) = if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) -> ((((ZZ>=` M) X. {0}):(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (((ZZ>=` M) X. {0})` k) /\ E.x(<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x) <-> (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k) /\ E.x(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x)))
43 0re 6942 . . . . . . . . 9 |- 0 e. RR
4443fconst6 16785 . . . . . . . 8 |- ((ZZ>=` M) X. {0}):(ZZ>=` M)-->RR
4543leidi 7238 . . . . . . . . . 10 |- 0 <_ 0
46 0cn 6933 . . . . . . . . . . . 12 |- 0 e. CC
4746elisseti 2579 . . . . . . . . . . 11 |- 0 e. _V
4847fvconst2 4953 . . . . . . . . . 10 |- (k e. (ZZ>=` M) -> (((ZZ>=` M) X. {0})` k) = 0)
4945, 48syl5breqr 3578 . . . . . . . . 9 |- (k e. (ZZ>=` M) -> 0 <_ (((ZZ>=` M) X. {0})` k))
5049rgen 2440 . . . . . . . 8 |- A.k e. (ZZ>=` M)0 <_ (((ZZ>=` M) X. {0})` k)
51 eluzel2 8052 . . . . . . . . . . 11 |- (N e. (ZZ>=` M) -> M e. ZZ)
528, 51ax-mp 7 . . . . . . . . . 10 |- M e. ZZ
53 serzclim0 8881 . . . . . . . . . 10 |- (M e. ZZ -> (<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> 0)
5452, 53ax-mp 7 . . . . . . . . 9 |- (<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> 0
55 breq2 3543 . . . . . . . . . 10 |- (x = 0 -> ((<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x <-> (<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> 0))
5647, 55cla4ev 2642 . . . . . . . . 9 |- ((<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> 0 -> E.x(<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x)
5754, 56ax-mp 7 . . . . . . . 8 |- E.x(<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x
5844, 50, 573pm3.2i 1326 . . . . . . 7 |- (((ZZ>=` M) X. {0}):(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (((ZZ>=` M) X. {0})` k) /\ E.x(<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x)
5932, 42, 58elimhyp 3247 . . . . . 6 |- (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k) /\ E.x(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x)
6059simp1i 1157 . . . . 5 |- if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR
6133anbi2i 1337 . . . . . . 7 |- ((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x) <-> (F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x))
62 ifbi 3222 . . . . . . 7 |- (((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x) <-> (F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x)) -> if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) = if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})))
6361, 62ax-mp 7 . . . . . 6 |- if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})) = if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))
6463feq1i 4692 . . . . 5 |- (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR <-> if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR)
6560, 64mpbi 254 . . . 4 |- if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})):(ZZ>=` M)-->RR
6659simp2i 1158 . . . . 5 |- A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)
6763fveq1i 4805 . . . . . . 7 |- (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k) = (if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)
6867breq2i 3547 . . . . . 6 |- (0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k) <-> 0 <_ (if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k))
6968ralbii 2407 . . . . 5 |- (A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k) <-> A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k))
7066, 69mpbi 254 . . . 4 |- A.k e. (ZZ>=` M)0 <_ (if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)
7159simp3i 1159 . . . . . 6 |- E.x(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x
72 ax-17 1634 . . . . . . 7 |- ((<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x -> A.v(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x)
73 ax-17 1634 . . . . . . . . 9 |- (u e. <.M, + >. -> A.x u e. <.M, + >.)
74 ax-17 1634 . . . . . . . . 9 |- (u e. seq -> A.x u e. seq )
7573, 74, 27hbopr 5039 . . . . . . . 8 |- (u e. (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) -> A.x u e. (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))))
76 ax-17 1634 . . . . . . . 8 |- (u e. ~~> -> A.x u e. ~~> )
77 ax-17 1634 . . . . . . . 8 |- (u e. v -> A.x u e. v)
7875, 76, 77hbbr 3586 . . . . . . 7 |- ((<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v -> A.x(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v)
79 breq2 3543 . . . . . . 7 |- (x = v -> ((<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x <-> (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v))
8072, 78, 79cbvex 1838 . . . . . 6 |- (E.x(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> x <-> E.v(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v)
8171, 80mpbi 254 . . . . 5 |- E.v(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v
8263opreq2i 5029 . . . . . . 7 |- (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) = (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0})))
8382breq1i 3546 . . . . . 6 |- ((<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v <-> (<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v)
8483exbii 1716 . . . . 5 |- (E.v(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v <-> E.v(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v)
8581, 84mpbi 254 . . . 4 |- E.v(<.M, + >. seq if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))) ~~> v
868, 65, 70, 85fsumleisumii 16910 . . 3 |- sum_k e. (M...N)(if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k) <_ sum_k e. (ZZ>=` M)(if((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x), F, ((ZZ>=` M) X. {0}))` k)
877, 86dedth 3240 . 2 |- ((F:(ZZ>=` M)-->RR /\ A.j e. (ZZ>=` M)0 <_ (F` j) /\ E.x(<.M, + >. seq F) ~~> x) -> sum_k e. (M...N)(F` k) <_ sum_k e. (ZZ>=` M)(F` k))
883, 87syl3an2b 1414 1 |- ((F:(ZZ>=` M)-->RR /\ A.k e. (ZZ>=` M)0 <_ (F` k) /\ E.x(<.M, + >. seq F) ~~> x) -> sum_k e. (M...N)(F` k) <_ sum_k e. (ZZ>=` M)(F` k))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 231   /\ w3a 1130   = wceq 1615   e. wcel 1617  E.wex 1644  A.wral 2385  ifcif 3212  {csn 3270  <.cop 3272   class class class wbr 3539   X. cxp 4149  -->wf 4159  ` cfv 4163  (class class class)co 5020  CCcc 6827  RRcr 6828  0cc0 6829   + caddc 6832   <_ cle 6943  ZZcz 7096  ZZ>=cuz 8045  ...cfz 8112   seq cseqz 8265   ~~> cli 8746  sum_csu 8751
This theorem is referenced by:  fsumleisum 16912
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906  ax-pre-sup 6907  ax-addopr 6908  ax-mulopr 6909
This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-1st 5166  df-2nd 5167  df-iota 5259  df-rdg 5344  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-sup 5932  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-div 7325  df-n 7543  df-2 7589  df-n0 7761  df-z 7798  df-uz 8046  df-fz 8113  df-seq1 8210  df-shft 8245  df-seqz 8267  df-exp 8312  df-sqr 8420  df-re 8501  df-im 8502  df-cj 8503  df-abs 8504  df-clim 8747  df-sum 8752
Copyright terms: Public domain