caratheodorylem1

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)

	Ref	Expression
Hypotheses	caratheodorylem1.o	$⊢ φ \to O \in OutMeas$
	caratheodorylem1.s	$⊢ S = CaraGen (O)$
	caratheodorylem1.z	$⊢ Z = ℤ_{\geq M}$
	caratheodorylem1.e	$⊢ φ \to E : Z ⟶ S$
	caratheodorylem1.dj	$⊢ φ \to \underset{n \in Z}{Disj} E (n)$
	caratheodorylem1.g	$⊢ G = (n \in Z ⟼ ⋃_{i = M}^{n} E (i))$
	caratheodorylem1.n	$⊢ φ \to N \in ℤ_{\geq M}$
Assertion	caratheodorylem1	$⊢ φ \to O (G (N)) = sum^((n \in (M \dots N) ⟼ O (E (n))))$

Proof

Step	Hyp	Ref	Expression
1		caratheodorylem1.o	$⊢ φ \to O \in OutMeas$
2		caratheodorylem1.s	$⊢ S = CaraGen (O)$
3		caratheodorylem1.z	$⊢ Z = ℤ_{\geq M}$
4		caratheodorylem1.e	$⊢ φ \to E : Z ⟶ S$
5		caratheodorylem1.dj	$⊢ φ \to \underset{n \in Z}{Disj} E (n)$
6		caratheodorylem1.g	$⊢ G = (n \in Z ⟼ ⋃_{i = M}^{n} E (i))$
7		caratheodorylem1.n	$⊢ φ \to N \in ℤ_{\geq M}$
8		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
9	7 8	syl	$⊢ φ \to N \in (M \dots N)$
10		id	$⊢ φ \to φ$
11		2fveq3	$⊢ j = M \to O (G (j)) = O (G (M))$
12		oveq2	$⊢ j = M \to (M \dots j) = (M \dots M)$
13	12	mpteq1d	$⊢ j = M \to (n \in (M \dots j) ⟼ O (E (n))) = (n \in (M \dots M) ⟼ O (E (n)))$
14	13	fveq2d	$⊢ j = M \to sum^((n \in (M \dots j) ⟼ O (E (n)))) = sum^((n \in (M \dots M) ⟼ O (E (n))))$
15	11 14	eqeq12d	$⊢ j = M \to (O (G (j)) = sum^((n \in (M \dots j) ⟼ O (E (n)))) \leftrightarrow O (G (M)) = sum^((n \in (M \dots M) ⟼ O (E (n)))))$
16	15	imbi2d	$⊢ j = M \to ((φ \to O (G (j)) = sum^((n \in (M \dots j) ⟼ O (E (n))))) \leftrightarrow (φ \to O (G (M)) = sum^((n \in (M \dots M) ⟼ O (E (n))))))$
17		2fveq3	$⊢ j = i \to O (G (j)) = O (G (i))$
18		oveq2	$⊢ j = i \to (M \dots j) = (M \dots i)$
19	18	mpteq1d	$⊢ j = i \to (n \in (M \dots j) ⟼ O (E (n))) = (n \in (M \dots i) ⟼ O (E (n)))$
20	19	fveq2d	$⊢ j = i \to sum^((n \in (M \dots j) ⟼ O (E (n)))) = sum^((n \in (M \dots i) ⟼ O (E (n))))$
21	17 20	eqeq12d	$⊢ j = i \to (O (G (j)) = sum^((n \in (M \dots j) ⟼ O (E (n)))) \leftrightarrow O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n)))))$
22	21	imbi2d	$⊢ j = i \to ((φ \to O (G (j)) = sum^((n \in (M \dots j) ⟼ O (E (n))))) \leftrightarrow (φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))))$
23		2fveq3	$⊢ j = i + 1 \to O (G (j)) = O (G (i + 1))$
24		oveq2	$⊢ j = i + 1 \to (M \dots j) = (M \dots i + 1)$
25	24	mpteq1d	$⊢ j = i + 1 \to (n \in (M \dots j) ⟼ O (E (n))) = (n \in (M \dots i + 1) ⟼ O (E (n)))$
26	25	fveq2d	$⊢ j = i + 1 \to sum^((n \in (M \dots j) ⟼ O (E (n)))) = sum^((n \in (M \dots i + 1) ⟼ O (E (n))))$
27	23 26	eqeq12d	$⊢ j = i + 1 \to (O (G (j)) = sum^((n \in (M \dots j) ⟼ O (E (n)))) \leftrightarrow O (G (i + 1)) = sum^((n \in (M \dots i + 1) ⟼ O (E (n)))))$
28	27	imbi2d	$⊢ j = i + 1 \to ((φ \to O (G (j)) = sum^((n \in (M \dots j) ⟼ O (E (n))))) \leftrightarrow (φ \to O (G (i + 1)) = sum^((n \in (M \dots i + 1) ⟼ O (E (n))))))$
29		2fveq3	$⊢ j = N \to O (G (j)) = O (G (N))$
30		oveq2	$⊢ j = N \to (M \dots j) = (M \dots N)$
31	30	mpteq1d	$⊢ j = N \to (n \in (M \dots j) ⟼ O (E (n))) = (n \in (M \dots N) ⟼ O (E (n)))$
32	31	fveq2d	$⊢ j = N \to sum^((n \in (M \dots j) ⟼ O (E (n)))) = sum^((n \in (M \dots N) ⟼ O (E (n))))$
33	29 32	eqeq12d	$⊢ j = N \to (O (G (j)) = sum^((n \in (M \dots j) ⟼ O (E (n)))) \leftrightarrow O (G (N)) = sum^((n \in (M \dots N) ⟼ O (E (n)))))$
34	33	imbi2d	$⊢ j = N \to ((φ \to O (G (j)) = sum^((n \in (M \dots j) ⟼ O (E (n))))) \leftrightarrow (φ \to O (G (N)) = sum^((n \in (M \dots N) ⟼ O (E (n))))))$
35		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
36	7 35	syl	$⊢ φ \to M \in ℤ$
37		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
38	36 37	syl	$⊢ φ \to (M \dots M) = \{M\}$
39	38	mpteq1d	$⊢ φ \to (n \in (M \dots M) ⟼ O (E (n))) = (n \in \{M\} ⟼ O (E (n)))$
40	39	fveq2d	$⊢ φ \to sum^((n \in (M \dots M) ⟼ O (E (n)))) = sum^((n \in \{M\} ⟼ O (E (n))))$
41	1	adantr	$⊢ (φ \land n \in \{M\}) \to O \in OutMeas$
42		eqid	$⊢ ⋃ dom O = ⋃ dom O$
43	2	caragenss	$⊢ O \in OutMeas \to S \subseteq dom O$
44	41 43	syl	$⊢ (φ \land n \in \{M\}) \to S \subseteq dom O$
45	4	adantr	$⊢ (φ \land n \in \{M\}) \to E : Z ⟶ S$
46		elsni	$⊢ n \in \{M\} \to n = M$
47	46	adantl	$⊢ (φ \land n \in \{M\}) \to n = M$
48		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
49	36 48	syl	$⊢ φ \to M \in ℤ_{\geq M}$
50	49 3	eleqtrrdi	$⊢ φ \to M \in Z$
51	50	adantr	$⊢ (φ \land n \in \{M\}) \to M \in Z$
52	47 51	eqeltrd	$⊢ (φ \land n \in \{M\}) \to n \in Z$
53	45 52	ffvelrnd	$⊢ (φ \land n \in \{M\}) \to E (n) \in S$
54	44 53	sseldd	$⊢ (φ \land n \in \{M\}) \to E (n) \in dom O$
55		elssuni	$⊢ E (n) \in dom O \to E (n) \subseteq ⋃ dom O$
56	54 55	syl	$⊢ (φ \land n \in \{M\}) \to E (n) \subseteq ⋃ dom O$
57	41 42 56	omecl	$⊢ (φ \land n \in \{M\}) \to O (E (n)) \in [0, +∞]$
58		eqid	$⊢ (n \in \{M\} ⟼ O (E (n))) = (n \in \{M\} ⟼ O (E (n)))$
59	57 58	fmptd	$⊢ φ \to (n \in \{M\} ⟼ O (E (n))) : \{M\} ⟶ [0, +∞]$
60	36 59	sge0sn	$⊢ φ \to sum^((n \in \{M\} ⟼ O (E (n)))) = (n \in \{M\} ⟼ O (E (n))) (M)$
61		eqidd	$⊢ φ \to (n \in \{M\} ⟼ O (E (n))) = (n \in \{M\} ⟼ O (E (n)))$
62	38	iuneq1d	$⊢ φ \to ⋃_{i = M}^{M} E (i) = ⋃_{i \in \{M\}} E (i)$
63		fveq2	$⊢ i = M \to E (i) = E (M)$
64	63	iunxsng	$⊢ M \in Z \to ⋃_{i \in \{M\}} E (i) = E (M)$
65	50 64	syl	$⊢ φ \to ⋃_{i \in \{M\}} E (i) = E (M)$
66		eqidd	$⊢ φ \to E (M) = E (M)$
67	62 65 66	3eqtrrd	$⊢ φ \to E (M) = ⋃_{i = M}^{M} E (i)$
68	67	adantr	$⊢ (φ \land n = M) \to E (M) = ⋃_{i = M}^{M} E (i)$
69		fveq2	$⊢ n = M \to E (n) = E (M)$
70	69	adantl	$⊢ (φ \land n = M) \to E (n) = E (M)$
71		oveq2	$⊢ n = M \to (M \dots n) = (M \dots M)$
72	71	iuneq1d	$⊢ n = M \to ⋃_{i = M}^{n} E (i) = ⋃_{i = M}^{M} E (i)$
73		ovex	$⊢ (M \dots M) \in V$
74		fvex	$⊢ E (i) \in V$
75	73 74	iunex	$⊢ ⋃_{i = M}^{M} E (i) \in V$
76	75	a1i	$⊢ φ \to ⋃_{i = M}^{M} E (i) \in V$
77	6 72 50 76	fvmptd3	$⊢ φ \to G (M) = ⋃_{i = M}^{M} E (i)$
78	77	adantr	$⊢ (φ \land n = M) \to G (M) = ⋃_{i = M}^{M} E (i)$
79	68 70 78	3eqtr4d	$⊢ (φ \land n = M) \to E (n) = G (M)$
80	79	fveq2d	$⊢ (φ \land n = M) \to O (E (n)) = O (G (M))$
81		snidg	$⊢ M \in Z \to M \in \{M\}$
82	50 81	syl	$⊢ φ \to M \in \{M\}$
83		fvexd	$⊢ φ \to O (G (M)) \in V$
84	61 80 82 83	fvmptd	$⊢ φ \to (n \in \{M\} ⟼ O (E (n))) (M) = O (G (M))$
85	40 60 84	3eqtrrd	$⊢ φ \to O (G (M)) = sum^((n \in (M \dots M) ⟼ O (E (n))))$
86	85	a1i	$⊢ N \in ℤ_{\geq M} \to (φ \to O (G (M)) = sum^((n \in (M \dots M) ⟼ O (E (n)))))$
87		simp3	$⊢ (i \in (M ..^N) \land (φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \land φ) \to φ$
88		simp1	$⊢ (i \in (M ..^N) \land (φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \land φ) \to i \in (M ..^N)$
89		id	$⊢ (φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to (φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n)))))$
90	89	imp	$⊢ ((φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \land φ) \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))$
91	90	3adant1	$⊢ (i \in (M ..^N) \land (φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \land φ) \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))$
92		elfzoel1	$⊢ i \in (M ..^N) \to M \in ℤ$
93		elfzoelz	$⊢ i \in (M ..^N) \to i \in ℤ$
94	93	peano2zd	$⊢ i \in (M ..^N) \to i + 1 \in ℤ$
95	92 94 94	3jca	$⊢ i \in (M ..^N) \to (M \in ℤ \land i + 1 \in ℤ \land i + 1 \in ℤ)$
96	92	zred	$⊢ i \in (M ..^N) \to M \in ℝ$
97	94	zred	$⊢ i \in (M ..^N) \to i + 1 \in ℝ$
98	93	zred	$⊢ i \in (M ..^N) \to i \in ℝ$
99		elfzole1	$⊢ i \in (M ..^N) \to M \leq i$
100	98	ltp1d	$⊢ i \in (M ..^N) \to i < i + 1$
101	96 98 97 99 100	lelttrd	$⊢ i \in (M ..^N) \to M < i + 1$
102	96 97 101	ltled	$⊢ i \in (M ..^N) \to M \leq i + 1$
103		leid	$⊢ i + 1 \in ℝ \to i + 1 \leq i + 1$
104	97 103	syl	$⊢ i \in (M ..^N) \to i + 1 \leq i + 1$
105	95 102 104	jca32	$⊢ i \in (M ..^N) \to ((M \in ℤ \land i + 1 \in ℤ \land i + 1 \in ℤ) \land (M \leq i + 1 \land i + 1 \leq i + 1))$
106		elfz2	$⊢ i + 1 \in (M \dots i + 1) \leftrightarrow ((M \in ℤ \land i + 1 \in ℤ \land i + 1 \in ℤ) \land (M \leq i + 1 \land i + 1 \leq i + 1))$
107	105 106	sylibr	$⊢ i \in (M ..^N) \to i + 1 \in (M \dots i + 1)$
108	107	adantl	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in (M \dots i + 1)$
109		fveq2	$⊢ j = i + 1 \to E (j) = E (i + 1)$
110	109	ssiun2s	$⊢ i + 1 \in (M \dots i + 1) \to E (i + 1) \subseteq ⋃_{j = M}^{i + 1} E (j)$
111	108 110	syl	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) \subseteq ⋃_{j = M}^{i + 1} E (j)$
112		fveq2	$⊢ i = j \to E (i) = E (j)$
113	112	cbviunv	$⊢ ⋃_{i = M}^{n} E (i) = ⋃_{j = M}^{n} E (j)$
114	113	mpteq2i	$⊢ (n \in Z ⟼ ⋃_{i = M}^{n} E (i)) = (n \in Z ⟼ ⋃_{j = M}^{n} E (j))$
115	6 114	eqtri	$⊢ G = (n \in Z ⟼ ⋃_{j = M}^{n} E (j))$
116		oveq2	$⊢ n = i + 1 \to (M \dots n) = (M \dots i + 1)$
117	116	iuneq1d	$⊢ n = i + 1 \to ⋃_{j = M}^{n} E (j) = ⋃_{j = M}^{i + 1} E (j)$
118	36	adantr	$⊢ (φ \land i \in (M ..^N)) \to M \in ℤ$
119	93	adantl	$⊢ (φ \land i \in (M ..^N)) \to i \in ℤ$
120	119	peano2zd	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in ℤ$
121	118	zred	$⊢ (φ \land i \in (M ..^N)) \to M \in ℝ$
122	120	zred	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in ℝ$
123	119	zred	$⊢ (φ \land i \in (M ..^N)) \to i \in ℝ$
124	99	adantl	$⊢ (φ \land i \in (M ..^N)) \to M \leq i$
125	123	ltp1d	$⊢ (φ \land i \in (M ..^N)) \to i < i + 1$
126	121 123 122 124 125	lelttrd	$⊢ (φ \land i \in (M ..^N)) \to M < i + 1$
127	121 122 126	ltled	$⊢ (φ \land i \in (M ..^N)) \to M \leq i + 1$
128	118 120 127	3jca	$⊢ (φ \land i \in (M ..^N)) \to (M \in ℤ \land i + 1 \in ℤ \land M \leq i + 1)$
129		eluz2	$⊢ i + 1 \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land i + 1 \in ℤ \land M \leq i + 1)$
130	128 129	sylibr	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in ℤ_{\geq M}$
131	3	eqcomi	$⊢ ℤ_{\geq M} = Z$
132	130 131	eleqtrdi	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in Z$
133		ovex	$⊢ (M \dots i + 1) \in V$
134		fvex	$⊢ E (j) \in V$
135	133 134	iunex	$⊢ ⋃_{j = M}^{i + 1} E (j) \in V$
136	135	a1i	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i + 1} E (j) \in V$
137	115 117 132 136	fvmptd3	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) = ⋃_{j = M}^{i + 1} E (j)$
138	137	eqcomd	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i + 1} E (j) = G (i + 1)$
139	111 138	sseqtrd	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) \subseteq G (i + 1)$
140		sseqin2	$⊢ E (i + 1) \subseteq G (i + 1) \leftrightarrow G (i + 1) \cap E (i + 1) = E (i + 1)$
141	140	biimpi	$⊢ E (i + 1) \subseteq G (i + 1) \to G (i + 1) \cap E (i + 1) = E (i + 1)$
142	139 141	syl	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) \cap E (i + 1) = E (i + 1)$
143	142	fveq2d	$⊢ (φ \land i \in (M ..^N)) \to O (G (i + 1) \cap E (i + 1)) = O (E (i + 1))$
144		nfcv	$⊢ \underline{Ⅎ} j E (i + 1)$
145		elfzouz	$⊢ i \in (M ..^N) \to i \in ℤ_{\geq M}$
146	145	adantl	$⊢ (φ \land i \in (M ..^N)) \to i \in ℤ_{\geq M}$
147	144 146 109	iunp1	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i + 1} E (j) = ⋃_{j = M}^{i} E (j) \cup E (i + 1)$
148	137 147	eqtrd	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) = ⋃_{j = M}^{i} E (j) \cup E (i + 1)$
149	148	difeq1d	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) ∖ E (i + 1) = (⋃_{j = M}^{i} E (j) \cup E (i + 1)) ∖ E (i + 1)$
150		fveq2	$⊢ n = j \to E (n) = E (j)$
151	150	cbvdisjv	$⊢ \underset{n \in Z}{Disj} E (n) \leftrightarrow \underset{j \in Z}{Disj} E (j)$
152	5 151	sylib	$⊢ φ \to \underset{j \in Z}{Disj} E (j)$
153	152	adantr	$⊢ (φ \land i \in (M ..^N)) \to \underset{j \in Z}{Disj} E (j)$
154		fzssuz	$⊢ (M \dots i) \subseteq ℤ_{\geq M}$
155	154 131	sseqtri	$⊢ (M \dots i) \subseteq Z$
156	155	a1i	$⊢ (φ \land i \in (M ..^N)) \to (M \dots i) \subseteq Z$
157		fzp1nel	$⊢ \neg i + 1 \in (M \dots i)$
158	157	a1i	$⊢ i \in (M ..^N) \to \neg i + 1 \in (M \dots i)$
159	158	adantl	$⊢ (φ \land i \in (M ..^N)) \to \neg i + 1 \in (M \dots i)$
160	132 159	eldifd	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in (Z ∖ (M \dots i))$
161	153 156 160 109	disjiun2	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) \cap E (i + 1) = \emptyset$
162		undif4	$⊢ ⋃_{j = M}^{i} E (j) \cap E (i + 1) = \emptyset \to ⋃_{j = M}^{i} E (j) \cup (E (i + 1) ∖ E (i + 1)) = (⋃_{j = M}^{i} E (j) \cup E (i + 1)) ∖ E (i + 1)$
163	161 162	syl	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) \cup (E (i + 1) ∖ E (i + 1)) = (⋃_{j = M}^{i} E (j) \cup E (i + 1)) ∖ E (i + 1)$
164	163	eqcomd	$⊢ (φ \land i \in (M ..^N)) \to (⋃_{j = M}^{i} E (j) \cup E (i + 1)) ∖ E (i + 1) = ⋃_{j = M}^{i} E (j) \cup (E (i + 1) ∖ E (i + 1))$
165		simpl	$⊢ (φ \land i \in (M ..^N)) \to φ$
166	146 131	eleqtrdi	$⊢ (φ \land i \in (M ..^N)) \to i \in Z$
167	115	a1i	$⊢ (φ \land i \in Z) \to G = (n \in Z ⟼ ⋃_{j = M}^{n} E (j))$
168		simpr	$⊢ ((φ \land i \in Z) \land n = i) \to n = i$
169	168	oveq2d	$⊢ ((φ \land i \in Z) \land n = i) \to (M \dots n) = (M \dots i)$
170	169	iuneq1d	$⊢ ((φ \land i \in Z) \land n = i) \to ⋃_{j = M}^{n} E (j) = ⋃_{j = M}^{i} E (j)$
171		simpr	$⊢ (φ \land i \in Z) \to i \in Z$
172		ovex	$⊢ (M \dots i) \in V$
173	172 134	iunex	$⊢ ⋃_{j = M}^{i} E (j) \in V$
174	173	a1i	$⊢ (φ \land i \in Z) \to ⋃_{j = M}^{i} E (j) \in V$
175	167 170 171 174	fvmptd	$⊢ (φ \land i \in Z) \to G (i) = ⋃_{j = M}^{i} E (j)$
176	165 166 175	syl2anc	$⊢ (φ \land i \in (M ..^N)) \to G (i) = ⋃_{j = M}^{i} E (j)$
177	176	eqcomd	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) = G (i)$
178		difid	$⊢ E (i + 1) ∖ E (i + 1) = \emptyset$
179	178	a1i	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) ∖ E (i + 1) = \emptyset$
180	177 179	uneq12d	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) \cup (E (i + 1) ∖ E (i + 1)) = G (i) \cup \emptyset$
181		un0	$⊢ G (i) \cup \emptyset = G (i)$
182	181	a1i	$⊢ (φ \land i \in (M ..^N)) \to G (i) \cup \emptyset = G (i)$
183	180 182	eqtrd	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) \cup (E (i + 1) ∖ E (i + 1)) = G (i)$
184	149 164 183	3eqtrd	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) ∖ E (i + 1) = G (i)$
185	184	fveq2d	$⊢ (φ \land i \in (M ..^N)) \to O (G (i + 1) ∖ E (i + 1)) = O (G (i))$
186	143 185	oveq12d	$⊢ (φ \land i \in (M ..^N)) \to O (G (i + 1) \cap E (i + 1)) +_{𝑒} O (G (i + 1) ∖ E (i + 1)) = O (E (i + 1)) +_{𝑒} O (G (i))$
187	186	3adant3	$⊢ (φ \land i \in (M ..^N) \land O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to O (G (i + 1) \cap E (i + 1)) +_{𝑒} O (G (i + 1) ∖ E (i + 1)) = O (E (i + 1)) +_{𝑒} O (G (i))$
188	1	adantr	$⊢ (φ \land i \in (M ..^N)) \to O \in OutMeas$
189	4	adantr	$⊢ (φ \land i \in (M ..^N)) \to E : Z ⟶ S$
190	189 132	ffvelrnd	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) \in S$
191		simpll	$⊢ ((φ \land i \in (M ..^N)) \land j \in (M \dots i + 1)) \to φ$
192	92	adantr	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to M \in ℤ$
193		elfzelz	$⊢ j \in (M \dots i + 1) \to j \in ℤ$
194	193	adantl	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to j \in ℤ$
195		elfzle1	$⊢ j \in (M \dots i + 1) \to M \leq j$
196	195	adantl	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to M \leq j$
197	192 194 196	3jca	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to (M \in ℤ \land j \in ℤ \land M \leq j)$
198		eluz2	$⊢ j \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land j \in ℤ \land M \leq j)$
199	197 198	sylibr	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to j \in ℤ_{\geq M}$
200	199 131	eleqtrdi	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to j \in Z$
201	200	adantll	$⊢ ((φ \land i \in (M ..^N)) \land j \in (M \dots i + 1)) \to j \in Z$
202	1 43	syl	$⊢ φ \to S \subseteq dom O$
203	202	adantr	$⊢ (φ \land j \in Z) \to S \subseteq dom O$
204	4	ffvelrnda	$⊢ (φ \land j \in Z) \to E (j) \in S$
205	203 204	sseldd	$⊢ (φ \land j \in Z) \to E (j) \in dom O$
206		elssuni	$⊢ E (j) \in dom O \to E (j) \subseteq ⋃ dom O$
207	205 206	syl	$⊢ (φ \land j \in Z) \to E (j) \subseteq ⋃ dom O$
208	191 201 207	syl2anc	$⊢ ((φ \land i \in (M ..^N)) \land j \in (M \dots i + 1)) \to E (j) \subseteq ⋃ dom O$
209	208	ralrimiva	$⊢ (φ \land i \in (M ..^N)) \to \forall j \in (M \dots i + 1) E (j) \subseteq ⋃ dom O$
210		iunss	$⊢ ⋃_{j = M}^{i + 1} E (j) \subseteq ⋃ dom O \leftrightarrow \forall j \in (M \dots i + 1) E (j) \subseteq ⋃ dom O$
211	209 210	sylibr	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i + 1} E (j) \subseteq ⋃ dom O$
212	137 211	eqsstrd	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) \subseteq ⋃ dom O$
213	188 2 42 190 212	caragensplit	$⊢ (φ \land i \in (M ..^N)) \to O (G (i + 1) \cap E (i + 1)) +_{𝑒} O (G (i + 1) ∖ E (i + 1)) = O (G (i + 1))$
214	213	eqcomd	$⊢ (φ \land i \in (M ..^N)) \to O (G (i + 1)) = O (G (i + 1) \cap E (i + 1)) +_{𝑒} O (G (i + 1) ∖ E (i + 1))$
215	214	3adant3	$⊢ (φ \land i \in (M ..^N) \land O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to O (G (i + 1)) = O (G (i + 1) \cap E (i + 1)) +_{𝑒} O (G (i + 1) ∖ E (i + 1))$
216	188	adantr	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to O \in OutMeas$
217	165	adantr	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to φ$
218		elfzuz	$⊢ n \in (M \dots i + 1) \to n \in ℤ_{\geq M}$
219	218 131	eleqtrdi	$⊢ n \in (M \dots i + 1) \to n \in Z$
220	219	adantl	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to n \in Z$
221	4 202	fssd	$⊢ φ \to E : Z ⟶ dom O$
222	221	ffvelrnda	$⊢ (φ \land n \in Z) \to E (n) \in dom O$
223	222 55	syl	$⊢ (φ \land n \in Z) \to E (n) \subseteq ⋃ dom O$
224	217 220 223	syl2anc	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to E (n) \subseteq ⋃ dom O$
225	216 42 224	omecl	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to O (E (n)) \in [0, +∞]$
226		2fveq3	$⊢ n = i + 1 \to O (E (n)) = O (E (i + 1))$
227	146 225 226	sge0p1	$⊢ (φ \land i \in (M ..^N)) \to sum^((n \in (M \dots i + 1) ⟼ O (E (n)))) = sum^((n \in (M \dots i) ⟼ O (E (n)))) +_{𝑒} O (E (i + 1))$
228	227	3adant3	$⊢ (φ \land i \in (M ..^N) \land O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to sum^((n \in (M \dots i + 1) ⟼ O (E (n)))) = sum^((n \in (M \dots i) ⟼ O (E (n)))) +_{𝑒} O (E (i + 1))$
229		id	$⊢ O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n)))) \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))$
230	229	eqcomd	$⊢ O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n)))) \to sum^((n \in (M \dots i) ⟼ O (E (n)))) = O (G (i))$
231	230	oveq1d	$⊢ O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n)))) \to sum^((n \in (M \dots i) ⟼ O (E (n)))) +_{𝑒} O (E (i + 1)) = O (G (i)) +_{𝑒} O (E (i + 1))$
232	231	3ad2ant3	$⊢ (φ \land i \in (M ..^N) \land O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to sum^((n \in (M \dots i) ⟼ O (E (n)))) +_{𝑒} O (E (i + 1)) = O (G (i)) +_{𝑒} O (E (i + 1))$
233		simpl	$⊢ (φ \land j \in (M \dots i)) \to φ$
234	155	sseli	$⊢ j \in (M \dots i) \to j \in Z$
235	234	adantl	$⊢ (φ \land j \in (M \dots i)) \to j \in Z$
236	233 235 207	syl2anc	$⊢ (φ \land j \in (M \dots i)) \to E (j) \subseteq ⋃ dom O$
237	236	adantlr	$⊢ ((φ \land i \in Z) \land j \in (M \dots i)) \to E (j) \subseteq ⋃ dom O$
238	237	ralrimiva	$⊢ (φ \land i \in Z) \to \forall j \in (M \dots i) E (j) \subseteq ⋃ dom O$
239		iunss	$⊢ ⋃_{j = M}^{i} E (j) \subseteq ⋃ dom O \leftrightarrow \forall j \in (M \dots i) E (j) \subseteq ⋃ dom O$
240	238 239	sylibr	$⊢ (φ \land i \in Z) \to ⋃_{j = M}^{i} E (j) \subseteq ⋃ dom O$
241	175 240	eqsstrd	$⊢ (φ \land i \in Z) \to G (i) \subseteq ⋃ dom O$
242	165 166 241	syl2anc	$⊢ (φ \land i \in (M ..^N)) \to G (i) \subseteq ⋃ dom O$
243	188 42 242	omexrcl	$⊢ (φ \land i \in (M ..^N)) \to O (G (i)) \in ℝ^{*}$
244	111 211	sstrd	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) \subseteq ⋃ dom O$
245	188 42 244	omexrcl	$⊢ (φ \land i \in (M ..^N)) \to O (E (i + 1)) \in ℝ^{*}$
246	243 245	xaddcomd	$⊢ (φ \land i \in (M ..^N)) \to O (G (i)) +_{𝑒} O (E (i + 1)) = O (E (i + 1)) +_{𝑒} O (G (i))$
247	246	3adant3	$⊢ (φ \land i \in (M ..^N) \land O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to O (G (i)) +_{𝑒} O (E (i + 1)) = O (E (i + 1)) +_{𝑒} O (G (i))$
248	228 232 247	3eqtrd	$⊢ (φ \land i \in (M ..^N) \land O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to sum^((n \in (M \dots i + 1) ⟼ O (E (n)))) = O (E (i + 1)) +_{𝑒} O (G (i))$
249	187 215 248	3eqtr4d	$⊢ (φ \land i \in (M ..^N) \land O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to O (G (i + 1)) = sum^((n \in (M \dots i + 1) ⟼ O (E (n))))$
250	87 88 91 249	syl3anc	$⊢ (i \in (M ..^N) \land (φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \land φ) \to O (G (i + 1)) = sum^((n \in (M \dots i + 1) ⟼ O (E (n))))$
251	250	3exp	$⊢ i \in (M ..^N) \to ((φ \to O (G (i)) = sum^((n \in (M \dots i) ⟼ O (E (n))))) \to (φ \to O (G (i + 1)) = sum^((n \in (M \dots i + 1) ⟼ O (E (n))))))$
252	16 22 28 34 86 251	fzind2	$⊢ N \in (M \dots N) \to (φ \to O (G (N)) = sum^((n \in (M \dots N) ⟼ O (E (n)))))$
253	9 10 252	sylc	$⊢ φ \to O (G (N)) = sum^((n \in (M \dots N) ⟼ O (E (n))))$

Metamath Proof Explorer

Theorem caratheodorylem1

Proof