Metamath Proof Explorer

Theorem sge0isum

Description: If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0isum.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
sge0isum.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
sge0isum.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( 0 [,) +∞ ) )
sge0isum.g ⊢ 𝐺 = seq 𝑀 ( + , 𝐹 )
sge0isum.gcnv ⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
Assertion sge0isum ( 𝜑 → ( Σ^ ‘ 𝐹 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 sge0isum.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 sge0isum.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 sge0isum.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( 0 [,) +∞ ) )
4 sge0isum.g ⊢ 𝐺 = seq 𝑀 ( + , 𝐹 )
5 sge0isum.gcnv ⊢ ( 𝜑 → 𝐺 ⇝ 𝐵 )
6 2 fvexi ⊢ 𝑍 ∈ V
7 6 a1i ⊢ ( 𝜑 → 𝑍 ∈ V )
8 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
9 8 a1i ⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) )
10 3 9 fssd ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( 0 [,] +∞ ) )
11 7 10 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )
12 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
13 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
14 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,) +∞ ) )
15 13 14 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
16 0xr ⊢ 0 ∈ ℝ*
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ∈ ℝ* )
18 pnfxr ⊢ +∞ ∈ ℝ*
19 18 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → +∞ ∈ ℝ* )
20 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,) +∞ ) ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
21 17 19 14 20 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
22 seqex ⊢ seq 𝑀 ( + , 𝐹 ) ∈ V
23 4 22 eqeltri ⊢ 𝐺 ∈ V
24 23 a1i ⊢ ( 𝜑 → 𝐺 ∈ V )
25 climcl ⊢ ( 𝐺 ⇝ 𝐵 → 𝐵 ∈ ℂ )
26 5 25 syl ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
27 breldmg ⊢ ( ( 𝐺 ∈ V ∧ 𝐵 ∈ ℂ ∧ 𝐺 ⇝ 𝐵 ) → 𝐺 ∈ dom ⇝ )
28 24 26 5 27 syl3anc ⊢ ( 𝜑 → 𝐺 ∈ dom ⇝ )
29 4 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐺 = seq 𝑀 ( + , 𝐹 ) )
30 29 fveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) )
31 2 eleq2i ⊢ ( 𝑗 ∈ 𝑍 ↔ 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
32 31 bilani ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
33 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → 𝜑 )
34 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
35 34 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
36 35 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → 𝑘 ∈ 𝑍 )
37 33 36 15 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
38 readdcl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ ) → ( 𝑘 + 𝑖 ) ∈ ℝ )
39 38 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ ) ) → ( 𝑘 + 𝑖 ) ∈ ℝ )
40 32 37 39 seqcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
41 30 40 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℝ )
42 41 recnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℂ )
43 42 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ∈ ℂ )
44 2 climbdd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐺 ∈ dom ⇝ ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ∈ ℂ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 )
45 1 28 43 44 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 )
46 41 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℝ )
47 42 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 ) → ( 𝐺 ‘ 𝑗 ) ∈ ℂ )
48 47 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 ) → ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ∈ ℝ )
49 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 ) → 𝑥 ∈ ℝ )
50 46 leabsd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 ) → ( 𝐺 ‘ 𝑗 ) ≤ ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) )
51 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 ) → ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 )
52 46 48 49 50 51 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 ) → ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
53 52 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 → ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) )
54 53 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 → ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) )
55 54 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( abs ‘ ( 𝐺 ‘ 𝑗 ) ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) )
56 45 55 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
57 2 4 1 12 15 21 56 isumsup2 ⊢ ( 𝜑 → 𝐺 ⇝ sup ( ran 𝐺 , ℝ , < ) )
58 2 1 57 41 climrecl ⊢ ( 𝜑 → sup ( ran 𝐺 , ℝ , < ) ∈ ℝ )
59 58 rexrd ⊢ ( 𝜑 → sup ( ran 𝐺 , ℝ , < ) ∈ ℝ* )
60 3 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) )
61 60 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
62 mpteq1 ⊢ ( 𝑦 = ∅ → ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) )
63 62 fveq2d ⊢ ( 𝑦 = ∅ → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
64 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) = ∅
65 64 fveq2i ⊢ ( Σ^ ‘ ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( Σ^ ‘ ∅ )
66 sge00 ⊢ ( Σ^ ‘ ∅ ) = 0
67 65 66 eqtri ⊢ ( Σ^ ‘ ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0
68 67 a1i ⊢ ( 𝑦 = ∅ → ( Σ^ ‘ ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 )
69 63 68 eqtrd ⊢ ( 𝑦 = ∅ → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 )
70 69 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = 0 )
71 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
72 38 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ ) ) → ( 𝑘 + 𝑖 ) ∈ ℝ )
73 2 1 15 72 seqf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
74 4 a1i ⊢ ( 𝜑 → 𝐺 = seq 𝑀 ( + , 𝐹 ) )
75 74 feq1d ⊢ ( 𝜑 → ( 𝐺 : 𝑍 ⟶ ℝ ↔ seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ ) )
76 73 75 mpbird ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ ℝ )
77 76 frnd ⊢ ( 𝜑 → ran 𝐺 ⊆ ℝ )
78 76 ffund ⊢ ( 𝜑 → Fun 𝐺 )
79 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
80 1 79 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
81 2 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
82 80 81 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
83 76 fdmd ⊢ ( 𝜑 → dom 𝐺 = 𝑍 )
84 83 eqcomd ⊢ ( 𝜑 → 𝑍 = dom 𝐺 )
85 82 84 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ dom 𝐺 )
86 fvelrn ⊢ ( ( Fun 𝐺 ∧ 𝑀 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑀 ) ∈ ran 𝐺 )
87 78 85 86 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) ∈ ran 𝐺 )
88 77 87 sseldd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) ∈ ℝ )
89 16 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
90 18 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
91 3 82 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ ( 0 [,) +∞ ) )
92 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐹 ‘ 𝑀 ) ∈ ( 0 [,) +∞ ) ) → 0 ≤ ( 𝐹 ‘ 𝑀 ) )
93 89 90 91 92 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝐹 ‘ 𝑀 ) )
94 4 fveq1i ⊢ ( 𝐺 ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 )
95 94 a1i ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) )
96 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
97 1 96 syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
98 95 97 eqtr2d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
99 93 98 breqtrd ⊢ ( 𝜑 → 0 ≤ ( 𝐺 ‘ 𝑀 ) )
100 87 ne0d ⊢ ( 𝜑 → ran 𝐺 ≠ ∅ )
101 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ∈ ran 𝐺 )
102 76 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑍 )
103 fvelrnb ⊢ ( 𝐺 Fn 𝑍 → ( 𝑧 ∈ ran 𝐺 ↔ ∃ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) = 𝑧 ) )
104 102 103 syl ⊢ ( 𝜑 → ( 𝑧 ∈ ran 𝐺 ↔ ∃ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) = 𝑧 ) )
105 104 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑧 ∈ ran 𝐺 ↔ ∃ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) = 𝑧 ) )
106 101 105 mpbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ∃ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) = 𝑧 )
107 106 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑧 ∈ ran 𝐺 ) → ∃ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) = 𝑧 )
108 nfv ⊢ Ⅎ 𝑗 𝜑
109 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥
110 108 109 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
111 nfv ⊢ Ⅎ 𝑗 𝑧 ∈ ran 𝐺
112 110 111 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑧 ∈ ran 𝐺 )
113 nfv ⊢ Ⅎ 𝑗 𝑧 ≤ 𝑥
114 rspa ⊢ ( ( ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
115 114 3adant3 ⊢ ( ( ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
116 simp3 ⊢ ( ( ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( 𝐺 ‘ 𝑗 ) = 𝑧 )
117 id ⊢ ( ( 𝐺 ‘ 𝑗 ) = 𝑧 → ( 𝐺 ‘ 𝑗 ) = 𝑧 )
118 117 eqcomd ⊢ ( ( 𝐺 ‘ 𝑗 ) = 𝑧 → 𝑧 = ( 𝐺 ‘ 𝑗 ) )
119 118 adantl ⊢ ( ( ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → 𝑧 = ( 𝐺 ‘ 𝑗 ) )
120 simpl ⊢ ( ( ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
121 119 120 eqbrtrd ⊢ ( ( ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → 𝑧 ≤ 𝑥 )
122 115 116 121 syl2anc ⊢ ( ( ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → 𝑧 ≤ 𝑥 )
123 122 3exp ⊢ ( ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 → ( 𝑗 ∈ 𝑍 → ( ( 𝐺 ‘ 𝑗 ) = 𝑧 → 𝑧 ≤ 𝑥 ) ) )
124 123 ad2antlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑗 ∈ 𝑍 → ( ( 𝐺 ‘ 𝑗 ) = 𝑧 → 𝑧 ≤ 𝑥 ) ) )
125 112 113 124 rexlimd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑧 ∈ ran 𝐺 ) → ( ∃ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) = 𝑧 → 𝑧 ≤ 𝑥 ) )
126 107 125 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ≤ 𝑥 )
127 126 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 )
128 127 ex ⊢ ( 𝜑 → ( ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 → ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 ) )
129 128 reximdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 ) )
130 56 129 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 )
131 suprub ⊢ ( ( ( ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 ) ∧ ( 𝐺 ‘ 𝑀 ) ∈ ran 𝐺 ) → ( 𝐺 ‘ 𝑀 ) ≤ sup ( ran 𝐺 , ℝ , < ) )
132 77 100 130 87 131 syl31anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) ≤ sup ( ran 𝐺 , ℝ , < ) )
133 71 88 58 99 132 letrd ⊢ ( 𝜑 → 0 ≤ sup ( ran 𝐺 , ℝ , < ) )
134 133 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑦 = ∅ ) → 0 ≤ sup ( ran 𝐺 , ℝ , < ) )
135 70 134 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) )
136 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) )
137 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝜑 )
138 elpwinss ⊢ ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑦 ⊆ 𝑍 )
139 138 sselda ⊢ ( ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝑍 )
140 139 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝑍 )
141 8 14 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) )
142 137 140 141 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) )
143 eqid ⊢ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) )
144 142 143 fmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) : 𝑦 ⟶ ( 0 [,] +∞ ) )
145 136 144 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ* )
146 145 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ* )
147 fzfid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ∈ Fin )
148 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
149 148 81 eleqtrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) → 𝑘 ∈ 𝑍 )
150 149 141 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) )
151 eqid ⊢ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) )
152 150 151 fmptd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) : ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ⟶ ( 0 [,] +∞ ) )
153 152 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) : ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ⟶ ( 0 [,] +∞ ) )
154 147 153 sge0xrcl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ* )
155 154 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ* )
156 59 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → sup ( ran 𝐺 , ℝ , < ) ∈ ℝ* )
157 156 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → sup ( ran 𝐺 , ℝ , < ) ∈ ℝ* )
158 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ) → 𝜑 )
159 149 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ) → 𝑘 ∈ 𝑍 )
160 158 159 141 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,] +∞ ) )
161 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑦 ∈ Fin )
162 2 138 161 ssuzfz ⊢ ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑦 ⊆ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) )
163 162 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑦 ⊆ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) )
164 147 160 163 sge0lessmpt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
165 164 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
166 77 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ran 𝐺 ⊆ ℝ )
167 166 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ran 𝐺 ⊆ ℝ )
168 100 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ran 𝐺 ≠ ∅ )
169 168 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ran 𝐺 ≠ ∅ )
170 130 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 )
171 170 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 )
172 158 159 14 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,) +∞ ) )
173 147 172 sge0fsummpt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ( 𝐹 ‘ 𝑘 ) )
174 173 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ( 𝐹 ‘ 𝑘 ) )
175 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) ∧ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
176 138 2 sseqtrdi ⊢ ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑦 ⊆ ( ℤ≥ ‘ 𝑀 ) )
177 176 adantr ⊢ ( ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 ⊆ ( ℤ≥ ‘ 𝑀 ) )
178 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
179 2 178 eqsstri ⊢ 𝑍 ⊆ ℤ
180 138 179 sstrdi ⊢ ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑦 ⊆ ℤ )
181 180 adantr ⊢ ( ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 ⊆ ℤ )
182 neqne ⊢ ( ¬ 𝑦 = ∅ → 𝑦 ≠ ∅ )
183 182 adantl ⊢ ( ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 ≠ ∅ )
184 161 adantr ⊢ ( ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 ∈ Fin )
185 suprfinzcl ⊢ ( ( 𝑦 ⊆ ℤ ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin ) → sup ( 𝑦 , ℝ , < ) ∈ 𝑦 )
186 181 183 184 185 syl3anc ⊢ ( ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ¬ 𝑦 = ∅ ) → sup ( 𝑦 , ℝ , < ) ∈ 𝑦 )
187 177 186 sseldd ⊢ ( ( 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ ¬ 𝑦 = ∅ ) → sup ( 𝑦 , ℝ , < ) ∈ ( ℤ≥ ‘ 𝑀 ) )
188 187 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → sup ( 𝑦 , ℝ , < ) ∈ ( ℤ≥ ‘ 𝑀 ) )
189 15 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
190 158 159 189 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
191 190 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) ∧ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
192 175 188 191 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → Σ 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ sup ( 𝑦 , ℝ , < ) ) )
193 4 eqcomi ⊢ seq 𝑀 ( + , 𝐹 ) = 𝐺
194 193 fveq1i ⊢ ( seq 𝑀 ( + , 𝐹 ) ‘ sup ( 𝑦 , ℝ , < ) ) = ( 𝐺 ‘ sup ( 𝑦 , ℝ , < ) )
195 194 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( seq 𝑀 ( + , 𝐹 ) ‘ sup ( 𝑦 , ℝ , < ) ) = ( 𝐺 ‘ sup ( 𝑦 , ℝ , < ) ) )
196 174 192 195 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝐺 ‘ sup ( 𝑦 , ℝ , < ) ) )
197 78 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Fun 𝐺 )
198 197 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → Fun 𝐺 )
199 188 81 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → sup ( 𝑦 , ℝ , < ) ∈ 𝑍 )
200 84 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → 𝑍 = dom 𝐺 )
201 199 200 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → sup ( 𝑦 , ℝ , < ) ∈ dom 𝐺 )
202 fvelrn ⊢ ( ( Fun 𝐺 ∧ sup ( 𝑦 , ℝ , < ) ∈ dom 𝐺 ) → ( 𝐺 ‘ sup ( 𝑦 , ℝ , < ) ) ∈ ran 𝐺 )
203 198 201 202 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( 𝐺 ‘ sup ( 𝑦 , ℝ , < ) ) ∈ ran 𝐺 )
204 196 203 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ran 𝐺 )
205 suprub ⊢ ( ( ( ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ran 𝐺 ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) )
206 167 169 171 204 205 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... sup ( 𝑦 , ℝ , < ) ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) )
207 146 155 157 165 206 xrletrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ¬ 𝑦 = ∅ ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) )
208 135 207 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) )
209 208 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) )
210 nfv ⊢ Ⅎ 𝑘 𝜑
211 210 7 141 59 sge0lefimpt ⊢ ( 𝜑 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) ↔ ∀ 𝑦 ∈ ( 𝒫 𝑍 ∩ Fin ) ( Σ^ ‘ ( 𝑘 ∈ 𝑦 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) ) )
212 209 211 mpbird ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ sup ( ran 𝐺 , ℝ , < ) )
213 61 212 eqbrtrd ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≤ sup ( ran 𝐺 , ℝ , < ) )
214 35 ssriv ⊢ ( 𝑀 ... 𝑗 ) ⊆ 𝑍
215 214 a1i ⊢ ( 𝜑 → ( 𝑀 ... 𝑗 ) ⊆ 𝑍 )
216 7 141 215 sge0lessmpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
217 216 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
218 fzfid ⊢ ( 𝜑 → ( 𝑀 ... 𝑗 ) ∈ Fin )
219 35 14 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 0 [,) +∞ ) )
220 218 219 sge0fsummpt ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐹 ‘ 𝑘 ) )
221 220 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐹 ‘ 𝑘 ) )
222 33 36 12 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
223 33 36 189 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
224 222 32 223 fsumser ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐹 ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) )
225 224 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐹 ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) )
226 221 225 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) )
227 193 fveq1i ⊢ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 )
228 227 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( 𝐺 ‘ 𝑗 ) )
229 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( 𝐺 ‘ 𝑗 ) = 𝑧 )
230 226 228 229 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → 𝑧 = ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
231 61 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( Σ^ ‘ 𝐹 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
232 230 231 breq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → ( 𝑧 ≤ ( Σ^ ‘ 𝐹 ) ↔ ( Σ^ ‘ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ) )
233 217 232 mpbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( 𝐺 ‘ 𝑗 ) = 𝑧 ) → 𝑧 ≤ ( Σ^ ‘ 𝐹 ) )
234 233 3exp ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 → ( ( 𝐺 ‘ 𝑗 ) = 𝑧 → 𝑧 ≤ ( Σ^ ‘ 𝐹 ) ) ) )
235 234 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( 𝑗 ∈ 𝑍 → ( ( 𝐺 ‘ 𝑗 ) = 𝑧 → 𝑧 ≤ ( Σ^ ‘ 𝐹 ) ) ) )
236 235 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → ( ∃ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) = 𝑧 → 𝑧 ≤ ( Σ^ ‘ 𝐹 ) ) )
237 106 236 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐺 ) → 𝑧 ≤ ( Σ^ ‘ 𝐹 ) )
238 237 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ ( Σ^ ‘ 𝐹 ) )
239 7 10 sge0cl ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
240 58 ltpnfd ⊢ ( 𝜑 → sup ( ran 𝐺 , ℝ , < ) < +∞ )
241 11 59 90 213 240 xrlelttrd ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) < +∞ )
242 11 90 241 xrgtned ⊢ ( 𝜑 → +∞ ≠ ( Σ^ ‘ 𝐹 ) )
243 242 necomd ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≠ +∞ )
244 ge0xrre ⊢ ( ( ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) ∧ ( Σ^ ‘ 𝐹 ) ≠ +∞ ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
245 239 243 244 syl2anc ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
246 suprleub ⊢ ( ( ( ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥 ) ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( sup ( ran 𝐺 , ℝ , < ) ≤ ( Σ^ ‘ 𝐹 ) ↔ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ ( Σ^ ‘ 𝐹 ) ) )
247 77 100 130 245 246 syl31anc ⊢ ( 𝜑 → ( sup ( ran 𝐺 , ℝ , < ) ≤ ( Σ^ ‘ 𝐹 ) ↔ ∀ 𝑧 ∈ ran 𝐺 𝑧 ≤ ( Σ^ ‘ 𝐹 ) ) )
248 238 247 mpbird ⊢ ( 𝜑 → sup ( ran 𝐺 , ℝ , < ) ≤ ( Σ^ ‘ 𝐹 ) )
249 11 59 213 248 xrletrid ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ , < ) )
250 climuni ⊢ ( ( 𝐺 ⇝ 𝐵 ∧ 𝐺 ⇝ sup ( ran 𝐺 , ℝ , < ) ) → 𝐵 = sup ( ran 𝐺 , ℝ , < ) )
251 5 57 250 syl2anc ⊢ ( 𝜑 → 𝐵 = sup ( ran 𝐺 , ℝ , < ) )
252 249 251 eqtr4d ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = 𝐵 )