sge0resplit - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sge0resplit		Structured version Visualization version GIF version

Theorem sge0resplit 46941

Description: Σ^{^} splits into two parts, when it's a real number. This is a special case of sge0split 46944. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
sge0resplit.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sge0resplit.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
sge0resplit.u	⊢ 𝑈 = (𝐴 ∪ 𝐵)
sge0resplit.in0	⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
sge0resplit.f	⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))
sge0resplit.re	⊢ (𝜑 → (Σ^{^}‘𝐹) ∈ ℝ)

**Assertion**
Ref	Expression
sge0resplit	⊢ (𝜑 → (Σ^{^}‘𝐹) = ((Σ^{^}‘(𝐹 ↾ 𝐴)) + (Σ^{^}‘(𝐹 ↾ 𝐵))))

Proof of Theorem sge0resplit Dummy variables 𝑎 𝑏 𝑟 𝑢 𝑣 𝑥 𝑦 𝑡 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0resplit.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		sge0resplit.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞))
3		ssun1 4128	. . . . . . . . . 10 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
4		sge0resplit.u	. . . . . . . . . . 11 ⊢ 𝑈 = (𝐴 ∪ 𝐵)
5	4	eqcomi 2770	. . . . . . . . . 10 ⊢ (𝐴 ∪ 𝐵) = 𝑈
6	3, 5	sseqtri 3982	. . . . . . . . 9 ⊢ 𝐴 ⊆ 𝑈
7	6	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
8	2, 7	fssresd 6726	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞))
9	4	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))
10		sge0resplit.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
11		unexg 7721	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V)
12	1, 10, 11	syl2anc 593	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)
13	9, 12	eqeltrd 2861	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ V)
14		sge0resplit.re	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘𝐹) ∈ ℝ)
15	13, 2, 14	sge0ssre 46932	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝐹 ↾ 𝐴)) ∈ ℝ)
16	1, 8, 15	sge0supre 46924	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝐹 ↾ 𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ))
17	16, 15	eqeltrrd 2862	. . . . 5 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) ∈ ℝ)
18		ssun2 4129	. . . . . . . . . 10 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
19	18, 5	sseqtri 3982	. . . . . . . . 9 ⊢ 𝐵 ⊆ 𝑈
20	19	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ 𝑈)
21	2, 20	fssresd 6726	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞))
22	13, 2, 14	sge0ssre 46932	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝐹 ↾ 𝐵)) ∈ ℝ)
23	10, 21, 22	sge0supre 46924	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝐹 ↾ 𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < ))
24	23, 22	eqeltrrd 2862	. . . . 5 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < ) ∈ ℝ)
25		rexadd 13229	. . . . 5 ⊢ ((sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) ∈ ℝ ∧ sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < ) ∈ ℝ) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) +_𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < )))
26	17, 24, 25	syl2anc 593	. . . 4 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) +_𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < )) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < )))
27	13, 2, 14	sge0rern 46923	. . . . . . . 8 ⊢ (𝜑 → ¬ +∞ ∈ ran 𝐹)
28		nelrnres 45726	. . . . . . . 8 ⊢ (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹 ↾ 𝐴))
29	27, 28	syl 17	. . . . . . 7 ⊢ (𝜑 → ¬ +∞ ∈ ran (𝐹 ↾ 𝐴))
30	8, 29	fge0iccico 46905	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶(0[,)+∞))
31	30	sge0rnre 46899	. . . . 5 ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ⊆ ℝ)
32		sge0rnn0 46903	. . . . . 6 ⊢ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ≠ ∅
33	32	a1i 11	. . . . 5 ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ≠ ∅)
34	1, 30	sge0reval 46907	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝐹 ↾ 𝐴)) = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ^*, < ))
35	34	eqcomd 2767	. . . . . . 7 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ^*, < ) = (Σ^{^}‘(𝐹 ↾ 𝐴)))
36	35, 15	eqeltrd 2861	. . . . . 6 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ^*, < ) ∈ ℝ)
37		supxrre3 45862	. . . . . . 7 ⊢ ((ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ^*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))𝑡 ≤ 𝑤))
38	31, 33, 37	syl2anc 593	. . . . . 6 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ^*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))𝑡 ≤ 𝑤))
39	36, 38	mpbid 234	. . . . 5 ⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))𝑡 ≤ 𝑤)
40		nelrnres 45726	. . . . . . . 8 ⊢ (¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran (𝐹 ↾ 𝐵))
41	27, 40	syl 17	. . . . . . 7 ⊢ (𝜑 → ¬ +∞ ∈ ran (𝐹 ↾ 𝐵))
42	21, 41	fge0iccico 46905	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶(0[,)+∞))
43	42	sge0rnre 46899	. . . . 5 ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) ⊆ ℝ)
44		sge0rnn0 46903	. . . . . 6 ⊢ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) ≠ ∅
45	44	a1i 11	. . . . 5 ⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) ≠ ∅)
46	10, 42	sge0reval 46907	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝐹 ↾ 𝐵)) = sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ^*, < ))
47	46	eqcomd 2767	. . . . . . 7 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ^*, < ) = (Σ^{^}‘(𝐹 ↾ 𝐵)))
48	47, 22	eqeltrd 2861	. . . . . 6 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ^*, < ) ∈ ℝ)
49		supxrre3 45862	. . . . . . 7 ⊢ ((ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) ⊆ ℝ ∧ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) ≠ ∅) → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ^*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑡 ≤ 𝑤))
50	43, 45, 49	syl2anc 593	. . . . . 6 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ^*, < ) ∈ ℝ ↔ ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑡 ≤ 𝑤))
51	48, 50	mpbid 234	. . . . 5 ⊢ (𝜑 → ∃𝑤 ∈ ℝ ∀𝑡 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑡 ≤ 𝑤)
52		eqid 2761	. . . . 5 ⊢ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}
53	31, 33, 39, 43, 45, 51, 52	supadd 12154	. . . 4 ⊢ (𝜑 → (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) + sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < )) = sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ))
54		simpl 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝜑)
55		vex 3457	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
56		eqeq1 2765	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑟 → (𝑧 = (𝑣 + 𝑢) ↔ 𝑟 = (𝑣 + 𝑢)))
57	56	rexbidv 3185	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑟 → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
58	57	rexbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑟 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢) ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
59	55, 58	elab 3637	. . . . . . . . . . 11 ⊢ (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
60	59	bilani 508	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
61		simpl 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)))) → 𝜑)
62		vex 3457	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑣 ∈ V
63		sumeq1 15707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑎 → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦))
64	63	cbvmptv 5201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦))
65	64	elrnmpt 5930	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 ∈ V → (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦)))
66	62, 65	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦))
67	66	birani 507	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦))
68		vex 3457	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑢 ∈ V
69		sumeq1 15707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑏 → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦) = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))
70	69	cbvmptv 5201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) = (𝑏 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))
71	70	elrnmpt 5930	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)))
72	68, 71	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) ↔ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))
73	72	bilani 508	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))) → ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))
74	67, 73	jca 519	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))) → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)))
75		reeanv 3233	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) ↔ (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ ∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)))
76	74, 75	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)))
77	76	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)))
78		eqid 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
79		elinel1 4151	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ 𝒫 𝐴)
80		elpwi 4559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴)
81		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 ⊆ 𝐴 → 𝑎 ⊆ 𝐴)
82	81, 6	sstrdi 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑎 ⊆ 𝐴 → 𝑎 ⊆ 𝑈)
83	80, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝑈)
84	79, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ⊆ 𝑈)
85	84	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ⊆ 𝑈)
86		elinel1 4151	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 𝐵)
87		elpwi 4559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
88		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ⊆ 𝐵 → 𝑏 ⊆ 𝐵)
89	88, 19	sstrdi 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑏 ⊆ 𝐵 → 𝑏 ⊆ 𝑈)
90	87, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝑈)
91	86, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ⊆ 𝑈)
92	91	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏 ⊆ 𝑈)
93	85, 92	unssd 4142	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎 ∪ 𝑏) ⊆ 𝑈)
94		vex 3457	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑎 ∈ V
95		vex 3457	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑏 ∈ V
96	94, 95	unex 7722	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∪ 𝑏) ∈ V
97	96	elpw 4556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∪ 𝑏) ∈ 𝒫 𝑈 ↔ (𝑎 ∪ 𝑏) ⊆ 𝑈)
98	93, 97	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎 ∪ 𝑏) ∈ 𝒫 𝑈)
99		elinel2 4152	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ Fin)
100	99	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑎 ∈ Fin)
101		elinel2 4152	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
102	101	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
103		unfi 9133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑎 ∪ 𝑏) ∈ Fin)
104	100, 102, 103	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎 ∪ 𝑏) ∈ Fin)
105	98, 104	elind 4150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (𝑎 ∪ 𝑏) ∈ (𝒫 𝑈 ∩ Fin))
106	105	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎 ∪ 𝑏) ∈ (𝒫 𝑈 ∩ Fin))
107	106	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑎 ∪ 𝑏) ∈ (𝒫 𝑈 ∩ Fin))
108		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) → 𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦))
109		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) → 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))
110	108, 109	oveq12d 7409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) → (𝑣 + 𝑢) = (Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) + Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)))
111	110	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) + Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)))
112	79, 80	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ⊆ 𝐴)
113	112	sselda 3934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 ∈ 𝑎) → 𝑦 ∈ 𝐴)
114		fvres 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
115	113, 114	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 ∈ 𝑎) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦))
116	115	sumeq2dv 15720	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ 𝑎 (𝐹‘𝑦))
117	116	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ 𝑎 (𝐹‘𝑦))
118	86, 87	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → 𝑏 ⊆ 𝐵)
119	118	sselda 3934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ∈ 𝑏) → 𝑦 ∈ 𝐵)
120		fvres 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑦) = (𝐹‘𝑦))
121	119, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑏 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑦 ∈ 𝑏) → ((𝐹 ↾ 𝐵)‘𝑦) = (𝐹‘𝑦))
122	121	sumeq2dv 15720	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 ∈ (𝒫 𝐵 ∩ Fin) → Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦) = Σ𝑦 ∈ 𝑏 (𝐹‘𝑦))
123	122	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦) = Σ𝑦 ∈ 𝑏 (𝐹‘𝑦))
124	117, 123	oveq12d 7409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → (Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) + Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) = (Σ𝑦 ∈ 𝑎 (𝐹‘𝑦) + Σ𝑦 ∈ 𝑏 (𝐹‘𝑦)))
125	124	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) → (Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) + Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) = (Σ𝑦 ∈ 𝑎 (𝐹‘𝑦) + Σ𝑦 ∈ 𝑏 (𝐹‘𝑦)))
126	111, 125	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) → (𝑣 + 𝑢) = (Σ𝑦 ∈ 𝑎 (𝐹‘𝑦) + Σ𝑦 ∈ 𝑏 (𝐹‘𝑦)))
127	126	ad4ant23 763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → (𝑣 + 𝑢) = (Σ𝑦 ∈ 𝑎 (𝐹‘𝑦) + Σ𝑦 ∈ 𝑏 (𝐹‘𝑦)))
128		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = (𝑣 + 𝑢))
129		sge0resplit.in0	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
130	129	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝐴 ∩ 𝐵) = ∅)
131	112	ad2antrl 738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑎 ⊆ 𝐴)
132	118	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑏 ⊆ 𝐵)
133	132	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → 𝑏 ⊆ 𝐵)
134		ssin0 45596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝑎 ⊆ 𝐴 ∧ 𝑏 ⊆ 𝐵) → (𝑎 ∩ 𝑏) = ∅)
135	130, 131, 133, 134	syl3anc 1389	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎 ∩ 𝑏) = ∅)
136		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎 ∪ 𝑏) = (𝑎 ∪ 𝑏))
137	104	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → (𝑎 ∪ 𝑏) ∈ Fin)
138		rge0ssre 13454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
139		ax-resscn 11124	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ℝ ⊆ ℂ
140	138, 139	sstri 3943	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0[,)+∞) ⊆ ℂ
141	2, 27	fge0iccico 46905	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐹:𝑈⟶(0[,)+∞))
142	141	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎 ∪ 𝑏)) → 𝐹:𝑈⟶(0[,)+∞))
143	93	sselda 3934	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) ∧ 𝑦 ∈ (𝑎 ∪ 𝑏)) → 𝑦 ∈ 𝑈)
144	143	adantll 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎 ∪ 𝑏)) → 𝑦 ∈ 𝑈)
145	142, 144	ffvelcdmd 7061	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎 ∪ 𝑏)) → (𝐹‘𝑦) ∈ (0[,)+∞))
146	140, 145	sselid 3932	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ 𝑦 ∈ (𝑎 ∪ 𝑏)) → (𝐹‘𝑦) ∈ ℂ)
147	135, 136, 137, 146	fsumsplit 15759	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → Σ𝑦 ∈ (𝑎 ∪ 𝑏)(𝐹‘𝑦) = (Σ𝑦 ∈ 𝑎 (𝐹‘𝑦) + Σ𝑦 ∈ 𝑏 (𝐹‘𝑦)))
148	147	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → Σ𝑦 ∈ (𝑎 ∪ 𝑏)(𝐹‘𝑦) = (Σ𝑦 ∈ 𝑎 (𝐹‘𝑦) + Σ𝑦 ∈ 𝑏 (𝐹‘𝑦)))
149	127, 128, 148	3eqtr4d 2806	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 = Σ𝑦 ∈ (𝑎 ∪ 𝑏)(𝐹‘𝑦))
150		sumeq1 15707	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (𝑎 ∪ 𝑏) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = Σ𝑦 ∈ (𝑎 ∪ 𝑏)(𝐹‘𝑦))
151	150	rspceeqv 3603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑎 ∪ 𝑏) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ (𝑎 ∪ 𝑏)(𝐹‘𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
152	107, 149, 151	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
153	55	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ V)
154	78, 152, 153	elrnmptd 5935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) ∧ 𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
155	154	ex 416	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) ∧ (𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
156	155	ex 416	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin))) → ((𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))))
157	156	ex 416	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 𝐵 ∩ Fin)) → ((𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))))
158	157	rexlimdvv 3217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦)) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))))
159	158	imp 410	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)∃𝑏 ∈ (𝒫 𝐵 ∩ Fin)(𝑣 = Σ𝑦 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑦) ∧ 𝑢 = Σ𝑦 ∈ 𝑏 ((𝐹 ↾ 𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
160	61, 77, 159	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
161	160	ex 416	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ 𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))) → (𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))))
162	161	rexlimdvv 3217	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
163	162	imp 410	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
164	54, 60, 163	syl2anc 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}) → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
165	164	ex 416	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} → 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
166	78	elrnmpt 5930	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
167	166	ibi 269	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
168	167	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
169		nfv 1933	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝜑
170		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝑟
171		nfmpt1 5196	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
172	171	nfrn 5924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
173	170, 172	nfel 2937	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
174	169, 173	nfan 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
175		nfmpt1 5196	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))
176	175	nfrn 5924	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))
177		nfmpt1 5196	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))
178	177	nfrn 5924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))
179		nfv 1933	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑟 = (𝑣 + 𝑢)
180	178, 179	nfrexw 3309	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
181	176, 180	nfrexw 3309	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)
182		inss2 4187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴
183	182	sseli 3930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐴) → 𝑦 ∈ 𝐴)
184	183	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → 𝑦 ∈ 𝐴)
185	114	eqcomd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐴 → (𝐹‘𝑦) = ((𝐹 ↾ 𝐴)‘𝑦))
186	184, 185	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → (𝐹‘𝑦) = ((𝐹 ↾ 𝐴)‘𝑦))
187	186	sumeq2dv 15720	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦))
188		sumeq1 15707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑧 → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐴)‘𝑦))
189	188	cbvmptv 5201	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐴)‘𝑦))
190		vex 3457	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑥 ∈ V
191	190	inex1 5270	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∩ 𝐴) ∈ V
192	191	elpw 4556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴)
193	182, 192	mpbir 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴
194	193	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴)
195		elinel2 4152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin)
196		inss1 4186	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥
197	196	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐴) ⊆ 𝑥)
198		ssfi 9135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝐴) ⊆ 𝑥) → (𝑥 ∩ 𝐴) ∈ Fin)
199	195, 197, 198	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐴) ∈ Fin)
200	194, 199	elind 4150	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐴) ∈ (𝒫 𝐴 ∩ Fin))
201		eqidd 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦))
202		sumeq1 15707	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑥 ∩ 𝐴) → Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦))
203	202	rspceeqv 3603	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥 ∩ 𝐴) ∈ (𝒫 𝐴 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐴)‘𝑦))
204	200, 201, 203	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐴)‘𝑦))
205		sumex 15706	. . . . . . . . . . . . . . . . . . 19 ⊢ Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) ∈ V
206	205	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) ∈ V)
207	189, 204, 206	elrnmptd 5935	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)))
208	187, 207	eqeltrd 2861	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)))
209	208	3ad2ant2 1146	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)))
210		sumeq1 15707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑧 → Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦) = Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐵)‘𝑦))
211	210	cbvmptv 5201	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) = (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐵)‘𝑦))
212		inss2 4187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∩ 𝐵) ⊆ 𝐵
213	190	inex1 5270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∩ 𝐵) ∈ V
214	213	elpw 4556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∩ 𝐵) ∈ 𝒫 𝐵 ↔ (𝑥 ∩ 𝐵) ⊆ 𝐵)
215	212, 214	mpbir 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∩ 𝐵) ∈ 𝒫 𝐵
216	215	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (𝑥 ∩ 𝐵) ∈ 𝒫 𝐵)
217		inss1 4186	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∩ 𝐵) ⊆ 𝑥
218	217	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐵) ⊆ 𝑥)
219		ssfi 9135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ Fin ∧ (𝑥 ∩ 𝐵) ⊆ 𝑥) → (𝑥 ∩ 𝐵) ∈ Fin)
220	195, 218, 219	syl2anc 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐵) ∈ Fin)
221	220	3ad2ant2 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (𝑥 ∩ 𝐵) ∈ Fin)
222	216, 221	elind 4150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → (𝑥 ∩ 𝐵) ∈ (𝒫 𝐵 ∩ Fin))
223	212	sseli 3930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐵) → 𝑦 ∈ 𝐵)
224	120	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐵 → (𝐹‘𝑦) = ((𝐹 ↾ 𝐵)‘𝑦))
225	223, 224	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝑥 ∩ 𝐵) → (𝐹‘𝑦) = ((𝐹 ↾ 𝐵)‘𝑦))
226	225	sumeq2i 15716	. . . . . . . . . . . . . . . . . . . 20 ⊢ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦)
227	226	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦))
228	227	3adant3 1144	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦))
229		sumeq1 15707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦))
230	229	rspceeqv 3603	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∩ 𝐵) ∈ (𝒫 𝐵 ∩ Fin) ∧ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) = Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐵)‘𝑦))
231	222, 228, 230	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) = Σ𝑦 ∈ 𝑧 ((𝐹 ↾ 𝐵)‘𝑦))
232		sumex 15706	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ V
233	232	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ V)
234	211, 231, 233	elrnmptd 5935	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)))
235		simp3 1150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))
236	182	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∩ 𝐴) ⊆ 𝐴)
237	212	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∩ 𝐵) ⊆ 𝐵)
238		ssin0 45596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ (𝑥 ∩ 𝐴) ⊆ 𝐴 ∧ (𝑥 ∩ 𝐵) ⊆ 𝐵) → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅)
239	129, 236, 237, 238	syl3anc 1389	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅)
240	239	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅)
241		elinel1 4151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈)
242		elpwi 4559	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝒫 𝑈 → 𝑥 ⊆ 𝑈)
243	241, 242	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ⊆ 𝑈)
244	4	ineq2i 4167	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∩ 𝑈) = (𝑥 ∩ (𝐴 ∪ 𝐵))
245	244	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ 𝑈 → (𝑥 ∩ 𝑈) = (𝑥 ∩ (𝐴 ∪ 𝐵)))
246		dfss 3921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ⊆ 𝑈 ↔ 𝑥 = (𝑥 ∩ 𝑈))
247	246	biimpi 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ 𝑈 → 𝑥 = (𝑥 ∩ 𝑈))
248		indi 4234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵))
249	248	eqcomi 2770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)) = (𝑥 ∩ (𝐴 ∪ 𝐵))
250	249	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ⊆ 𝑈 → ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)) = (𝑥 ∩ (𝐴 ∪ 𝐵)))
251	245, 247, 250	3eqtr4d 2806	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ⊆ 𝑈 → 𝑥 = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)))
252	243, 251	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)))
253	252	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)))
254	195	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin)
255	141	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑈⟶(0[,)+∞))
256	243	sselda 3934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑈)
257	256	adantll 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑈)
258	255, 257	ffvelcdmd 7061	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,)+∞))
259	140, 258	sselid 3932	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℂ)
260	240, 253, 254, 259	fsumsplit 15759	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
261	260	3adant3 1144	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
262	235, 261	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑟 = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
263		oveq2 7399	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + 𝑢) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)))
264	263	rspceeqv 3603	. . . . . . . . . . . . . . . 16 ⊢ ((Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)) ∧ 𝑟 = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦))) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + 𝑢))
265	234, 262, 264	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + 𝑢))
266		oveq1 7398	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) → (𝑣 + 𝑢) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + 𝑢))
267	266	eqeq2d 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) → (𝑟 = (𝑣 + 𝑢) ↔ 𝑟 = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + 𝑢)))
268	267	rexbidv 3185	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) → (∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢) ↔ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + 𝑢)))
269	268	rspcev 3580	. . . . . . . . . . . . . . 15 ⊢ ((Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)) ∧ ∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + 𝑢)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
270	209, 265, 269	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
271	270	3exp 1131	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
272	271	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))))
273	174, 181, 272	rexlimd 3268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑟 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢)))
274	168, 273	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑟 = (𝑣 + 𝑢))
275	274, 59	sylibr 236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)})
276	275	ex 416	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}))
277	165, 276	impbid 214	. . . . . . 7 ⊢ (𝜑 → (𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
278	277	alrimiv 1946	. . . . . 6 ⊢ (𝜑 → ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
279		dfcleq 2754	. . . . . 6 ⊢ ({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∀𝑟(𝑟 ∈ {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} ↔ 𝑟 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))))
280	278, 279	sylibr 236	. . . . 5 ⊢ (𝜑 → {𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)} = ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)))
281	280	supeq1d 9386	. . . 4 ⊢ (𝜑 → sup({𝑧 ∣ ∃𝑣 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦))∃𝑢 ∈ ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦))𝑧 = (𝑣 + 𝑢)}, ℝ, < ) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ))
282	26, 53, 281	3eqtrrd 2801	. . 3 ⊢ (𝜑 → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) +_𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < )))
283	13, 2, 14	sge0supre 46924	. . 3 ⊢ (𝜑 → (Σ^{^}‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ, < ))
284	16, 23	oveq12d 7409	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝐹 ↾ 𝐴)) +_𝑒 (Σ^{^}‘(𝐹 ↾ 𝐵))) = (sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐴)‘𝑦)), ℝ, < ) +_𝑒 sup(ran (𝑥 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 ((𝐹 ↾ 𝐵)‘𝑦)), ℝ, < )))
285	282, 283, 284	3eqtr4d 2806	. 2 ⊢ (𝜑 → (Σ^{^}‘𝐹) = ((Σ^{^}‘(𝐹 ↾ 𝐴)) +_𝑒 (Σ^{^}‘(𝐹 ↾ 𝐵))))
286		rexadd 13229	. . 3 ⊢ (((Σ^{^}‘(𝐹 ↾ 𝐴)) ∈ ℝ ∧ (Σ^{^}‘(𝐹 ↾ 𝐵)) ∈ ℝ) → ((Σ^{^}‘(𝐹 ↾ 𝐴)) +_𝑒 (Σ^{^}‘(𝐹 ↾ 𝐵))) = ((Σ^{^}‘(𝐹 ↾ 𝐴)) + (Σ^{^}‘(𝐹 ↾ 𝐵))))
287	15, 22, 286	syl2anc 593	. 2 ⊢ (𝜑 → ((Σ^{^}‘(𝐹 ↾ 𝐴)) +_𝑒 (Σ^{^}‘(𝐹 ↾ 𝐵))) = ((Σ^{^}‘(𝐹 ↾ 𝐴)) + (Σ^{^}‘(𝐹 ↾ 𝐵))))
288	285, 287	eqtrd 2796	1 ⊢ (𝜑 → (Σ^{^}‘𝐹) = ((Σ^{^}‘(𝐹 ↾ 𝐴)) + (Σ^{^}‘(𝐹 ↾ 𝐵))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 ∀wal 1557 = wceq 1559 ∈ wcel 2141 {cab 2739 ≠ wne 2956 ∀wral 3075 ∃wrex 3085 Vcvv 3453 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4283 𝒫 cpw 4552 class class class wbr 5097 ↦ cmpt 5178 ran crn 5644 ↾ cres 5645 ⟶wf 6512 ‘cfv 6516 (class class class)co 7391 Fincfn 8921 supcsup 9380 ℂcc 11065 ℝcr 11066 0cc0 11067 + caddc 11070 +∞cpnf 11207 ℝ^*cxr 11209 < clt 11210 ≤ cle 11211 +_𝑒 cxad 13106 [,)cico 13345 [,]cicc 13346 Σcsu 15704 Σ^{^}csumge0 46897

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-inf2 9590 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-er 8672 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9382 df-oi 9452 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-n0 12476 df-z 12563 df-uz 12834 df-rp 12988 df-xadd 13109 df-ico 13349 df-icc 13350 df-fz 13507 df-fzo 13654 df-seq 14009 df-exp 14069 df-hash 14338 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-clim 15506 df-sum 15705 df-sumge0 46898

This theorem is referenced by: sge0split 46944

W3C validator