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 47535

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 13665	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
3	1, 2	syl 18	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
4		id 23	. 2 ⊢ (𝜑 → 𝜑)
5		2fveq3 6890	. . . . 5 ⊢ (𝑗 = 𝑀 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑀)))
6		oveq2 7428	. . . . . . 7 ⊢ (𝑗 = 𝑀 → (𝑀...𝑗) = (𝑀...𝑀))
7	6	mpteq1d 5195	. . . . . 6 ⊢ (𝑗 = 𝑀 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))
8	7	fveq2d 6889	. . . . 5 ⊢ (𝑗 = 𝑀 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
9	5, 8	eqeq12d 2777	. . . 4 ⊢ (𝑗 = 𝑀 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
10	9	imbi2d 343	. . 3 ⊢ (𝑗 = 𝑀 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))))
11		2fveq3 6890	. . . . 5 ⊢ (𝑗 = 𝑖 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑖)))
12		oveq2 7428	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (𝑀...𝑗) = (𝑀...𝑖))
13	12	mpteq1d 5195	. . . . . 6 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))
14	13	fveq2d 6889	. . . . 5 ⊢ (𝑗 = 𝑖 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
15	11, 14	eqeq12d 2777	. . . 4 ⊢ (𝑗 = 𝑖 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
16	15	imbi2d 343	. . 3 ⊢ (𝑗 = 𝑖 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))))
17		2fveq3 6890	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘(𝑖 + 1))))
18		oveq2 7428	. . . . . . 7 ⊢ (𝑗 = (𝑖 + 1) → (𝑀...𝑗) = (𝑀...(𝑖 + 1)))
19	18	mpteq1d 5195	. . . . . 6 ⊢ (𝑗 = (𝑖 + 1) → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))
20	19	fveq2d 6889	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
21	17, 20	eqeq12d 2777	. . . 4 ⊢ (𝑗 = (𝑖 + 1) → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))))
22	21	imbi2d 343	. . 3 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
23		2fveq3 6890	. . . . 5 ⊢ (𝑗 = 𝑁 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑁)))
24		oveq2 7428	. . . . . . 7 ⊢ (𝑗 = 𝑁 → (𝑀...𝑗) = (𝑀...𝑁))
25	24	mpteq1d 5195	. . . . . 6 ⊢ (𝑗 = 𝑁 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))
26	25	fveq2d 6889	. . . . 5 ⊢ (𝑗 = 𝑁 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))
27	23, 26	eqeq12d 2777	. . . 4 ⊢ (𝑗 = 𝑁 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
28	27	imbi2d 343	. . 3 ⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))))
29		eluzel2 12970	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
30	1, 29	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
31		fzsn 13700	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
32	30, 31	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑀...𝑀) = {𝑀})
33	32	mpteq1d 5195	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
34	33	fveq2d 6889	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))))
35		caratheodorylem1.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 ∈ OutMeas)
36	35	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑂 ∈ OutMeas)
37		eqid 2761	. . . . . . . 8 ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
38		caratheodorylem1.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (CaraGen‘𝑂)
39	38	caragenss 47513	. . . . . . . . . . 11 ⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂)
40	36, 39	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑆 ⊆ dom 𝑂)
41		caratheodorylem1.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)
42	41	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝐸:𝑍⟶𝑆)
43		elsni 4601	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑀} → 𝑛 = 𝑀)
44	43	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 = 𝑀)
45		uzid 12980	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
46	30, 45	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
47		caratheodorylem1.z	. . . . . . . . . . . . . 14 ⊢ 𝑍 = (ℤ_≥‘𝑀)
48	46, 47	eleqtrrdi 2872	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
49	48	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑀 ∈ 𝑍)
50	44, 49	eqeltrd 2861	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 ∈ 𝑍)
51	42, 50	ffvelcdmd 7085	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ 𝑆)
52	40, 51	sseldd 3932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ dom 𝑂)
53		elssuni 4899	. . . . . . . . 9 ⊢ ((𝐸‘𝑛) ∈ dom 𝑂 → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
54	52, 53	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
55	36, 37, 54	omecl 47512	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
56		eqid 2761	. . . . . . 7 ⊢ (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))
57	55, 56	fmptd 7114	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))):{𝑀}⟶(0[,]+∞))
58	30, 57	sge0sn 47388	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀))
59		eqidd 2762	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
60	32	iuneq1d 4979	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖))
61		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝐸‘𝑖) = (𝐸‘𝑀))
62	61	iunxsng 5050	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑍 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
63	48, 62	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
64		eqidd 2762	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑀) = (𝐸‘𝑀))
65	60, 63, 64	3eqtrrd 2801	. . . . . . . . 9 ⊢ (𝜑 → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
66	65	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
67		fveq2 6885	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → (𝐸‘𝑛) = (𝐸‘𝑀))
68	67	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐸‘𝑀))
69		caratheodorylem1.g	. . . . . . . . . 10 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))
70		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
71	70	iuneq1d 4979	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
72		ovex 7453	. . . . . . . . . . . 12 ⊢ (𝑀...𝑀) ∈ V
73		fvex 6898	. . . . . . . . . . . 12 ⊢ (𝐸‘𝑖) ∈ V
74	72, 73	iunex 7980	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V
75	74	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V)
76	69, 71, 48, 75	fvmptd3 7017	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
77	76	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
78	66, 68, 77	3eqtr4d 2806	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐺‘𝑀))
79	78	fveq2d 6889	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐺‘𝑀)))
80		snidg 4621	. . . . . . 7 ⊢ (𝑀 ∈ 𝑍 → 𝑀 ∈ {𝑀})
81	48, 80	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑀})
82		fvexd 6900	. . . . . 6 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) ∈ V)
83	59, 79, 81, 82	fvmptd 7001	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀) = (𝑂‘(𝐺‘𝑀)))
84	34, 58, 83	3eqtrrd 2801	. . . 4 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
85	84	a1i 11	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
86		simp3 1156	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝜑)
87		simp1 1154	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝑖 ∈ (𝑀..^𝑁))
88		id 23	. . . . . . 7 ⊢ ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
89	88	imp 412	. . . . . 6 ⊢ (((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
90	89	3adant1 1148	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
91		elfzoel1 13791	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℤ)
92		elfzoelz 13793	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℤ)
93	92	peano2zd 12806	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℤ)
94	91	zred 12803	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℝ)
95	93	zred 12803	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℝ)
96	92	zred 12803	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℝ)
97		elfzole1 13802	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑖)
98	96	ltp1d 12247	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 < (𝑖 + 1))
99	94, 96, 95, 97, 98	lelttrd 11468	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 < (𝑖 + 1))
100	94, 95, 99	ltled 11458	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ (𝑖 + 1))
101		leid 11406	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ ℝ → (𝑖 + 1) ≤ (𝑖 + 1))
102	95, 101	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ≤ (𝑖 + 1))
103	91, 93, 93, 100, 102	elfzd 13647	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
104	103	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
105		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑖 + 1) → (𝐸‘𝑗) = (𝐸‘(𝑖 + 1)))
106	105	ssiun2s 5007	. . . . . . . . . . . 12 ⊢ ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
107	104, 106	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
108		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → (𝐸‘𝑖) = (𝐸‘𝑗))
109	108	cbviunv 4997	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)
110	109	mpteq2i 5201	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
111	69, 110	eqtri 2784	. . . . . . . . . . . . 13 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
112		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑖 + 1) → (𝑀...𝑛) = (𝑀...(𝑖 + 1)))
113	112	iuneq1d 4979	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑖 + 1) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
114	30	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ)
115	92	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℤ)
116	115	peano2zd 12806	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℤ)
117	114	zred 12803	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
118	116	zred 12803	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℝ)
119	115	zred 12803	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℝ)
120	97	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑖)
121	119	ltp1d 12247	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 < (𝑖 + 1))
122	117, 119, 118, 120, 121	lelttrd 11468	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 < (𝑖 + 1))
123	117, 118, 122	ltled 11458	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ (𝑖 + 1))
124	114, 116, 123	3jca 1146	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
125		eluz2 12971	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
126	124, 125	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (ℤ_≥‘𝑀))
127	47	eqcomi 2770	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) = 𝑍
128	126, 127	eleqtrdi 2871	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ 𝑍)
129		ovex 7453	. . . . . . . . . . . . . . 15 ⊢ (𝑀...(𝑖 + 1)) ∈ V
130		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘𝑗) ∈ V
131	129, 130	iunex 7980	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V
132	131	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V)
133	111, 113, 128, 132	fvmptd3 7017	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
134	133	eqcomd 2767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (𝐺‘(𝑖 + 1)))
135	107, 134	sseqtrd 3967	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)))
136		sseqin2 4169	. . . . . . . . . . 11 ⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) ↔ ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
137	136	biimpi 219	. . . . . . . . . 10 ⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
138	135, 137	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
139	138	fveq2d 6889	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐸‘(𝑖 + 1))))
140		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝐸‘(𝑖 + 1))
141		elfzouz 13798	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ (ℤ_≥‘𝑀))
142	141	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ (ℤ_≥‘𝑀))
143	140, 142, 105	iunp1 46082	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
144	133, 143	eqtrd 2796	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
145	144	difeq1d 4073	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
146		caratheodorylem1.dj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛))
147		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝐸‘𝑛) = (𝐸‘𝑗))
148	147	cbvdisjv 5081	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
149	146, 148	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
150	149	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
151		fzssuz 13699	. . . . . . . . . . . . . . 15 ⊢ (𝑀...𝑖) ⊆ (ℤ_≥‘𝑀)
152	151, 127	sseqtri 3979	. . . . . . . . . . . . . 14 ⊢ (𝑀...𝑖) ⊆ 𝑍
153	152	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀...𝑖) ⊆ 𝑍)
154		fzp1nel 13745	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝑖 + 1) ∈ (𝑀...𝑖)
155	154	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
156	155	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
157	128, 156	eldifd 3910	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑍 ∖ (𝑀...𝑖)))
158	150, 153, 157, 105	disjiun2 46074	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅)
159		undif4 4420	. . . . . . . . . . . 12 ⊢ ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅ → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
160	158, 159	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
161	160	eqcomd 2767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))))
162		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝜑)
163	142, 127	eleqtrdi 2871	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ 𝑍)
164	111	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)))
165		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → 𝑛 = 𝑖)
166	165	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → (𝑀...𝑛) = (𝑀...𝑖))
167	166	iuneq1d 4979	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
168		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍)
169		ovex 7453	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀...𝑖) ∈ V
170	169, 130	iunex 7980	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V
171	170	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V)
172	164, 167, 168, 171	fvmptd 7001	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
173	162, 163, 172	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
174	173	eqcomd 2767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) = (𝐺‘𝑖))
175		difid 4325	. . . . . . . . . . . . 13 ⊢ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅
176	175	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅)
177	174, 176	uneq12d 4116	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((𝐺‘𝑖) ∪ ∅))
178		un0 4344	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖)
179	178	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖))
180	177, 179	eqtrd 2796	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝐺‘𝑖))
181	145, 161, 180	3eqtrd 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = (𝐺‘𝑖))
182	181	fveq2d 6889	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐺‘𝑖)))
183	139, 182	oveq12d 7438	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_e (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_e (𝑂‘(𝐺‘𝑖))))
184	183	3adant3 1150	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_e (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_e (𝑂‘(𝐺‘𝑖))))
185	35	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑂 ∈ OutMeas)
186	41	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝐸:𝑍⟶𝑆)
187	186, 128	ffvelcdmd 7085	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ∈ 𝑆)
188		simpll 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
189	91	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ∈ ℤ)
190		elfzelz 13656	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑗 ∈ ℤ)
191	190	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ ℤ)
192		elfzle1 13660	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑀 ≤ 𝑗)
193	192	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ≤ 𝑗)
194	189, 191, 193	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
195		eluz2 12971	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
196	194, 195	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ (ℤ_≥‘𝑀))
197	196, 127	eleqtrdi 2871	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
198	197	adantll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
199	35, 39	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ⊆ dom 𝑂)
200	199	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑆 ⊆ dom 𝑂)
201	41	ffvelcdmda 7084	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ 𝑆)
202	200, 201	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ dom 𝑂)
203		elssuni 4899	. . . . . . . . . . . . . 14 ⊢ ((𝐸‘𝑗) ∈ dom 𝑂 → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
204	202, 203	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
205	188, 198, 204	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
206	205	ralrimiva 3155	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
207		iunss 5003	. . . . . . . . . . 11 ⊢ (∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
208	206, 207	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
209	133, 208	eqsstrd 3965	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
210	185, 38, 37, 187, 209	caragensplit 47509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_e (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = (𝑂‘(𝐺‘(𝑖 + 1))))
211	210	eqcomd 2767	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_e (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
212	211	3adant3 1150	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_e (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
213	185	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑂 ∈ OutMeas)
214	162	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
215		elfzuz 13652	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ (ℤ_≥‘𝑀))
216	215, 127	eleqtrdi 2871	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ 𝑍)
217	216	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑛 ∈ 𝑍)
218	41, 199	fssd 6727	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑂)
219	218	ffvelcdmda 7084	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑂)
220	219, 53	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
221	214, 217, 220	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
222	213, 37, 221	omecl 47512	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
223		2fveq3 6890	. . . . . . . . 9 ⊢ (𝑛 = (𝑖 + 1) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐸‘(𝑖 + 1))))
224	142, 222, 223	sge0p1 47423	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_e (𝑂‘(𝐸‘(𝑖 + 1)))))
225	224	3adant3 1150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_e (𝑂‘(𝐸‘(𝑖 + 1)))))
226		id 23	. . . . . . . . . 10 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
227	226	eqcomd 2767	. . . . . . . . 9 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) = (𝑂‘(𝐺‘𝑖)))
228	227	oveq1d 7435	. . . . . . . 8 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_e (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_e (𝑂‘(𝐸‘(𝑖 + 1)))))
229	228	3ad2ant3 1153	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_e (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_e (𝑂‘(𝐸‘(𝑖 + 1)))))
230		simpl 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝜑)
231	152	sseli 3927	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ 𝑍)
232	231	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ 𝑍)
233	230, 232, 204	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
234	233	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
235	234	ralrimiva 3155	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
236		iunss 5003	. . . . . . . . . . . . 13 ⊢ (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
237	235, 236	sylibr 237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
238	172, 237	eqsstrd 3965	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
239	162, 163, 238	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
240	185, 37, 239	omexrcl 47516	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘𝑖)) ∈ ℝ^*)
241	107, 208	sstrd 3941	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
242	185, 37, 241	omexrcl 47516	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐸‘(𝑖 + 1))) ∈ ℝ^*)
243	240, 242	xaddcomd 46335	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘(𝐺‘𝑖)) +_e (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_e (𝑂‘(𝐺‘𝑖))))
244	243	3adant3 1150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘(𝐺‘𝑖)) +_e (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_e (𝑂‘(𝐺‘𝑖))))
245	225, 229, 244	3eqtrd 2800	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_e (𝑂‘(𝐺‘𝑖))))
246	184, 212, 245	3eqtr4d 2806	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
247	86, 87, 90, 246	syl3anc 1398	. . . 4 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
248	247	3exp 1137	. . 3 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
249	10, 16, 22, 28, 85, 248	fzind2 13923	. 2 ⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
250	3, 4, 249	sylc 66	1 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3077 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 {csn 4584 ∪ cuni 4867 ∪ ciun 4951 Disj wdisj 5070 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 +∞cpnf 11340 ≤ cle 11344 ℤcz 12693 ℤ_≥cuz 12965 +_e cxad 13239 [,]cicc 13479 ...cfz 13639 ..^cfzo 13788 Σ^{^}csumge0 47371 OutMeascome 47498 CaraGenccaragen 47500

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-sup 9434 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-xadd 13242 df-ico 13482 df-icc 13483 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-sum 15854 df-sumge0 47372 df-ome 47499 df-caragen 47501

This theorem is used by: caratheodorylem2 47536

W3C validator