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 41550
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 6460 . . . . 5 𝑍 ∈ V
32a1i 11 . . . 4 (𝜑𝑍 ∈ V)
4 sge0isum.f . . . . 5 (𝜑𝐹:𝑍⟶(0[,)+∞))
5 icossicc 12573 . . . . . 6 (0[,)+∞) ⊆ (0[,]+∞)
65a1i 11 . . . . 5 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
74, 6fssd 6305 . . . 4 (𝜑𝐹:𝑍⟶(0[,]+∞))
83, 7sge0xrcl 41508 . . 3 (𝜑 → (Σ^𝐹) ∈ ℝ*)
9 sge0isum.m . . . . 5 (𝜑𝑀 ∈ ℤ)
10 sge0isum.g . . . . . 6 𝐺 = seq𝑀( + , 𝐹)
11 eqidd 2778 . . . . . 6 ((𝜑𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
12 rge0ssre 12594 . . . . . . 7 (0[,)+∞) ⊆ ℝ
134ffvelrnda 6623 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ (0[,)+∞))
1412, 13sseldi 3818 . . . . . 6 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
15 0xr 10423 . . . . . . . 8 0 ∈ ℝ*
1615a1i 11 . . . . . . 7 ((𝜑𝑘𝑍) → 0 ∈ ℝ*)
17 pnfxr 10430 . . . . . . . 8 +∞ ∈ ℝ*
1817a1i 11 . . . . . . 7 ((𝜑𝑘𝑍) → +∞ ∈ ℝ*)
19 icogelb 12537 . . . . . . 7 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑘))
2016, 18, 13, 19syl3anc 1439 . . . . . 6 ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))
21 seqex 13121 . . . . . . . . . . 11 seq𝑀( + , 𝐹) ∈ V
2210, 21eqeltri 2854 . . . . . . . . . 10 𝐺 ∈ V
2322a1i 11 . . . . . . . . 9 (𝜑𝐺 ∈ V)
24 sge0isum.gcnv . . . . . . . . . 10 (𝜑𝐺𝐵)
25 climcl 14638 . . . . . . . . . 10 (𝐺𝐵𝐵 ∈ ℂ)
2624, 25syl 17 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
27 breldmg 5575 . . . . . . . . 9 ((𝐺 ∈ V ∧ 𝐵 ∈ ℂ ∧ 𝐺𝐵) → 𝐺 ∈ dom ⇝ )
2823, 26, 24, 27syl3anc 1439 . . . . . . . 8 (𝜑𝐺 ∈ dom ⇝ )
2910a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝐺 = seq𝑀( + , 𝐹))
3029fveq1d 6448 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (𝐺𝑗) = (seq𝑀( + , 𝐹)‘𝑗))
311eleq2i 2850 . . . . . . . . . . . . . 14 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
3231biimpi 208 . . . . . . . . . . . . 13 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
3332adantl 475 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
34 simpll 757 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑)
35 elfzuz 12655 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ𝑀))
3635, 1syl6eleqr 2869 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑀...𝑗) → 𝑘𝑍)
3736adantl 475 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘𝑍)
3834, 37, 14syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ ℝ)
39 readdcl 10355 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ)
4039adantl 475 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
4133, 38, 40seqcl 13139 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
4230, 41eqeltrd 2858 . . . . . . . . . 10 ((𝜑𝑗𝑍) → (𝐺𝑗) ∈ ℝ)
4342recnd 10405 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝐺𝑗) ∈ ℂ)
4443ralrimiva 3147 . . . . . . . 8 (𝜑 → ∀𝑗𝑍 (𝐺𝑗) ∈ ℂ)
451climbdd 14810 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝐺 ∈ dom ⇝ ∧ ∀𝑗𝑍 (𝐺𝑗) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥)
469, 28, 44, 45syl3anc 1439 . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥)
4742ad4ant13 741 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ∈ ℝ)
4843ad4ant13 741 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ∈ ℂ)
4948abscld 14583 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (abs‘(𝐺𝑗)) ∈ ℝ)
50 simpllr 766 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → 𝑥 ∈ ℝ)
5147leabsd 14561 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ≤ (abs‘(𝐺𝑗)))
52 simpr 479 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (abs‘(𝐺𝑗)) ≤ 𝑥)
5347, 49, 50, 51, 52letrd 10533 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ≤ 𝑥)
5453ex 403 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) → ((abs‘(𝐺𝑗)) ≤ 𝑥 → (𝐺𝑗) ≤ 𝑥))
5554ralimdva 3143 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥 → ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥))
5655reximdva 3197 . . . . . . 7 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥))
5746, 56mpd 15 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥)
581, 10, 9, 11, 14, 20, 57isumsup2 14982 . . . . 5 (𝜑𝐺 ⇝ sup(ran 𝐺, ℝ, < ))
591, 9, 58, 42climrecl 14722 . . . 4 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ)
6059rexrd 10426 . . 3 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
614feqmptd 6509 . . . . 5 (𝜑𝐹 = (𝑘𝑍 ↦ (𝐹𝑘)))
6261fveq2d 6450 . . . 4 (𝜑 → (Σ^𝐹) = (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
63 mpteq1 4972 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑘𝑦 ↦ (𝐹𝑘)) = (𝑘 ∈ ∅ ↦ (𝐹𝑘)))
6463fveq2d 6450 . . . . . . . . . 10 (𝑦 = ∅ → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))))
65 mpt0 6267 . . . . . . . . . . . . 13 (𝑘 ∈ ∅ ↦ (𝐹𝑘)) = ∅
6665fveq2i 6449 . . . . . . . . . . . 12 ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = (Σ^‘∅)
67 sge00 41499 . . . . . . . . . . . 12 ^‘∅) = 0
6866, 67eqtri 2801 . . . . . . . . . . 11 ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = 0
6968a1i 11 . . . . . . . . . 10 (𝑦 = ∅ → (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = 0)
7064, 69eqtrd 2813 . . . . . . . . 9 (𝑦 = ∅ → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = 0)
7170adantl 475 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = 0)
72 0red 10380 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
7339adantl 475 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
741, 9, 14, 73seqf 13140 . . . . . . . . . . . . 13 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
7510a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐺 = seq𝑀( + , 𝐹))
7675feq1d 6276 . . . . . . . . . . . . 13 (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ))
7774, 76mpbird 249 . . . . . . . . . . . 12 (𝜑𝐺:𝑍⟶ℝ)
7877frnd 6298 . . . . . . . . . . 11 (𝜑 → ran 𝐺 ⊆ ℝ)
7977ffund 6295 . . . . . . . . . . . 12 (𝜑 → Fun 𝐺)
80 uzid 12007 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
819, 80syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ𝑀))
821eqcomi 2786 . . . . . . . . . . . . . 14 (ℤ𝑀) = 𝑍
8381, 82syl6eleq 2868 . . . . . . . . . . . . 13 (𝜑𝑀𝑍)
8477fdmd 6300 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑍)
8584eqcomd 2783 . . . . . . . . . . . . 13 (𝜑𝑍 = dom 𝐺)
8683, 85eleqtrd 2860 . . . . . . . . . . . 12 (𝜑𝑀 ∈ dom 𝐺)
87 fvelrn 6616 . . . . . . . . . . . 12 ((Fun 𝐺𝑀 ∈ dom 𝐺) → (𝐺𝑀) ∈ ran 𝐺)
8879, 86, 87syl2anc 579 . . . . . . . . . . 11 (𝜑 → (𝐺𝑀) ∈ ran 𝐺)
8978, 88sseldd 3821 . . . . . . . . . 10 (𝜑 → (𝐺𝑀) ∈ ℝ)
9015a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℝ*)
9117a1i 11 . . . . . . . . . . . 12 (𝜑 → +∞ ∈ ℝ*)
924, 83ffvelrnd 6624 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑀) ∈ (0[,)+∞))
93 icogelb 12537 . . . . . . . . . . . 12 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑀) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑀))
9490, 91, 92, 93syl3anc 1439 . . . . . . . . . . 11 (𝜑 → 0 ≤ (𝐹𝑀))
9510fveq1i 6447 . . . . . . . . . . . . 13 (𝐺𝑀) = (seq𝑀( + , 𝐹)‘𝑀)
9695a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐺𝑀) = (seq𝑀( + , 𝐹)‘𝑀))
97 seq1 13132 . . . . . . . . . . . . 13 (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
989, 97syl 17 . . . . . . . . . . . 12 (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
9996, 98eqtr2d 2814 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) = (𝐺𝑀))
10094, 99breqtrd 4912 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝐺𝑀))
10188ne0d 4149 . . . . . . . . . . 11 (𝜑 → ran 𝐺 ≠ ∅)
102 simpr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺)
10377ffnd 6292 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 Fn 𝑍)
104 fvelrnb 6503 . . . . . . . . . . . . . . . . . . . 20 (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
105103, 104syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
106105adantr 474 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
107102, 106mpbid 224 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ ran 𝐺) → ∃𝑗𝑍 (𝐺𝑗) = 𝑧)
108107adantlr 705 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗𝑍 (𝐺𝑗) = 𝑧)
109 nfv 1957 . . . . . . . . . . . . . . . . . . 19 𝑗𝜑
110 nfra1 3122 . . . . . . . . . . . . . . . . . . 19 𝑗𝑗𝑍 (𝐺𝑗) ≤ 𝑥
111109, 110nfan 1946 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥)
112 nfv 1957 . . . . . . . . . . . . . . . . . 18 𝑗 𝑧 ∈ ran 𝐺
113111, 112nfan 1946 . . . . . . . . . . . . . . . . 17 𝑗((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺)
114 nfv 1957 . . . . . . . . . . . . . . . . 17 𝑗 𝑧𝑥
115 rspa 3111 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍) → (𝐺𝑗) ≤ 𝑥)
1161153adant3 1123 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) ≤ 𝑥)
117 simp3 1129 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) = 𝑧)
118 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺𝑗) = 𝑧 → (𝐺𝑗) = 𝑧)
119118eqcomd 2783 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺𝑗) = 𝑧𝑧 = (𝐺𝑗))
120119adantl 475 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → 𝑧 = (𝐺𝑗))
121 simpl 476 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) ≤ 𝑥)
122120, 121eqbrtrd 4908 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → 𝑧𝑥)
123116, 117, 122syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧𝑥)
1241233exp 1109 . . . . . . . . . . . . . . . . . 18 (∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧𝑥)))
125124ad2antlr 717 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧𝑥)))
126113, 114, 125rexlimd 3207 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗𝑍 (𝐺𝑗) = 𝑧𝑧𝑥))
127108, 126mpd 15 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → 𝑧𝑥)
128127ralrimiva 3147 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) → ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
129128ex 403 . . . . . . . . . . . . 13 (𝜑 → (∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐺 𝑧𝑥))
130129reximdv 3196 . . . . . . . . . . . 12 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥))
13157, 130mpd 15 . . . . . . . . . . 11 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
132 suprub 11338 . . . . . . . . . . 11 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (𝐺𝑀) ∈ ran 𝐺) → (𝐺𝑀) ≤ sup(ran 𝐺, ℝ, < ))
13378, 101, 131, 88, 132syl31anc 1441 . . . . . . . . . 10 (𝜑 → (𝐺𝑀) ≤ sup(ran 𝐺, ℝ, < ))
13472, 89, 59, 100, 133letrd 10533 . . . . . . . . 9 (𝜑 → 0 ≤ sup(ran 𝐺, ℝ, < ))
135134ad2antrr 716 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → 0 ≤ sup(ran 𝐺, ℝ, < ))
13671, 135eqbrtrd 4908 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
137 simpr 479 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ∈ (𝒫 𝑍 ∩ Fin))
138 simpll 757 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → 𝜑)
139 elpwinss 40130 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦𝑍)
140139sselda 3820 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘𝑦) → 𝑘𝑍)
141140adantll 704 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → 𝑘𝑍)
1425, 13sseldi 3818 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ (0[,]+∞))
143138, 141, 142syl2anc 579 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → (𝐹𝑘) ∈ (0[,]+∞))
144 eqid 2777 . . . . . . . . . . 11 (𝑘𝑦 ↦ (𝐹𝑘)) = (𝑘𝑦 ↦ (𝐹𝑘))
145143, 144fmptd 6648 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘𝑦 ↦ (𝐹𝑘)):𝑦⟶(0[,]+∞))
146137, 145sge0xrcl 41508 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ∈ ℝ*)
147146adantr 474 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ∈ ℝ*)
148 fzfid 13091 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑀...sup(𝑦, ℝ, < )) ∈ Fin)
149 elfzuz 12655 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ (ℤ𝑀))
150149, 82syl6eleq 2868 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘𝑍)
151150, 142sylan2 586 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,]+∞))
152 eqid 2777 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)) = (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))
153151, 152fmptd 6648 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
154153adantr 474 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
155148, 154sge0xrcl 41508 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ℝ*)
156155adantr 474 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ℝ*)
15760adantr 474 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
158157adantr 474 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
159 simpll 757 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝜑)
160150adantl 475 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝑘𝑍)
161159, 160, 142syl2anc 579 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,]+∞))
162 elinel2 4022 . . . . . . . . . . . 12 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ∈ Fin)
1631, 139, 162ssuzfz 40455 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
164163adantl 475 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
165148, 161, 164sge0lessmpt 41522 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))))
166165adantr 474 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))))
16778adantr 474 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ⊆ ℝ)
168167adantr 474 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ⊆ ℝ)
169101adantr 474 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ≠ ∅)
170169adantr 474 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ≠ ∅)
171131adantr 474 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
172171adantr 474 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
173159, 160, 13syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,)+∞))
174148, 173sge0fsummpt 41513 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘))
175174adantr 474 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘))
176 eqidd 2778 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) = (𝐹𝑘))
177139, 1syl6sseq 3869 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (ℤ𝑀))
178177adantr 474 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ (ℤ𝑀))
179 uzssz 12012 . . . . . . . . . . . . . . . . . 18 (ℤ𝑀) ⊆ ℤ
1801, 179eqsstri 3853 . . . . . . . . . . . . . . . . 17 𝑍 ⊆ ℤ
181139, 180syl6ss 3832 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ ℤ)
182181adantr 474 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ ℤ)
183 neqne 2976 . . . . . . . . . . . . . . . 16 𝑦 = ∅ → 𝑦 ≠ ∅)
184183adantl 475 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
185162adantr 474 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ Fin)
186 suprfinzcl 11844 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ ℤ ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin) → sup(𝑦, ℝ, < ) ∈ 𝑦)
187182, 184, 185, 186syl3anc 1439 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑦)
188178, 187sseldd 3821 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ𝑀))
189188adantll 704 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ𝑀))
19014recnd 10405 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
191159, 160, 190syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ ℂ)
192191adantlr 705 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ ℂ)
193176, 189, 192fsumser 14868 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘) = (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )))
19410eqcomi 2786 . . . . . . . . . . . . 13 seq𝑀( + , 𝐹) = 𝐺
195194fveq1i 6447 . . . . . . . . . . . 12 (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < ))
196195a1i 11 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < )))
197175, 193, 1963eqtrd 2817 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = (𝐺‘sup(𝑦, ℝ, < )))
19879adantr 474 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → Fun 𝐺)
199198adantr 474 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Fun 𝐺)
200189, 82syl6eleq 2868 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑍)
20185ad2antrr 716 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → 𝑍 = dom 𝐺)
202200, 201eleqtrd 2860 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ dom 𝐺)
203 fvelrn 6616 . . . . . . . . . . 11 ((Fun 𝐺 ∧ sup(𝑦, ℝ, < ) ∈ dom 𝐺) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
204199, 202, 203syl2anc 579 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
205197, 204eqeltrd 2858 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ran 𝐺)
206 suprub 11338 . . . . . . . . 9 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ran 𝐺) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
207168, 170, 172, 205, 206syl31anc 1441 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
208147, 156, 158, 166, 207xrletrd 12305 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
209136, 208pm2.61dan 803 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
210209ralrimiva 3147 . . . . 5 (𝜑 → ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
211 nfv 1957 . . . . . 6 𝑘𝜑
212211, 3, 142, 60sge0lefimpt 41546 . . . . 5 (𝜑 → ((Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ) ↔ ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < )))
213210, 212mpbird 249 . . . 4 (𝜑 → (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
21462, 213eqbrtrd 4908 . . 3 (𝜑 → (Σ^𝐹) ≤ sup(ran 𝐺, ℝ, < ))
21536ssriv 3824 . . . . . . . . . . . . 13 (𝑀...𝑗) ⊆ 𝑍
216215a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑀...𝑗) ⊆ 𝑍)
2173, 142, 216sge0lessmpt 41522 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
2182173ad2ant1 1124 . . . . . . . . . 10 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
219 fzfid 13091 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀...𝑗) ∈ Fin)
22036, 13sylan2 586 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ (0[,)+∞))
221219, 220sge0fsummpt 41513 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘))
2222213ad2ant1 1124 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘))
22334, 37, 11syl2anc 579 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) = (𝐹𝑘))
22434, 37, 190syl2anc 579 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ ℂ)
225223, 33, 224fsumser 14868 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
2262253adant3 1123 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
227222, 226eqtrd 2813 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = (seq𝑀( + , 𝐹)‘𝑗))
228194fveq1i 6447 . . . . . . . . . . . . 13 (seq𝑀( + , 𝐹)‘𝑗) = (𝐺𝑗)
229228a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺𝑗))
230 simp3 1129 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) = 𝑧)
231227, 229, 2303eqtrrd 2818 . . . . . . . . . . 11 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧 = (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))))
232623ad2ant1 1124 . . . . . . . . . . 11 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^𝐹) = (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
233231, 232breq12d 4899 . . . . . . . . . 10 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝑧 ≤ (Σ^𝐹) ↔ (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘)))))
234218, 233mpbird 249 . . . . . . . . 9 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧 ≤ (Σ^𝐹))
2352343exp 1109 . . . . . . . 8 (𝜑 → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹))))
236235adantr 474 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹))))
237236rexlimdv 3211 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → (∃𝑗𝑍 (𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹)))
238107, 237mpd 15 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ≤ (Σ^𝐹))
239238ralrimiva 3147 . . . 4 (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹))
2403, 7sge0cl 41504 . . . . . 6 (𝜑 → (Σ^𝐹) ∈ (0[,]+∞))
24159ltpnfd 12266 . . . . . . . . 9 (𝜑 → sup(ran 𝐺, ℝ, < ) < +∞)
2428, 60, 91, 214, 241xrlelttrd 12303 . . . . . . . 8 (𝜑 → (Σ^𝐹) < +∞)
2438, 91, 242xrgtned 40428 . . . . . . 7 (𝜑 → +∞ ≠ (Σ^𝐹))
244243necomd 3023 . . . . . 6 (𝜑 → (Σ^𝐹) ≠ +∞)
245 ge0xrre 40648 . . . . . 6 (((Σ^𝐹) ∈ (0[,]+∞) ∧ (Σ^𝐹) ≠ +∞) → (Σ^𝐹) ∈ ℝ)
246240, 244, 245syl2anc 579 . . . . 5 (𝜑 → (Σ^𝐹) ∈ ℝ)
247 suprleub 11343 . . . . 5 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (Σ^𝐹) ∈ ℝ) → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹)))
24878, 101, 131, 246, 247syl31anc 1441 . . . 4 (𝜑 → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹)))
249239, 248mpbird 249 . . 3 (𝜑 → sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹))
2508, 60, 214, 249xrletrid 12298 . 2 (𝜑 → (Σ^𝐹) = sup(ran 𝐺, ℝ, < ))
251 climuni 14691 . . 3 ((𝐺𝐵𝐺 ⇝ sup(ran 𝐺, ℝ, < )) → 𝐵 = sup(ran 𝐺, ℝ, < ))
25224, 58, 251syl2anc 579 . 2 (𝜑𝐵 = sup(ran 𝐺, ℝ, < ))
253250, 252eqtr4d 2816 1 (𝜑 → (Σ^𝐹) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2106  wne 2968  wral 3089  wrex 3090  Vcvv 3397  cin 3790  wss 3791  c0 4140  𝒫 cpw 4378   class class class wbr 4886  cmpt 4965  dom cdm 5355  ran crn 5356  Fun wfun 6129   Fn wfn 6130  wf 6131  cfv 6135  (class class class)co 6922  Fincfn 8241  supcsup 8634  cc 10270  cr 10271  0cc0 10272   + caddc 10275  +∞cpnf 10408  *cxr 10410   < clt 10411  cle 10412  cz 11728  cuz 11992  [,)cico 12489  [,]cicc 12490  ...cfz 12643  seqcseq 13119  abscabs 14381  cli 14623  Σcsu 14824  Σ^csumge0 41485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-n0 11643  df-z 11729  df-uz 11993  df-rp 12138  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-rlim 14628  df-sum 14825  df-sumge0 41486
This theorem is referenced by:  sge0isummpt  41553
  Copyright terms: Public domain W3C validator