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