carageniuncllem1

Description: The outer measure of A i^i ( Gn ) is the sum of the outer measures of A i^i ( Fm ) . These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	carageniuncllem1.o	$⊢ φ \to O \in OutMeas$
	carageniuncllem1.s	$⊢ S = CaraGen (O)$
	carageniuncllem1.x	$⊢ X = ⋃ dom O$
	carageniuncllem1.a	$⊢ φ \to A \subseteq X$
	carageniuncllem1.re	$⊢ φ \to O (A) \in ℝ$
	carageniuncllem1.z	$⊢ Z = ℤ_{\geq M}$
	carageniuncllem1.e	$⊢ φ \to E : Z ⟶ S$
	carageniuncllem1.g	$⊢ G = (n \in Z ⟼ ⋃_{i = M}^{n} E (i))$
	carageniuncllem1.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (M ..^n)} E (i))$
	carageniuncllem1.k	$⊢ φ \to K \in Z$
Assertion	carageniuncllem1	$⊢ φ \to \sum_{n = M}^{K} O (A \cap F (n)) = O (A \cap G (K))$

Proof

Step	Hyp	Ref	Expression
1		carageniuncllem1.o	$⊢ φ \to O \in OutMeas$
2		carageniuncllem1.s	$⊢ S = CaraGen (O)$
3		carageniuncllem1.x	$⊢ X = ⋃ dom O$
4		carageniuncllem1.a	$⊢ φ \to A \subseteq X$
5		carageniuncllem1.re	$⊢ φ \to O (A) \in ℝ$
6		carageniuncllem1.z	$⊢ Z = ℤ_{\geq M}$
7		carageniuncllem1.e	$⊢ φ \to E : Z ⟶ S$
8		carageniuncllem1.g	$⊢ G = (n \in Z ⟼ ⋃_{i = M}^{n} E (i))$
9		carageniuncllem1.f	$⊢ F = (n \in Z ⟼ E (n) ∖ ⋃_{i \in (M ..^n)} E (i))$
10		carageniuncllem1.k	$⊢ φ \to K \in Z$
11	10 6	eleqtrdi	$⊢ φ \to K \in ℤ_{\geq M}$
12		eluzfz2	$⊢ K \in ℤ_{\geq M} \to K \in (M \dots K)$
13	11 12	syl	$⊢ φ \to K \in (M \dots K)$
14		id	$⊢ φ \to φ$
15		oveq2	$⊢ k = M \to (M \dots k) = (M \dots M)$
16	15	sumeq1d	$⊢ k = M \to \sum_{n = M}^{k} O (A \cap F (n)) = \sum_{n = M}^{M} O (A \cap F (n))$
17		fveq2	$⊢ k = M \to G (k) = G (M)$
18	17	ineq2d	$⊢ k = M \to A \cap G (k) = A \cap G (M)$
19	18	fveq2d	$⊢ k = M \to O (A \cap G (k)) = O (A \cap G (M))$
20	16 19	eqeq12d	$⊢ k = M \to (\sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k)) \leftrightarrow \sum_{n = M}^{M} O (A \cap F (n)) = O (A \cap G (M)))$
21	20	imbi2d	$⊢ k = M \to ((φ \to \sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k))) \leftrightarrow (φ \to \sum_{n = M}^{M} O (A \cap F (n)) = O (A \cap G (M))))$
22		oveq2	$⊢ k = j \to (M \dots k) = (M \dots j)$
23	22	sumeq1d	$⊢ k = j \to \sum_{n = M}^{k} O (A \cap F (n)) = \sum_{n = M}^{j} O (A \cap F (n))$
24		fveq2	$⊢ k = j \to G (k) = G (j)$
25	24	ineq2d	$⊢ k = j \to A \cap G (k) = A \cap G (j)$
26	25	fveq2d	$⊢ k = j \to O (A \cap G (k)) = O (A \cap G (j))$
27	23 26	eqeq12d	$⊢ k = j \to (\sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k)) \leftrightarrow \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j)))$
28	27	imbi2d	$⊢ k = j \to ((φ \to \sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k))) \leftrightarrow (φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))))$
29		oveq2	$⊢ k = j + 1 \to (M \dots k) = (M \dots j + 1)$
30	29	sumeq1d	$⊢ k = j + 1 \to \sum_{n = M}^{k} O (A \cap F (n)) = \sum_{n = M}^{j + 1} O (A \cap F (n))$
31		fveq2	$⊢ k = j + 1 \to G (k) = G (j + 1)$
32	31	ineq2d	$⊢ k = j + 1 \to A \cap G (k) = A \cap G (j + 1)$
33	32	fveq2d	$⊢ k = j + 1 \to O (A \cap G (k)) = O (A \cap G (j + 1))$
34	30 33	eqeq12d	$⊢ k = j + 1 \to (\sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k)) \leftrightarrow \sum_{n = M}^{j + 1} O (A \cap F (n)) = O (A \cap G (j + 1)))$
35	34	imbi2d	$⊢ k = j + 1 \to ((φ \to \sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k))) \leftrightarrow (φ \to \sum_{n = M}^{j + 1} O (A \cap F (n)) = O (A \cap G (j + 1))))$
36		oveq2	$⊢ k = K \to (M \dots k) = (M \dots K)$
37	36	sumeq1d	$⊢ k = K \to \sum_{n = M}^{k} O (A \cap F (n)) = \sum_{n = M}^{K} O (A \cap F (n))$
38		fveq2	$⊢ k = K \to G (k) = G (K)$
39	38	ineq2d	$⊢ k = K \to A \cap G (k) = A \cap G (K)$
40	39	fveq2d	$⊢ k = K \to O (A \cap G (k)) = O (A \cap G (K))$
41	37 40	eqeq12d	$⊢ k = K \to (\sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k)) \leftrightarrow \sum_{n = M}^{K} O (A \cap F (n)) = O (A \cap G (K)))$
42	41	imbi2d	$⊢ k = K \to ((φ \to \sum_{n = M}^{k} O (A \cap F (n)) = O (A \cap G (k))) \leftrightarrow (φ \to \sum_{n = M}^{K} O (A \cap F (n)) = O (A \cap G (K))))$
43		eluzel2	$⊢ K \in ℤ_{\geq M} \to M \in ℤ$
44	11 43	syl	$⊢ φ \to M \in ℤ$
45		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
46	44 45	syl	$⊢ φ \to (M \dots M) = \{M\}$
47	46	sumeq1d	$⊢ φ \to \sum_{n = M}^{M} O (A \cap F (n)) = \sum_{n \in \{M\}} O (A \cap F (n))$
48		inss1	$⊢ A \cap F (M) \subseteq A$
49	48	a1i	$⊢ φ \to A \cap F (M) \subseteq A$
50	1 3 4 5 49	omessre	$⊢ φ \to O (A \cap F (M)) \in ℝ$
51	50	recnd	$⊢ φ \to O (A \cap F (M)) \in ℂ$
52		fveq2	$⊢ n = M \to F (n) = F (M)$
53	52	ineq2d	$⊢ n = M \to A \cap F (n) = A \cap F (M)$
54	53	fveq2d	$⊢ n = M \to O (A \cap F (n)) = O (A \cap F (M))$
55	54	sumsn	$⊢ (M \in ℤ \land O (A \cap F (M)) \in ℂ) \to \sum_{n \in \{M\}} O (A \cap F (n)) = O (A \cap F (M))$
56	44 51 55	syl2anc	$⊢ φ \to \sum_{n \in \{M\}} O (A \cap F (n)) = O (A \cap F (M))$
57		eqidd	$⊢ φ \to O (A \cap E (M)) = O (A \cap E (M))$
58		fveq2	$⊢ n = M \to E (n) = E (M)$
59		oveq2	$⊢ n = M \to (M ..^n) = (M ..^M)$
60	59	iuneq1d	$⊢ n = M \to ⋃_{i \in (M ..^n)} E (i) = ⋃_{i \in (M ..^M)} E (i)$
61	58 60	difeq12d	$⊢ n = M \to E (n) ∖ ⋃_{i \in (M ..^n)} E (i) = E (M) ∖ ⋃_{i \in (M ..^M)} E (i)$
62		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
63	44 62	syl	$⊢ φ \to M \in ℤ_{\geq M}$
64	6	a1i	$⊢ φ \to Z = ℤ_{\geq M}$
65	64	eqcomd	$⊢ φ \to ℤ_{\geq M} = Z$
66	63 65	eleqtrd	$⊢ φ \to M \in Z$
67		fvex	$⊢ E (M) \in V$
68		difexg	$⊢ E (M) \in V \to E (M) ∖ ⋃_{i \in (M ..^M)} E (i) \in V$
69	67 68	ax-mp	$⊢ E (M) ∖ ⋃_{i \in (M ..^M)} E (i) \in V$
70	69	a1i	$⊢ φ \to E (M) ∖ ⋃_{i \in (M ..^M)} E (i) \in V$
71	9 61 66 70	fvmptd3	$⊢ φ \to F (M) = E (M) ∖ ⋃_{i \in (M ..^M)} E (i)$
72		fzo0	$⊢ (M ..^M) = \emptyset$
73		iuneq1	$⊢ (M ..^M) = \emptyset \to ⋃_{i \in (M ..^M)} E (i) = ⋃_{i \in \emptyset} E (i)$
74	72 73	ax-mp	$⊢ ⋃_{i \in (M ..^M)} E (i) = ⋃_{i \in \emptyset} E (i)$
75		0iun	$⊢ ⋃_{i \in \emptyset} E (i) = \emptyset$
76	74 75	eqtri	$⊢ ⋃_{i \in (M ..^M)} E (i) = \emptyset$
77	76	difeq2i	$⊢ E (M) ∖ ⋃_{i \in (M ..^M)} E (i) = E (M) ∖ \emptyset$
78	77	a1i	$⊢ φ \to E (M) ∖ ⋃_{i \in (M ..^M)} E (i) = E (M) ∖ \emptyset$
79		dif0	$⊢ E (M) ∖ \emptyset = E (M)$
80	79	a1i	$⊢ φ \to E (M) ∖ \emptyset = E (M)$
81	71 78 80	3eqtrd	$⊢ φ \to F (M) = E (M)$
82	81	ineq2d	$⊢ φ \to A \cap F (M) = A \cap E (M)$
83	82	fveq2d	$⊢ φ \to O (A \cap F (M)) = O (A \cap E (M))$
84		oveq2	$⊢ n = M \to (M \dots n) = (M \dots M)$
85	84	iuneq1d	$⊢ n = M \to ⋃_{i = M}^{n} E (i) = ⋃_{i = M}^{M} E (i)$
86		ovex	$⊢ (M \dots M) \in V$
87		fvex	$⊢ E (i) \in V$
88	86 87	iunex	$⊢ ⋃_{i = M}^{M} E (i) \in V$
89	88	a1i	$⊢ φ \to ⋃_{i = M}^{M} E (i) \in V$
90	8 85 66 89	fvmptd3	$⊢ φ \to G (M) = ⋃_{i = M}^{M} E (i)$
91	46	iuneq1d	$⊢ φ \to ⋃_{i = M}^{M} E (i) = ⋃_{i \in \{M\}} E (i)$
92		fveq2	$⊢ i = M \to E (i) = E (M)$
93	92	iunxsng	$⊢ M \in ℤ \to ⋃_{i \in \{M\}} E (i) = E (M)$
94	44 93	syl	$⊢ φ \to ⋃_{i \in \{M\}} E (i) = E (M)$
95	90 91 94	3eqtrd	$⊢ φ \to G (M) = E (M)$
96	95	ineq2d	$⊢ φ \to A \cap G (M) = A \cap E (M)$
97	96	fveq2d	$⊢ φ \to O (A \cap G (M)) = O (A \cap E (M))$
98	57 83 97	3eqtr4d	$⊢ φ \to O (A \cap F (M)) = O (A \cap G (M))$
99	47 56 98	3eqtrd	$⊢ φ \to \sum_{n = M}^{M} O (A \cap F (n)) = O (A \cap G (M))$
100	99	a1i	$⊢ K \in ℤ_{\geq M} \to (φ \to \sum_{n = M}^{M} O (A \cap F (n)) = O (A \cap G (M)))$
101		simp3	$⊢ (j \in (M ..^K) \land (φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \land φ) \to φ$
102		simp1	$⊢ (j \in (M ..^K) \land (φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \land φ) \to j \in (M ..^K)$
103		id	$⊢ (φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \to (φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j)))$
104	103	imp	$⊢ ((φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \land φ) \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))$
105	104	3adant1	$⊢ (j \in (M ..^K) \land (φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \land φ) \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))$
106		elfzouz	$⊢ j \in (M ..^K) \to j \in ℤ_{\geq M}$
107	106	adantl	$⊢ (φ \land j \in (M ..^K)) \to j \in ℤ_{\geq M}$
108	1	adantr	$⊢ (φ \land n \in (M \dots j + 1)) \to O \in OutMeas$
109	4	adantr	$⊢ (φ \land n \in (M \dots j + 1)) \to A \subseteq X$
110	5	adantr	$⊢ (φ \land n \in (M \dots j + 1)) \to O (A) \in ℝ$
111		inss1	$⊢ A \cap F (n) \subseteq A$
112	111	a1i	$⊢ (φ \land n \in (M \dots j + 1)) \to A \cap F (n) \subseteq A$
113	108 3 109 110 112	omessre	$⊢ (φ \land n \in (M \dots j + 1)) \to O (A \cap F (n)) \in ℝ$
114	113	recnd	$⊢ (φ \land n \in (M \dots j + 1)) \to O (A \cap F (n)) \in ℂ$
115	114	adantlr	$⊢ ((φ \land j \in (M ..^K)) \land n \in (M \dots j + 1)) \to O (A \cap F (n)) \in ℂ$
116		fveq2	$⊢ n = j + 1 \to F (n) = F (j + 1)$
117	116	ineq2d	$⊢ n = j + 1 \to A \cap F (n) = A \cap F (j + 1)$
118	117	fveq2d	$⊢ n = j + 1 \to O (A \cap F (n)) = O (A \cap F (j + 1))$
119	107 115 118	fsump1	$⊢ (φ \land j \in (M ..^K)) \to \sum_{n = M}^{j + 1} O (A \cap F (n)) = \sum_{n = M}^{j} O (A \cap F (n)) + O (A \cap F (j + 1))$
120	119	3adant3	$⊢ (φ \land j \in (M ..^K) \land \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \to \sum_{n = M}^{j + 1} O (A \cap F (n)) = \sum_{n = M}^{j} O (A \cap F (n)) + O (A \cap F (j + 1))$
121		oveq1	$⊢ \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j)) \to \sum_{n = M}^{j} O (A \cap F (n)) + O (A \cap F (j + 1)) = O (A \cap G (j)) + O (A \cap F (j + 1))$
122	121	3ad2ant3	$⊢ (φ \land j \in (M ..^K) \land \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \to \sum_{n = M}^{j} O (A \cap F (n)) + O (A \cap F (j + 1)) = O (A \cap G (j)) + O (A \cap F (j + 1))$
123		fzssp1	$⊢ (M \dots j) \subseteq (M \dots j + 1)$
124		iunss1	$⊢ (M \dots j) \subseteq (M \dots j + 1) \to ⋃_{i = M}^{j} E (i) \subseteq ⋃_{i = M}^{j + 1} E (i)$
125	123 124	ax-mp	$⊢ ⋃_{i = M}^{j} E (i) \subseteq ⋃_{i = M}^{j + 1} E (i)$
126	125	a1i	$⊢ j \in (M ..^K) \to ⋃_{i = M}^{j} E (i) \subseteq ⋃_{i = M}^{j + 1} E (i)$
127		oveq2	$⊢ n = j \to (M \dots n) = (M \dots j)$
128	127	iuneq1d	$⊢ n = j \to ⋃_{i = M}^{n} E (i) = ⋃_{i = M}^{j} E (i)$
129	106 6	eleqtrrdi	$⊢ j \in (M ..^K) \to j \in Z$
130		ovex	$⊢ (M \dots j) \in V$
131	130 87	iunex	$⊢ ⋃_{i = M}^{j} E (i) \in V$
132	131	a1i	$⊢ j \in (M ..^K) \to ⋃_{i = M}^{j} E (i) \in V$
133	8 128 129 132	fvmptd3	$⊢ j \in (M ..^K) \to G (j) = ⋃_{i = M}^{j} E (i)$
134		oveq2	$⊢ n = j + 1 \to (M \dots n) = (M \dots j + 1)$
135	134	iuneq1d	$⊢ n = j + 1 \to ⋃_{i = M}^{n} E (i) = ⋃_{i = M}^{j + 1} E (i)$
136		peano2uz	$⊢ j \in ℤ_{\geq M} \to j + 1 \in ℤ_{\geq M}$
137	106 136	syl	$⊢ j \in (M ..^K) \to j + 1 \in ℤ_{\geq M}$
138	6	eqcomi	$⊢ ℤ_{\geq M} = Z$
139	137 138	eleqtrdi	$⊢ j \in (M ..^K) \to j + 1 \in Z$
140		ovex	$⊢ (M \dots j + 1) \in V$
141	140 87	iunex	$⊢ ⋃_{i = M}^{j + 1} E (i) \in V$
142	141	a1i	$⊢ j \in (M ..^K) \to ⋃_{i = M}^{j + 1} E (i) \in V$
143	8 135 139 142	fvmptd3	$⊢ j \in (M ..^K) \to G (j + 1) = ⋃_{i = M}^{j + 1} E (i)$
144	133 143	sseq12d	$⊢ j \in (M ..^K) \to (G (j) \subseteq G (j + 1) \leftrightarrow ⋃_{i = M}^{j} E (i) \subseteq ⋃_{i = M}^{j + 1} E (i))$
145	126 144	mpbird	$⊢ j \in (M ..^K) \to G (j) \subseteq G (j + 1)$
146		inabs3	$⊢ G (j) \subseteq G (j + 1) \to (A \cap G (j + 1)) \cap G (j) = A \cap G (j)$
147	145 146	syl	$⊢ j \in (M ..^K) \to (A \cap G (j + 1)) \cap G (j) = A \cap G (j)$
148	147	fveq2d	$⊢ j \in (M ..^K) \to O ((A \cap G (j + 1)) \cap G (j)) = O (A \cap G (j))$
149	148	eqcomd	$⊢ j \in (M ..^K) \to O (A \cap G (j)) = O ((A \cap G (j + 1)) \cap G (j))$
150	149	adantl	$⊢ (φ \land j \in (M ..^K)) \to O (A \cap G (j)) = O ((A \cap G (j + 1)) \cap G (j))$
151		elfzoelz	$⊢ j \in (M ..^K) \to j \in ℤ$
152		fzval3	$⊢ j \in ℤ \to (M \dots j) = (M ..^j + 1)$
153	151 152	syl	$⊢ j \in (M ..^K) \to (M \dots j) = (M ..^j + 1)$
154	153	eqcomd	$⊢ j \in (M ..^K) \to (M ..^j + 1) = (M \dots j)$
155	154	iuneq1d	$⊢ j \in (M ..^K) \to ⋃_{i \in (M ..^j + 1)} E (i) = ⋃_{i = M}^{j} E (i)$
156	155	difeq2d	$⊢ j \in (M ..^K) \to E (j + 1) ∖ ⋃_{i \in (M ..^j + 1)} E (i) = E (j + 1) ∖ ⋃_{i = M}^{j} E (i)$
157	156	adantl	$⊢ (φ \land j \in (M ..^K)) \to E (j + 1) ∖ ⋃_{i \in (M ..^j + 1)} E (i) = E (j + 1) ∖ ⋃_{i = M}^{j} E (i)$
158		fveq2	$⊢ n = j + 1 \to E (n) = E (j + 1)$
159		oveq2	$⊢ n = j + 1 \to (M ..^n) = (M ..^j + 1)$
160	159	iuneq1d	$⊢ n = j + 1 \to ⋃_{i \in (M ..^n)} E (i) = ⋃_{i \in (M ..^j + 1)} E (i)$
161	158 160	difeq12d	$⊢ n = j + 1 \to E (n) ∖ ⋃_{i \in (M ..^n)} E (i) = E (j + 1) ∖ ⋃_{i \in (M ..^j + 1)} E (i)$
162		fvex	$⊢ E (j + 1) \in V$
163		difexg	$⊢ E (j + 1) \in V \to E (j + 1) ∖ ⋃_{i \in (M ..^j + 1)} E (i) \in V$
164	162 163	ax-mp	$⊢ E (j + 1) ∖ ⋃_{i \in (M ..^j + 1)} E (i) \in V$
165	164	a1i	$⊢ j \in (M ..^K) \to E (j + 1) ∖ ⋃_{i \in (M ..^j + 1)} E (i) \in V$
166	9 161 139 165	fvmptd3	$⊢ j \in (M ..^K) \to F (j + 1) = E (j + 1) ∖ ⋃_{i \in (M ..^j + 1)} E (i)$
167	166	adantl	$⊢ (φ \land j \in (M ..^K)) \to F (j + 1) = E (j + 1) ∖ ⋃_{i \in (M ..^j + 1)} E (i)$
168		nfcv	$⊢ \underline{Ⅎ} i E (j + 1)$
169		fveq2	$⊢ i = j + 1 \to E (i) = E (j + 1)$
170	168 106 169	iunp1	$⊢ j \in (M ..^K) \to ⋃_{i = M}^{j + 1} E (i) = ⋃_{i = M}^{j} E (i) \cup E (j + 1)$
171	143 170	eqtrd	$⊢ j \in (M ..^K) \to G (j + 1) = ⋃_{i = M}^{j} E (i) \cup E (j + 1)$
172	171 133	difeq12d	$⊢ j \in (M ..^K) \to G (j + 1) ∖ G (j) = (⋃_{i = M}^{j} E (i) \cup E (j + 1)) ∖ ⋃_{i = M}^{j} E (i)$
173		difundir	$⊢ (⋃_{i = M}^{j} E (i) \cup E (j + 1)) ∖ ⋃_{i = M}^{j} E (i) = (⋃_{i = M}^{j} E (i) ∖ ⋃_{i = M}^{j} E (i)) \cup (E (j + 1) ∖ ⋃_{i = M}^{j} E (i))$
174		difid	$⊢ ⋃_{i = M}^{j} E (i) ∖ ⋃_{i = M}^{j} E (i) = \emptyset$
175	174	uneq1i	$⊢ (⋃_{i = M}^{j} E (i) ∖ ⋃_{i = M}^{j} E (i)) \cup (E (j + 1) ∖ ⋃_{i = M}^{j} E (i)) = \emptyset \cup (E (j + 1) ∖ ⋃_{i = M}^{j} E (i))$
176		0un	$⊢ \emptyset \cup (E (j + 1) ∖ ⋃_{i = M}^{j} E (i)) = E (j + 1) ∖ ⋃_{i = M}^{j} E (i)$
177	173 175 176	3eqtri	$⊢ (⋃_{i = M}^{j} E (i) \cup E (j + 1)) ∖ ⋃_{i = M}^{j} E (i) = E (j + 1) ∖ ⋃_{i = M}^{j} E (i)$
178	177	a1i	$⊢ j \in (M ..^K) \to (⋃_{i = M}^{j} E (i) \cup E (j + 1)) ∖ ⋃_{i = M}^{j} E (i) = E (j + 1) ∖ ⋃_{i = M}^{j} E (i)$
179	172 178	eqtrd	$⊢ j \in (M ..^K) \to G (j + 1) ∖ G (j) = E (j + 1) ∖ ⋃_{i = M}^{j} E (i)$
180	179	adantl	$⊢ (φ \land j \in (M ..^K)) \to G (j + 1) ∖ G (j) = E (j + 1) ∖ ⋃_{i = M}^{j} E (i)$
181	157 167 180	3eqtr4d	$⊢ (φ \land j \in (M ..^K)) \to F (j + 1) = G (j + 1) ∖ G (j)$
182	181	ineq2d	$⊢ (φ \land j \in (M ..^K)) \to A \cap F (j + 1) = A \cap (G (j + 1) ∖ G (j))$
183		indif2	$⊢ A \cap (G (j + 1) ∖ G (j)) = (A \cap G (j + 1)) ∖ G (j)$
184	183	eqcomi	$⊢ (A \cap G (j + 1)) ∖ G (j) = A \cap (G (j + 1) ∖ G (j))$
185	184	a1i	$⊢ (φ \land j \in (M ..^K)) \to (A \cap G (j + 1)) ∖ G (j) = A \cap (G (j + 1) ∖ G (j))$
186	182 185	eqtr4d	$⊢ (φ \land j \in (M ..^K)) \to A \cap F (j + 1) = (A \cap G (j + 1)) ∖ G (j)$
187	186	fveq2d	$⊢ (φ \land j \in (M ..^K)) \to O (A \cap F (j + 1)) = O ((A \cap G (j + 1)) ∖ G (j))$
188	150 187	oveq12d	$⊢ (φ \land j \in (M ..^K)) \to O (A \cap G (j)) + O (A \cap F (j + 1)) = O ((A \cap G (j + 1)) \cap G (j)) + O ((A \cap G (j + 1)) ∖ G (j))$
189		inss1	$⊢ (A \cap G (j + 1)) \cap G (j) \subseteq A \cap G (j + 1)$
190		inss1	$⊢ A \cap G (j + 1) \subseteq A$
191	189 190	sstri	$⊢ (A \cap G (j + 1)) \cap G (j) \subseteq A$
192	191	a1i	$⊢ φ \to (A \cap G (j + 1)) \cap G (j) \subseteq A$
193	1 3 4 5 192	omessre	$⊢ φ \to O ((A \cap G (j + 1)) \cap G (j)) \in ℝ$
194	193	adantr	$⊢ (φ \land j \in (M ..^K)) \to O ((A \cap G (j + 1)) \cap G (j)) \in ℝ$
195	1	adantr	$⊢ (φ \land j \in (M ..^K)) \to O \in OutMeas$
196	4	adantr	$⊢ (φ \land j \in (M ..^K)) \to A \subseteq X$
197	5	adantr	$⊢ (φ \land j \in (M ..^K)) \to O (A) \in ℝ$
198		difss	$⊢ (A \cap G (j + 1)) ∖ G (j) \subseteq A \cap G (j + 1)$
199	198 190	sstri	$⊢ (A \cap G (j + 1)) ∖ G (j) \subseteq A$
200	199	a1i	$⊢ (φ \land j \in (M ..^K)) \to (A \cap G (j + 1)) ∖ G (j) \subseteq A$
201	195 3 196 197 200	omessre	$⊢ (φ \land j \in (M ..^K)) \to O ((A \cap G (j + 1)) ∖ G (j)) \in ℝ$
202		rexadd	$⊢ (O ((A \cap G (j + 1)) \cap G (j)) \in ℝ \land O ((A \cap G (j + 1)) ∖ G (j)) \in ℝ) \to O ((A \cap G (j + 1)) \cap G (j)) +_{𝑒} O ((A \cap G (j + 1)) ∖ G (j)) = O ((A \cap G (j + 1)) \cap G (j)) + O ((A \cap G (j + 1)) ∖ G (j))$
203	194 201 202	syl2anc	$⊢ (φ \land j \in (M ..^K)) \to O ((A \cap G (j + 1)) \cap G (j)) +_{𝑒} O ((A \cap G (j + 1)) ∖ G (j)) = O ((A \cap G (j + 1)) \cap G (j)) + O ((A \cap G (j + 1)) ∖ G (j))$
204	203	eqcomd	$⊢ (φ \land j \in (M ..^K)) \to O ((A \cap G (j + 1)) \cap G (j)) + O ((A \cap G (j + 1)) ∖ G (j)) = O ((A \cap G (j + 1)) \cap G (j)) +_{𝑒} O ((A \cap G (j + 1)) ∖ G (j))$
205	133	adantl	$⊢ (φ \land j \in (M ..^K)) \to G (j) = ⋃_{i = M}^{j} E (i)$
206		nfv	$⊢ Ⅎ i φ$
207		fzfid	$⊢ φ \to (M \dots j) \in Fin$
208	7	adantr	$⊢ (φ \land i \in (M \dots j)) \to E : Z ⟶ S$
209		elfzuz	$⊢ i \in (M \dots j) \to i \in ℤ_{\geq M}$
210	138	a1i	$⊢ i \in (M \dots j) \to ℤ_{\geq M} = Z$
211	209 210	eleqtrd	$⊢ i \in (M \dots j) \to i \in Z$
212	211	adantl	$⊢ (φ \land i \in (M \dots j)) \to i \in Z$
213	208 212	ffvelcdmd	$⊢ (φ \land i \in (M \dots j)) \to E (i) \in S$
214	206 1 2 207 213	caragenfiiuncl	$⊢ φ \to ⋃_{i = M}^{j} E (i) \in S$
215	214	adantr	$⊢ (φ \land j \in (M ..^K)) \to ⋃_{i = M}^{j} E (i) \in S$
216	205 215	eqeltrd	$⊢ (φ \land j \in (M ..^K)) \to G (j) \in S$
217	4	ssinss1d	$⊢ φ \to A \cap G (j + 1) \subseteq X$
218	217	adantr	$⊢ (φ \land j \in (M ..^K)) \to A \cap G (j + 1) \subseteq X$
219	195 2 3 216 218	caragensplit	$⊢ (φ \land j \in (M ..^K)) \to O ((A \cap G (j + 1)) \cap G (j)) +_{𝑒} O ((A \cap G (j + 1)) ∖ G (j)) = O (A \cap G (j + 1))$
220	188 204 219	3eqtrd	$⊢ (φ \land j \in (M ..^K)) \to O (A \cap G (j)) + O (A \cap F (j + 1)) = O (A \cap G (j + 1))$
221	220	3adant3	$⊢ (φ \land j \in (M ..^K) \land \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \to O (A \cap G (j)) + O (A \cap F (j + 1)) = O (A \cap G (j + 1))$
222	120 122 221	3eqtrd	$⊢ (φ \land j \in (M ..^K) \land \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \to \sum_{n = M}^{j + 1} O (A \cap F (n)) = O (A \cap G (j + 1))$
223	101 102 105 222	syl3anc	$⊢ (j \in (M ..^K) \land (φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \land φ) \to \sum_{n = M}^{j + 1} O (A \cap F (n)) = O (A \cap G (j + 1))$
224	223	3exp	$⊢ j \in (M ..^K) \to ((φ \to \sum_{n = M}^{j} O (A \cap F (n)) = O (A \cap G (j))) \to (φ \to \sum_{n = M}^{j + 1} O (A \cap F (n)) = O (A \cap G (j + 1))))$
225	21 28 35 42 100 224	fzind2	$⊢ K \in (M \dots K) \to (φ \to \sum_{n = M}^{K} O (A \cap F (n)) = O (A \cap G (K)))$
226	13 14 225	sylc	$⊢ φ \to \sum_{n = M}^{K} O (A \cap F (n)) = O (A \cap G (K))$

Metamath Proof Explorer

Theorem carageniuncllem1

Proof