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 ⇝ )