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 46634

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 13432	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
4		id 22	. 2 ⊢ (𝜑 → 𝜑)
5		2fveq3 6827	. . . . 5 ⊢ (𝑗 = 𝑀 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑀)))
6		oveq2 7354	. . . . . . 7 ⊢ (𝑗 = 𝑀 → (𝑀...𝑗) = (𝑀...𝑀))
7	6	mpteq1d 5179	. . . . . 6 ⊢ (𝑗 = 𝑀 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))
8	7	fveq2d 6826	. . . . 5 ⊢ (𝑗 = 𝑀 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
9	5, 8	eqeq12d 2747	. . . 4 ⊢ (𝑗 = 𝑀 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
10	9	imbi2d 340	. . 3 ⊢ (𝑗 = 𝑀 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))))
11		2fveq3 6827	. . . . 5 ⊢ (𝑗 = 𝑖 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑖)))
12		oveq2 7354	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (𝑀...𝑗) = (𝑀...𝑖))
13	12	mpteq1d 5179	. . . . . 6 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))
14	13	fveq2d 6826	. . . . 5 ⊢ (𝑗 = 𝑖 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
15	11, 14	eqeq12d 2747	. . . 4 ⊢ (𝑗 = 𝑖 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
16	15	imbi2d 340	. . 3 ⊢ (𝑗 = 𝑖 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))))
17		2fveq3 6827	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘(𝑖 + 1))))
18		oveq2 7354	. . . . . . 7 ⊢ (𝑗 = (𝑖 + 1) → (𝑀...𝑗) = (𝑀...(𝑖 + 1)))
19	18	mpteq1d 5179	. . . . . 6 ⊢ (𝑗 = (𝑖 + 1) → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))
20	19	fveq2d 6826	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
21	17, 20	eqeq12d 2747	. . . 4 ⊢ (𝑗 = (𝑖 + 1) → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))))
22	21	imbi2d 340	. . 3 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
23		2fveq3 6827	. . . . 5 ⊢ (𝑗 = 𝑁 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑁)))
24		oveq2 7354	. . . . . . 7 ⊢ (𝑗 = 𝑁 → (𝑀...𝑗) = (𝑀...𝑁))
25	24	mpteq1d 5179	. . . . . 6 ⊢ (𝑗 = 𝑁 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))
26	25	fveq2d 6826	. . . . 5 ⊢ (𝑗 = 𝑁 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))
27	23, 26	eqeq12d 2747	. . . 4 ⊢ (𝑗 = 𝑁 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
28	27	imbi2d 340	. . 3 ⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))))
29		eluzel2 12737	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
30	1, 29	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
31		fzsn 13466	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
32	30, 31	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑀...𝑀) = {𝑀})
33	32	mpteq1d 5179	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
34	33	fveq2d 6826	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))))
35		caratheodorylem1.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 ∈ OutMeas)
36	35	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑂 ∈ OutMeas)
37		eqid 2731	. . . . . . . 8 ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
38		caratheodorylem1.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (CaraGen‘𝑂)
39	38	caragenss 46612	. . . . . . . . . . 11 ⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂)
40	36, 39	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑆 ⊆ dom 𝑂)
41		caratheodorylem1.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)
42	41	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝐸:𝑍⟶𝑆)
43		elsni 4590	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑀} → 𝑛 = 𝑀)
44	43	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 = 𝑀)
45		uzid 12747	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
46	30, 45	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
47		caratheodorylem1.z	. . . . . . . . . . . . . 14 ⊢ 𝑍 = (ℤ_≥‘𝑀)
48	46, 47	eleqtrrdi 2842	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
49	48	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑀 ∈ 𝑍)
50	44, 49	eqeltrd 2831	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 ∈ 𝑍)
51	42, 50	ffvelcdmd 7018	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ 𝑆)
52	40, 51	sseldd 3930	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ dom 𝑂)
53		elssuni 4887	. . . . . . . . 9 ⊢ ((𝐸‘𝑛) ∈ dom 𝑂 → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
54	52, 53	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
55	36, 37, 54	omecl 46611	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
56		eqid 2731	. . . . . . 7 ⊢ (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))
57	55, 56	fmptd 7047	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))):{𝑀}⟶(0[,]+∞))
58	30, 57	sge0sn 46487	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀))
59		eqidd 2732	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
60	32	iuneq1d 4967	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖))
61		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝐸‘𝑖) = (𝐸‘𝑀))
62	61	iunxsng 5036	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑍 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
63	48, 62	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
64		eqidd 2732	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑀) = (𝐸‘𝑀))
65	60, 63, 64	3eqtrrd 2771	. . . . . . . . 9 ⊢ (𝜑 → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
66	65	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
67		fveq2 6822	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → (𝐸‘𝑛) = (𝐸‘𝑀))
68	67	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐸‘𝑀))
69		caratheodorylem1.g	. . . . . . . . . 10 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))
70		oveq2 7354	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
71	70	iuneq1d 4967	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
72		ovex 7379	. . . . . . . . . . . 12 ⊢ (𝑀...𝑀) ∈ V
73		fvex 6835	. . . . . . . . . . . 12 ⊢ (𝐸‘𝑖) ∈ V
74	72, 73	iunex 7900	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V
75	74	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V)
76	69, 71, 48, 75	fvmptd3 6952	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
77	76	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
78	66, 68, 77	3eqtr4d 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐺‘𝑀))
79	78	fveq2d 6826	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐺‘𝑀)))
80		snidg 4610	. . . . . . 7 ⊢ (𝑀 ∈ 𝑍 → 𝑀 ∈ {𝑀})
81	48, 80	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑀})
82		fvexd 6837	. . . . . 6 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) ∈ V)
83	59, 79, 81, 82	fvmptd 6936	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀) = (𝑂‘(𝐺‘𝑀)))
84	34, 58, 83	3eqtrrd 2771	. . . 4 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
85	84	a1i 11	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
86		simp3 1138	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝜑)
87		simp1 1136	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝑖 ∈ (𝑀..^𝑁))
88		id 22	. . . . . . 7 ⊢ ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
89	88	imp 406	. . . . . 6 ⊢ (((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
90	89	3adant1 1130	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
91		elfzoel1 13557	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℤ)
92		elfzoelz 13559	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℤ)
93	92	peano2zd 12580	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℤ)
94	91	zred 12577	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℝ)
95	93	zred 12577	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℝ)
96	92	zred 12577	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℝ)
97		elfzole1 13567	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑖)
98	96	ltp1d 12052	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 < (𝑖 + 1))
99	94, 96, 95, 97, 98	lelttrd 11271	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 < (𝑖 + 1))
100	94, 95, 99	ltled 11261	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ (𝑖 + 1))
101		leid 11209	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ ℝ → (𝑖 + 1) ≤ (𝑖 + 1))
102	95, 101	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ≤ (𝑖 + 1))
103	91, 93, 93, 100, 102	elfzd 13415	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
104	103	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
105		fveq2 6822	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑖 + 1) → (𝐸‘𝑗) = (𝐸‘(𝑖 + 1)))
106	105	ssiun2s 4995	. . . . . . . . . . . 12 ⊢ ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
107	104, 106	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
108		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝐸‘𝑖) = (𝐸‘𝑗))
109	108	cbviunv 4987	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)
110	109	mpteq2i 5185	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
111	69, 110	eqtri 2754	. . . . . . . . . . . . 13 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
112		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑖 + 1) → (𝑀...𝑛) = (𝑀...(𝑖 + 1)))
113	112	iuneq1d 4967	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑖 + 1) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
114	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ)
115	92	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℤ)
116	115	peano2zd 12580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℤ)
117	114	zred 12577	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
118	116	zred 12577	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℝ)
119	115	zred 12577	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℝ)
120	97	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑖)
121	119	ltp1d 12052	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 < (𝑖 + 1))
122	117, 119, 118, 120, 121	lelttrd 11271	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 < (𝑖 + 1))
123	117, 118, 122	ltled 11261	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ (𝑖 + 1))
124	114, 116, 123	3jca 1128	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
125		eluz2 12738	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
126	124, 125	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (ℤ_≥‘𝑀))
127	47	eqcomi 2740	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) = 𝑍
128	126, 127	eleqtrdi 2841	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ 𝑍)
129		ovex 7379	. . . . . . . . . . . . . . 15 ⊢ (𝑀...(𝑖 + 1)) ∈ V
130		fvex 6835	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘𝑗) ∈ V
131	129, 130	iunex 7900	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V
132	131	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V)
133	111, 113, 128, 132	fvmptd3 6952	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
134	133	eqcomd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (𝐺‘(𝑖 + 1)))
135	107, 134	sseqtrd 3966	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)))
136		sseqin2 4170	. . . . . . . . . . 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 6826	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐸‘(𝑖 + 1))))
140		nfcv 2894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝐸‘(𝑖 + 1))
141		elfzouz 13563	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ (ℤ_≥‘𝑀))
142	141	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ (ℤ_≥‘𝑀))
143	140, 142, 105	iunp1 45173	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
144	133, 143	eqtrd 2766	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
145	144	difeq1d 4072	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
146		caratheodorylem1.dj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛))
147		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝐸‘𝑛) = (𝐸‘𝑗))
148	147	cbvdisjv 5067	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
149	146, 148	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
150	149	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
151		fzssuz 13465	. . . . . . . . . . . . . . 15 ⊢ (𝑀...𝑖) ⊆ (ℤ_≥‘𝑀)
152	151, 127	sseqtri 3978	. . . . . . . . . . . . . 14 ⊢ (𝑀...𝑖) ⊆ 𝑍
153	152	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀...𝑖) ⊆ 𝑍)
154		fzp1nel 13511	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝑖 + 1) ∈ (𝑀...𝑖)
155	154	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
156	155	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
157	128, 156	eldifd 3908	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑍 ∖ (𝑀...𝑖)))
158	150, 153, 157, 105	disjiun2 45165	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅)
159		undif4 4414	. . . . . . . . . . . 12 ⊢ ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅ → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
160	158, 159	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
161	160	eqcomd 2737	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))))
162		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝜑)
163	142, 127	eleqtrdi 2841	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ 𝑍)
164	111	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)))
165		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → 𝑛 = 𝑖)
166	165	oveq2d 7362	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → (𝑀...𝑛) = (𝑀...𝑖))
167	166	iuneq1d 4967	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
168		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍)
169		ovex 7379	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀...𝑖) ∈ V
170	169, 130	iunex 7900	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V
171	170	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V)
172	164, 167, 168, 171	fvmptd 6936	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
173	162, 163, 172	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
174	173	eqcomd 2737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) = (𝐺‘𝑖))
175		difid 4323	. . . . . . . . . . . . 13 ⊢ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅
176	175	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅)
177	174, 176	uneq12d 4116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((𝐺‘𝑖) ∪ ∅))
178		un0 4341	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖)
179	178	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖))
180	177, 179	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝐺‘𝑖))
181	145, 161, 180	3eqtrd 2770	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = (𝐺‘𝑖))
182	181	fveq2d 6826	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐺‘𝑖)))
183	139, 182	oveq12d 7364	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
184	183	3adant3 1132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
185	35	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑂 ∈ OutMeas)
186	41	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝐸:𝑍⟶𝑆)
187	186, 128	ffvelcdmd 7018	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ∈ 𝑆)
188		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
189	91	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ∈ ℤ)
190		elfzelz 13424	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑗 ∈ ℤ)
191	190	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ ℤ)
192		elfzle1 13427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑀 ≤ 𝑗)
193	192	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ≤ 𝑗)
194	189, 191, 193	3jca 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
195		eluz2 12738	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
196	194, 195	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ (ℤ_≥‘𝑀))
197	196, 127	eleqtrdi 2841	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
198	197	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
199	35, 39	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ⊆ dom 𝑂)
200	199	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑆 ⊆ dom 𝑂)
201	41	ffvelcdmda 7017	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ 𝑆)
202	200, 201	sseldd 3930	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ dom 𝑂)
203		elssuni 4887	. . . . . . . . . . . . . 14 ⊢ ((𝐸‘𝑗) ∈ dom 𝑂 → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
204	202, 203	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
205	188, 198, 204	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
206	205	ralrimiva 3124	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
207		iunss 4992	. . . . . . . . . . 11 ⊢ (∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
208	206, 207	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
209	133, 208	eqsstrd 3964	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
210	185, 38, 37, 187, 209	caragensplit 46608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = (𝑂‘(𝐺‘(𝑖 + 1))))
211	210	eqcomd 2737	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
212	211	3adant3 1132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
213	185	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑂 ∈ OutMeas)
214	162	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
215		elfzuz 13420	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ (ℤ_≥‘𝑀))
216	215, 127	eleqtrdi 2841	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ 𝑍)
217	216	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑛 ∈ 𝑍)
218	41, 199	fssd 6668	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑂)
219	218	ffvelcdmda 7017	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑂)
220	219, 53	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
221	214, 217, 220	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
222	213, 37, 221	omecl 46611	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
223		2fveq3 6827	. . . . . . . . 9 ⊢ (𝑛 = (𝑖 + 1) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐸‘(𝑖 + 1))))
224	142, 222, 223	sge0p1 46522	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
225	224	3adant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
226		id 22	. . . . . . . . . 10 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
227	226	eqcomd 2737	. . . . . . . . 9 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) = (𝑂‘(𝐺‘𝑖)))
228	227	oveq1d 7361	. . . . . . . 8 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
229	228	3ad2ant3 1135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
230		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝜑)
231	152	sseli 3925	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ 𝑍)
232	231	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ 𝑍)
233	230, 232, 204	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
234	233	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
235	234	ralrimiva 3124	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
236		iunss 4992	. . . . . . . . . . . . 13 ⊢ (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
237	235, 236	sylibr 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
238	172, 237	eqsstrd 3964	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
239	162, 163, 238	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
240	185, 37, 239	omexrcl 46615	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘𝑖)) ∈ ℝ^*)
241	107, 208	sstrd 3940	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
242	185, 37, 241	omexrcl 46615	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐸‘(𝑖 + 1))) ∈ ℝ^*)
243	240, 242	xaddcomd 45433	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
244	243	3adant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
245	225, 229, 244	3eqtrd 2770	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
246	184, 212, 245	3eqtr4d 2776	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
247	86, 87, 90, 246	syl3anc 1373	. . . 4 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
248	247	3exp 1119	. . 3 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
249	10, 16, 22, 28, 85, 248	fzind2 13688	. 2 ⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
250	3, 4, 249	sylc 65	1 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ∀wral 3047 Vcvv 3436 ∖ cdif 3894 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ∅c0 4280 {csn 4573 ∪ cuni 4856 ∪ ciun 4939 Disj wdisj 5056 class class class wbr 5089 ↦ cmpt 5170 dom cdm 5614 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 +∞cpnf 11143 ≤ cle 11147 ℤcz 12468 ℤ_≥cuz 12732 +_𝑒 cxad 13009 [,]cicc 13248 ...cfz 13407 ..^cfzo 13554 Σ^{^}csumge0 46470 OutMeascome 46597 CaraGenccaragen 46599

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-disj 5057 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-oi 9396 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-xadd 13012 df-ico 13251 df-icc 13252 df-fz 13408 df-fzo 13555 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-sum 15594 df-sumge0 46471 df-ome 46598 df-caragen 46600

This theorem is referenced by: caratheodorylem2 46635

W3C validator