Table of ContentsTable of Contents Mathbox for Jeff Madsen < Previous   Next >
Related theorems
Unicode version
Theorem fsumleisumi 15826
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 fveq1 4680 . . . . 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))
21sumeq2sdv 8253 . . . 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))
31sumeq2sdv 8253 . . . 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))
42, 3breq12d 3351 . . 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)))
5 fsumleisumi.1 . . . 4 |- N e. (ZZ>=` M)
6 feq1 4551 . . . . . . . 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))
7 ax-17 1317 . . . . . . . . . 10 |- (u e. F -> A.k u e. F)
8 ax-17 1317 . . . . . . . . . . . 12 |- (F:(ZZ>=` M)-->RR -> A.k F:(ZZ>=` M)-->RR)
9 hbra1 2147 . . . . . . . . . . . 12 |- (A.k e. (ZZ>=` M)0 <_ (F` k) -> A.kA.k e. (ZZ>=` M)0 <_ (F` k))
10 ax-17 1317 . . . . . . . . . . . 12 |- (E.x(<.M, + >. seq F) ~~> x -> A.kE.x(<.M, + >. seq F) ~~> x)
118, 9, 10hb3an 1359 . . . . . . . . . . 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))
12 ax-17 1317 . . . . . . . . . . 11 |- (u e. ((ZZ>=` M) X. {0}) -> A.k u e. ((ZZ>=` M) X. {0}))
1311, 7, 12hbif 2999 . . . . . . . . . 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})))
147, 13hbeq 1995 . . . . . . . . 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})))
15 fveq1 4680 . . . . . . . . . 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))
1615breq2d 3350 . . . . . . . . 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)))
1714, 16ralbid 2121 . . . . . . . 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)))
18 ax-17 1317 . . . . . . . . . 10 |- (u e. F -> A.x u e. F)
19 ax-17 1317 . . . . . . . . . . . 12 |- (F:(ZZ>=` M)-->RR -> A.x F:(ZZ>=` M)-->RR)
20 ax-17 1317 . . . . . . . . . . . 12 |- (A.k e. (ZZ>=` M)0 <_ (F` k) -> A.xA.k e. (ZZ>=` M)0 <_ (F` k))
21 hbe1 1363 . . . . . . . . . . . 12 |- (E.x(<.M, + >. seq F) ~~> x -> A.xE.x(<.M, + >. seq F) ~~> x)
2219, 20, 21hb3an 1359 . . . . . . . . . . 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))
23 ax-17 1317 . . . . . . . . . . 11 |- (u e. ((ZZ>=` M) X. {0}) -> A.x u e. ((ZZ>=` M) X. {0}))
2422, 18, 23hbif 2999 . . . . . . . . . 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})))
2518, 24hbeq 1995 . . . . . . . . 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})))
26 opreq2 4890 . . . . . . . . . 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}))))
2726breq1d 3348 . . . . . . . . 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))
2825, 27exbid 1460 . . . . . . . 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))
296, 17, 283anbi123d 1168 . . . . . . 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)))
30 feq1 4551 . . . . . . . 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))
3112, 13hbeq 1995 . . . . . . . . 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})))
32 fveq1 4680 . . . . . . . . . 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))
3332breq2d 3350 . . . . . . . . 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)))
3431, 33ralbid 2121 . . . . . . . 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)))
3523, 24hbeq 1995 . . . . . . . . 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})))
36 opreq2 4890 . . . . . . . . . 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}))))
3736breq1d 3348 . . . . . . . . 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))
3835, 37exbid 1460 . . . . . . . 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))
3930, 34, 383anbi123d 1168 . . . . . . 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)))
40 0re 6603 . . . . . . . . 9 |- 0 e. RR
4140fconst6 15700 . . . . . . . 8 |- ((ZZ>=` M) X. {0}):(ZZ>=` M)-->RR
42 0cn 6481 . . . . . . . . . . . 12 |- 0 e. CC
4342elisseti 2301 . . . . . . . . . . 11 |- 0 e. _V
4443fvconst2 4822 . . . . . . . . . 10 |- (k e. (ZZ>=` M) -> (((ZZ>=` M) X. {0})` k) = 0)
4540leidi 6790 . . . . . . . . . 10 |- 0 <_ 0
4644, 45syl5breqr 3373 . . . . . . . . 9 |- (k e. (ZZ>=` M) -> 0 <_ (((ZZ>=` M) X. {0})` k))
4746rgen 2159 . . . . . . . 8 |- A.k e. (ZZ>=` M)0 <_ (((ZZ>=` M) X. {0})` k)
48 eluzel2 7593 . . . . . . . . . . 11 |- (N e. (ZZ>=` M) -> M e. ZZ)
495, 48ax-mp 7 . . . . . . . . . 10 |- M e. ZZ
50 serzclim0 8369 . . . . . . . . . 10 |- (M e. ZZ -> (<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> 0)
5149, 50ax-mp 7 . . . . . . . . 9 |- (<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> 0
52 breq2 3342 . . . . . . . . . 10 |- (x = 0 -> ((<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x <-> (<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> 0))
5343, 52cla4ev 2371 . . . . . . . . 9 |- ((<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> 0 -> E.x(<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x)
5451, 53ax-mp 7 . . . . . . . 8 |- E.x(<.M, + >. seq ((ZZ>=` M) X. {0})) ~~> x
5541, 47, 543pm3.2i 1048 . . . . . . 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)
5629, 39, 55elimhyp 3021 . . . . . 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)
5756simp1i 885 . . . . 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
58 fveq2 4681 . . . . . . . . . 10 |- (k = j -> (F` k) = (F` j))
5958breq2d 3350 . . . . . . . . 9 |- (k = j -> (0 <_ (F` k) <-> 0 <_ (F` j)))
6059cbvralv 2280 . . . . . . . 8 |- (A.k e. (ZZ>=` M)0 <_ (F` k) <-> A.j e. (ZZ>=` M)0 <_ (F` j))
61603anbi2i 1059 . . . . . . 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 2995 . . . . . . 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 4558 . . . . 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)
6557, 64mpbi 206 . . . 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
6656simp2i 886 . . . . 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 4682 . . . . . . 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 3346 . . . . . 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 2127 . . . . 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 206 . . . 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)
7156simp3i 887 . . . . . 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 1317 . . . . . . 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 1317 . . . . . . . . 9 |- (u e. <.M, + >. -> A.x u e. <.M, + >.)
74 ax-17 1317 . . . . . . . . 9 |- (u e. seq -> A.x u e. seq )
7573, 74, 24hbopr 4904 . . . . . . . 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 1317 . . . . . . . 8 |- (u e. ~~> -> A.x u e. ~~> )
77 ax-17 1317 . . . . . . . 8 |- (u e. v -> A.x u e. v)
7875, 76, 77hbbr 3381 . . . . . . 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 3342 . . . . . . 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 1529 . . . . . 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 206 . . . . 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 4893 . . . . . . 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 3345 . . . . . 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 1398 . . . . 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 206 . . . 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
865, 65, 70, 85fsumleisumii 15825 . . 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)
874, 86dedth 3011 . 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))
8887, 60syl3an2b 1134 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 163   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  ifcif 2982  {csn 3044  <.cop 3046   class class class wbr 3338   X. cxp 3984  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386   + caddc 6389   <_ cle 6448  ZZcz 6451  ZZ>=cuz 7586  ...cfz 7637   seq cseqz 7774   ~~> cli 8234  sum_csu 8239
This theorem is referenced by:  fsumleisum 15827
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-clim 8235  df-sum 8240
Copyright terms: Public domain