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 42586
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 6677 . . . . 5 𝑍 ∈ V
32a1i 11 . . . 4 (𝜑𝑍 ∈ V)
4 sge0isum.f . . . . 5 (𝜑𝐹:𝑍⟶(0[,)+∞))
5 icossicc 12812 . . . . . 6 (0[,)+∞) ⊆ (0[,]+∞)
65a1i 11 . . . . 5 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
74, 6fssd 6521 . . . 4 (𝜑𝐹:𝑍⟶(0[,]+∞))
83, 7sge0xrcl 42544 . . 3 (𝜑 → (Σ^𝐹) ∈ ℝ*)
9 sge0isum.m . . . . 5 (𝜑𝑀 ∈ ℤ)
10 sge0isum.g . . . . . 6 𝐺 = seq𝑀( + , 𝐹)
11 eqidd 2819 . . . . . 6 ((𝜑𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
12 rge0ssre 12832 . . . . . . 7 (0[,)+∞) ⊆ ℝ
134ffvelrnda 6843 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ (0[,)+∞))
1412, 13sseldi 3962 . . . . . 6 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
15 0xr 10676 . . . . . . . 8 0 ∈ ℝ*
1615a1i 11 . . . . . . 7 ((𝜑𝑘𝑍) → 0 ∈ ℝ*)
17 pnfxr 10683 . . . . . . . 8 +∞ ∈ ℝ*
1817a1i 11 . . . . . . 7 ((𝜑𝑘𝑍) → +∞ ∈ ℝ*)
19 icogelb 12776 . . . . . . 7 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑘))
2016, 18, 13, 19syl3anc 1363 . . . . . 6 ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))
21 seqex 13359 . . . . . . . . . . 11 seq𝑀( + , 𝐹) ∈ V
2210, 21eqeltri 2906 . . . . . . . . . 10 𝐺 ∈ V
2322a1i 11 . . . . . . . . 9 (𝜑𝐺 ∈ V)
24 sge0isum.gcnv . . . . . . . . . 10 (𝜑𝐺𝐵)
25 climcl 14844 . . . . . . . . . 10 (𝐺𝐵𝐵 ∈ ℂ)
2624, 25syl 17 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
27 breldmg 5771 . . . . . . . . 9 ((𝐺 ∈ V ∧ 𝐵 ∈ ℂ ∧ 𝐺𝐵) → 𝐺 ∈ dom ⇝ )
2823, 26, 24, 27syl3anc 1363 . . . . . . . 8 (𝜑𝐺 ∈ dom ⇝ )
2910a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝐺 = seq𝑀( + , 𝐹))
3029fveq1d 6665 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (𝐺𝑗) = (seq𝑀( + , 𝐹)‘𝑗))
311eleq2i 2901 . . . . . . . . . . . . . 14 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
3231biimpi 217 . . . . . . . . . . . . 13 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
3332adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
34 simpll 763 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑)
35 elfzuz 12892 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ𝑀))
3635, 1eleqtrrdi 2921 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑀...𝑗) → 𝑘𝑍)
3736adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘𝑍)
3834, 37, 14syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ ℝ)
39 readdcl 10608 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ)
4039adantl 482 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
4133, 38, 40seqcl 13378 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
4230, 41eqeltrd 2910 . . . . . . . . . 10 ((𝜑𝑗𝑍) → (𝐺𝑗) ∈ ℝ)
4342recnd 10657 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝐺𝑗) ∈ ℂ)
4443ralrimiva 3179 . . . . . . . 8 (𝜑 → ∀𝑗𝑍 (𝐺𝑗) ∈ ℂ)
451climbdd 15016 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝐺 ∈ dom ⇝ ∧ ∀𝑗𝑍 (𝐺𝑗) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥)
469, 28, 44, 45syl3anc 1363 . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥)
4742ad4ant13 747 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ∈ ℝ)
4843ad4ant13 747 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ∈ ℂ)
4948abscld 14784 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (abs‘(𝐺𝑗)) ∈ ℝ)
50 simpllr 772 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → 𝑥 ∈ ℝ)
5147leabsd 14762 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ≤ (abs‘(𝐺𝑗)))
52 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (abs‘(𝐺𝑗)) ≤ 𝑥)
5347, 49, 50, 51, 52letrd 10785 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ≤ 𝑥)
5453ex 413 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) → ((abs‘(𝐺𝑗)) ≤ 𝑥 → (𝐺𝑗) ≤ 𝑥))
5554ralimdva 3174 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥 → ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥))
5655reximdva 3271 . . . . . . 7 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥))
5746, 56mpd 15 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥)
581, 10, 9, 11, 14, 20, 57isumsup2 15189 . . . . 5 (𝜑𝐺 ⇝ sup(ran 𝐺, ℝ, < ))
591, 9, 58, 42climrecl 14928 . . . 4 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ)
6059rexrd 10679 . . 3 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
614feqmptd 6726 . . . . 5 (𝜑𝐹 = (𝑘𝑍 ↦ (𝐹𝑘)))
6261fveq2d 6667 . . . 4 (𝜑 → (Σ^𝐹) = (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
63 mpteq1 5145 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑘𝑦 ↦ (𝐹𝑘)) = (𝑘 ∈ ∅ ↦ (𝐹𝑘)))
6463fveq2d 6667 . . . . . . . . . 10 (𝑦 = ∅ → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))))
65 mpt0 6483 . . . . . . . . . . . . 13 (𝑘 ∈ ∅ ↦ (𝐹𝑘)) = ∅
6665fveq2i 6666 . . . . . . . . . . . 12 ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = (Σ^‘∅)
67 sge00 42535 . . . . . . . . . . . 12 ^‘∅) = 0
6866, 67eqtri 2841 . . . . . . . . . . 11 ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = 0
6968a1i 11 . . . . . . . . . 10 (𝑦 = ∅ → (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = 0)
7064, 69eqtrd 2853 . . . . . . . . 9 (𝑦 = ∅ → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = 0)
7170adantl 482 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = 0)
72 0red 10632 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
7339adantl 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
741, 9, 14, 73seqf 13379 . . . . . . . . . . . . 13 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
7510a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐺 = seq𝑀( + , 𝐹))
7675feq1d 6492 . . . . . . . . . . . . 13 (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ))
7774, 76mpbird 258 . . . . . . . . . . . 12 (𝜑𝐺:𝑍⟶ℝ)
7877frnd 6514 . . . . . . . . . . 11 (𝜑 → ran 𝐺 ⊆ ℝ)
7977ffund 6511 . . . . . . . . . . . 12 (𝜑 → Fun 𝐺)
80 uzid 12246 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
819, 80syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ𝑀))
821eqcomi 2827 . . . . . . . . . . . . . 14 (ℤ𝑀) = 𝑍
8381, 82eleqtrdi 2920 . . . . . . . . . . . . 13 (𝜑𝑀𝑍)
8477fdmd 6516 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑍)
8584eqcomd 2824 . . . . . . . . . . . . 13 (𝜑𝑍 = dom 𝐺)
8683, 85eleqtrd 2912 . . . . . . . . . . . 12 (𝜑𝑀 ∈ dom 𝐺)
87 fvelrn 6836 . . . . . . . . . . . 12 ((Fun 𝐺𝑀 ∈ dom 𝐺) → (𝐺𝑀) ∈ ran 𝐺)
8879, 86, 87syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐺𝑀) ∈ ran 𝐺)
8978, 88sseldd 3965 . . . . . . . . . 10 (𝜑 → (𝐺𝑀) ∈ ℝ)
9015a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℝ*)
9117a1i 11 . . . . . . . . . . . 12 (𝜑 → +∞ ∈ ℝ*)
924, 83ffvelrnd 6844 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑀) ∈ (0[,)+∞))
93 icogelb 12776 . . . . . . . . . . . 12 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑀) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑀))
9490, 91, 92, 93syl3anc 1363 . . . . . . . . . . 11 (𝜑 → 0 ≤ (𝐹𝑀))
9510fveq1i 6664 . . . . . . . . . . . . 13 (𝐺𝑀) = (seq𝑀( + , 𝐹)‘𝑀)
9695a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐺𝑀) = (seq𝑀( + , 𝐹)‘𝑀))
97 seq1 13370 . . . . . . . . . . . . 13 (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
989, 97syl 17 . . . . . . . . . . . 12 (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
9996, 98eqtr2d 2854 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) = (𝐺𝑀))
10094, 99breqtrd 5083 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝐺𝑀))
10188ne0d 4298 . . . . . . . . . . 11 (𝜑 → ran 𝐺 ≠ ∅)
102 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺)
10377ffnd 6508 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 Fn 𝑍)
104 fvelrnb 6719 . . . . . . . . . . . . . . . . . . . 20 (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
106105adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
107102, 106mpbid 233 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ ran 𝐺) → ∃𝑗𝑍 (𝐺𝑗) = 𝑧)
108107adantlr 711 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗𝑍 (𝐺𝑗) = 𝑧)
109 nfv 1906 . . . . . . . . . . . . . . . . . . 19 𝑗𝜑
110 nfra1 3216 . . . . . . . . . . . . . . . . . . 19 𝑗𝑗𝑍 (𝐺𝑗) ≤ 𝑥
111109, 110nfan 1891 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥)
112 nfv 1906 . . . . . . . . . . . . . . . . . 18 𝑗 𝑧 ∈ ran 𝐺
113111, 112nfan 1891 . . . . . . . . . . . . . . . . 17 𝑗((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺)
114 nfv 1906 . . . . . . . . . . . . . . . . 17 𝑗 𝑧𝑥
115 rspa 3203 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍) → (𝐺𝑗) ≤ 𝑥)
1161153adant3 1124 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) ≤ 𝑥)
117 simp3 1130 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) = 𝑧)
118 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺𝑗) = 𝑧 → (𝐺𝑗) = 𝑧)
119118eqcomd 2824 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺𝑗) = 𝑧𝑧 = (𝐺𝑗))
120119adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → 𝑧 = (𝐺𝑗))
121 simpl 483 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) ≤ 𝑥)
122120, 121eqbrtrd 5079 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → 𝑧𝑥)
123116, 117, 122syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧𝑥)
1241233exp 1111 . . . . . . . . . . . . . . . . . 18 (∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧𝑥)))
125124ad2antlr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧𝑥)))
126113, 114, 125rexlimd 3314 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗𝑍 (𝐺𝑗) = 𝑧𝑧𝑥))
127108, 126mpd 15 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → 𝑧𝑥)
128127ralrimiva 3179 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) → ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
129128ex 413 . . . . . . . . . . . . 13 (𝜑 → (∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐺 𝑧𝑥))
130129reximdv 3270 . . . . . . . . . . . 12 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥))
13157, 130mpd 15 . . . . . . . . . . 11 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
132 suprub 11590 . . . . . . . . . . 11 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (𝐺𝑀) ∈ ran 𝐺) → (𝐺𝑀) ≤ sup(ran 𝐺, ℝ, < ))
13378, 101, 131, 88, 132syl31anc 1365 . . . . . . . . . 10 (𝜑 → (𝐺𝑀) ≤ sup(ran 𝐺, ℝ, < ))
13472, 89, 59, 100, 133letrd 10785 . . . . . . . . 9 (𝜑 → 0 ≤ sup(ran 𝐺, ℝ, < ))
135134ad2antrr 722 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → 0 ≤ sup(ran 𝐺, ℝ, < ))
13671, 135eqbrtrd 5079 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
137 simpr 485 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ∈ (𝒫 𝑍 ∩ Fin))
138 simpll 763 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → 𝜑)
139 elpwinss 41188 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦𝑍)
140139sselda 3964 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘𝑦) → 𝑘𝑍)
141140adantll 710 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → 𝑘𝑍)
1425, 13sseldi 3962 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ (0[,]+∞))
143138, 141, 142syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → (𝐹𝑘) ∈ (0[,]+∞))
144 eqid 2818 . . . . . . . . . . 11 (𝑘𝑦 ↦ (𝐹𝑘)) = (𝑘𝑦 ↦ (𝐹𝑘))
145143, 144fmptd 6870 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘𝑦 ↦ (𝐹𝑘)):𝑦⟶(0[,]+∞))
146137, 145sge0xrcl 42544 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ∈ ℝ*)
147146adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ∈ ℝ*)
148 fzfid 13329 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑀...sup(𝑦, ℝ, < )) ∈ Fin)
149 elfzuz 12892 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ (ℤ𝑀))
150149, 82eleqtrdi 2920 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘𝑍)
151150, 142sylan2 592 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,]+∞))
152 eqid 2818 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)) = (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))
153151, 152fmptd 6870 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
154153adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
155148, 154sge0xrcl 42544 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ℝ*)
156155adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ℝ*)
15760adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
158157adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
159 simpll 763 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝜑)
160150adantl 482 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝑘𝑍)
161159, 160, 142syl2anc 584 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,]+∞))
162 elinel2 4170 . . . . . . . . . . . 12 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ∈ Fin)
1631, 139, 162ssuzfz 41493 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
164163adantl 482 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
165148, 161, 164sge0lessmpt 42558 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))))
166165adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))))
16778adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ⊆ ℝ)
168167adantr 481 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ⊆ ℝ)
169101adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ≠ ∅)
170169adantr 481 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ≠ ∅)
171131adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
172171adantr 481 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
173159, 160, 13syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,)+∞))
174148, 173sge0fsummpt 42549 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘))
175174adantr 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘))
176 eqidd 2819 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) = (𝐹𝑘))
177139, 1sseqtrdi 4014 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (ℤ𝑀))
178177adantr 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ (ℤ𝑀))
179 uzssz 12252 . . . . . . . . . . . . . . . . . 18 (ℤ𝑀) ⊆ ℤ
1801, 179eqsstri 3998 . . . . . . . . . . . . . . . . 17 𝑍 ⊆ ℤ
181139, 180sstrdi 3976 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ ℤ)
182181adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ ℤ)
183 neqne 3021 . . . . . . . . . . . . . . . 16 𝑦 = ∅ → 𝑦 ≠ ∅)
184183adantl 482 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
185162adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ Fin)
186 suprfinzcl 12085 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ ℤ ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin) → sup(𝑦, ℝ, < ) ∈ 𝑦)
187182, 184, 185, 186syl3anc 1363 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑦)
188178, 187sseldd 3965 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ𝑀))
189188adantll 710 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ𝑀))
19014recnd 10657 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
191159, 160, 190syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ ℂ)
192191adantlr 711 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ ℂ)
193176, 189, 192fsumser 15075 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘) = (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )))
19410eqcomi 2827 . . . . . . . . . . . . 13 seq𝑀( + , 𝐹) = 𝐺
195194fveq1i 6664 . . . . . . . . . . . 12 (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < ))
196195a1i 11 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < )))
197175, 193, 1963eqtrd 2857 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = (𝐺‘sup(𝑦, ℝ, < )))
19879adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → Fun 𝐺)
199198adantr 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Fun 𝐺)
200189, 82eleqtrdi 2920 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑍)
20185ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → 𝑍 = dom 𝐺)
202200, 201eleqtrd 2912 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ dom 𝐺)
203 fvelrn 6836 . . . . . . . . . . 11 ((Fun 𝐺 ∧ sup(𝑦, ℝ, < ) ∈ dom 𝐺) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
204199, 202, 203syl2anc 584 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
205197, 204eqeltrd 2910 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ran 𝐺)
206 suprub 11590 . . . . . . . . 9 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ran 𝐺) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
207168, 170, 172, 205, 206syl31anc 1365 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
208147, 156, 158, 166, 207xrletrd 12543 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
209136, 208pm2.61dan 809 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
210209ralrimiva 3179 . . . . 5 (𝜑 → ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
211 nfv 1906 . . . . . 6 𝑘𝜑
212211, 3, 142, 60sge0lefimpt 42582 . . . . 5 (𝜑 → ((Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ) ↔ ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < )))
213210, 212mpbird 258 . . . 4 (𝜑 → (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
21462, 213eqbrtrd 5079 . . 3 (𝜑 → (Σ^𝐹) ≤ sup(ran 𝐺, ℝ, < ))
21536ssriv 3968 . . . . . . . . . . . . 13 (𝑀...𝑗) ⊆ 𝑍
216215a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑀...𝑗) ⊆ 𝑍)
2173, 142, 216sge0lessmpt 42558 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
2182173ad2ant1 1125 . . . . . . . . . 10 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
219 fzfid 13329 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀...𝑗) ∈ Fin)
22036, 13sylan2 592 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ (0[,)+∞))
221219, 220sge0fsummpt 42549 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘))
2222213ad2ant1 1125 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘))
22334, 37, 11syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) = (𝐹𝑘))
22434, 37, 190syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ ℂ)
225223, 33, 224fsumser 15075 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
2262253adant3 1124 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
227222, 226eqtrd 2853 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = (seq𝑀( + , 𝐹)‘𝑗))
228194fveq1i 6664 . . . . . . . . . . . . 13 (seq𝑀( + , 𝐹)‘𝑗) = (𝐺𝑗)
229228a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺𝑗))
230 simp3 1130 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) = 𝑧)
231227, 229, 2303eqtrrd 2858 . . . . . . . . . . 11 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧 = (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))))
232623ad2ant1 1125 . . . . . . . . . . 11 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^𝐹) = (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
233231, 232breq12d 5070 . . . . . . . . . 10 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝑧 ≤ (Σ^𝐹) ↔ (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘)))))
234218, 233mpbird 258 . . . . . . . . 9 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧 ≤ (Σ^𝐹))
2352343exp 1111 . . . . . . . 8 (𝜑 → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹))))
236235adantr 481 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹))))
237236rexlimdv 3280 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → (∃𝑗𝑍 (𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹)))
238107, 237mpd 15 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ≤ (Σ^𝐹))
239238ralrimiva 3179 . . . 4 (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹))
2403, 7sge0cl 42540 . . . . . 6 (𝜑 → (Σ^𝐹) ∈ (0[,]+∞))
24159ltpnfd 12504 . . . . . . . . 9 (𝜑 → sup(ran 𝐺, ℝ, < ) < +∞)
2428, 60, 91, 214, 241xrlelttrd 12541 . . . . . . . 8 (𝜑 → (Σ^𝐹) < +∞)
2438, 91, 242xrgtned 41466 . . . . . . 7 (𝜑 → +∞ ≠ (Σ^𝐹))
244243necomd 3068 . . . . . 6 (𝜑 → (Σ^𝐹) ≠ +∞)
245 ge0xrre 41683 . . . . . 6 (((Σ^𝐹) ∈ (0[,]+∞) ∧ (Σ^𝐹) ≠ +∞) → (Σ^𝐹) ∈ ℝ)
246240, 244, 245syl2anc 584 . . . . 5 (𝜑 → (Σ^𝐹) ∈ ℝ)
247 suprleub 11595 . . . . 5 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (Σ^𝐹) ∈ ℝ) → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹)))
24878, 101, 131, 246, 247syl31anc 1365 . . . 4 (𝜑 → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹)))
249239, 248mpbird 258 . . 3 (𝜑 → sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹))
2508, 60, 214, 249xrletrid 12536 . 2 (𝜑 → (Σ^𝐹) = sup(ran 𝐺, ℝ, < ))
251 climuni 14897 . . 3 ((𝐺𝐵𝐺 ⇝ sup(ran 𝐺, ℝ, < )) → 𝐵 = sup(ran 𝐺, ℝ, < ))
25224, 58, 251syl2anc 584 . 2 (𝜑𝐵 = sup(ran 𝐺, ℝ, < ))
253250, 252eqtr4d 2856 1 (𝜑 → (Σ^𝐹) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  Vcvv 3492  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535   class class class wbr 5057  cmpt 5137  dom cdm 5548  ran crn 5549  Fun wfun 6342   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  Fincfn 8497  supcsup 8892  cc 10523  cr 10524  0cc0 10525   + caddc 10528  +∞cpnf 10660  *cxr 10662   < clt 10663  cle 10664  cz 11969  cuz 12231  [,)cico 12728  [,]cicc 12729  ...cfz 12880  seqcseq 13357  abscabs 14581  cli 14829  Σcsu 15030  Σ^csumge0 42521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-pm 8398  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-rp 12378  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-seq 13358  df-exp 13418  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-clim 14833  df-rlim 14834  df-sum 15031  df-sumge0 42522
This theorem is referenced by:  sge0isummpt  42589
  Copyright terms: Public domain W3C validator