Theorem sge0ltfirp 45415

Description: If the sum of nonnegative extended reals is real, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
sge0ltfirp.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
sge0ltfirp.f	⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))
sge0ltfirp.y	⊢ (𝜑 → 𝑌 ∈ ℝ+)
sge0ltfirp.re	⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)

Assertion

Ref	Expression
sge0ltfirp	⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))

Distinct variable groups:   𝑥,𝐹   𝑥,𝑋   𝑥,𝑌   𝜑,𝑥

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem sge0ltfirp

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0ltfirp.f	. . . . 5 ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞))
2		sge0ltfirp.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
3		sge0ltfirp.re	. . . . . 6 ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ)
4	2, 1, 3	sge0rern 45403	. . . . 5 ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)
5	1, 4	fge0iccico 45385	. . . 4 ⊢ (𝜑 → 𝐹:𝑋⟶(0[,)+∞))
6	5	sge0rnre 45379	. . 3 ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ)
7		sge0rnn0 45383	. . . 4 ⊢ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅
8	7	a1i 11	. . 3 ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ≠ ∅)
9	2, 1, 3	sge0rnbnd 45408	. . 3 ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑤 ≤ 𝑧)
10		sge0ltfirp.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ ℝ+)
11	6, 8, 9, 10	suprltrp 44337	. 2 ⊢ (𝜑 → ∃𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤)
12		nfv 1916	. . 3 ⊢ Ⅎ𝑤𝜑
13		nfv 1916	. . 3 ⊢ Ⅎ𝑤∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌)
14		simp1 1135	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤) → 𝜑)
15		vex 3477	. . . . . . . . . 10 ⊢ 𝑤 ∈ V
16		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
17	16	elrnmpt 5955	. . . . . . . . . 10 ⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
18	15, 17	ax-mp 5	. . . . . . . . 9 ⊢ (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
19	18	biimpi 215	. . . . . . . 8 ⊢ (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
20	19	adantr 480	. . . . . . 7 ⊢ ((𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
21		nfmpt1 5256	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
22	21	nfrn 5951	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
23		nfcv 2902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥ℝ
24		nfcv 2902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 <
25	22, 23, 24	nfsup 9450	. . . . . . . . . . 11 ⊢ Ⅎ𝑥sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < )
26		nfcv 2902	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 −
27		nfcv 2902	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝑌
28	25, 26, 27	nfov 7442	. . . . . . . . . 10 ⊢ Ⅎ𝑥(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌)
29		nfcv 2902	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑤
30	28, 24, 29	nfbr 5195	. . . . . . . . 9 ⊢ Ⅎ𝑥(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤
31		simpl 482	. . . . . . . . . . . 12 ⊢ (((sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤 ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤)
32		simpr 484	. . . . . . . . . . . 12 ⊢ (((sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤 ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
33	31, 32	breqtrd 5174	. . . . . . . . . . 11 ⊢ (((sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤 ∧ 𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
34	33	ex 412	. . . . . . . . . 10 ⊢ ((sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤 → (𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
35	34	a1d 25	. . . . . . . . 9 ⊢ ((sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤 → (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → (𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
36	30, 35	reximdai 3257	. . . . . . . 8 ⊢ ((sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤 → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
37	36	adantl 481	. . . . . . 7 ⊢ ((𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤) → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)𝑤 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
38	20, 37	mpd 15	. . . . . 6 ⊢ ((𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
39	38	3adant1 1129	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
40		simpl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)))
41	2, 1, 3	sge0supre 45404	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ))
42	41	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((Σ^‘𝐹) − 𝑌) = (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌))
43	42	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ((Σ^‘𝐹) − 𝑌) = (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌))
44		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
45	43, 44	eqbrtrd 5170	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
46	45	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
47		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ ((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
48	3	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (Σ^‘𝐹) ∈ ℝ)
49	10	rpred 13021	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ ℝ)
50	49	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑌 ∈ ℝ)
51		elinel2 4196	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ∈ Fin)
52	51	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ∈ Fin)
53		rge0ssre 13438	. . . . . . . . . . . . . . 15 ⊢ (0[,)+∞) ⊆ ℝ
54	5	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝐹:𝑋⟶(0[,)+∞))
55	54	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑋⟶(0[,)+∞))
56		elpwinss 44038	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝒫 𝑋 ∩ Fin) → 𝑥 ⊆ 𝑋)
57	56	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → 𝑥 ⊆ 𝑋)
58	57	sselda 3982	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑋)
59	55, 58	ffvelcdmd 7087	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,)+∞))
60	53, 59	sselid 3980	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ)
61	52, 60	fsumrecl 15685	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ ℝ)
62	48, 50, 61	ltsubaddd 11815	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ↔ (Σ^‘𝐹) < (Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) + 𝑌)))
63	62	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ ((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ↔ (Σ^‘𝐹) < (Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) + 𝑌)))
64	47, 63	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ ((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (Σ^‘𝐹) < (Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) + 𝑌))
65	54, 57	fssresd 6758	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥⟶(0[,)+∞))
66	52, 65	sge0fsum 45402	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (Σ^‘(𝐹 ↾ 𝑥)) = Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦))
67		fvres 6910	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ 𝑥 → ((𝐹 ↾ 𝑥)‘𝑦) = (𝐹‘𝑦))
68	67	sumeq2i 15650	. . . . . . . . . . . . . 14 ⊢ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)
69	68	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝑥)‘𝑦) = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
70	66, 69	eqtr2d 2772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (Σ^‘(𝐹 ↾ 𝑥)))
71	70	oveq1d 7427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → (Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) + 𝑌) = ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))
72	71	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ ((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) + 𝑌) = ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))
73	64, 72	breqtrd 5174	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ ((Σ^‘𝐹) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))
74	40, 46, 73	syl2anc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))
75	74	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑋 ∩ Fin)) → ((sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → (Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌)))
76	75	reximdva 3167	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌)))
77	76	imp 406	. . . . 5 ⊢ ((𝜑 ∧ ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))
78	14, 39, 77	syl2anc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ∧ (sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤) → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))
79	78	3exp 1118	. . 3 ⊢ (𝜑 → (𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ((sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))))
80	12, 13, 79	rexlimd 3262	. 2 ⊢ (𝜑 → (∃𝑤 ∈ ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))(sup(ran (𝑥 ∈ (𝒫 𝑋 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) − 𝑌) < 𝑤 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌)))
81	11, 80	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑋 ∩ Fin)(Σ^‘𝐹) < ((Σ^‘(𝐹 ↾ 𝑥)) + 𝑌))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   ≠ wne 2939  ∃wrex 3069  Vcvv 3473   ∩ cin 3947   ⊆ wss 3948  ∅c0 4322  𝒫 cpw 4602   class class class wbr 5148   ↦ cmpt 5231  ran crn 5677   ↾ cres 5678  ⟶wf 6539  ‘cfv 6543  (class class class)co 7412  Fincfn 8943  supcsup 9439  ℝcr 11113  0cc0 11114   + caddc 11117  +∞cpnf 11250   < clt 11253   − cmin 11449  ℝ⁺crp 12979  [,)cico 13331  [,]cicc 13332  Σcsu 15637  Σ^{^}csumge0 45377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9640  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191  ax-pre-sup 11192

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-sup 9441  df-oi 9509  df-card 9938  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-n0 12478  df-z 12564  df-uz 12828  df-rp 12980  df-ico 13335  df-icc 13336  df-fz 13490  df-fzo 13633  df-seq 13972  df-exp 14033  df-hash 14296  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-clim 15437  df-sum 15638  df-sumge0 45378

This theorem is referenced by:  sge0ltfirpmpt  45423  sge0ltfirpmpt2  45441