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 40407
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 𝑍 = (ℤ𝑀)
2 fvex 6188 . . . . . 6 (ℤ𝑀) ∈ V
31, 2eqeltri 2695 . . . . 5 𝑍 ∈ V
43a1i 11 . . . 4 (𝜑𝑍 ∈ V)
5 sge0isum.f . . . . 5 (𝜑𝐹:𝑍⟶(0[,)+∞))
6 icossicc 12245 . . . . . 6 (0[,)+∞) ⊆ (0[,]+∞)
76a1i 11 . . . . 5 (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
85, 7fssd 6044 . . . 4 (𝜑𝐹:𝑍⟶(0[,]+∞))
94, 8sge0xrcl 40365 . . 3 (𝜑 → (Σ^𝐹) ∈ ℝ*)
10 sge0isum.m . . . . 5 (𝜑𝑀 ∈ ℤ)
11 sge0isum.g . . . . . 6 𝐺 = seq𝑀( + , 𝐹)
12 eqidd 2621 . . . . . 6 ((𝜑𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
13 rge0ssre 12265 . . . . . . 7 (0[,)+∞) ⊆ ℝ
145ffvelrnda 6345 . . . . . . 7 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ (0[,)+∞))
1513, 14sseldi 3593 . . . . . 6 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
16 0xr 10071 . . . . . . . 8 0 ∈ ℝ*
1716a1i 11 . . . . . . 7 ((𝜑𝑘𝑍) → 0 ∈ ℝ*)
18 pnfxr 10077 . . . . . . . 8 +∞ ∈ ℝ*
1918a1i 11 . . . . . . 7 ((𝜑𝑘𝑍) → +∞ ∈ ℝ*)
20 icogelb 12210 . . . . . . 7 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑘))
2117, 19, 14, 20syl3anc 1324 . . . . . 6 ((𝜑𝑘𝑍) → 0 ≤ (𝐹𝑘))
22 seqex 12786 . . . . . . . . . . 11 seq𝑀( + , 𝐹) ∈ V
2311, 22eqeltri 2695 . . . . . . . . . 10 𝐺 ∈ V
2423a1i 11 . . . . . . . . 9 (𝜑𝐺 ∈ V)
25 sge0isum.gcnv . . . . . . . . . 10 (𝜑𝐺𝐵)
26 climcl 14211 . . . . . . . . . 10 (𝐺𝐵𝐵 ∈ ℂ)
2725, 26syl 17 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
28 breldmg 5319 . . . . . . . . 9 ((𝐺 ∈ V ∧ 𝐵 ∈ ℂ ∧ 𝐺𝐵) → 𝐺 ∈ dom ⇝ )
2924, 27, 25, 28syl3anc 1324 . . . . . . . 8 (𝜑𝐺 ∈ dom ⇝ )
3011a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝐺 = seq𝑀( + , 𝐹))
3130fveq1d 6180 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (𝐺𝑗) = (seq𝑀( + , 𝐹)‘𝑗))
321eleq2i 2691 . . . . . . . . . . . . . 14 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
3332biimpi 206 . . . . . . . . . . . . 13 (𝑗𝑍𝑗 ∈ (ℤ𝑀))
3433adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
35 simpll 789 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑)
36 elfzuz 12323 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ𝑀))
3736, 1syl6eleqr 2710 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑀...𝑗) → 𝑘𝑍)
3837adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘𝑍)
3935, 38, 15syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ ℝ)
40 readdcl 10004 . . . . . . . . . . . . 13 ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ)
4140adantl 482 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
4234, 39, 41seqcl 12804 . . . . . . . . . . 11 ((𝜑𝑗𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
4331, 42eqeltrd 2699 . . . . . . . . . 10 ((𝜑𝑗𝑍) → (𝐺𝑗) ∈ ℝ)
4443recnd 10053 . . . . . . . . 9 ((𝜑𝑗𝑍) → (𝐺𝑗) ∈ ℂ)
4544ralrimiva 2963 . . . . . . . 8 (𝜑 → ∀𝑗𝑍 (𝐺𝑗) ∈ ℂ)
461climbdd 14383 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝐺 ∈ dom ⇝ ∧ ∀𝑗𝑍 (𝐺𝑗) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥)
4710, 29, 45, 46syl3anc 1324 . . . . . . 7 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥)
4843ad4ant13 1290 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ∈ ℝ)
4944ad4ant13 1290 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ∈ ℂ)
5049abscld 14156 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (abs‘(𝐺𝑗)) ∈ ℝ)
51 simpllr 798 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → 𝑥 ∈ ℝ)
5248leabsd 14134 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ≤ (abs‘(𝐺𝑗)))
53 simpr 477 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (abs‘(𝐺𝑗)) ≤ 𝑥)
5448, 50, 51, 52, 53letrd 10179 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) ∧ (abs‘(𝐺𝑗)) ≤ 𝑥) → (𝐺𝑗) ≤ 𝑥)
5554ex 450 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗𝑍) → ((abs‘(𝐺𝑗)) ≤ 𝑥 → (𝐺𝑗) ≤ 𝑥))
5655ralimdva 2959 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ) → (∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥 → ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥))
5756reximdva 3014 . . . . . . 7 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍 (abs‘(𝐺𝑗)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥))
5847, 57mpd 15 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥)
591, 11, 10, 12, 15, 21, 58isumsup2 14559 . . . . 5 (𝜑𝐺 ⇝ sup(ran 𝐺, ℝ, < ))
601, 10, 59, 43climrecl 14295 . . . 4 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ)
6160rexrd 10074 . . 3 (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
625feqmptd 6236 . . . . 5 (𝜑𝐹 = (𝑘𝑍 ↦ (𝐹𝑘)))
6362fveq2d 6182 . . . 4 (𝜑 → (Σ^𝐹) = (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
64 mpteq1 4728 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑘𝑦 ↦ (𝐹𝑘)) = (𝑘 ∈ ∅ ↦ (𝐹𝑘)))
6564fveq2d 6182 . . . . . . . . . 10 (𝑦 = ∅ → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))))
66 mpt0 6008 . . . . . . . . . . . . 13 (𝑘 ∈ ∅ ↦ (𝐹𝑘)) = ∅
6766fveq2i 6181 . . . . . . . . . . . 12 ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = (Σ^‘∅)
68 sge00 40356 . . . . . . . . . . . 12 ^‘∅) = 0
6967, 68eqtri 2642 . . . . . . . . . . 11 ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = 0
7069a1i 11 . . . . . . . . . 10 (𝑦 = ∅ → (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹𝑘))) = 0)
7165, 70eqtrd 2654 . . . . . . . . 9 (𝑦 = ∅ → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = 0)
7271adantl 482 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) = 0)
73 0red 10026 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
7440adantl 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
751, 10, 15, 74seqf 12805 . . . . . . . . . . . . 13 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
7611a1i 11 . . . . . . . . . . . . . 14 (𝜑𝐺 = seq𝑀( + , 𝐹))
7776feq1d 6017 . . . . . . . . . . . . 13 (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ))
7875, 77mpbird 247 . . . . . . . . . . . 12 (𝜑𝐺:𝑍⟶ℝ)
79 frn 6040 . . . . . . . . . . . 12 (𝐺:𝑍⟶ℝ → ran 𝐺 ⊆ ℝ)
8078, 79syl 17 . . . . . . . . . . 11 (𝜑 → ran 𝐺 ⊆ ℝ)
81 ffun 6035 . . . . . . . . . . . . 13 (𝐺:𝑍⟶ℝ → Fun 𝐺)
8278, 81syl 17 . . . . . . . . . . . 12 (𝜑 → Fun 𝐺)
83 uzid 11687 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
8410, 83syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ𝑀))
851eqcomi 2629 . . . . . . . . . . . . . 14 (ℤ𝑀) = 𝑍
8684, 85syl6eleq 2709 . . . . . . . . . . . . 13 (𝜑𝑀𝑍)
87 fdm 6038 . . . . . . . . . . . . . . 15 (𝐺:𝑍⟶ℝ → dom 𝐺 = 𝑍)
8878, 87syl 17 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑍)
8988eqcomd 2626 . . . . . . . . . . . . 13 (𝜑𝑍 = dom 𝐺)
9086, 89eleqtrd 2701 . . . . . . . . . . . 12 (𝜑𝑀 ∈ dom 𝐺)
91 fvelrn 6338 . . . . . . . . . . . 12 ((Fun 𝐺𝑀 ∈ dom 𝐺) → (𝐺𝑀) ∈ ran 𝐺)
9282, 90, 91syl2anc 692 . . . . . . . . . . 11 (𝜑 → (𝐺𝑀) ∈ ran 𝐺)
9380, 92sseldd 3596 . . . . . . . . . 10 (𝜑 → (𝐺𝑀) ∈ ℝ)
9416a1i 11 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℝ*)
9518a1i 11 . . . . . . . . . . . 12 (𝜑 → +∞ ∈ ℝ*)
965, 86ffvelrnd 6346 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑀) ∈ (0[,)+∞))
97 icogelb 12210 . . . . . . . . . . . 12 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹𝑀) ∈ (0[,)+∞)) → 0 ≤ (𝐹𝑀))
9894, 95, 96, 97syl3anc 1324 . . . . . . . . . . 11 (𝜑 → 0 ≤ (𝐹𝑀))
9911fveq1i 6179 . . . . . . . . . . . . 13 (𝐺𝑀) = (seq𝑀( + , 𝐹)‘𝑀)
10099a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐺𝑀) = (seq𝑀( + , 𝐹)‘𝑀))
101 seq1 12797 . . . . . . . . . . . . 13 (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
10210, 101syl 17 . . . . . . . . . . . 12 (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹𝑀))
103100, 102eqtr2d 2655 . . . . . . . . . . 11 (𝜑 → (𝐹𝑀) = (𝐺𝑀))
10498, 103breqtrd 4670 . . . . . . . . . 10 (𝜑 → 0 ≤ (𝐺𝑀))
105 ne0i 3913 . . . . . . . . . . . 12 ((𝐺𝑀) ∈ ran 𝐺 → ran 𝐺 ≠ ∅)
10692, 105syl 17 . . . . . . . . . . 11 (𝜑 → ran 𝐺 ≠ ∅)
107 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺)
108 ffn 6032 . . . . . . . . . . . . . . . . . . . . 21 (𝐺:𝑍⟶ℝ → 𝐺 Fn 𝑍)
10978, 108syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 Fn 𝑍)
110 fvelrnb 6230 . . . . . . . . . . . . . . . . . . . 20 (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
111109, 110syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
112111adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗𝑍 (𝐺𝑗) = 𝑧))
113107, 112mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧 ∈ ran 𝐺) → ∃𝑗𝑍 (𝐺𝑗) = 𝑧)
114113adantlr 750 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗𝑍 (𝐺𝑗) = 𝑧)
115 nfv 1841 . . . . . . . . . . . . . . . . . . 19 𝑗𝜑
116 nfra1 2938 . . . . . . . . . . . . . . . . . . 19 𝑗𝑗𝑍 (𝐺𝑗) ≤ 𝑥
117115, 116nfan 1826 . . . . . . . . . . . . . . . . . 18 𝑗(𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥)
118 nfv 1841 . . . . . . . . . . . . . . . . . 18 𝑗 𝑧 ∈ ran 𝐺
119117, 118nfan 1826 . . . . . . . . . . . . . . . . 17 𝑗((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺)
120 nfv 1841 . . . . . . . . . . . . . . . . 17 𝑗 𝑧𝑥
121 rspa 2927 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍) → (𝐺𝑗) ≤ 𝑥)
1221213adant3 1079 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) ≤ 𝑥)
123 simp3 1061 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) = 𝑧)
124 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺𝑗) = 𝑧 → (𝐺𝑗) = 𝑧)
125124eqcomd 2626 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺𝑗) = 𝑧𝑧 = (𝐺𝑗))
126125adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → 𝑧 = (𝐺𝑗))
127 simpl 473 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) ≤ 𝑥)
128126, 127eqbrtrd 4666 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝑗) ≤ 𝑥 ∧ (𝐺𝑗) = 𝑧) → 𝑧𝑥)
129122, 123, 128syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧𝑥)
1301293exp 1262 . . . . . . . . . . . . . . . . . 18 (∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧𝑥)))
131130ad2antlr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧𝑥)))
132119, 120, 131rexlimd 3022 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗𝑍 (𝐺𝑗) = 𝑧𝑧𝑥))
133114, 132mpd 15 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → 𝑧𝑥)
134133ralrimiva 2963 . . . . . . . . . . . . . 14 ((𝜑 ∧ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥) → ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
135134ex 450 . . . . . . . . . . . . 13 (𝜑 → (∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐺 𝑧𝑥))
136135reximdv 3013 . . . . . . . . . . . 12 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗𝑍 (𝐺𝑗) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥))
13758, 136mpd 15 . . . . . . . . . . 11 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
138 suprub 10969 . . . . . . . . . . 11 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (𝐺𝑀) ∈ ran 𝐺) → (𝐺𝑀) ≤ sup(ran 𝐺, ℝ, < ))
13980, 106, 137, 92, 138syl31anc 1327 . . . . . . . . . 10 (𝜑 → (𝐺𝑀) ≤ sup(ran 𝐺, ℝ, < ))
14073, 93, 60, 104, 139letrd 10179 . . . . . . . . 9 (𝜑 → 0 ≤ sup(ran 𝐺, ℝ, < ))
141140ad2antrr 761 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → 0 ≤ sup(ran 𝐺, ℝ, < ))
14272, 141eqbrtrd 4666 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
143 simpr 477 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ∈ (𝒫 𝑍 ∩ Fin))
144 simpll 789 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → 𝜑)
145 elpwinss 39036 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦𝑍)
146145sselda 3595 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘𝑦) → 𝑘𝑍)
147146adantll 749 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → 𝑘𝑍)
1486, 14sseldi 3593 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ (0[,]+∞))
149144, 147, 148syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑦) → (𝐹𝑘) ∈ (0[,]+∞))
150 eqid 2620 . . . . . . . . . . 11 (𝑘𝑦 ↦ (𝐹𝑘)) = (𝑘𝑦 ↦ (𝐹𝑘))
151149, 150fmptd 6371 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘𝑦 ↦ (𝐹𝑘)):𝑦⟶(0[,]+∞))
152143, 151sge0xrcl 40365 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ∈ ℝ*)
153152adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ∈ ℝ*)
154 fzfid 12755 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑀...sup(𝑦, ℝ, < )) ∈ Fin)
155 elfzuz 12323 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ (ℤ𝑀))
156155, 85syl6eleq 2709 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘𝑍)
157156, 148sylan2 491 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,]+∞))
158 eqid 2620 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)) = (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))
159157, 158fmptd 6371 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
160159adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
161154, 160sge0xrcl 40365 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ℝ*)
162161adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ℝ*)
16361adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
164163adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
165 simpll 789 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝜑)
166156adantl 482 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝑘𝑍)
167165, 166, 148syl2anc 692 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,]+∞))
168 elinel2 3792 . . . . . . . . . . . 12 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ∈ Fin)
1691, 145, 168ssuzfz 39378 . . . . . . . . . . 11 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
170169adantl 482 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
171154, 167, 170sge0lessmpt 40379 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))))
172171adantr 481 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))))
17380adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ⊆ ℝ)
174173adantr 481 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ⊆ ℝ)
175106adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ≠ ∅)
176175adantr 481 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ≠ ∅)
177137adantr 481 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
178177adantr 481 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥)
179165, 166, 14syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ (0[,)+∞))
180154, 179sge0fsummpt 40370 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘))
181180adantr 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘))
182 eqidd 2621 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) = (𝐹𝑘))
183145, 1syl6sseq 3643 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (ℤ𝑀))
184183adantr 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ (ℤ𝑀))
185 uzssz 11692 . . . . . . . . . . . . . . . . . 18 (ℤ𝑀) ⊆ ℤ
1861, 185eqsstri 3627 . . . . . . . . . . . . . . . . 17 𝑍 ⊆ ℤ
187145, 186syl6ss 3607 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ ℤ)
188187adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ ℤ)
189 neqne 2799 . . . . . . . . . . . . . . . 16 𝑦 = ∅ → 𝑦 ≠ ∅)
190189adantl 482 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
191168adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ Fin)
192 suprfinzcl 11477 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ ℤ ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin) → sup(𝑦, ℝ, < ) ∈ 𝑦)
193188, 190, 191, 192syl3anc 1324 . . . . . . . . . . . . . 14 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑦)
194184, 193sseldd 3596 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ𝑀))
195194adantll 749 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ𝑀))
19615recnd 10053 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
197165, 166, 196syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ ℂ)
198197adantlr 750 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹𝑘) ∈ ℂ)
199182, 195, 198fsumser 14442 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹𝑘) = (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )))
20011eqcomi 2629 . . . . . . . . . . . . 13 seq𝑀( + , 𝐹) = 𝐺
201200fveq1i 6179 . . . . . . . . . . . 12 (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < ))
202201a1i 11 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < )))
203181, 199, 2023eqtrd 2658 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) = (𝐺‘sup(𝑦, ℝ, < )))
20482adantr 481 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → Fun 𝐺)
205204adantr 481 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Fun 𝐺)
206195, 85syl6eleq 2709 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑍)
20789ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → 𝑍 = dom 𝐺)
208206, 207eleqtrd 2701 . . . . . . . . . . 11 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ dom 𝐺)
209 fvelrn 6338 . . . . . . . . . . 11 ((Fun 𝐺 ∧ sup(𝑦, ℝ, < ) ∈ dom 𝐺) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
210205, 208, 209syl2anc 692 . . . . . . . . . 10 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
211203, 210eqeltrd 2699 . . . . . . . . 9 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ran 𝐺)
212 suprub 10969 . . . . . . . . 9 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ∈ ran 𝐺) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
213174, 176, 178, 211, 212syl31anc 1327 . . . . . . . 8 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
214153, 162, 164, 172, 213xrletrd 11978 . . . . . . 7 (((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
215142, 214pm2.61dan 831 . . . . . 6 ((𝜑𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
216215ralrimiva 2963 . . . . 5 (𝜑 → ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
217 nfv 1841 . . . . . 6 𝑘𝜑
218217, 4, 148, 61sge0lefimpt 40403 . . . . 5 (𝜑 → ((Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ) ↔ ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘𝑦 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < )))
219216, 218mpbird 247 . . . 4 (𝜑 → (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
22063, 219eqbrtrd 4666 . . 3 (𝜑 → (Σ^𝐹) ≤ sup(ran 𝐺, ℝ, < ))
22137ssriv 3599 . . . . . . . . . . . . 13 (𝑀...𝑗) ⊆ 𝑍
222221a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑀...𝑗) ⊆ 𝑍)
2234, 148, 222sge0lessmpt 40379 . . . . . . . . . . 11 (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
2242233ad2ant1 1080 . . . . . . . . . 10 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
225 fzfid 12755 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀...𝑗) ∈ Fin)
22637, 14sylan2 491 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ (0[,)+∞))
227225, 226sge0fsummpt 40370 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘))
2282273ad2ant1 1080 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘))
22935, 38, 12syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) = (𝐹𝑘))
23035, 38, 196syl2anc 692 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹𝑘) ∈ ℂ)
231229, 34, 230fsumser 14442 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
2322313adant3 1079 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
233228, 232eqtrd 2654 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) = (seq𝑀( + , 𝐹)‘𝑗))
234200fveq1i 6179 . . . . . . . . . . . . 13 (seq𝑀( + , 𝐹)‘𝑗) = (𝐺𝑗)
235234a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺𝑗))
236 simp3 1061 . . . . . . . . . . . 12 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝐺𝑗) = 𝑧)
237233, 235, 2363eqtrrd 2659 . . . . . . . . . . 11 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧 = (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))))
238633ad2ant1 1080 . . . . . . . . . . 11 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (Σ^𝐹) = (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘))))
239237, 238breq12d 4657 . . . . . . . . . 10 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → (𝑧 ≤ (Σ^𝐹) ↔ (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹𝑘))) ≤ (Σ^‘(𝑘𝑍 ↦ (𝐹𝑘)))))
240224, 239mpbird 247 . . . . . . . . 9 ((𝜑𝑗𝑍 ∧ (𝐺𝑗) = 𝑧) → 𝑧 ≤ (Σ^𝐹))
2412403exp 1262 . . . . . . . 8 (𝜑 → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹))))
242241adantr 481 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐺) → (𝑗𝑍 → ((𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹))))
243242rexlimdv 3026 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐺) → (∃𝑗𝑍 (𝐺𝑗) = 𝑧𝑧 ≤ (Σ^𝐹)))
244113, 243mpd 15 . . . . 5 ((𝜑𝑧 ∈ ran 𝐺) → 𝑧 ≤ (Σ^𝐹))
245244ralrimiva 2963 . . . 4 (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹))
2464, 8sge0cl 40361 . . . . . 6 (𝜑 → (Σ^𝐹) ∈ (0[,]+∞))
24760ltpnfd 11940 . . . . . . . . 9 (𝜑 → sup(ran 𝐺, ℝ, < ) < +∞)
2489, 61, 95, 220, 247xrlelttrd 11976 . . . . . . . 8 (𝜑 → (Σ^𝐹) < +∞)
2499, 95, 248xrgtned 39351 . . . . . . 7 (𝜑 → +∞ ≠ (Σ^𝐹))
250249necomd 2846 . . . . . 6 (𝜑 → (Σ^𝐹) ≠ +∞)
251 ge0xrre 39561 . . . . . 6 (((Σ^𝐹) ∈ (0[,]+∞) ∧ (Σ^𝐹) ≠ +∞) → (Σ^𝐹) ∈ ℝ)
252246, 250, 251syl2anc 692 . . . . 5 (𝜑 → (Σ^𝐹) ∈ ℝ)
253 suprleub 10974 . . . . 5 (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧𝑥) ∧ (Σ^𝐹) ∈ ℝ) → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹)))
25480, 106, 137, 252, 253syl31anc 1327 . . . 4 (𝜑 → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^𝐹)))
255245, 254mpbird 247 . . 3 (𝜑 → sup(ran 𝐺, ℝ, < ) ≤ (Σ^𝐹))
2569, 61, 220, 255xrletrid 11971 . 2 (𝜑 → (Σ^𝐹) = sup(ran 𝐺, ℝ, < ))
257 climuni 14264 . . 3 ((𝐺𝐵𝐺 ⇝ sup(ran 𝐺, ℝ, < )) → 𝐵 = sup(ran 𝐺, ℝ, < ))
25825, 59, 257syl2anc 692 . 2 (𝜑𝐵 = sup(ran 𝐺, ℝ, < ))
259256, 258eqtr4d 2657 1 (𝜑 → (Σ^𝐹) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  Vcvv 3195  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149   class class class wbr 4644  cmpt 4720  dom cdm 5104  ran crn 5105  Fun wfun 5870   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  Fincfn 7940  supcsup 8331  cc 9919  cr 9920  0cc0 9921   + caddc 9924  +∞cpnf 10056  *cxr 10058   < clt 10059  cle 10060  cz 11362  cuz 11672  [,)cico 12162  [,]cicc 12163  ...cfz 12311  seqcseq 12784  abscabs 13955  cli 14196  Σcsu 14397  Σ^csumge0 40342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-z 11363  df-uz 11673  df-rp 11818  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-rlim 14201  df-sum 14398  df-sumge0 40343
This theorem is referenced by:  sge0isummpt  40410
  Copyright terms: Public domain W3C validator