Metamath Proof Explorer

Theorem esumpcvgval

Description: The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017)

Ref Expression
Hypotheses esumpcvgval.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
esumpcvgval.2 ⊢ ( 𝑘 = 𝑙 → 𝐴 = 𝐵 )
esumpcvgval.3 ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ )
Assertion esumpcvgval ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = Σ 𝑘 ∈ ℕ 𝐴 )

Proof

Step Hyp Ref Expression
1 esumpcvgval.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
2 esumpcvgval.2 ⊢ ( 𝑘 = 𝑙 → 𝐴 = 𝐵 )
3 esumpcvgval.3 ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ dom ⇝ )
4 xrltso ⊢ < Or ℝ*
5 4 a1i ⊢ ( 𝜑 → < Or ℝ* )
6 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
7 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
8 eqcom ⊢ ( 𝑘 = 𝑙 ↔ 𝑙 = 𝑘 )
9 eqcom ⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
10 2 8 9 3imtr3i ⊢ ( 𝑙 = 𝑘 → 𝐵 = 𝐴 )
11 10 cbvmptv ⊢ ( 𝑙 ∈ ℕ ↦ 𝐵 ) = ( 𝑘 ∈ ℕ ↦ 𝐴 )
12 1 11 fmptd ⊢ ( 𝜑 → ( 𝑙 ∈ ℕ ↦ 𝐵 ) : ℕ ⟶ ( 0 [,) +∞ ) )
13 12 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
14 elrege0 ⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ) )
15 14 simplbi ⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ℝ )
16 13 15 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑥 ) ∈ ℝ )
17 6 7 16 serfre ⊢ ( 𝜑 → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) : ℕ ⟶ ℝ )
18 12 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑙 ∈ ℕ ↦ 𝐵 ) : ℕ ⟶ ( 0 [,) +∞ ) )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
20 19 peano2nnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
21 18 20 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,) +∞ ) )
22 elrege0 ⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) )
23 22 simprbi ⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) )
24 21 23 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) )
25 17 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ∈ ℝ )
26 22 simplbi ⊢ ( ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ( 0 [,) +∞ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
27 21 26 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
28 25 27 addge01d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 ≤ ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ↔ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) + ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) ) )
29 24 28 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) + ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) )
30 19 6 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
31 seqp1 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) + ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) = ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) + ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ ( 𝑛 + 1 ) ) ) )
33 29 32 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ ( 𝑛 + 1 ) ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
35 11 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝐴 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
36 34 1 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
37 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
38 37 1 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ )
39 17 feqmptd ⊢ ( 𝜑 → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) )
40 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝜑 )
41 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) → 𝑘 ∈ ℕ )
42 41 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
43 40 42 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
44 38 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℂ )
45 40 42 44 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ℂ )
46 43 30 45 fsumser ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
47 46 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
48 47 mpteq2dva ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
49 39 48 eqtr2d ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) )
50 49 3 eqeltrrd ⊢ ( 𝜑 → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ∈ dom ⇝ )
51 6 7 36 38 50 isumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ 𝐴 ∈ ℝ )
52 1zzd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℤ )
53 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
54 fzssuz ⊢ ( 1 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 1 )
55 54 6 sseqtrri ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
56 55 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ )
57 36 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
58 38 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ )
59 1 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
60 elrege0 ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
61 60 simprbi ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝐴 )
62 59 61 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ 𝐴 )
63 50 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ∈ dom ⇝ )
64 6 52 53 56 57 58 62 63 isumless ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ≤ Σ 𝑘 ∈ ℕ 𝐴 )
65 46 64 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ Σ 𝑘 ∈ ℕ 𝐴 )
66 65 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ Σ 𝑘 ∈ ℕ 𝐴 )
67 brralrspcev ⊢ ( ( Σ 𝑘 ∈ ℕ 𝐴 ∈ ℝ ∧ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ Σ 𝑘 ∈ ℕ 𝐴 ) → ∃ 𝑠 ∈ ℝ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 )
68 51 66 67 syl2anc ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℝ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 )
69 6 7 17 33 68 climsup ⊢ ( 𝜑 → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⇝ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
70 6 7 69 25 climrecl ⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ )
71 70 rexrd ⊢ ( 𝜑 → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ* )
72 eqid ⊢ ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) = ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 )
73 sumex ⊢ Σ 𝑘 ∈ 𝑏 𝐴 ∈ V
74 72 73 elrnmpti ⊢ ( 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ↔ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 )
75 ssnnssfz ⊢ ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) → ∃ 𝑚 ∈ ℕ 𝑏 ⊆ ( 1 ... 𝑚 ) )
76 fzfid ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) → ( 1 ... 𝑚 ) ∈ Fin )
77 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑚 ) → 𝑘 ∈ ℕ )
78 77 1 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ( 0 [,) +∞ ) )
79 60 simplbi ⊢ ( 𝐴 ∈ ( 0 [,) +∞ ) → 𝐴 ∈ ℝ )
80 78 79 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ℝ )
81 80 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ℝ )
82 78 61 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 0 ≤ 𝐴 )
83 82 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 0 ≤ 𝐴 )
84 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) → 𝑏 ⊆ ( 1 ... 𝑚 ) )
85 76 81 83 84 fsumless ⊢ ( ( 𝜑 ∧ 𝑏 ⊆ ( 1 ... 𝑚 ) ) → Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 )
86 85 ex ⊢ ( 𝜑 → ( 𝑏 ⊆ ( 1 ... 𝑚 ) → Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) )
87 86 reximdv ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ 𝑏 ⊆ ( 1 ... 𝑚 ) → ∃ 𝑚 ∈ ℕ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) )
88 87 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑚 ∈ ℕ 𝑏 ⊆ ( 1 ... 𝑚 ) ) → ∃ 𝑚 ∈ ℕ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 )
89 75 88 sylan2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ∃ 𝑚 ∈ ℕ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 )
90 breq1 ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 → ( 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ↔ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) )
91 90 rexbidv ⊢ ( 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 → ( ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ↔ ∃ 𝑚 ∈ ℕ Σ 𝑘 ∈ 𝑏 𝐴 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) )
92 89 91 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 → ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) )
93 92 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 → ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) )
94 93 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 )
95 74 94 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → ∃ 𝑚 ∈ ℕ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 )
96 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 )
97 inss2 ⊢ ( 𝒫 ℕ ∩ Fin ) ⊆ Fin
98 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) )
99 97 98 sselid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑏 ∈ Fin )
100 simpll ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝜑 )
101 inss1 ⊢ ( 𝒫 ℕ ∩ Fin ) ⊆ 𝒫 ℕ
102 simplr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) )
103 101 102 sselid ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑏 ∈ 𝒫 ℕ )
104 103 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑏 ⊆ ℕ )
105 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑘 ∈ 𝑏 )
106 104 105 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝑘 ∈ ℕ )
107 100 106 1 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
108 107 79 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝐴 ∈ ℝ )
109 99 108 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → Σ 𝑘 ∈ 𝑏 𝐴 ∈ ℝ )
110 109 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → Σ 𝑘 ∈ 𝑏 𝐴 ∈ ℝ )
111 96 110 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → 𝑥 ∈ ℝ )
112 111 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑥 = Σ 𝑘 ∈ 𝑏 𝐴 ) → 𝑥 ∈ ℝ )
113 74 112 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → 𝑥 ∈ ℝ )
114 113 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → 𝑥 ∈ ℝ )
115 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑚 ) ∈ Fin )
116 115 80 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ℝ )
117 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ℝ )
118 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ )
119 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 )
120 17 frnd ⊢ ( 𝜑 → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ )
121 120 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ )
122 1nn ⊢ 1 ∈ ℕ
123 122 ne0ii ⊢ ℕ ≠ ∅
124 dm0rn0 ⊢ ( dom seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ∅ ↔ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ∅ )
125 17 fdmd ⊢ ( 𝜑 → dom seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ℕ )
126 125 eqeq1d ⊢ ( 𝜑 → ( dom seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ∅ ↔ ℕ = ∅ ) )
127 124 126 bitr3id ⊢ ( 𝜑 → ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ∅ ↔ ℕ = ∅ ) )
128 127 necon3bid ⊢ ( 𝜑 → ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ↔ ℕ ≠ ∅ ) )
129 123 128 mpbiri ⊢ ( 𝜑 → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ )
130 129 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ )
131 1z ⊢ 1 ∈ ℤ
132 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 ) )
133 131 132 ax-mp ⊢ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 )
134 6 fneq2i ⊢ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ( ℤ≥ ‘ 1 ) )
135 133 134 mpbir ⊢ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ
136 dffn5 ⊢ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) Fn ℕ ↔ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) )
137 135 136 mpbi ⊢ seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
138 fvex ⊢ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ∈ V
139 137 138 elrnmpti ⊢ ( 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
140 r19.29 ⊢ ( ( ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ ∃ 𝑛 ∈ ℕ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → ∃ 𝑛 ∈ ℕ ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) )
141 breq1 ⊢ ( 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) → ( 𝑧 ≤ 𝑠 ↔ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ) )
142 141 biimparc ⊢ ( ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑧 ≤ 𝑠 )
143 142 rexlimivw ⊢ ( ∃ 𝑛 ∈ ℕ ( ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑧 ≤ 𝑠 )
144 140 143 syl ⊢ ( ( ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ ∃ 𝑛 ∈ ℕ 𝑧 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑧 ≤ 𝑠 )
145 139 144 sylan2b ⊢ ( ( ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 ∧ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ) → 𝑧 ≤ 𝑠 )
146 145 ralrimiva ⊢ ( ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 → ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 )
147 146 reximi ⊢ ( ∃ 𝑠 ∈ ℝ ∀ 𝑛 ∈ ℕ ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ≤ 𝑠 → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 )
148 68 147 syl ⊢ ( 𝜑 → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 )
149 148 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 )
150 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
151 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝜑 )
152 77 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝑘 ∈ ℕ )
153 151 152 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑙 ∈ ℕ ↦ 𝐵 ) ‘ 𝑘 ) = 𝐴 )
154 150 6 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) )
155 151 152 1 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ( 0 [,) +∞ ) )
156 155 79 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ℝ )
157 156 recnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑚 ) ) → 𝐴 ∈ ℂ )
158 153 154 157 fsumser ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑚 ) )
159 fveq2 ⊢ ( 𝑛 = 𝑚 → ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑚 ) )
160 159 rspceeqv ⊢ ( ( 𝑚 ∈ ℕ ∧ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑚 ) ) → ∃ 𝑛 ∈ ℕ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
161 150 158 160 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ∃ 𝑛 ∈ ℕ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
162 137 138 elrnmpti ⊢ ( Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ↔ ∃ 𝑛 ∈ ℕ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
163 161 162 sylibr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) )
164 163 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) )
165 suprub ⊢ ( ( ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) ∧ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
166 121 130 149 164 165 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
167 114 117 118 119 166 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑥 ≤ Σ 𝑘 ∈ ( 1 ... 𝑚 ) 𝐴 ) ) → 𝑥 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
168 95 167 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → 𝑥 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
169 70 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ )
170 113 169 lenltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → ( 𝑥 ≤ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ ¬ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) < 𝑥 ) )
171 168 170 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) → ¬ sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) < 𝑥 )
172 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ∧ 0 ≤ 𝑥 ∧ 𝑥 = +∞ ) ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
173 172 3anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
174 71 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ* )
175 pnfnlt ⊢ ( sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ∈ ℝ* → ¬ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
176 174 175 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → ¬ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
177 breq1 ⊢ ( 𝑥 = +∞ → ( 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) )
178 177 notbid ⊢ ( 𝑥 = +∞ → ( ¬ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ ¬ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) )
179 178 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → ( ¬ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ ¬ +∞ < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) )
180 176 179 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → ¬ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
181 173 180 pm2.21dd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 = +∞ ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
182 simplll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝜑 )
183 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) → 𝑥 ∈ ℝ* )
184 183 3anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝑥 ∈ ℝ* )
185 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 0 ≤ 𝑥 )
186 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝑥 < +∞ )
187 0xr ⊢ 0 ∈ ℝ*
188 pnfxr ⊢ +∞ ∈ ℝ*
189 elico1 ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) )
190 187 188 189 mp2an ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) )
191 184 185 186 190 syl3anbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝑥 ∈ ( 0 [,) +∞ ) )
192 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ∧ 0 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
193 192 3anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
194 120 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ )
195 129 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ )
196 148 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 )
197 194 195 196 3jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) )
198 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → 𝑥 ∈ ( 0 [,) +∞ ) )
199 37 198 sselid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → 𝑥 ∈ ℝ )
200 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
201 suprlub ⊢ ( ( ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ↔ ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 ) )
202 201 biimpa ⊢ ( ( ( ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ℝ ∧ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ≠ ∅ ∧ ∃ 𝑠 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑧 ≤ 𝑠 ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) → ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 )
203 197 199 200 202 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 )
204 41 ssriv ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
205 ovex ⊢ ( 1 ... 𝑛 ) ∈ V
206 205 elpw ⊢ ( ( 1 ... 𝑛 ) ∈ 𝒫 ℕ ↔ ( 1 ... 𝑛 ) ⊆ ℕ )
207 204 206 mpbir ⊢ ( 1 ... 𝑛 ) ∈ 𝒫 ℕ
208 fzfi ⊢ ( 1 ... 𝑛 ) ∈ Fin
209 elin ⊢ ( ( 1 ... 𝑛 ) ∈ ( 𝒫 ℕ ∩ Fin ) ↔ ( ( 1 ... 𝑛 ) ∈ 𝒫 ℕ ∧ ( 1 ... 𝑛 ) ∈ Fin ) )
210 207 208 209 mpbir2an ⊢ ( 1 ... 𝑛 ) ∈ ( 𝒫 ℕ ∩ Fin )
211 210 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → ( 1 ... 𝑛 ) ∈ ( 𝒫 ℕ ∩ Fin ) )
212 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
213 46 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
214 212 213 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → 𝑦 = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
215 sumeq1 ⊢ ( 𝑏 = ( 1 ... 𝑛 ) → Σ 𝑘 ∈ 𝑏 𝐴 = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
216 215 rspceeqv ⊢ ( ( ( 1 ... 𝑛 ) ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 𝑦 = Σ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 )
217 211 214 216 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 )
218 217 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 ) )
219 218 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 ) )
220 137 138 elrnmpti ⊢ ( 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = ( seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ‘ 𝑛 ) )
221 72 73 elrnmpti ⊢ ( 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ↔ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 𝑦 = Σ 𝑘 ∈ 𝑏 𝐴 )
222 219 220 221 3imtr4g ⊢ ( 𝜑 → ( 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) → 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ) )
223 222 ssrdv ⊢ ( 𝜑 → ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) )
224 ssrexv ⊢ ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) ⊆ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) → ( ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) )
225 223 224 syl ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 ) )
226 225 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑦 ∈ ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) 𝑥 < 𝑦 ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
227 203 226 syldan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
228 182 191 193 227 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) ∧ 𝑥 < +∞ ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
229 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
230 xrlelttric ⊢ ( ( +∞ ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( +∞ ≤ 𝑥 ∨ 𝑥 < +∞ ) )
231 188 230 mpan ⊢ ( 𝑥 ∈ ℝ* → ( +∞ ≤ 𝑥 ∨ 𝑥 < +∞ ) )
232 xgepnf ⊢ ( 𝑥 ∈ ℝ* → ( +∞ ≤ 𝑥 ↔ 𝑥 = +∞ ) )
233 232 orbi1d ⊢ ( 𝑥 ∈ ℝ* → ( ( +∞ ≤ 𝑥 ∨ 𝑥 < +∞ ) ↔ ( 𝑥 = +∞ ∨ 𝑥 < +∞ ) ) )
234 231 233 mpbid ⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 = +∞ ∨ 𝑥 < +∞ ) )
235 229 234 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) → ( 𝑥 = +∞ ∨ 𝑥 < +∞ ) )
236 181 228 235 mpjaodan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 0 ≤ 𝑥 ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
237 0elpw ⊢ ∅ ∈ 𝒫 ℕ
238 0fi ⊢ ∅ ∈ Fin
239 elin ⊢ ( ∅ ∈ ( 𝒫 ℕ ∩ Fin ) ↔ ( ∅ ∈ 𝒫 ℕ ∧ ∅ ∈ Fin ) )
240 237 238 239 mpbir2an ⊢ ∅ ∈ ( 𝒫 ℕ ∩ Fin )
241 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐴 = 0
242 241 eqcomi ⊢ 0 = Σ 𝑘 ∈ ∅ 𝐴
243 sumeq1 ⊢ ( 𝑏 = ∅ → Σ 𝑘 ∈ 𝑏 𝐴 = Σ 𝑘 ∈ ∅ 𝐴 )
244 243 rspceeqv ⊢ ( ( ∅ ∈ ( 𝒫 ℕ ∩ Fin ) ∧ 0 = Σ 𝑘 ∈ ∅ 𝐴 ) → ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 0 = Σ 𝑘 ∈ 𝑏 𝐴 )
245 240 242 244 mp2an ⊢ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 0 = Σ 𝑘 ∈ 𝑏 𝐴
246 72 73 elrnmpti ⊢ ( 0 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ↔ ∃ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) 0 = Σ 𝑘 ∈ 𝑏 𝐴 )
247 245 246 mpbir ⊢ 0 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 )
248 breq2 ⊢ ( 𝑦 = 0 → ( 𝑥 < 𝑦 ↔ 𝑥 < 0 ) )
249 248 rspcev ⊢ ( ( 0 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) ∧ 𝑥 < 0 ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
250 247 249 mpan ⊢ ( 𝑥 < 0 → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
251 250 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) ∧ 𝑥 < 0 ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
252 xrlelttric ⊢ ( ( 0 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 0 ≤ 𝑥 ∨ 𝑥 < 0 ) )
253 187 252 mpan ⊢ ( 𝑥 ∈ ℝ* → ( 0 ≤ 𝑥 ∨ 𝑥 < 0 ) )
254 253 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ( 0 ≤ 𝑥 ∨ 𝑥 < 0 ) )
255 236 251 254 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 𝑥 < sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) ) ) → ∃ 𝑦 ∈ ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) 𝑥 < 𝑦 )
256 5 71 171 255 eqsupd ⊢ ( 𝜑 → sup ( ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) , ℝ* , < ) = sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
257 nfv ⊢ Ⅎ 𝑘 𝜑
258 nfcv ⊢ Ⅎ 𝑘 ℕ
259 nnex ⊢ ℕ ∈ V
260 259 a1i ⊢ ( 𝜑 → ℕ ∈ V )
261 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
262 261 1 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
263 elex ⊢ ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) → 𝑏 ∈ V )
264 263 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → 𝑏 ∈ V )
265 107 fmpttd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) : 𝑏 ⟶ ( 0 [,) +∞ ) )
266 esumpfinvallem ⊢ ( ( 𝑏 ∈ V ∧ ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) : 𝑏 ⟶ ( 0 [,) +∞ ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) )
267 264 265 266 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) )
268 108 recnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) ∧ 𝑘 ∈ 𝑏 ) → 𝐴 ∈ ℂ )
269 99 268 gsumfsum ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ℂfld Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) = Σ 𝑘 ∈ 𝑏 𝐴 )
270 267 269 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑏 ↦ 𝐴 ) ) = Σ 𝑘 ∈ 𝑏 𝐴 )
271 257 258 260 262 270 esumval ⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = sup ( ran ( 𝑏 ∈ ( 𝒫 ℕ ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑏 𝐴 ) , ℝ* , < ) )
272 6 7 36 44 69 isumclim ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ 𝐴 = sup ( ran seq 1 ( + , ( 𝑙 ∈ ℕ ↦ 𝐵 ) ) , ℝ , < ) )
273 256 271 272 3eqtr4d ⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = Σ 𝑘 ∈ ℕ 𝐴 )