This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isumltss

Description: A partial sum of a series with positive terms is less than the infinite sum. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Mar-2015)

Ref Expression
Hypotheses isumltss.1 
|- Z = ( ZZ>= ` M )
isumltss.2 
|- ( ph -> M e. ZZ )
isumltss.3 
|- ( ph -> A e. Fin )
isumltss.4 
|- ( ph -> A C_ Z )
isumltss.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
isumltss.6 
|- ( ( ph /\ k e. Z ) -> B e. RR+ )
isumltss.7 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion isumltss 
|- ( ph -> sum_ k e. A B < sum_ k e. Z B )

Proof

Step Hyp Ref Expression
1 isumltss.1 
 |-  Z = ( ZZ>= ` M )
2 isumltss.2 
 |-  ( ph -> M e. ZZ )
3 isumltss.3 
 |-  ( ph -> A e. Fin )
4 isumltss.4 
 |-  ( ph -> A C_ Z )
5 isumltss.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
6 isumltss.6 
 |-  ( ( ph /\ k e. Z ) -> B e. RR+ )
7 isumltss.7 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
8 1 uzinf 
 |-  ( M e. ZZ -> -. Z e. Fin )
9 2 8 syl 
 |-  ( ph -> -. Z e. Fin )
10 ssdif0 
 |-  ( Z C_ A <-> ( Z \ A ) = (/) )
11 eqss 
 |-  ( A = Z <-> ( A C_ Z /\ Z C_ A ) )
12 eleq1 
 |-  ( A = Z -> ( A e. Fin <-> Z e. Fin ) )
13 3 12 syl5ibcom 
 |-  ( ph -> ( A = Z -> Z e. Fin ) )
14 11 13 biimtrrid 
 |-  ( ph -> ( ( A C_ Z /\ Z C_ A ) -> Z e. Fin ) )
15 4 14 mpand 
 |-  ( ph -> ( Z C_ A -> Z e. Fin ) )
16 10 15 biimtrrid 
 |-  ( ph -> ( ( Z \ A ) = (/) -> Z e. Fin ) )
17 9 16 mtod 
 |-  ( ph -> -. ( Z \ A ) = (/) )
18 neq0 
 |-  ( -. ( Z \ A ) = (/) <-> E. x x e. ( Z \ A ) )
19 17 18 sylib 
 |-  ( ph -> E. x x e. ( Z \ A ) )
20 3 adantr 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> A e. Fin )
21 4 adantr 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> A C_ Z )
22 21 sselda 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. A ) -> k e. Z )
23 6 adantlr 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. Z ) -> B e. RR+ )
24 23 rpred 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. Z ) -> B e. RR )
25 22 24 syldan 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. A ) -> B e. RR )
26 20 25 fsumrecl 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. A B e. RR )
27 snfi 
 |-  { x } e. Fin
28 unfi 
 |-  ( ( A e. Fin /\ { x } e. Fin ) -> ( A u. { x } ) e. Fin )
29 20 27 28 sylancl 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> ( A u. { x } ) e. Fin )
30 eldifi 
 |-  ( x e. ( Z \ A ) -> x e. Z )
31 30 snssd 
 |-  ( x e. ( Z \ A ) -> { x } C_ Z )
32 4 31 anim12i 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> ( A C_ Z /\ { x } C_ Z ) )
33 unss 
 |-  ( ( A C_ Z /\ { x } C_ Z ) <-> ( A u. { x } ) C_ Z )
34 32 33 sylib 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> ( A u. { x } ) C_ Z )
35 34 sselda 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. ( A u. { x } ) ) -> k e. Z )
36 35 24 syldan 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. ( A u. { x } ) ) -> B e. RR )
37 29 36 fsumrecl 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. ( A u. { x } ) B e. RR )
38 2 adantr 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> M e. ZZ )
39 5 adantlr 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. Z ) -> ( F ` k ) = B )
40 7 adantr 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> seq M ( + , F ) e. dom ~~> )
41 1 38 39 24 40 isumrecl 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. Z B e. RR )
42 27 a1i 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> { x } e. Fin )
43 vex 
 |-  x e. _V
44 43 snnz 
 |-  { x } =/= (/)
45 44 a1i 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> { x } =/= (/) )
46 31 adantl 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> { x } C_ Z )
47 46 sselda 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. { x } ) -> k e. Z )
48 47 23 syldan 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. { x } ) -> B e. RR+ )
49 42 45 48 fsumrpcl 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. { x } B e. RR+ )
50 26 49 ltaddrpd 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. A B < ( sum_ k e. A B + sum_ k e. { x } B ) )
51 eldifn 
 |-  ( x e. ( Z \ A ) -> -. x e. A )
52 51 adantl 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> -. x e. A )
53 disjsn 
 |-  ( ( A i^i { x } ) = (/) <-> -. x e. A )
54 52 53 sylibr 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> ( A i^i { x } ) = (/) )
55 eqidd 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> ( A u. { x } ) = ( A u. { x } ) )
56 23 rpcnd 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. Z ) -> B e. CC )
57 35 56 syldan 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. ( A u. { x } ) ) -> B e. CC )
58 54 55 29 57 fsumsplit 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. ( A u. { x } ) B = ( sum_ k e. A B + sum_ k e. { x } B ) )
59 50 58 breqtrrd 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. A B < sum_ k e. ( A u. { x } ) B )
60 23 rpge0d 
 |-  ( ( ( ph /\ x e. ( Z \ A ) ) /\ k e. Z ) -> 0 <_ B )
61 1 38 29 34 39 24 60 40 isumless 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. ( A u. { x } ) B <_ sum_ k e. Z B )
62 26 37 41 59 61 ltletrd 
 |-  ( ( ph /\ x e. ( Z \ A ) ) -> sum_ k e. A B < sum_ k e. Z B )
63 19 62 exlimddv 
 |-  ( ph -> sum_ k e. A B < sum_ k e. Z B )