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	zred	$⊢ i \in (M ..^N) \to M \in ℝ$
96	94	zred	$⊢ i \in (M ..^N) \to i + 1 \in ℝ$
97	93	zred	$⊢ i \in (M ..^N) \to i \in ℝ$
98		elfzole1	$⊢ i \in (M ..^N) \to M \leq i$
99	97	ltp1d	$⊢ i \in (M ..^N) \to i < i + 1$
100	95 97 96 98 99	lelttrd	$⊢ i \in (M ..^N) \to M < i + 1$
101	95 96 100	ltled	$⊢ i \in (M ..^N) \to M \leq i + 1$
102		leid	$⊢ i + 1 \in ℝ \to i + 1 \leq i + 1$
103	96 102	syl	$⊢ i \in (M ..^N) \to i + 1 \leq i + 1$
104	92 94 94 101 103	elfzd	$⊢ i \in (M ..^N) \to i + 1 \in (M \dots i + 1)$
105	104	adantl	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in (M \dots i + 1)$
106		fveq2	$⊢ j = i + 1 \to E (j) = E (i + 1)$
107	106	ssiun2s	$⊢ i + 1 \in (M \dots i + 1) \to E (i + 1) \subseteq ⋃_{j = M}^{i + 1} E (j)$
108	105 107	syl	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) \subseteq ⋃_{j = M}^{i + 1} E (j)$
109		fveq2	$⊢ i = j \to E (i) = E (j)$
110	109	cbviunv	$⊢ ⋃_{i = M}^{n} E (i) = ⋃_{j = M}^{n} E (j)$
111	110	mpteq2i	$⊢ (n \in Z ⟼ ⋃_{i = M}^{n} E (i)) = (n \in Z ⟼ ⋃_{j = M}^{n} E (j))$
112	6 111	eqtri	$⊢ G = (n \in Z ⟼ ⋃_{j = M}^{n} E (j))$
113		oveq2	$⊢ n = i + 1 \to (M \dots n) = (M \dots i + 1)$
114	113	iuneq1d	$⊢ n = i + 1 \to ⋃_{j = M}^{n} E (j) = ⋃_{j = M}^{i + 1} E (j)$
115	36	adantr	$⊢ (φ \land i \in (M ..^N)) \to M \in ℤ$
116	93	adantl	$⊢ (φ \land i \in (M ..^N)) \to i \in ℤ$
117	116	peano2zd	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in ℤ$
118	115	zred	$⊢ (φ \land i \in (M ..^N)) \to M \in ℝ$
119	117	zred	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in ℝ$
120	116	zred	$⊢ (φ \land i \in (M ..^N)) \to i \in ℝ$
121	98	adantl	$⊢ (φ \land i \in (M ..^N)) \to M \leq i$
122	120	ltp1d	$⊢ (φ \land i \in (M ..^N)) \to i < i + 1$
123	118 120 119 121 122	lelttrd	$⊢ (φ \land i \in (M ..^N)) \to M < i + 1$
124	118 119 123	ltled	$⊢ (φ \land i \in (M ..^N)) \to M \leq i + 1$
125	115 117 124	3jca	$⊢ (φ \land i \in (M ..^N)) \to (M \in ℤ \land i + 1 \in ℤ \land M \leq i + 1)$
126		eluz2	$⊢ i + 1 \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land i + 1 \in ℤ \land M \leq i + 1)$
127	125 126	sylibr	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in ℤ_{\geq M}$
128	3	eqcomi	$⊢ ℤ_{\geq M} = Z$
129	127 128	eleqtrdi	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in Z$
130		ovex	$⊢ (M \dots i + 1) \in V$
131		fvex	$⊢ E (j) \in V$
132	130 131	iunex	$⊢ ⋃_{j = M}^{i + 1} E (j) \in V$
133	132	a1i	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i + 1} E (j) \in V$
134	112 114 129 133	fvmptd3	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) = ⋃_{j = M}^{i + 1} E (j)$
135	134	eqcomd	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i + 1} E (j) = G (i + 1)$
136	108 135	sseqtrd	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) \subseteq G (i + 1)$
137		sseqin2	$⊢ E (i + 1) \subseteq G (i + 1) \leftrightarrow G (i + 1) \cap E (i + 1) = E (i + 1)$
138	137	biimpi	$⊢ E (i + 1) \subseteq G (i + 1) \to G (i + 1) \cap E (i + 1) = E (i + 1)$
139	136 138	syl	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) \cap E (i + 1) = E (i + 1)$
140	139	fveq2d	$⊢ (φ \land i \in (M ..^N)) \to O (G (i + 1) \cap E (i + 1)) = O (E (i + 1))$
141		nfcv	$⊢ \underline{Ⅎ} j E (i + 1)$
142		elfzouz	$⊢ i \in (M ..^N) \to i \in ℤ_{\geq M}$
143	142	adantl	$⊢ (φ \land i \in (M ..^N)) \to i \in ℤ_{\geq M}$
144	141 143 106	iunp1	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i + 1} E (j) = ⋃_{j = M}^{i} E (j) \cup E (i + 1)$
145	134 144	eqtrd	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) = ⋃_{j = M}^{i} E (j) \cup E (i + 1)$
146	145	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)$
147		fveq2	$⊢ n = j \to E (n) = E (j)$
148	147	cbvdisjv	$⊢ \underset{n \in Z}{Disj} E (n) \leftrightarrow \underset{j \in Z}{Disj} E (j)$
149	5 148	sylib	$⊢ φ \to \underset{j \in Z}{Disj} E (j)$
150	149	adantr	$⊢ (φ \land i \in (M ..^N)) \to \underset{j \in Z}{Disj} E (j)$
151		fzssuz	$⊢ (M \dots i) \subseteq ℤ_{\geq M}$
152	151 128	sseqtri	$⊢ (M \dots i) \subseteq Z$
153	152	a1i	$⊢ (φ \land i \in (M ..^N)) \to (M \dots i) \subseteq Z$
154		fzp1nel	$⊢ \neg i + 1 \in (M \dots i)$
155	154	a1i	$⊢ i \in (M ..^N) \to \neg i + 1 \in (M \dots i)$
156	155	adantl	$⊢ (φ \land i \in (M ..^N)) \to \neg i + 1 \in (M \dots i)$
157	129 156	eldifd	$⊢ (φ \land i \in (M ..^N)) \to i + 1 \in (Z ∖ (M \dots i))$
158	150 153 157 106	disjiun2	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) \cap E (i + 1) = \emptyset$
159		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)$
160	158 159	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)$
161	160	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))$
162		simpl	$⊢ (φ \land i \in (M ..^N)) \to φ$
163	143 128	eleqtrdi	$⊢ (φ \land i \in (M ..^N)) \to i \in Z$
164	112	a1i	$⊢ (φ \land i \in Z) \to G = (n \in Z ⟼ ⋃_{j = M}^{n} E (j))$
165		simpr	$⊢ ((φ \land i \in Z) \land n = i) \to n = i$
166	165	oveq2d	$⊢ ((φ \land i \in Z) \land n = i) \to (M \dots n) = (M \dots i)$
167	166	iuneq1d	$⊢ ((φ \land i \in Z) \land n = i) \to ⋃_{j = M}^{n} E (j) = ⋃_{j = M}^{i} E (j)$
168		simpr	$⊢ (φ \land i \in Z) \to i \in Z$
169		ovex	$⊢ (M \dots i) \in V$
170	169 131	iunex	$⊢ ⋃_{j = M}^{i} E (j) \in V$
171	170	a1i	$⊢ (φ \land i \in Z) \to ⋃_{j = M}^{i} E (j) \in V$
172	164 167 168 171	fvmptd	$⊢ (φ \land i \in Z) \to G (i) = ⋃_{j = M}^{i} E (j)$
173	162 163 172	syl2anc	$⊢ (φ \land i \in (M ..^N)) \to G (i) = ⋃_{j = M}^{i} E (j)$
174	173	eqcomd	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) = G (i)$
175		difid	$⊢ E (i + 1) ∖ E (i + 1) = \emptyset$
176	175	a1i	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) ∖ E (i + 1) = \emptyset$
177	174 176	uneq12d	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) \cup (E (i + 1) ∖ E (i + 1)) = G (i) \cup \emptyset$
178		un0	$⊢ G (i) \cup \emptyset = G (i)$
179	178	a1i	$⊢ (φ \land i \in (M ..^N)) \to G (i) \cup \emptyset = G (i)$
180	177 179	eqtrd	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i} E (j) \cup (E (i + 1) ∖ E (i + 1)) = G (i)$
181	146 161 180	3eqtrd	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) ∖ E (i + 1) = G (i)$
182	181	fveq2d	$⊢ (φ \land i \in (M ..^N)) \to O (G (i + 1) ∖ E (i + 1)) = O (G (i))$
183	140 182	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))$
184	183	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))$
185	1	adantr	$⊢ (φ \land i \in (M ..^N)) \to O \in OutMeas$
186	4	adantr	$⊢ (φ \land i \in (M ..^N)) \to E : Z ⟶ S$
187	186 129	ffvelrnd	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) \in S$
188		simpll	$⊢ ((φ \land i \in (M ..^N)) \land j \in (M \dots i + 1)) \to φ$
189	92	adantr	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to M \in ℤ$
190		elfzelz	$⊢ j \in (M \dots i + 1) \to j \in ℤ$
191	190	adantl	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to j \in ℤ$
192		elfzle1	$⊢ j \in (M \dots i + 1) \to M \leq j$
193	192	adantl	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to M \leq j$
194	189 191 193	3jca	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to (M \in ℤ \land j \in ℤ \land M \leq j)$
195		eluz2	$⊢ j \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land j \in ℤ \land M \leq j)$
196	194 195	sylibr	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to j \in ℤ_{\geq M}$
197	196 128	eleqtrdi	$⊢ (i \in (M ..^N) \land j \in (M \dots i + 1)) \to j \in Z$
198	197	adantll	$⊢ ((φ \land i \in (M ..^N)) \land j \in (M \dots i + 1)) \to j \in Z$
199	1 43	syl	$⊢ φ \to S \subseteq dom O$
200	199	adantr	$⊢ (φ \land j \in Z) \to S \subseteq dom O$
201	4	ffvelrnda	$⊢ (φ \land j \in Z) \to E (j) \in S$
202	200 201	sseldd	$⊢ (φ \land j \in Z) \to E (j) \in dom O$
203		elssuni	$⊢ E (j) \in dom O \to E (j) \subseteq ⋃ dom O$
204	202 203	syl	$⊢ (φ \land j \in Z) \to E (j) \subseteq ⋃ dom O$
205	188 198 204	syl2anc	$⊢ ((φ \land i \in (M ..^N)) \land j \in (M \dots i + 1)) \to E (j) \subseteq ⋃ dom O$
206	205	ralrimiva	$⊢ (φ \land i \in (M ..^N)) \to \forall j \in (M \dots i + 1) E (j) \subseteq ⋃ dom O$
207		iunss	$⊢ ⋃_{j = M}^{i + 1} E (j) \subseteq ⋃ dom O \leftrightarrow \forall j \in (M \dots i + 1) E (j) \subseteq ⋃ dom O$
208	206 207	sylibr	$⊢ (φ \land i \in (M ..^N)) \to ⋃_{j = M}^{i + 1} E (j) \subseteq ⋃ dom O$
209	134 208	eqsstrd	$⊢ (φ \land i \in (M ..^N)) \to G (i + 1) \subseteq ⋃ dom O$
210	185 2 42 187 209	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))$
211	210	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))$
212	211	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))$
213	185	adantr	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to O \in OutMeas$
214	162	adantr	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to φ$
215		elfzuz	$⊢ n \in (M \dots i + 1) \to n \in ℤ_{\geq M}$
216	215 128	eleqtrdi	$⊢ n \in (M \dots i + 1) \to n \in Z$
217	216	adantl	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to n \in Z$
218	4 199	fssd	$⊢ φ \to E : Z ⟶ dom O$
219	218	ffvelrnda	$⊢ (φ \land n \in Z) \to E (n) \in dom O$
220	219 55	syl	$⊢ (φ \land n \in Z) \to E (n) \subseteq ⋃ dom O$
221	214 217 220	syl2anc	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to E (n) \subseteq ⋃ dom O$
222	213 42 221	omecl	$⊢ ((φ \land i \in (M ..^N)) \land n \in (M \dots i + 1)) \to O (E (n)) \in [0, +∞]$
223		2fveq3	$⊢ n = i + 1 \to O (E (n)) = O (E (i + 1))$
224	143 222 223	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))$
225	224	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))$
226		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))))$
227	226	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))$
228	227	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))$
229	228	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))$
230		simpl	$⊢ (φ \land j \in (M \dots i)) \to φ$
231	152	sseli	$⊢ j \in (M \dots i) \to j \in Z$
232	231	adantl	$⊢ (φ \land j \in (M \dots i)) \to j \in Z$
233	230 232 204	syl2anc	$⊢ (φ \land j \in (M \dots i)) \to E (j) \subseteq ⋃ dom O$
234	233	adantlr	$⊢ ((φ \land i \in Z) \land j \in (M \dots i)) \to E (j) \subseteq ⋃ dom O$
235	234	ralrimiva	$⊢ (φ \land i \in Z) \to \forall j \in (M \dots i) E (j) \subseteq ⋃ dom O$
236		iunss	$⊢ ⋃_{j = M}^{i} E (j) \subseteq ⋃ dom O \leftrightarrow \forall j \in (M \dots i) E (j) \subseteq ⋃ dom O$
237	235 236	sylibr	$⊢ (φ \land i \in Z) \to ⋃_{j = M}^{i} E (j) \subseteq ⋃ dom O$
238	172 237	eqsstrd	$⊢ (φ \land i \in Z) \to G (i) \subseteq ⋃ dom O$
239	162 163 238	syl2anc	$⊢ (φ \land i \in (M ..^N)) \to G (i) \subseteq ⋃ dom O$
240	185 42 239	omexrcl	$⊢ (φ \land i \in (M ..^N)) \to O (G (i)) \in ℝ^{*}$
241	108 208	sstrd	$⊢ (φ \land i \in (M ..^N)) \to E (i + 1) \subseteq ⋃ dom O$
242	185 42 241	omexrcl	$⊢ (φ \land i \in (M ..^N)) \to O (E (i + 1)) \in ℝ^{*}$
243	240 242	xaddcomd	$⊢ (φ \land i \in (M ..^N)) \to O (G (i)) +_{𝑒} O (E (i + 1)) = O (E (i + 1)) +_{𝑒} O (G (i))$
244	243	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))$
245	225 229 244	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))$
246	184 212 245	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))))$
247	87 88 91 246	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))))$
248	247	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))))))$
249	16 22 28 34 86 248	fzind2	$⊢ N \in (M \dots N) \to (φ \to O (G (N)) = sum^((n \in (M \dots N) ⟼ O (E (n)))))$
250	9 10 249	sylc	$⊢ φ \to O (G (N)) = sum^((n \in (M \dots N) ⟼ O (E (n))))$

Metamath Proof Explorer

Theorem caratheodorylem1

Proof