Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0isum Structured version   Visualization version   GIF version

Theorem sge0isum 45604
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.)
Hypotheses
Ref Expression
sge0isum.m (𝜑𝑀 ∈ ℤ)
sge0isum.z 𝑍 = (ℤ𝑀)
sge0isum.f (𝜑𝐹:𝑍⟶(0[,)+∞))
sge0isum.g 𝐺 = seq𝑀( + , 𝐹)
sge0isum.gcnv (𝜑𝐺𝐵)
Assertion
Ref Expression
sge0isum (𝜑 → (Σ^𝐹) = 𝐵)

Proof of Theorem sge0isum
Dummy variables 𝑖 𝑗 𝑘 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sge0isum.z . . . . . 6 𝑍 = (ℤ𝑀)
21fvexi 6905 . . . . 5 𝑍 ∈ V
32a1i 11 . . . 4 (𝜑𝑍 ∈ V)
4 sge0isum.f . . . . 5 (𝜑𝐹:𝑍⟶(0[,)+∞))
5 icossicc 13420 . . . . . 6 (0[,)+∞) ⊆ (0[,]+∞)
65a1i 11 . . . . 5 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
74, 6fssd 6735 . . . 4 (𝜑𝐹:𝑍⟶(0[,]+∞))
83, 7sge0xrcl 45562 . . 3 (𝜑 → (Σ^𝐹) ∈ ℝ*)
9 sge0isum.m . . . . 5 (𝜑𝑀 ∈ ℤ)
10 sge0isum.g . . . . . 6 𝐺 = seq𝑀( + , 𝐹)
11 eqidd 2732 . . . . . 6 ((𝜑𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
12 rge0ssre 13440 . . . . . . 7 (0[,)+∞) ⊆ ℝ
134ffvelcdmda 7086 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ (0[,)+∞))
1412, 13sselid 3980 . . . . . 6 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
15 0xr 11268 . . . . . . . 8 0 ∈ ℝ*
1615a1i 11 . . . . . . 7 ((𝜑𝑘𝑍) → 0 ∈ ℝ*)
17 pnfxr 11275 . . . . . . . 8 +∞ ∈ ℝ*
1817a1i 11 . . . . . . 7 ((𝜑𝑘𝑍) → +∞ ∈ ℝ*)
19 icogelb 13382 . . . . . . 7 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑘))
2016, 18, 13, 19syl3anc 1370 . . . . . 6 ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))
21 seqex 13975 . . . . . . . . . . 11 seq𝑀( + , 𝐹) ∈ V
2210, 21eqeltri 2828 . . . . . . . . . 10 𝐺 ∈ V
2322a1i 11 . . . . . . . . 9 (𝜑𝐺 ∈ V)
24 sge0isum.gcnv . . . . . . . . . 10 (𝜑𝐺𝐵)
25 climcl 15450 . . . . . . . . . 10 (𝐺𝐵𝐵 ∈ ℂ)
2624, 25syl 17 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
27 breldmg 5909 . . . . . . . . 9 ((𝐺 ∈ V ∧ 𝐵 ∈ ℂ ∧ 𝐺𝐵) → 𝐺 ∈ dom ⇝ )
2823, 26, 24, 27syl3anc 1370 . . . . . . . 8 (𝜑𝐺 ∈ dom ⇝ )
2910a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝐺 = seq𝑀( + , 𝐹))
3029fveq1d 6893 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (𝐺𝑗) = (seq𝑀( + , 𝐹)‘𝑗))
311eleq2i 2824 . . . . . . . . . . . . . 14 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
3231biimpi 215 . . . . . . . . . . . . 13 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
3332adantl 481 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
34 simpll 764 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑)
35 elfzuz 13504 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ𝑀))
3635, 1eleqtrrdi 2843 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑀...𝑗) → 𝑘𝑍)
3736adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘𝑍)
3834, 37, 14syl2anc 583 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ ℝ)
39 readdcl 11199 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ)
4039adantl 481 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
4133, 38, 40seqcl 13995 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
4230, 41eqeltrd 2832 . . . . . . . . . 10 ((𝜑𝑗𝑍) → (𝐺𝑗) ∈ ℝ)
4342recnd 11249 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝐺𝑗) ∈ ℂ)
4443ralrimiva 3145 . . . . . . . 8 (𝜑 → ∀𝑗𝑍 (𝐺𝑗) ∈ ℂ)
451climbdd 15625 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝐺 ∈ dom ⇝ ∧ ∀𝑗𝑍 (𝐺𝑗) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥)
469, 28, 44, 45syl3anc 1370 . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥)
4742ad4ant13 748 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ∈ ℝ)
4843ad4ant13 748 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ∈ ℂ)
4948abscld 15390 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (abs‘(𝐺𝑗)) ∈ ℝ)
50 simpllr 773 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → 𝑥 ∈ ℝ)
5147leabsd 15368 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ≤ (abs‘(𝐺𝑗)))
52 simpr 484 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (abs‘(𝐺𝑗)) ≤ 𝑥)
5347, 49, 50, 51, 52letrd 11378 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ≤ 𝑥)
5453ex 412 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) → ((abs‘(𝐺𝑗)) ≤ 𝑥 → (𝐺𝑗) ≤ 𝑥))
5554ralimdva 3166 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥 → ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥))
5655reximdva 3167 . . . . . . 7 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥))
5746, 56mpd 15 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥)
581, 10, 9, 11, 14, 20, 57isumsup2 15799 . . . . 5 (𝜑𝐺 ⇝ sup(ran 𝐺, ℝ, < ))
591, 9, 58, 42climrecl 15534 . . . 4 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ)
6059rexrd 11271 . . 3 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
614feqmptd 6960 . . . . 5 (𝜑𝐹 = (𝑘𝑍 ↦ (𝐹𝑘)))
6261fveq2d 6895 . . . 4 (𝜑 → (Σ^𝐹) = (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
63 mpteq1 5241 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑘𝑦 ↦ (𝐹𝑘)) = (𝑘 ∈ ∅ ↦ (𝐹𝑘)))
6463fveq2d 6895 . . . . . . . . . 10 (𝑦 = ∅ → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))))
65 mpt0 6692 . . . . . . . . . . . . 13 (𝑘 ∈ ∅ ↦ (𝐹𝑘)) = ∅
6665fveq2i 6894 . . . . . . . . . . . 12 ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = (Σ^‘∅)
67 sge00 45553 . . . . . . . . . . . 12 ^‘∅) = 0
6866, 67eqtri 2759 . . . . . . . . . . 11 ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = 0
6968a1i 11 . . . . . . . . . 10 (𝑦 = ∅ → (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = 0)
7064, 69eqtrd 2771 . . . . . . . . 9 (𝑦 = ∅ → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = 0)
7170adantl 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = 0)
72 0red 11224 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
7339adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
741, 9, 14, 73seqf 13996 . . . . . . . . . . . . 13 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
7510a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐺 = seq𝑀( + , 𝐹))
7675feq1d 6702 . . . . . . . . . . . . 13 (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ))
7774, 76mpbird 257 . . . . . . . . . . . 12 (𝜑𝐺:𝑍⟶ℝ)
7877frnd 6725 . . . . . . . . . . 11 (𝜑 → ran 𝐺 ⊆ ℝ)
7977ffund 6721 . . . . . . . . . . . 12 (𝜑 → Fun 𝐺)
80 uzid 12844 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
819, 80syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ𝑀))
821eqcomi 2740 . . . . . . . . . . . . . 14 (ℤ𝑀) = 𝑍
8381, 82eleqtrdi 2842 . . . . . . . . . . . . 13 (𝜑𝑀𝑍)
8477fdmd 6728 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑍)
8584eqcomd 2737 . . . . . . . . . . . . 13 (𝜑𝑍 = dom 𝐺)
8683, 85eleqtrd 2834 . . . . . . . . . . . 12 (𝜑𝑀 ∈ dom 𝐺)
87 fvelrn 7078 . . . . . . . . . . . 12 ((Fun 𝐺𝑀 ∈ dom 𝐺) → (𝐺𝑀) ∈ ran 𝐺)
8879, 86, 87syl2anc 583 . . . . . . . . . . 11 (𝜑 → (𝐺𝑀) ∈ ran 𝐺)
8978, 88sseldd 3983 . . . . . . . . . 10 (𝜑 → (𝐺𝑀) ∈ ℝ)
9015a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℝ*)
9117a1i 11 . . . . . . . . . . . 12 (𝜑 → +∞ ∈ ℝ*)
924, 83ffvelcdmd 7087 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑀) ∈ (0[,)+∞))
93 icogelb 13382 . . . . . . . . . . . 12 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑀) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑀))
9490, 91, 92, 93syl3anc 1370 . . . . . . . . . . 11 (𝜑 → 0 ≤ (𝐹𝑀))
9510fveq1i 6892 . . . . . . . . . . . . 13 (𝐺𝑀) = (seq𝑀( + , 𝐹)‘𝑀)
9695a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐺𝑀) = (seq𝑀( + , 𝐹)‘𝑀))
97 seq1 13986 . . . . . . . . . . . . 13 (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
989, 97syl 17 . . . . . . . . . . . 12 (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
9996, 98eqtr2d 2772 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) = (𝐺𝑀))
10094, 99breqtrd 5174 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝐺𝑀))
10188ne0d 4335 . . . . . . . . . . 11 (𝜑 → ran 𝐺 ≠ ∅)
102 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺)
10377ffnd 6718 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 Fn 𝑍)
104 fvelrnb 6952 . . . . . . . . . . . . . . . . . . . 20 (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
106105adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
107102, 106mpbid 231 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ ran 𝐺) → ∃𝑗𝑍 (𝐺𝑗) = 𝑧)
108107adantlr 712 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗𝑍 (𝐺𝑗) = 𝑧)
109 nfv 1916 . . . . . . . . . . . . . . . . . . 19 𝑗𝜑
110 nfra1 3280 . . . . . . . . . . . . . . . . . . 19 𝑗𝑗𝑍 (𝐺𝑗) ≤ 𝑥
111109, 110nfan 1901 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥)
112 nfv 1916 . . . . . . . . . . . . . . . . . 18 𝑗 𝑧 ∈ ran 𝐺
113111, 112nfan 1901 . . . . . . . . . . . . . . . . 17 𝑗((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺)
114 nfv 1916 . . . . . . . . . . . . . . . . 17 𝑗 𝑧𝑥
115 rspa 3244 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍) → (𝐺𝑗) ≤ 𝑥)
1161153adant3 1131 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) ≤ 𝑥)
117 simp3 1137 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) = 𝑧)
118 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺𝑗) = 𝑧 → (𝐺𝑗) = 𝑧)
119118eqcomd 2737 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺𝑗) = 𝑧𝑧 = (𝐺𝑗))
120119adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → 𝑧 = (𝐺𝑗))
121 simpl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) ≤ 𝑥)
122120, 121eqbrtrd 5170 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → 𝑧𝑥)
123116, 117, 122syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧𝑥)
1241233exp 1118 . . . . . . . . . . . . . . . . . 18 (∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧𝑥)))
125124ad2antlr 724 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧𝑥)))
126113, 114, 125rexlimd 3262 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗𝑍 (𝐺𝑗) = 𝑧𝑧𝑥))
127108, 126mpd 15 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → 𝑧𝑥)
128127ralrimiva 3145 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) → ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
129128ex 412 . . . . . . . . . . . . 13 (𝜑 → (∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐺 𝑧𝑥))
130129reximdv 3169 . . . . . . . . . . . 12 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥))
13157, 130mpd 15 . . . . . . . . . . 11 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
132 suprub 12182 . . . . . . . . . . 11 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (𝐺𝑀) ∈ ran 𝐺) → (𝐺𝑀) ≤ sup(ran 𝐺, ℝ, < ))
13378, 101, 131, 88, 132syl31anc 1372 . . . . . . . . . 10 (𝜑 → (𝐺𝑀) ≤ sup(ran 𝐺, ℝ, < ))
13472, 89, 59, 100, 133letrd 11378 . . . . . . . . 9 (𝜑 → 0 ≤ sup(ran 𝐺, ℝ, < ))
135134ad2antrr 723 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → 0 ≤ sup(ran 𝐺, ℝ, < ))
13671, 135eqbrtrd 5170 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
137 simpr 484 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ∈ (𝒫 𝑍 ∩ Fin))
138 simpll 764 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → 𝜑)
139 elpwinss 44200 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦𝑍)
140139sselda 3982 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘𝑦) → 𝑘𝑍)
141140adantll 711 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → 𝑘𝑍)
1425, 13sselid 3980 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ (0[,]+∞))
143138, 141, 142syl2anc 583 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → (𝐹𝑘) ∈ (0[,]+∞))
144 eqid 2731 . . . . . . . . . . 11 (𝑘𝑦 ↦ (𝐹𝑘)) = (𝑘𝑦 ↦ (𝐹𝑘))
145143, 144fmptd 7115 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘𝑦 ↦ (𝐹𝑘)):𝑦⟶(0[,]+∞))
146137, 145sge0xrcl 45562 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ∈ ℝ*)
147146adantr 480 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ∈ ℝ*)
148 fzfid 13945 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑀...sup(𝑦, ℝ, < )) ∈ Fin)
149 elfzuz 13504 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ (ℤ𝑀))
150149, 82eleqtrdi 2842 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘𝑍)
151150, 142sylan2 592 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,]+∞))
152 eqid 2731 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)) = (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))
153151, 152fmptd 7115 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
154153adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
155148, 154sge0xrcl 45562 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ℝ*)
156155adantr 480 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ℝ*)
15760adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
158157adantr 480 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
159 simpll 764 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝜑)
160150adantl 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝑘𝑍)
161159, 160, 142syl2anc 583 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,]+∞))
162 elinel2 4196 . . . . . . . . . . . 12 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ∈ Fin)
1631, 139, 162ssuzfz 44520 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
164163adantl 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
165148, 161, 164sge0lessmpt 45576 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))))
166165adantr 480 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))))
16778adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ⊆ ℝ)
168167adantr 480 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ⊆ ℝ)
169101adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ≠ ∅)
170169adantr 480 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ≠ ∅)
171131adantr 480 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
172171adantr 480 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
173159, 160, 13syl2anc 583 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,)+∞))
174148, 173sge0fsummpt 45567 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘))
175174adantr 480 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘))
176 eqidd 2732 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) = (𝐹𝑘))
177139, 1sseqtrdi 4032 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (ℤ𝑀))
178177adantr 480 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ (ℤ𝑀))
179 uzssz 12850 . . . . . . . . . . . . . . . . . 18 (ℤ𝑀) ⊆ ℤ
1801, 179eqsstri 4016 . . . . . . . . . . . . . . . . 17 𝑍 ⊆ ℤ
181139, 180sstrdi 3994 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ ℤ)
182181adantr 480 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ ℤ)
183 neqne 2947 . . . . . . . . . . . . . . . 16 𝑦 = ∅ → 𝑦 ≠ ∅)
184183adantl 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
185162adantr 480 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ Fin)
186 suprfinzcl 12683 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ ℤ ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin) → sup(𝑦, ℝ, < ) ∈ 𝑦)
187182, 184, 185, 186syl3anc 1370 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑦)
188178, 187sseldd 3983 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ𝑀))
189188adantll 711 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ𝑀))
19014recnd 11249 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
191159, 160, 190syl2anc 583 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ ℂ)
192191adantlr 712 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ ℂ)
193176, 189, 192fsumser 15683 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘) = (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )))
19410eqcomi 2740 . . . . . . . . . . . . 13 seq𝑀( + , 𝐹) = 𝐺
195194fveq1i 6892 . . . . . . . . . . . 12 (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < ))
196195a1i 11 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < )))
197175, 193, 1963eqtrd 2775 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = (𝐺‘sup(𝑦, ℝ, < )))
19879adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → Fun 𝐺)
199198adantr 480 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Fun 𝐺)
200189, 82eleqtrdi 2842 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑍)
20185ad2antrr 723 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → 𝑍 = dom 𝐺)
202200, 201eleqtrd 2834 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ dom 𝐺)
203 fvelrn 7078 . . . . . . . . . . 11 ((Fun 𝐺 ∧ sup(𝑦, ℝ, < ) ∈ dom 𝐺) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
204199, 202, 203syl2anc 583 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
205197, 204eqeltrd 2832 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ran 𝐺)
206 suprub 12182 . . . . . . . . 9 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ran 𝐺) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
207168, 170, 172, 205, 206syl31anc 1372 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
208147, 156, 158, 166, 207xrletrd 13148 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
209136, 208pm2.61dan 810 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
210209ralrimiva 3145 . . . . 5 (𝜑 → ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
211 nfv 1916 . . . . . 6 𝑘𝜑
212211, 3, 142, 60sge0lefimpt 45600 . . . . 5 (𝜑 → ((Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ) ↔ ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < )))
213210, 212mpbird 257 . . . 4 (𝜑 → (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
21462, 213eqbrtrd 5170 . . 3 (𝜑 → (Σ^𝐹) ≤ sup(ran 𝐺, ℝ, < ))
21536ssriv 3986 . . . . . . . . . . . . 13 (𝑀...𝑗) ⊆ 𝑍
216215a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑀...𝑗) ⊆ 𝑍)
2173, 142, 216sge0lessmpt 45576 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
2182173ad2ant1 1132 . . . . . . . . . 10 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
219 fzfid 13945 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀...𝑗) ∈ Fin)
22036, 13sylan2 592 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ (0[,)+∞))
221219, 220sge0fsummpt 45567 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘))
2222213ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘))
22334, 37, 11syl2anc 583 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) = (𝐹𝑘))
22434, 37, 190syl2anc 583 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ ℂ)
225223, 33, 224fsumser 15683 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
2262253adant3 1131 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
227222, 226eqtrd 2771 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = (seq𝑀( + , 𝐹)‘𝑗))
228194fveq1i 6892 . . . . . . . . . . . . 13 (seq𝑀( + , 𝐹)‘𝑗) = (𝐺𝑗)
229228a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺𝑗))
230 simp3 1137 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) = 𝑧)
231227, 229, 2303eqtrrd 2776 . . . . . . . . . . 11 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧 = (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))))
232623ad2ant1 1132 . . . . . . . . . . 11 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^𝐹) = (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
233231, 232breq12d 5161 . . . . . . . . . 10 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝑧 ≤ (Σ^𝐹) ↔ (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘)))))
234218, 233mpbird 257 . . . . . . . . 9 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧 ≤ (Σ^𝐹))
2352343exp 1118 . . . . . . . 8 (𝜑 → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹))))
236235adantr 480 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹))))
237236rexlimdv 3152 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → (∃𝑗𝑍 (𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹)))
238107, 237mpd 15 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ≤ (Σ^𝐹))
239238ralrimiva 3145 . . . 4 (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹))
2403, 7sge0cl 45558 . . . . . 6 (𝜑 → (Σ^𝐹) ∈ (0[,]+∞))
24159ltpnfd 13108 . . . . . . . . 9 (𝜑 → sup(ran 𝐺, ℝ, < ) < +∞)
2428, 60, 91, 214, 241xrlelttrd 13146 . . . . . . . 8 (𝜑 → (Σ^𝐹) < +∞)
2438, 91, 242xrgtned 44493 . . . . . . 7 (𝜑 → +∞ ≠ (Σ^𝐹))
244243necomd 2995 . . . . . 6 (𝜑 → (Σ^𝐹) ≠ +∞)
245 ge0xrre 44705 . . . . . 6 (((Σ^𝐹) ∈ (0[,]+∞) ∧ (Σ^𝐹) ≠ +∞) → (Σ^𝐹) ∈ ℝ)
246240, 244, 245syl2anc 583 . . . . 5 (𝜑 → (Σ^𝐹) ∈ ℝ)
247 suprleub 12187 . . . . 5 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (Σ^𝐹) ∈ ℝ) → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹)))
24878, 101, 131, 246, 247syl31anc 1372 . . . 4 (𝜑 → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹)))
249239, 248mpbird 257 . . 3 (𝜑 → sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹))
2508, 60, 214, 249xrletrid 13141 . 2 (𝜑 → (Σ^𝐹) = sup(ran 𝐺, ℝ, < ))
251 climuni 15503 . . 3 ((𝐺𝐵𝐺 ⇝ sup(ran 𝐺, ℝ, < )) → 𝐵 = sup(ran 𝐺, ℝ, < ))
25224, 58, 251syl2anc 583 . 2 (𝜑𝐵 = sup(ran 𝐺, ℝ, < ))
253250, 252eqtr4d 2774 1 (𝜑 → (Σ^𝐹) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1086   = wceq 1540  wcel 2105  wne 2939  wral 3060  wrex 3069  Vcvv 3473  cin 3947  wss 3948  c0 4322  𝒫 cpw 4602   class class class wbr 5148  cmpt 5231  dom cdm 5676  ran crn 5677  Fun wfun 6537   Fn wfn 6538  wf 6539  cfv 6543  (class class class)co 7412  Fincfn 8945  supcsup 9441  cc 11114  cr 11115  0cc0 11116   + caddc 11119  +∞cpnf 11252  *cxr 11254   < clt 11255  cle 11256  cz 12565  cuz 12829  [,)cico 13333  [,]cicc 13334  ...cfz 13491  seqcseq 13973  abscabs 15188  cli 15435  Σcsu 15639  Σ^csumge0 45539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9642  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-er 8709  df-pm 8829  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-sup 9443  df-inf 9444  df-oi 9511  df-card 9940  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-n0 12480  df-z 12566  df-uz 12830  df-rp 12982  df-ico 13337  df-icc 13338  df-fz 13492  df-fzo 13635  df-fl 13764  df-seq 13974  df-exp 14035  df-hash 14298  df-cj 15053  df-re 15054  df-im 15055  df-sqrt 15189  df-abs 15190  df-clim 15439  df-rlim 15440  df-sum 15640  df-sumge0 45540
This theorem is referenced by:  sge0isummpt  45607
  Copyright terms: Public domain W3C validator