caratheodorylem1 - Mathbox for Glauco Siliprandi

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

Theorem caratheodorylem1 46977

Description: Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
caratheodorylem1.o	⊢ (𝜑 → 𝑂 ∈ OutMeas)
caratheodorylem1.s	⊢ 𝑆 = (CaraGen‘𝑂)
caratheodorylem1.z	⊢ 𝑍 = (ℤ_≥‘𝑀)
caratheodorylem1.e	⊢ (𝜑 → 𝐸:𝑍⟶𝑆)
caratheodorylem1.dj	⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛))
caratheodorylem1.g	⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))
caratheodorylem1.n	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))

**Assertion**
Ref	Expression
caratheodorylem1	⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))

Distinct variable groups: 𝑖,𝐸,𝑛 𝑖,𝐺,𝑛 𝑖,𝑀,𝑛 𝑖,𝑁,𝑛 𝑖,𝑂,𝑛 𝑛,𝑍 𝜑,𝑖,𝑛 Allowed substitution hints: 𝑆(𝑖,𝑛) 𝑍(𝑖)

Proof of Theorem caratheodorylem1 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		caratheodorylem1.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
2		eluzfz2 13478	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
4		id 22	. 2 ⊢ (𝜑 → 𝜑)
5		2fveq3 6833	. . . . 5 ⊢ (𝑗 = 𝑀 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑀)))
6		oveq2 7365	. . . . . . 7 ⊢ (𝑗 = 𝑀 → (𝑀...𝑗) = (𝑀...𝑀))
7	6	mpteq1d 5163	. . . . . 6 ⊢ (𝑗 = 𝑀 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))
8	7	fveq2d 6832	. . . . 5 ⊢ (𝑗 = 𝑀 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
9	5, 8	eqeq12d 2755	. . . 4 ⊢ (𝑗 = 𝑀 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
10	9	imbi2d 341	. . 3 ⊢ (𝑗 = 𝑀 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))))
11		2fveq3 6833	. . . . 5 ⊢ (𝑗 = 𝑖 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑖)))
12		oveq2 7365	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (𝑀...𝑗) = (𝑀...𝑖))
13	12	mpteq1d 5163	. . . . . 6 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))
14	13	fveq2d 6832	. . . . 5 ⊢ (𝑗 = 𝑖 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
15	11, 14	eqeq12d 2755	. . . 4 ⊢ (𝑗 = 𝑖 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
16	15	imbi2d 341	. . 3 ⊢ (𝑗 = 𝑖 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))))
17		2fveq3 6833	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘(𝑖 + 1))))
18		oveq2 7365	. . . . . . 7 ⊢ (𝑗 = (𝑖 + 1) → (𝑀...𝑗) = (𝑀...(𝑖 + 1)))
19	18	mpteq1d 5163	. . . . . 6 ⊢ (𝑗 = (𝑖 + 1) → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))
20	19	fveq2d 6832	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
21	17, 20	eqeq12d 2755	. . . 4 ⊢ (𝑗 = (𝑖 + 1) → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))))
22	21	imbi2d 341	. . 3 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
23		2fveq3 6833	. . . . 5 ⊢ (𝑗 = 𝑁 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑁)))
24		oveq2 7365	. . . . . . 7 ⊢ (𝑗 = 𝑁 → (𝑀...𝑗) = (𝑀...𝑁))
25	24	mpteq1d 5163	. . . . . 6 ⊢ (𝑗 = 𝑁 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))
26	25	fveq2d 6832	. . . . 5 ⊢ (𝑗 = 𝑁 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))
27	23, 26	eqeq12d 2755	. . . 4 ⊢ (𝑗 = 𝑁 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
28	27	imbi2d 341	. . 3 ⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))))
29		eluzel2 12785	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
30	1, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
31		fzsn 13512	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
32	30, 31	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑀...𝑀) = {𝑀})
33	32	mpteq1d 5163	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
34	33	fveq2d 6832	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))))
35		caratheodorylem1.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 ∈ OutMeas)
36	35	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑂 ∈ OutMeas)
37		eqid 2739	. . . . . . . 8 ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
38		caratheodorylem1.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (CaraGen‘𝑂)
39	38	caragenss 46955	. . . . . . . . . . 11 ⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂)
40	36, 39	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑆 ⊆ dom 𝑂)
41		caratheodorylem1.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)
42	41	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝐸:𝑍⟶𝑆)
43		elsni 4573	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑀} → 𝑛 = 𝑀)
44	43	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 = 𝑀)
45		uzid 12795	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
46	30, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
47		caratheodorylem1.z	. . . . . . . . . . . . . 14 ⊢ 𝑍 = (ℤ_≥‘𝑀)
48	46, 47	eleqtrrdi 2850	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
49	48	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑀 ∈ 𝑍)
50	44, 49	eqeltrd 2839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 ∈ 𝑍)
51	42, 50	ffvelcdmd 7027	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ 𝑆)
52	40, 51	sseldd 3916	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ dom 𝑂)
53		elssuni 4870	. . . . . . . . 9 ⊢ ((𝐸‘𝑛) ∈ dom 𝑂 → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
54	52, 53	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
55	36, 37, 54	omecl 46954	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
56		eqid 2739	. . . . . . 7 ⊢ (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))
57	55, 56	fmptd 7056	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))):{𝑀}⟶(0[,]+∞))
58	30, 57	sge0sn 46830	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀))
59		eqidd 2740	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
60	32	iuneq1d 4950	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖))
61		fveq2 6828	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝐸‘𝑖) = (𝐸‘𝑀))
62	61	iunxsng 5020	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑍 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
63	48, 62	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
64		eqidd 2740	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑀) = (𝐸‘𝑀))
65	60, 63, 64	3eqtrrd 2779	. . . . . . . . 9 ⊢ (𝜑 → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
66	65	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
67		fveq2 6828	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → (𝐸‘𝑛) = (𝐸‘𝑀))
68	67	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐸‘𝑀))
69		caratheodorylem1.g	. . . . . . . . . 10 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))
70		oveq2 7365	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
71	70	iuneq1d 4950	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
72		ovex 7390	. . . . . . . . . . . 12 ⊢ (𝑀...𝑀) ∈ V
73		fvex 6841	. . . . . . . . . . . 12 ⊢ (𝐸‘𝑖) ∈ V
74	72, 73	iunex 7911	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V
75	74	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V)
76	69, 71, 48, 75	fvmptd3 6960	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
77	76	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
78	66, 68, 77	3eqtr4d 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐺‘𝑀))
79	78	fveq2d 6832	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐺‘𝑀)))
80		snidg 4593	. . . . . . 7 ⊢ (𝑀 ∈ 𝑍 → 𝑀 ∈ {𝑀})
81	48, 80	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑀})
82		fvexd 6843	. . . . . 6 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) ∈ V)
83	59, 79, 81, 82	fvmptd 6944	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀) = (𝑂‘(𝐺‘𝑀)))
84	34, 58, 83	3eqtrrd 2779	. . . 4 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
85	84	a1i 11	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
86		simp3 1144	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝜑)
87		simp1 1142	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝑖 ∈ (𝑀..^𝑁))
88		id 22	. . . . . . 7 ⊢ ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
89	88	imp 407	. . . . . 6 ⊢ (((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
90	89	3adant1 1136	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
91		elfzoel1 13603	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℤ)
92		elfzoelz 13605	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℤ)
93	92	peano2zd 12628	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℤ)
94	91	zred 12625	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℝ)
95	93	zred 12625	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℝ)
96	92	zred 12625	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℝ)
97		elfzole1 13614	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑖)
98	96	ltp1d 12078	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 < (𝑖 + 1))
99	94, 96, 95, 97, 98	lelttrd 11296	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 < (𝑖 + 1))
100	94, 95, 99	ltled 11286	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ (𝑖 + 1))
101		leid 11234	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ ℝ → (𝑖 + 1) ≤ (𝑖 + 1))
102	95, 101	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ≤ (𝑖 + 1))
103	91, 93, 93, 100, 102	elfzd 13461	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
104	103	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
105		fveq2 6828	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑖 + 1) → (𝐸‘𝑗) = (𝐸‘(𝑖 + 1)))
106	105	ssiun2s 4979	. . . . . . . . . . . 12 ⊢ ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
107	104, 106	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
108		fveq2 6828	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝐸‘𝑖) = (𝐸‘𝑗))
109	108	cbviunv 4969	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)
110	109	mpteq2i 5169	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
111	69, 110	eqtri 2762	. . . . . . . . . . . . 13 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
112		oveq2 7365	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑖 + 1) → (𝑀...𝑛) = (𝑀...(𝑖 + 1)))
113	112	iuneq1d 4950	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑖 + 1) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
114	30	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ)
115	92	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℤ)
116	115	peano2zd 12628	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℤ)
117	114	zred 12625	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
118	116	zred 12625	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℝ)
119	115	zred 12625	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℝ)
120	97	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑖)
121	119	ltp1d 12078	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 < (𝑖 + 1))
122	117, 119, 118, 120, 121	lelttrd 11296	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 < (𝑖 + 1))
123	117, 118, 122	ltled 11286	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ (𝑖 + 1))
124	114, 116, 123	3jca 1134	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
125		eluz2 12786	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
126	124, 125	sylibr 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (ℤ_≥‘𝑀))
127	47	eqcomi 2748	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) = 𝑍
128	126, 127	eleqtrdi 2849	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ 𝑍)
129		ovex 7390	. . . . . . . . . . . . . . 15 ⊢ (𝑀...(𝑖 + 1)) ∈ V
130		fvex 6841	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘𝑗) ∈ V
131	129, 130	iunex 7911	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V
132	131	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V)
133	111, 113, 128, 132	fvmptd3 6960	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
134	133	eqcomd 2745	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (𝐺‘(𝑖 + 1)))
135	107, 134	sseqtrd 3951	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)))
136		sseqin2 4153	. . . . . . . . . . 11 ⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) ↔ ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
137	136	biimpi 217	. . . . . . . . . 10 ⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
138	135, 137	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
139	138	fveq2d 6832	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐸‘(𝑖 + 1))))
140		nfcv 2901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝐸‘(𝑖 + 1))
141		elfzouz 13610	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ (ℤ_≥‘𝑀))
142	141	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ (ℤ_≥‘𝑀))
143	140, 142, 105	iunp1 45523	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
144	133, 143	eqtrd 2774	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
145	144	difeq1d 4057	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
146		caratheodorylem1.dj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛))
147		fveq2 6828	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝐸‘𝑛) = (𝐸‘𝑗))
148	147	cbvdisjv 5051	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
149	146, 148	sylib 219	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
150	149	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
151		fzssuz 13511	. . . . . . . . . . . . . . 15 ⊢ (𝑀...𝑖) ⊆ (ℤ_≥‘𝑀)
152	151, 127	sseqtri 3963	. . . . . . . . . . . . . 14 ⊢ (𝑀...𝑖) ⊆ 𝑍
153	152	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀...𝑖) ⊆ 𝑍)
154		fzp1nel 13557	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝑖 + 1) ∈ (𝑀...𝑖)
155	154	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
156	155	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
157	128, 156	eldifd 3894	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑍 ∖ (𝑀...𝑖)))
158	150, 153, 157, 105	disjiun2 45515	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅)
159		undif4 4396	. . . . . . . . . . . 12 ⊢ ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅ → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
160	158, 159	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
161	160	eqcomd 2745	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))))
162		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝜑)
163	142, 127	eleqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ 𝑍)
164	111	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)))
165		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → 𝑛 = 𝑖)
166	165	oveq2d 7373	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → (𝑀...𝑛) = (𝑀...𝑖))
167	166	iuneq1d 4950	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
168		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍)
169		ovex 7390	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀...𝑖) ∈ V
170	169, 130	iunex 7911	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V
171	170	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V)
172	164, 167, 168, 171	fvmptd 6944	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
173	162, 163, 172	syl2anc 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
174	173	eqcomd 2745	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) = (𝐺‘𝑖))
175		difid 4305	. . . . . . . . . . . . 13 ⊢ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅
176	175	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅)
177	174, 176	uneq12d 4100	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((𝐺‘𝑖) ∪ ∅))
178		un0 4323	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖)
179	178	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖))
180	177, 179	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝐺‘𝑖))
181	145, 161, 180	3eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = (𝐺‘𝑖))
182	181	fveq2d 6832	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐺‘𝑖)))
183	139, 182	oveq12d 7375	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
184	183	3adant3 1138	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
185	35	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑂 ∈ OutMeas)
186	41	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝐸:𝑍⟶𝑆)
187	186, 128	ffvelcdmd 7027	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ∈ 𝑆)
188		simpll 772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
189	91	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ∈ ℤ)
190		elfzelz 13470	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑗 ∈ ℤ)
191	190	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ ℤ)
192		elfzle1 13473	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑀 ≤ 𝑗)
193	192	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ≤ 𝑗)
194	189, 191, 193	3jca 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
195		eluz2 12786	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
196	194, 195	sylibr 235	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ (ℤ_≥‘𝑀))
197	196, 127	eleqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
198	197	adantll 720	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
199	35, 39	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ⊆ dom 𝑂)
200	199	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑆 ⊆ dom 𝑂)
201	41	ffvelcdmda 7026	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ 𝑆)
202	200, 201	sseldd 3916	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ dom 𝑂)
203		elssuni 4870	. . . . . . . . . . . . . 14 ⊢ ((𝐸‘𝑗) ∈ dom 𝑂 → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
204	202, 203	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
205	188, 198, 204	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
206	205	ralrimiva 3131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
207		iunss 4975	. . . . . . . . . . 11 ⊢ (∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
208	206, 207	sylibr 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
209	133, 208	eqsstrd 3949	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
210	185, 38, 37, 187, 209	caragensplit 46951	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = (𝑂‘(𝐺‘(𝑖 + 1))))
211	210	eqcomd 2745	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
212	211	3adant3 1138	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
213	185	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑂 ∈ OutMeas)
214	162	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
215		elfzuz 13466	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ (ℤ_≥‘𝑀))
216	215, 127	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ 𝑍)
217	216	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑛 ∈ 𝑍)
218	41, 199	fssd 6673	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑂)
219	218	ffvelcdmda 7026	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑂)
220	219, 53	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
221	214, 217, 220	syl2anc 590	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
222	213, 37, 221	omecl 46954	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
223		2fveq3 6833	. . . . . . . . 9 ⊢ (𝑛 = (𝑖 + 1) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐸‘(𝑖 + 1))))
224	142, 222, 223	sge0p1 46865	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
225	224	3adant3 1138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
226		id 22	. . . . . . . . . 10 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
227	226	eqcomd 2745	. . . . . . . . 9 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) = (𝑂‘(𝐺‘𝑖)))
228	227	oveq1d 7372	. . . . . . . 8 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
229	228	3ad2ant3 1141	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
230		simpl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝜑)
231	152	sseli 3911	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ 𝑍)
232	231	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ 𝑍)
233	230, 232, 204	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
234	233	adantlr 721	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
235	234	ralrimiva 3131	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
236		iunss 4975	. . . . . . . . . . . . 13 ⊢ (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
237	235, 236	sylibr 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
238	172, 237	eqsstrd 3949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
239	162, 163, 238	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
240	185, 37, 239	omexrcl 46958	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘𝑖)) ∈ ℝ^*)
241	107, 208	sstrd 3925	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
242	185, 37, 241	omexrcl 46958	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐸‘(𝑖 + 1))) ∈ ℝ^*)
243	240, 242	xaddcomd 45777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
244	243	3adant3 1138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
245	225, 229, 244	3eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
246	184, 212, 245	3eqtr4d 2784	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
247	86, 87, 90, 246	syl3anc 1379	. . . 4 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
248	247	3exp 1125	. . 3 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
249	10, 16, 22, 28, 85, 248	fzind2 13735	. 2 ⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
250	3, 4, 249	sylc 65	1 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∀wral 3053 Vcvv 3431 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4262 {csn 4556 ∪ cuni 4839 ∪ ciun 4922 Disj wdisj 5040 class class class wbr 5073 ↦ cmpt 5154 dom cdm 5619 ⟶wf 6482 ‘cfv 6486 (class class class)co 7357 ℝcr 11029 0cc0 11030 1c1 11031 + caddc 11033 +∞cpnf 11168 ≤ cle 11172 ℤcz 12516 ℤ_≥cuz 12780 +_𝑒 cxad 13053 [,]cicc 13293 ...cfz 13453 ..^cfzo 13600 Σ^{^}csumge0 46813 OutMeascome 46940 CaraGenccaragen 46942

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 5200 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-inf2 9554 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108

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 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4840 df-int 4879 df-iun 4924 df-disj 5041 df-br 5074 df-opab 5136 df-mpt 5155 df-tr 5181 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7808 df-1st 7932 df-2nd 7933 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-er 8634 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-sup 9346 df-oi 9416 df-card 9855 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-div 11800 df-nn 12167 df-2 12236 df-3 12237 df-n0 12430 df-z 12517 df-uz 12781 df-rp 12935 df-xadd 13056 df-ico 13296 df-icc 13297 df-fz 13454 df-fzo 13601 df-seq 13956 df-exp 14016 df-hash 14285 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-clim 15442 df-sum 15641 df-sumge0 46814 df-ome 46941 df-caragen 46943

This theorem is referenced by: caratheodorylem2 46978

W3C validator