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 46541

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 13572	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
4		id 22	. 2 ⊢ (𝜑 → 𝜑)
5		2fveq3 6911	. . . . 5 ⊢ (𝑗 = 𝑀 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑀)))
6		oveq2 7439	. . . . . . 7 ⊢ (𝑗 = 𝑀 → (𝑀...𝑗) = (𝑀...𝑀))
7	6	mpteq1d 5237	. . . . . 6 ⊢ (𝑗 = 𝑀 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))
8	7	fveq2d 6910	. . . . 5 ⊢ (𝑗 = 𝑀 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
9	5, 8	eqeq12d 2753	. . . 4 ⊢ (𝑗 = 𝑀 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
10	9	imbi2d 340	. . 3 ⊢ (𝑗 = 𝑀 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))))
11		2fveq3 6911	. . . . 5 ⊢ (𝑗 = 𝑖 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑖)))
12		oveq2 7439	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (𝑀...𝑗) = (𝑀...𝑖))
13	12	mpteq1d 5237	. . . . . 6 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))
14	13	fveq2d 6910	. . . . 5 ⊢ (𝑗 = 𝑖 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
15	11, 14	eqeq12d 2753	. . . 4 ⊢ (𝑗 = 𝑖 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
16	15	imbi2d 340	. . 3 ⊢ (𝑗 = 𝑖 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))))
17		2fveq3 6911	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘(𝑖 + 1))))
18		oveq2 7439	. . . . . . 7 ⊢ (𝑗 = (𝑖 + 1) → (𝑀...𝑗) = (𝑀...(𝑖 + 1)))
19	18	mpteq1d 5237	. . . . . 6 ⊢ (𝑗 = (𝑖 + 1) → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))
20	19	fveq2d 6910	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
21	17, 20	eqeq12d 2753	. . . 4 ⊢ (𝑗 = (𝑖 + 1) → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))))
22	21	imbi2d 340	. . 3 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
23		2fveq3 6911	. . . . 5 ⊢ (𝑗 = 𝑁 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑁)))
24		oveq2 7439	. . . . . . 7 ⊢ (𝑗 = 𝑁 → (𝑀...𝑗) = (𝑀...𝑁))
25	24	mpteq1d 5237	. . . . . 6 ⊢ (𝑗 = 𝑁 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))
26	25	fveq2d 6910	. . . . 5 ⊢ (𝑗 = 𝑁 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))
27	23, 26	eqeq12d 2753	. . . 4 ⊢ (𝑗 = 𝑁 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
28	27	imbi2d 340	. . 3 ⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))))
29		eluzel2 12883	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
30	1, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
31		fzsn 13606	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
32	30, 31	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑀...𝑀) = {𝑀})
33	32	mpteq1d 5237	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
34	33	fveq2d 6910	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))))
35		caratheodorylem1.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 ∈ OutMeas)
36	35	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑂 ∈ OutMeas)
37		eqid 2737	. . . . . . . 8 ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
38		caratheodorylem1.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (CaraGen‘𝑂)
39	38	caragenss 46519	. . . . . . . . . . 11 ⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂)
40	36, 39	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑆 ⊆ dom 𝑂)
41		caratheodorylem1.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)
42	41	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝐸:𝑍⟶𝑆)
43		elsni 4643	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑀} → 𝑛 = 𝑀)
44	43	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 = 𝑀)
45		uzid 12893	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
46	30, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
47		caratheodorylem1.z	. . . . . . . . . . . . . 14 ⊢ 𝑍 = (ℤ_≥‘𝑀)
48	46, 47	eleqtrrdi 2852	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
49	48	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑀 ∈ 𝑍)
50	44, 49	eqeltrd 2841	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 ∈ 𝑍)
51	42, 50	ffvelcdmd 7105	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ 𝑆)
52	40, 51	sseldd 3984	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ dom 𝑂)
53		elssuni 4937	. . . . . . . . 9 ⊢ ((𝐸‘𝑛) ∈ dom 𝑂 → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
54	52, 53	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
55	36, 37, 54	omecl 46518	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
56		eqid 2737	. . . . . . 7 ⊢ (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))
57	55, 56	fmptd 7134	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))):{𝑀}⟶(0[,]+∞))
58	30, 57	sge0sn 46394	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀))
59		eqidd 2738	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
60	32	iuneq1d 5019	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖))
61		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝐸‘𝑖) = (𝐸‘𝑀))
62	61	iunxsng 5090	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑍 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
63	48, 62	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
64		eqidd 2738	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑀) = (𝐸‘𝑀))
65	60, 63, 64	3eqtrrd 2782	. . . . . . . . 9 ⊢ (𝜑 → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
66	65	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
67		fveq2 6906	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → (𝐸‘𝑛) = (𝐸‘𝑀))
68	67	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐸‘𝑀))
69		caratheodorylem1.g	. . . . . . . . . 10 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))
70		oveq2 7439	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
71	70	iuneq1d 5019	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
72		ovex 7464	. . . . . . . . . . . 12 ⊢ (𝑀...𝑀) ∈ V
73		fvex 6919	. . . . . . . . . . . 12 ⊢ (𝐸‘𝑖) ∈ V
74	72, 73	iunex 7993	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V
75	74	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V)
76	69, 71, 48, 75	fvmptd3 7039	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
77	76	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
78	66, 68, 77	3eqtr4d 2787	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐺‘𝑀))
79	78	fveq2d 6910	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐺‘𝑀)))
80		snidg 4660	. . . . . . 7 ⊢ (𝑀 ∈ 𝑍 → 𝑀 ∈ {𝑀})
81	48, 80	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑀})
82		fvexd 6921	. . . . . 6 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) ∈ V)
83	59, 79, 81, 82	fvmptd 7023	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀) = (𝑂‘(𝐺‘𝑀)))
84	34, 58, 83	3eqtrrd 2782	. . . 4 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
85	84	a1i 11	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
86		simp3 1139	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝜑)
87		simp1 1137	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝑖 ∈ (𝑀..^𝑁))
88		id 22	. . . . . . 7 ⊢ ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
89	88	imp 406	. . . . . 6 ⊢ (((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
90	89	3adant1 1131	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
91		elfzoel1 13697	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℤ)
92		elfzoelz 13699	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℤ)
93	92	peano2zd 12725	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℤ)
94	91	zred 12722	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℝ)
95	93	zred 12722	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℝ)
96	92	zred 12722	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℝ)
97		elfzole1 13707	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑖)
98	96	ltp1d 12198	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 < (𝑖 + 1))
99	94, 96, 95, 97, 98	lelttrd 11419	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 < (𝑖 + 1))
100	94, 95, 99	ltled 11409	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ (𝑖 + 1))
101		leid 11357	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ ℝ → (𝑖 + 1) ≤ (𝑖 + 1))
102	95, 101	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ≤ (𝑖 + 1))
103	91, 93, 93, 100, 102	elfzd 13555	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
104	103	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
105		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑖 + 1) → (𝐸‘𝑗) = (𝐸‘(𝑖 + 1)))
106	105	ssiun2s 5048	. . . . . . . . . . . 12 ⊢ ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
107	104, 106	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
108		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝐸‘𝑖) = (𝐸‘𝑗))
109	108	cbviunv 5040	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)
110	109	mpteq2i 5247	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
111	69, 110	eqtri 2765	. . . . . . . . . . . . 13 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
112		oveq2 7439	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑖 + 1) → (𝑀...𝑛) = (𝑀...(𝑖 + 1)))
113	112	iuneq1d 5019	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑖 + 1) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
114	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ)
115	92	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℤ)
116	115	peano2zd 12725	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℤ)
117	114	zred 12722	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
118	116	zred 12722	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℝ)
119	115	zred 12722	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℝ)
120	97	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑖)
121	119	ltp1d 12198	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 < (𝑖 + 1))
122	117, 119, 118, 120, 121	lelttrd 11419	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 < (𝑖 + 1))
123	117, 118, 122	ltled 11409	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ (𝑖 + 1))
124	114, 116, 123	3jca 1129	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
125		eluz2 12884	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
126	124, 125	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (ℤ_≥‘𝑀))
127	47	eqcomi 2746	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) = 𝑍
128	126, 127	eleqtrdi 2851	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ 𝑍)
129		ovex 7464	. . . . . . . . . . . . . . 15 ⊢ (𝑀...(𝑖 + 1)) ∈ V
130		fvex 6919	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘𝑗) ∈ V
131	129, 130	iunex 7993	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V
132	131	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V)
133	111, 113, 128, 132	fvmptd3 7039	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
134	133	eqcomd 2743	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (𝐺‘(𝑖 + 1)))
135	107, 134	sseqtrd 4020	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)))
136		sseqin2 4223	. . . . . . . . . . 11 ⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) ↔ ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
137	136	biimpi 216	. . . . . . . . . 10 ⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
138	135, 137	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
139	138	fveq2d 6910	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐸‘(𝑖 + 1))))
140		nfcv 2905	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝐸‘(𝑖 + 1))
141		elfzouz 13703	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ (ℤ_≥‘𝑀))
142	141	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ (ℤ_≥‘𝑀))
143	140, 142, 105	iunp1 45071	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
144	133, 143	eqtrd 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
145	144	difeq1d 4125	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
146		caratheodorylem1.dj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛))
147		fveq2 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝐸‘𝑛) = (𝐸‘𝑗))
148	147	cbvdisjv 5121	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
149	146, 148	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
150	149	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
151		fzssuz 13605	. . . . . . . . . . . . . . 15 ⊢ (𝑀...𝑖) ⊆ (ℤ_≥‘𝑀)
152	151, 127	sseqtri 4032	. . . . . . . . . . . . . 14 ⊢ (𝑀...𝑖) ⊆ 𝑍
153	152	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀...𝑖) ⊆ 𝑍)
154		fzp1nel 13651	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝑖 + 1) ∈ (𝑀...𝑖)
155	154	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
156	155	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
157	128, 156	eldifd 3962	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑍 ∖ (𝑀...𝑖)))
158	150, 153, 157, 105	disjiun2 45063	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅)
159		undif4 4467	. . . . . . . . . . . 12 ⊢ ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅ → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
160	158, 159	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
161	160	eqcomd 2743	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))))
162		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝜑)
163	142, 127	eleqtrdi 2851	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ 𝑍)
164	111	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)))
165		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → 𝑛 = 𝑖)
166	165	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → (𝑀...𝑛) = (𝑀...𝑖))
167	166	iuneq1d 5019	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
168		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍)
169		ovex 7464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀...𝑖) ∈ V
170	169, 130	iunex 7993	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V
171	170	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V)
172	164, 167, 168, 171	fvmptd 7023	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
173	162, 163, 172	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
174	173	eqcomd 2743	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) = (𝐺‘𝑖))
175		difid 4376	. . . . . . . . . . . . 13 ⊢ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅
176	175	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅)
177	174, 176	uneq12d 4169	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((𝐺‘𝑖) ∪ ∅))
178		un0 4394	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖)
179	178	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖))
180	177, 179	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝐺‘𝑖))
181	145, 161, 180	3eqtrd 2781	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = (𝐺‘𝑖))
182	181	fveq2d 6910	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐺‘𝑖)))
183	139, 182	oveq12d 7449	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
184	183	3adant3 1133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
185	35	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑂 ∈ OutMeas)
186	41	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝐸:𝑍⟶𝑆)
187	186, 128	ffvelcdmd 7105	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ∈ 𝑆)
188		simpll 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
189	91	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ∈ ℤ)
190		elfzelz 13564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑗 ∈ ℤ)
191	190	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ ℤ)
192		elfzle1 13567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑀 ≤ 𝑗)
193	192	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ≤ 𝑗)
194	189, 191, 193	3jca 1129	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
195		eluz2 12884	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
196	194, 195	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ (ℤ_≥‘𝑀))
197	196, 127	eleqtrdi 2851	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
198	197	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
199	35, 39	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ⊆ dom 𝑂)
200	199	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑆 ⊆ dom 𝑂)
201	41	ffvelcdmda 7104	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ 𝑆)
202	200, 201	sseldd 3984	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ dom 𝑂)
203		elssuni 4937	. . . . . . . . . . . . . 14 ⊢ ((𝐸‘𝑗) ∈ dom 𝑂 → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
204	202, 203	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
205	188, 198, 204	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
206	205	ralrimiva 3146	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
207		iunss 5045	. . . . . . . . . . 11 ⊢ (∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
208	206, 207	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
209	133, 208	eqsstrd 4018	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
210	185, 38, 37, 187, 209	caragensplit 46515	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = (𝑂‘(𝐺‘(𝑖 + 1))))
211	210	eqcomd 2743	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
212	211	3adant3 1133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
213	185	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑂 ∈ OutMeas)
214	162	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
215		elfzuz 13560	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ (ℤ_≥‘𝑀))
216	215, 127	eleqtrdi 2851	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ 𝑍)
217	216	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑛 ∈ 𝑍)
218	41, 199	fssd 6753	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑂)
219	218	ffvelcdmda 7104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑂)
220	219, 53	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
221	214, 217, 220	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
222	213, 37, 221	omecl 46518	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
223		2fveq3 6911	. . . . . . . . 9 ⊢ (𝑛 = (𝑖 + 1) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐸‘(𝑖 + 1))))
224	142, 222, 223	sge0p1 46429	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
225	224	3adant3 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
226		id 22	. . . . . . . . . 10 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
227	226	eqcomd 2743	. . . . . . . . 9 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) = (𝑂‘(𝐺‘𝑖)))
228	227	oveq1d 7446	. . . . . . . 8 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
229	228	3ad2ant3 1136	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
230		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝜑)
231	152	sseli 3979	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ 𝑍)
232	231	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ 𝑍)
233	230, 232, 204	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
234	233	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
235	234	ralrimiva 3146	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
236		iunss 5045	. . . . . . . . . . . . 13 ⊢ (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
237	235, 236	sylibr 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
238	172, 237	eqsstrd 4018	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
239	162, 163, 238	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
240	185, 37, 239	omexrcl 46522	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘𝑖)) ∈ ℝ^*)
241	107, 208	sstrd 3994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
242	185, 37, 241	omexrcl 46522	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐸‘(𝑖 + 1))) ∈ ℝ^*)
243	240, 242	xaddcomd 45335	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
244	243	3adant3 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
245	225, 229, 244	3eqtrd 2781	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
246	184, 212, 245	3eqtr4d 2787	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
247	86, 87, 90, 246	syl3anc 1373	. . . 4 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
248	247	3exp 1120	. . 3 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
249	10, 16, 22, 28, 85, 248	fzind2 13824	. 2 ⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
250	3, 4, 249	sylc 65	1 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 {csn 4626 ∪ cuni 4907 ∪ ciun 4991 Disj wdisj 5110 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 +∞cpnf 11292 ≤ cle 11296 ℤcz 12613 ℤ_≥cuz 12878 +_𝑒 cxad 13152 [,]cicc 13390 ...cfz 13547 ..^cfzo 13694 Σ^{^}csumge0 46377 OutMeascome 46504 CaraGenccaragen 46506

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-z 12614 df-uz 12879 df-rp 13035 df-xadd 13155 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-clim 15524 df-sum 15723 df-sumge0 46378 df-ome 46505 df-caragen 46507

This theorem is referenced by: caratheodorylem2 46542

W3C validator