Metamath Proof Explorer


Theorem fsumcvg3

Description: A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumcvg3.1 𝑍 = ( ℤ𝑀 )
fsumcvg3.2 ( 𝜑𝑀 ∈ ℤ )
fsumcvg3.3 ( 𝜑𝐴 ∈ Fin )
fsumcvg3.4 ( 𝜑𝐴𝑍 )
fsumcvg3.5 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 0 ) )
fsumcvg3.6 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
Assertion fsumcvg3 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 fsumcvg3.1 𝑍 = ( ℤ𝑀 )
2 fsumcvg3.2 ( 𝜑𝑀 ∈ ℤ )
3 fsumcvg3.3 ( 𝜑𝐴 ∈ Fin )
4 fsumcvg3.4 ( 𝜑𝐴𝑍 )
5 fsumcvg3.5 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 0 ) )
6 fsumcvg3.6 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
7 sseq1 ( 𝐴 = ∅ → ( 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ↔ ∅ ⊆ ( 𝑀 ... 𝑛 ) ) )
8 7 rexbidv ( 𝐴 = ∅ → ( ∃ 𝑛 ∈ ( ℤ𝑀 ) 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ↔ ∃ 𝑛 ∈ ( ℤ𝑀 ) ∅ ⊆ ( 𝑀 ... 𝑛 ) ) )
9 4 adantr ( ( 𝜑𝐴 ≠ ∅ ) → 𝐴𝑍 )
10 9 1 sseqtrdi ( ( 𝜑𝐴 ≠ ∅ ) → 𝐴 ⊆ ( ℤ𝑀 ) )
11 ltso < Or ℝ
12 3 adantr ( ( 𝜑𝐴 ≠ ∅ ) → 𝐴 ∈ Fin )
13 simpr ( ( 𝜑𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
14 uzssz ( ℤ𝑀 ) ⊆ ℤ
15 zssre ℤ ⊆ ℝ
16 14 15 sstri ( ℤ𝑀 ) ⊆ ℝ
17 1 16 eqsstri 𝑍 ⊆ ℝ
18 9 17 sstrdi ( ( 𝜑𝐴 ≠ ∅ ) → 𝐴 ⊆ ℝ )
19 12 13 18 3jca ( ( 𝜑𝐴 ≠ ∅ ) → ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ℝ ) )
20 fisupcl ( ( < Or ℝ ∧ ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐴 ⊆ ℝ ) ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
21 11 19 20 sylancr ( ( 𝜑𝐴 ≠ ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ 𝐴 )
22 10 21 sseldd ( ( 𝜑𝐴 ≠ ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ ( ℤ𝑀 ) )
23 fimaxre2 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → ∃ 𝑘 ∈ ℝ ∀ 𝑛𝐴 𝑛𝑘 )
24 18 12 23 syl2anc ( ( 𝜑𝐴 ≠ ∅ ) → ∃ 𝑘 ∈ ℝ ∀ 𝑛𝐴 𝑛𝑘 )
25 18 13 24 3jca ( ( 𝜑𝐴 ≠ ∅ ) → ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑛𝐴 𝑛𝑘 ) )
26 suprub ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑘 ∈ ℝ ∀ 𝑛𝐴 𝑛𝑘 ) ∧ 𝑘𝐴 ) → 𝑘 ≤ sup ( 𝐴 , ℝ , < ) )
27 25 26 sylan ( ( ( 𝜑𝐴 ≠ ∅ ) ∧ 𝑘𝐴 ) → 𝑘 ≤ sup ( 𝐴 , ℝ , < ) )
28 10 sselda ( ( ( 𝜑𝐴 ≠ ∅ ) ∧ 𝑘𝐴 ) → 𝑘 ∈ ( ℤ𝑀 ) )
29 14 22 sselid ( ( 𝜑𝐴 ≠ ∅ ) → sup ( 𝐴 , ℝ , < ) ∈ ℤ )
30 29 adantr ( ( ( 𝜑𝐴 ≠ ∅ ) ∧ 𝑘𝐴 ) → sup ( 𝐴 , ℝ , < ) ∈ ℤ )
31 elfz5 ( ( 𝑘 ∈ ( ℤ𝑀 ) ∧ sup ( 𝐴 , ℝ , < ) ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ↔ 𝑘 ≤ sup ( 𝐴 , ℝ , < ) ) )
32 28 30 31 syl2anc ( ( ( 𝜑𝐴 ≠ ∅ ) ∧ 𝑘𝐴 ) → ( 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ↔ 𝑘 ≤ sup ( 𝐴 , ℝ , < ) ) )
33 27 32 mpbird ( ( ( 𝜑𝐴 ≠ ∅ ) ∧ 𝑘𝐴 ) → 𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
34 33 ex ( ( 𝜑𝐴 ≠ ∅ ) → ( 𝑘𝐴𝑘 ∈ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) )
35 34 ssrdv ( ( 𝜑𝐴 ≠ ∅ ) → 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
36 oveq2 ( 𝑛 = sup ( 𝐴 , ℝ , < ) → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) )
37 36 sseq2d ( 𝑛 = sup ( 𝐴 , ℝ , < ) → ( 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ↔ 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) )
38 37 rspcev ( ( sup ( 𝐴 , ℝ , < ) ∈ ( ℤ𝑀 ) ∧ 𝐴 ⊆ ( 𝑀 ... sup ( 𝐴 , ℝ , < ) ) ) → ∃ 𝑛 ∈ ( ℤ𝑀 ) 𝐴 ⊆ ( 𝑀 ... 𝑛 ) )
39 22 35 38 syl2anc ( ( 𝜑𝐴 ≠ ∅ ) → ∃ 𝑛 ∈ ( ℤ𝑀 ) 𝐴 ⊆ ( 𝑀 ... 𝑛 ) )
40 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
41 2 40 syl ( 𝜑𝑀 ∈ ( ℤ𝑀 ) )
42 0ss ∅ ⊆ ( 𝑀 ... 𝑀 )
43 oveq2 ( 𝑛 = 𝑀 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑀 ) )
44 43 sseq2d ( 𝑛 = 𝑀 → ( ∅ ⊆ ( 𝑀 ... 𝑛 ) ↔ ∅ ⊆ ( 𝑀 ... 𝑀 ) ) )
45 44 rspcev ( ( 𝑀 ∈ ( ℤ𝑀 ) ∧ ∅ ⊆ ( 𝑀 ... 𝑀 ) ) → ∃ 𝑛 ∈ ( ℤ𝑀 ) ∅ ⊆ ( 𝑀 ... 𝑛 ) )
46 41 42 45 sylancl ( 𝜑 → ∃ 𝑛 ∈ ( ℤ𝑀 ) ∅ ⊆ ( 𝑀 ... 𝑛 ) )
47 8 39 46 pm2.61ne ( 𝜑 → ∃ 𝑛 ∈ ( ℤ𝑀 ) 𝐴 ⊆ ( 𝑀 ... 𝑛 ) )
48 1 eleq2i ( 𝑘𝑍𝑘 ∈ ( ℤ𝑀 ) )
49 48 5 sylan2br ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 0 ) )
50 49 adantlr ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ𝑀 ) ∧ 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ) ) ∧ 𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝐹𝑘 ) = if ( 𝑘𝐴 , 𝐵 , 0 ) )
51 simprl ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ𝑀 ) ∧ 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ) ) → 𝑛 ∈ ( ℤ𝑀 ) )
52 6 adantlr ( ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ𝑀 ) ∧ 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ) ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ℂ )
53 simprr ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ𝑀 ) ∧ 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ) ) → 𝐴 ⊆ ( 𝑀 ... 𝑛 ) )
54 50 51 52 53 fsumcvg2 ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ𝑀 ) ∧ 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ) ) → seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) )
55 climrel Rel ⇝
56 55 releldmi ( seq 𝑀 ( + , 𝐹 ) ⇝ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
57 54 56 syl ( ( 𝜑 ∧ ( 𝑛 ∈ ( ℤ𝑀 ) ∧ 𝐴 ⊆ ( 𝑀 ... 𝑛 ) ) ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
58 47 57 rexlimddv ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )