Theorem sge0isum 46870

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.

Step	Hyp	Ref	Expression
1		sge0isum.z	. . . . . 6 ⊢ 𝑍 = (ℤ≥‘𝑀)
2	1	fvexi 6841	. . . . 5 ⊢ 𝑍 ∈ V
3	2	a1i 11	. . . 4 ⊢ (𝜑 → 𝑍 ∈ V)
4		sge0isum.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑍⟶(0[,)+∞))
5		icossicc 13380	. . . . . 6 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
6	5	a1i 11	. . . . 5 ⊢ (𝜑 → (0[,)+∞) ⊆ (0[,]+∞))
7	4, 6	fssd 6672	. . . 4 ⊢ (𝜑 → 𝐹:𝑍⟶(0[,]+∞))
8	3, 7	sge0xrcl 46828	. . 3 ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*)
9		sge0isum.m	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℤ)
10		sge0isum.g	. . . . . 6 ⊢ 𝐺 = seq𝑀( + , 𝐹)
11		eqidd 2740	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘))
12		rge0ssre 13400	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ
13	4	ffvelcdmda 7025	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,)+∞))
14	12, 13	sselid 3913	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)
15		0xr 11183	. . . . . . . 8 ⊢ 0 ∈ ℝ*
16	15	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ∈ ℝ*)
17		pnfxr 11190	. . . . . . . 8 ⊢ +∞ ∈ ℝ*
18	17	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → +∞ ∈ ℝ*)
19		icogelb 13340	. . . . . . 7 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹‘𝑘) ∈ (0[,)+∞)) → 0 ≤ (𝐹‘𝑘))
20	16, 18, 13, 19	syl3anc 1379	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐹‘𝑘))
21		seqex 13956	. . . . . . . . . . 11 ⊢ seq𝑀( + , 𝐹) ∈ V
22	10, 21	eqeltri 2835	. . . . . . . . . 10 ⊢ 𝐺 ∈ V
23	22	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ V)
24		sge0isum.gcnv	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⇝ 𝐵)
25		climcl 15452	. . . . . . . . . 10 ⊢ (𝐺 ⇝ 𝐵 → 𝐵 ∈ ℂ)
26	24, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
27		breldmg 5851	. . . . . . . . 9 ⊢ ((𝐺 ∈ V ∧ 𝐵 ∈ ℂ ∧ 𝐺 ⇝ 𝐵) → 𝐺 ∈ dom ⇝ )
28	23, 26, 24, 27	syl3anc 1379	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ dom ⇝ )
29	10	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐺 = seq𝑀( + , 𝐹))
30	29	fveq1d 6829	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) = (seq𝑀( + , 𝐹)‘𝑗))
31	1	eleq2i 2831	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀))
32	31	bilani 505	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀))
33		simpll 772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝜑)
34		elfzuz 13465	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ (ℤ≥‘𝑀))
35	34, 1	eleqtrrdi 2850	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (𝑀...𝑗) → 𝑘 ∈ 𝑍)
36	35	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → 𝑘 ∈ 𝑍)
37	33, 36, 14	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℝ)
38		readdcl 11112	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ) → (𝑘 + 𝑖) ∈ ℝ)
39	38	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
40	32, 37, 39	seqcl 13975	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ)
41	30, 40	eqeltrd 2839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ∈ ℝ)
42	41	recnd 11164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ∈ ℂ)
43	42	ralrimiva 3131	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ∈ ℂ)
44	1	climbdd 15625	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝐺 ∈ dom ⇝ ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ∈ ℂ) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥)
45	9, 28, 43, 44	syl3anc 1379	. . . . . . 7 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥)
46	41	ad4ant13 757	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ∈ ℝ)
47	42	ad4ant13 757	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ∈ ℂ)
48	47	abscld 15392	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (abs‘(𝐺‘𝑗)) ∈ ℝ)
49		simpllr 781	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → 𝑥 ∈ ℝ)
50	46	leabsd 15368	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ≤ (abs‘(𝐺‘𝑗)))
51		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (abs‘(𝐺‘𝑗)) ≤ 𝑥)
52	46, 48, 49, 50, 51	letrd 11294	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ (abs‘(𝐺‘𝑗)) ≤ 𝑥) → (𝐺‘𝑗) ≤ 𝑥)
53	52	ex 413	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) → ((abs‘(𝐺‘𝑗)) ≤ 𝑥 → (𝐺‘𝑗) ≤ 𝑥))
54	53	ralimdva 3151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥 → ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥))
55	54	reximdva 3152	. . . . . . 7 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (abs‘(𝐺‘𝑗)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥))
56	45, 55	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥)
57	1, 10, 9, 11, 14, 20, 56	isumsup2 15802	. . . . 5 ⊢ (𝜑 → 𝐺 ⇝ sup(ran 𝐺, ℝ, < ))
58	1, 9, 57, 41	climrecl 15536	. . . 4 ⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ)
59	58	rexrd 11186	. . 3 ⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
60	4	feqmptd 6895	. . . . 5 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))
61	60	fveq2d 6831	. . . 4 ⊢ (𝜑 → (Σ^‘𝐹) = (Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))))
62		mpteq1 5161	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)) = (𝑘 ∈ ∅ ↦ (𝐹‘𝑘)))
63	62	fveq2d 6831	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) = (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))))
64		mpt0 6627	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ∅ ↦ (𝐹‘𝑘)) = ∅
65	64	fveq2i 6830	. . . . . . . . . . . 12 ⊢ (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) = (Σ^‘∅)
66		sge00 46819	. . . . . . . . . . . 12 ⊢ (Σ^‘∅) = 0
67	65, 66	eqtri 2762	. . . . . . . . . . 11 ⊢ (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) = 0
68	67	a1i 11	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → (Σ^‘(𝑘 ∈ ∅ ↦ (𝐹‘𝑘))) = 0)
69	63, 68	eqtrd 2774	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) = 0)
70	69	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) = 0)
71		0red 11138	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
72	38	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ ℝ ∧ 𝑖 ∈ ℝ)) → (𝑘 + 𝑖) ∈ ℝ)
73	1, 9, 14, 72	seqf 13976	. . . . . . . . . . . . 13 ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
74	10	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 = seq𝑀( + , 𝐹))
75	74	feq1d 6637	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺:𝑍⟶ℝ ↔ seq𝑀( + , 𝐹):𝑍⟶ℝ))
76	73, 75	mpbird 258	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:𝑍⟶ℝ)
77	76	frnd 6663	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐺 ⊆ ℝ)
78	76	ffund 6659	. . . . . . . . . . . 12 ⊢ (𝜑 → Fun 𝐺)
79		uzid 12794	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
80	9, 79	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
81	1	eqcomi 2748	. . . . . . . . . . . . . 14 ⊢ (ℤ≥‘𝑀) = 𝑍
82	80, 81	eleqtrdi 2849	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
83	76	fdmd 6665	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑍)
84	83	eqcomd 2745	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 = dom 𝐺)
85	82, 84	eleqtrd 2841	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ dom 𝐺)
86		fvelrn 7017	. . . . . . . . . . . 12 ⊢ ((Fun 𝐺 ∧ 𝑀 ∈ dom 𝐺) → (𝐺‘𝑀) ∈ ran 𝐺)
87	78, 85, 86	syl2anc 590	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺‘𝑀) ∈ ran 𝐺)
88	77, 87	sseldd 3916	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘𝑀) ∈ ℝ)
89	15	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℝ*)
90	17	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → +∞ ∈ ℝ*)
91	4, 82	ffvelcdmd 7026	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘𝑀) ∈ (0[,)+∞))
92		icogelb 13340	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝐹‘𝑀) ∈ (0[,)+∞)) → 0 ≤ (𝐹‘𝑀))
93	89, 90, 91, 92	syl3anc 1379	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ≤ (𝐹‘𝑀))
94	10	fveq1i 6828	. . . . . . . . . . . . 13 ⊢ (𝐺‘𝑀) = (seq𝑀( + , 𝐹)‘𝑀)
95	94	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺‘𝑀) = (seq𝑀( + , 𝐹)‘𝑀))
96		seq1 13967	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℤ → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
97	9, 96	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
98	95, 97	eqtr2d 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝑀) = (𝐺‘𝑀))
99	93, 98	breqtrd 5098	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (𝐺‘𝑀))
100	87	ne0d 4270	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐺 ≠ ∅)
101		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ∈ ran 𝐺)
102	76	ffnd 6656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 Fn 𝑍)
103		fvelrnb 6887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Fn 𝑍 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧))
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧))
105	104	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑧 ∈ ran 𝐺 ↔ ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧))
106	101, 105	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)
107	106	adantlr 721	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → ∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧)
108		nfv 1921	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝜑
109		nfra1 3263	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥
110	108, 109	nfan 1906	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥)
111		nfv 1921	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗 𝑧 ∈ ran 𝐺
112	110, 111	nfan 1906	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺)
113		nfv 1921	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗 𝑧 ≤ 𝑥
114		rspa 3228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍) → (𝐺‘𝑗) ≤ 𝑥)
115	114	3adant3 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) ≤ 𝑥)
116		simp3 1144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) = 𝑧)
117		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐺‘𝑗) = 𝑧 → (𝐺‘𝑗) = 𝑧)
118	117	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺‘𝑗) = 𝑧 → 𝑧 = (𝐺‘𝑗))
119	118	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 = (𝐺‘𝑗))
120		simpl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) ≤ 𝑥)
121	119, 120	eqbrtrd 5094	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺‘𝑗) ≤ 𝑥 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤ 𝑥)
122	115, 116, 121	syl2anc 590	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤ 𝑥)
123	122	3exp 1125	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥)))
124	123	ad2antlr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥)))
125	112, 113, 124	rexlimd 3246	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧 → 𝑧 ≤ 𝑥))
126	107, 125	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ≤ 𝑥)
127	126	ralrimiva 3131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥) → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥)
128	127	ex 413	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥))
129	128	reximdv 3154	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 (𝐺‘𝑗) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥))
130	56, 129	mpd 15	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥)
131		suprub 12108	. . . . . . . . . . 11 ⊢ (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧ (𝐺‘𝑀) ∈ ran 𝐺) → (𝐺‘𝑀) ≤ sup(ran 𝐺, ℝ, < ))
132	77, 100, 130, 87, 131	syl31anc 1381	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘𝑀) ≤ sup(ran 𝐺, ℝ, < ))
133	71, 88, 58, 99, 132	letrd 11294	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ sup(ran 𝐺, ℝ, < ))
134	133	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → 0 ≤ sup(ran 𝐺, ℝ, < ))
135	70, 134	eqbrtrd 5094	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
136		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ∈ (𝒫 𝑍 ∩ Fin))
137		simpll 772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝜑)
138		elpwinss 45497	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ 𝑍)
139	138	sselda 3915	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑍)
140	139	adantll 720	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ 𝑍)
141	5, 13	sselid 3913	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (0[,]+∞))
142	137, 140, 141	syl2anc 590	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝐹‘𝑘) ∈ (0[,]+∞))
143		eqid 2739	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)) = (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))
144	142, 143	fmptd 7055	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘)):𝑦⟶(0[,]+∞))
145	136, 144	sge0xrcl 46828	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ∈ ℝ*)
146	145	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ∈ ℝ*)
147		fzfid 13926	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑀...sup(𝑦, ℝ, < )) ∈ Fin)
148		elfzuz 13465	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ (ℤ≥‘𝑀))
149	148, 81	eleqtrdi 2849	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) → 𝑘 ∈ 𝑍)
150	149, 141	sylan2 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,]+∞))
151		eqid 2739	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)) = (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))
152	150, 151	fmptd 7055	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
153	152	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘)):(𝑀...sup(𝑦, ℝ, < ))⟶(0[,]+∞))
154	147, 153	sge0xrcl 46828	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈ ℝ*)
155	154	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈ ℝ*)
156	59	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
157	156	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(ran 𝐺, ℝ, < ) ∈ ℝ*)
158		simpll 772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝜑)
159	149	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → 𝑘 ∈ 𝑍)
160	158, 159, 141	syl2anc 590	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,]+∞))
161		elinel2 4131	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ∈ Fin)
162	1, 138, 161	ssuzfz 45794	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
163	162	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑦 ⊆ (𝑀...sup(𝑦, ℝ, < )))
164	147, 160, 163	sge0lessmpt 46842	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))))
165	164	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))))
166	77	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ⊆ ℝ)
167	166	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ⊆ ℝ)
168	100	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ran 𝐺 ≠ ∅)
169	168	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ran 𝐺 ≠ ∅)
170	130	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥)
171	170	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥)
172	158, 159, 13	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ (0[,)+∞))
173	147, 172	sge0fsummpt 46833	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘))
174	173	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘))
175		eqidd 2740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) = (𝐹‘𝑘))
176	138, 1	sseqtrdi 3955	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ (ℤ≥‘𝑀))
177	176	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ (ℤ≥‘𝑀))
178		uzssz 12800	. . . . . . . . . . . . . . . . . 18 ⊢ (ℤ≥‘𝑀) ⊆ ℤ
179	1, 178	eqsstri 3961	. . . . . . . . . . . . . . . . 17 ⊢ 𝑍 ⊆ ℤ
180	138, 179	sstrdi 3927	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (𝒫 𝑍 ∩ Fin) → 𝑦 ⊆ ℤ)
181	180	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ⊆ ℤ)
182		neqne 2942	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑦 = ∅ → 𝑦 ≠ ∅)
183	182	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ≠ ∅)
184	161	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → 𝑦 ∈ Fin)
185		suprfinzcl 12634	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ⊆ ℤ ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin) → sup(𝑦, ℝ, < ) ∈ 𝑦)
186	181, 183, 184, 185	syl3anc 1379	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑦)
187	177, 186	sseldd 3916	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝑍 ∩ Fin) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ≥‘𝑀))
188	187	adantll 720	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ (ℤ≥‘𝑀))
189	14	recnd 11164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
190	158, 159, 189	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ ℂ)
191	190	adantlr 721	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) ∧ 𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))) → (𝐹‘𝑘) ∈ ℂ)
192	175, 188, 191	fsumser 15683	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Σ𝑘 ∈ (𝑀...sup(𝑦, ℝ, < ))(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )))
193	10	eqcomi 2748	. . . . . . . . . . . . 13 ⊢ seq𝑀( + , 𝐹) = 𝐺
194	193	fveq1i 6828	. . . . . . . . . . . 12 ⊢ (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < ))
195	194	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (seq𝑀( + , 𝐹)‘sup(𝑦, ℝ, < )) = (𝐺‘sup(𝑦, ℝ, < )))
196	174, 192, 195	3eqtrd 2778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) = (𝐺‘sup(𝑦, ℝ, < )))
197	78	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → Fun 𝐺)
198	197	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → Fun 𝐺)
199	188, 81	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ 𝑍)
200	84	ad2antrr 732	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → 𝑍 = dom 𝐺)
201	199, 200	eleqtrd 2841	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → sup(𝑦, ℝ, < ) ∈ dom 𝐺)
202		fvelrn 7017	. . . . . . . . . . 11 ⊢ ((Fun 𝐺 ∧ sup(𝑦, ℝ, < ) ∈ dom 𝐺) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
203	198, 201, 202	syl2anc 590	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (𝐺‘sup(𝑦, ℝ, < )) ∈ ran 𝐺)
204	196, 203	eqeltrd 2839	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈ ran 𝐺)
205		suprub 12108	. . . . . . . . 9 ⊢ (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧ (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ∈ ran 𝐺) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
206	167, 169, 171, 204, 205	syl31anc 1381	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ (𝑀...sup(𝑦, ℝ, < )) ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
207	146, 155, 157, 165, 206	xrletrd 13104	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) ∧ ¬ 𝑦 = ∅) → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
208	135, 207	pm2.61dan 818	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
209	208	ralrimiva 3131	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
210		nfv 1921	. . . . . 6 ⊢ Ⅎ𝑘𝜑
211	210, 3, 141, 59	sge0lefimpt 46866	. . . . 5 ⊢ (𝜑 → ((Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ) ↔ ∀𝑦 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑘 ∈ 𝑦 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < )))
212	209, 211	mpbird 258	. . . 4 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))) ≤ sup(ran 𝐺, ℝ, < ))
213	61, 212	eqbrtrd 5094	. . 3 ⊢ (𝜑 → (Σ^‘𝐹) ≤ sup(ran 𝐺, ℝ, < ))
214	35	ssriv 3919	. . . . . . . . . . . . 13 ⊢ (𝑀...𝑗) ⊆ 𝑍
215	214	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀...𝑗) ⊆ 𝑍)
216	3, 141, 215	sge0lessmpt 46842	. . . . . . . . . . 11 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤ (Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))))
217	216	3ad2ant1 1139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤ (Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))))
218		fzfid 13926	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀...𝑗) ∈ Fin)
219	35, 13	sylan2 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ (0[,)+∞))
220	218, 219	sge0fsummpt 46833	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))
221	220	3ad2ant1 1139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘))
222	33, 36, 11	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) = (𝐹‘𝑘))
223	33, 36, 189	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (𝑀...𝑗)) → (𝐹‘𝑘) ∈ ℂ)
224	222, 32, 223	fsumser 15683	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
225	224	3adant3 1138	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → Σ𝑘 ∈ (𝑀...𝑗)(𝐹‘𝑘) = (seq𝑀( + , 𝐹)‘𝑗))
226	221, 225	eqtrd 2774	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) = (seq𝑀( + , 𝐹)‘𝑗))
227	193	fveq1i 6828	. . . . . . . . . . . . 13 ⊢ (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗)
228	227	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (seq𝑀( + , 𝐹)‘𝑗) = (𝐺‘𝑗))
229		simp3 1144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝐺‘𝑗) = 𝑧)
230	226, 228, 229	3eqtrrd 2779	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 = (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))))
231	61	3ad2ant1 1139	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (Σ^‘𝐹) = (Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘))))
232	230, 231	breq12d 5085	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → (𝑧 ≤ (Σ^‘𝐹) ↔ (Σ^‘(𝑘 ∈ (𝑀...𝑗) ↦ (𝐹‘𝑘))) ≤ (Σ^‘(𝑘 ∈ 𝑍 ↦ (𝐹‘𝑘)))))
233	217, 232	mpbird 258	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ (𝐺‘𝑗) = 𝑧) → 𝑧 ≤ (Σ^‘𝐹))
234	233	3exp 1125	. . . . . . . 8 ⊢ (𝜑 → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤ (Σ^‘𝐹))))
235	234	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (𝑗 ∈ 𝑍 → ((𝐺‘𝑗) = 𝑧 → 𝑧 ≤ (Σ^‘𝐹))))
236	235	rexlimdv 3138	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → (∃𝑗 ∈ 𝑍 (𝐺‘𝑗) = 𝑧 → 𝑧 ≤ (Σ^‘𝐹)))
237	106, 236	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ran 𝐺) → 𝑧 ≤ (Σ^‘𝐹))
238	237	ralrimiva 3131	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^‘𝐹))
239	3, 7	sge0cl 46824	. . . . . 6 ⊢ (𝜑 → (Σ^‘𝐹) ∈ (0[,]+∞))
240	58	ltpnfd 13063	. . . . . . . . 9 ⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) < +∞)
241	8, 59, 90, 213, 240	xrlelttrd 13102	. . . . . . . 8 ⊢ (𝜑 → (Σ^‘𝐹) < +∞)
242	8, 90, 241	xrgtned 13106	. . . . . . 7 ⊢ (𝜑 → +∞ ≠ (Σ^‘𝐹))
243	242	necomd 2989	. . . . . 6 ⊢ (𝜑 → (Σ^‘𝐹) ≠ +∞)
244		ge0xrre 45976	. . . . . 6 ⊢ (((Σ^‘𝐹) ∈ (0[,]+∞) ∧ (Σ^‘𝐹) ≠ +∞) → (Σ^‘𝐹) ∈ ℝ)
245	239, 243, 244	syl2anc 590	. . . . 5 ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)
246		suprleub 12113	. . . . 5 ⊢ (((ran 𝐺 ⊆ ℝ ∧ ran 𝐺 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ 𝑥) ∧ (Σ^‘𝐹) ∈ ℝ) → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^‘𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^‘𝐹)))
247	77, 100, 130, 245, 246	syl31anc 1381	. . . 4 ⊢ (𝜑 → (sup(ran 𝐺, ℝ, < ) ≤ (Σ^‘𝐹) ↔ ∀𝑧 ∈ ran 𝐺 𝑧 ≤ (Σ^‘𝐹)))
248	238, 247	mpbird 258	. . 3 ⊢ (𝜑 → sup(ran 𝐺, ℝ, < ) ≤ (Σ^‘𝐹))
249	8, 59, 213, 248	xrletrid 13097	. 2 ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran 𝐺, ℝ, < ))
250		climuni 15505	. . 3 ⊢ ((𝐺 ⇝ 𝐵 ∧ 𝐺 ⇝ sup(ran 𝐺, ℝ, < )) → 𝐵 = sup(ran 𝐺, ℝ, < ))
251	24, 57, 250	syl2anc 590	. 2 ⊢ (𝜑 → 𝐵 = sup(ran 𝐺, ℝ, < ))
252	249, 251	eqtr4d 2777	1 ⊢ (𝜑 → (Σ^‘𝐹) = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  Vcvv 3431   ∩ cin 3882   ⊆ wss 3883  ∅c0 4261  𝒫 cpw 4529   class class class wbr 5072   ↦ cmpt 5153  dom cdm 5618  ran crn 5619  Fun wfun 6479   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356  Fincfn 8883  supcsup 9343  ℂcc 11027  ℝcr 11028  0cc0 11029   + caddc 11032  +∞cpnf 11167  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171  ℤcz 12515  ℤ_≥cuz 12779  [,)cico 13291  [,]cicc 13292  ...cfz 13452  seqcseq 13954  abscabs 15187   ⇝ cli 15437  Σcsu 15639  Σ^{^}csumge0 46805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8633  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9345  df-inf 9346  df-oi 9415  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-n0 12429  df-z 12516  df-uz 12780  df-rp 12934  df-ico 13295  df-icc 13296  df-fz 13453  df-fzo 13600  df-fl 13742  df-seq 13955  df-exp 14015  df-hash 14284  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15441  df-rlim 15442  df-sum 15640  df-sumge0 46806

This theorem is referenced by:  sge0isummpt  46873