voliunlem1

	Ref	Expression
Hypotheses	voliunlem.3	$⊢ φ \to F : ℕ ⟶ dom vol$
	voliunlem.5	$⊢ φ \to \underset{i \in ℕ}{Disj} F (i)$
	voliunlem1.6	$⊢ H = (n \in ℕ ⟼ {vol}^{*} (E \cap F (n)))$
	voliunlem1.7	$⊢ φ \to E \subseteq ℝ$
	voliunlem1.8	$⊢ φ \to {vol}^{*} (E) \in ℝ$
Assertion	voliunlem1	$⊢ (φ \land k \in ℕ) \to seq 1 (+ H) (k) + {vol}^{} (E ∖ ⋃ ran F) \leq {vol}^{} (E)$

Proof

Step	Hyp	Ref	Expression
1		voliunlem.3	$⊢ φ \to F : ℕ ⟶ dom vol$
2		voliunlem.5	$⊢ φ \to \underset{i \in ℕ}{Disj} F (i)$
3		voliunlem1.6	$⊢ H = (n \in ℕ ⟼ {vol}^{*} (E \cap F (n)))$
4		voliunlem1.7	$⊢ φ \to E \subseteq ℝ$
5		voliunlem1.8	$⊢ φ \to {vol}^{*} (E) \in ℝ$
6		difss	$⊢ E ∖ ⋃ ran F \subseteq E$
7	5	adantr	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E) \in ℝ$
8		ovolsscl	$⊢ (E ∖ ⋃ ran F \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E ∖ ⋃ ran F) \in ℝ$
9	6 4 7 8	mp3an2ani	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E ∖ ⋃ ran F) \in ℝ$
10		difss	$⊢ E ∖ ⋃_{n = 1}^{k} F (n) \subseteq E$
11		ovolsscl	$⊢ (E ∖ ⋃_{n = 1}^{k} F (n) \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E ∖ ⋃_{n = 1}^{k} F (n)) \in ℝ$
12	10 4 7 11	mp3an2ani	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E ∖ ⋃_{n = 1}^{k} F (n)) \in ℝ$
13		inss1	$⊢ E \cap ⋃_{n = 1}^{k} F (n) \subseteq E$
14		ovolsscl	$⊢ (E \cap ⋃_{n = 1}^{k} F (n) \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) \in ℝ$
15	13 4 7 14	mp3an2ani	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E \cap ⋃_{n = 1}^{k} F (n)) \in ℝ$
16		elfznn	$⊢ n \in (1 \dots k) \to n \in ℕ$
17	1	ffnd	$⊢ φ \to F Fn ℕ$
18		fnfvelrn	$⊢ (F Fn ℕ \land n \in ℕ) \to F (n) \in ran F$
19	17 18	sylan	$⊢ (φ \land n \in ℕ) \to F (n) \in ran F$
20		elssuni	$⊢ F (n) \in ran F \to F (n) \subseteq ⋃ ran F$
21	19 20	syl	$⊢ (φ \land n \in ℕ) \to F (n) \subseteq ⋃ ran F$
22	16 21	sylan2	$⊢ (φ \land n \in (1 \dots k)) \to F (n) \subseteq ⋃ ran F$
23	22	ralrimiva	$⊢ φ \to \forall n \in (1 \dots k) F (n) \subseteq ⋃ ran F$
24	23	adantr	$⊢ (φ \land k \in ℕ) \to \forall n \in (1 \dots k) F (n) \subseteq ⋃ ran F$
25		iunss	$⊢ ⋃_{n = 1}^{k} F (n) \subseteq ⋃ ran F \leftrightarrow \forall n \in (1 \dots k) F (n) \subseteq ⋃ ran F$
26	24 25	sylibr	$⊢ (φ \land k \in ℕ) \to ⋃_{n = 1}^{k} F (n) \subseteq ⋃ ran F$
27	26	sscond	$⊢ (φ \land k \in ℕ) \to E ∖ ⋃ ran F \subseteq E ∖ ⋃_{n = 1}^{k} F (n)$
28	4	adantr	$⊢ (φ \land k \in ℕ) \to E \subseteq ℝ$
29	10 28	sstrid	$⊢ (φ \land k \in ℕ) \to E ∖ ⋃_{n = 1}^{k} F (n) \subseteq ℝ$
30		ovolss	$⊢ (E ∖ ⋃ ran F \subseteq E ∖ ⋃_{n = 1}^{k} F (n) \land E ∖ ⋃_{n = 1}^{k} F (n) \subseteq ℝ) \to {vol}^{} (E ∖ ⋃ ran F) \leq {vol}^{} (E ∖ ⋃_{n = 1}^{k} F (n))$
31	27 29 30	syl2anc	$⊢ (φ \land k \in ℕ) \to {vol}^{} (E ∖ ⋃ ran F) \leq {vol}^{} (E ∖ ⋃_{n = 1}^{k} F (n))$
32	9 12 15 31	leadd2dd	$⊢ (φ \land k \in ℕ) \to {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{} (E ∖ ⋃ ran F) \leq {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{} (E ∖ ⋃_{n = 1}^{k} F (n))$
33		oveq2	$⊢ z = 1 \to (1 \dots z) = (1 \dots 1)$
34	33	iuneq1d	$⊢ z = 1 \to ⋃_{n = 1}^{z} F (n) = ⋃_{n = 1}^{1} F (n)$
35	34	eleq1d	$⊢ z = 1 \to (⋃_{n = 1}^{z} F (n) \in dom vol \leftrightarrow ⋃_{n = 1}^{1} F (n) \in dom vol)$
36	34	ineq2d	$⊢ z = 1 \to E \cap ⋃_{n = 1}^{z} F (n) = E \cap ⋃_{n = 1}^{1} F (n)$
37	36	fveq2d	$⊢ z = 1 \to {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = {vol}^{} (E \cap ⋃_{n = 1}^{1} F (n))$
38		fveq2	$⊢ z = 1 \to seq 1 (+ H) (z) = seq 1 (+ H) (1)$
39	37 38	eqeq12d	$⊢ z = 1 \to ({vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z) \leftrightarrow {vol}^{} (E \cap ⋃_{n = 1}^{1} F (n)) = seq 1 (+ H) (1))$
40	35 39	anbi12d	$⊢ z = 1 \to ((⋃_{n = 1}^{z} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z)) \leftrightarrow (⋃_{n = 1}^{1} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{1} F (n)) = seq 1 (+ H) (1)))$
41	40	imbi2d	$⊢ z = 1 \to ((φ \to (⋃_{n = 1}^{z} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z))) \leftrightarrow (φ \to (⋃_{n = 1}^{1} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{1} F (n)) = seq 1 (+ H) (1))))$
42		oveq2	$⊢ z = k \to (1 \dots z) = (1 \dots k)$
43	42	iuneq1d	$⊢ z = k \to ⋃_{n = 1}^{z} F (n) = ⋃_{n = 1}^{k} F (n)$
44	43	eleq1d	$⊢ z = k \to (⋃_{n = 1}^{z} F (n) \in dom vol \leftrightarrow ⋃_{n = 1}^{k} F (n) \in dom vol)$
45	43	ineq2d	$⊢ z = k \to E \cap ⋃_{n = 1}^{z} F (n) = E \cap ⋃_{n = 1}^{k} F (n)$
46	45	fveq2d	$⊢ z = k \to {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n))$
47		fveq2	$⊢ z = k \to seq 1 (+ H) (z) = seq 1 (+ H) (k)$
48	46 47	eqeq12d	$⊢ z = k \to ({vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z) \leftrightarrow {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k))$
49	44 48	anbi12d	$⊢ z = k \to ((⋃_{n = 1}^{z} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z)) \leftrightarrow (⋃_{n = 1}^{k} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k)))$
50	49	imbi2d	$⊢ z = k \to ((φ \to (⋃_{n = 1}^{z} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z))) \leftrightarrow (φ \to (⋃_{n = 1}^{k} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k))))$
51		oveq2	$⊢ z = k + 1 \to (1 \dots z) = (1 \dots k + 1)$
52	51	iuneq1d	$⊢ z = k + 1 \to ⋃_{n = 1}^{z} F (n) = ⋃_{n = 1}^{k + 1} F (n)$
53	52	eleq1d	$⊢ z = k + 1 \to (⋃_{n = 1}^{z} F (n) \in dom vol \leftrightarrow ⋃_{n = 1}^{k + 1} F (n) \in dom vol)$
54	52	ineq2d	$⊢ z = k + 1 \to E \cap ⋃_{n = 1}^{z} F (n) = E \cap ⋃_{n = 1}^{k + 1} F (n)$
55	54	fveq2d	$⊢ z = k + 1 \to {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n))$
56		fveq2	$⊢ z = k + 1 \to seq 1 (+ H) (z) = seq 1 (+ H) (k + 1)$
57	55 56	eqeq12d	$⊢ z = k + 1 \to ({vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z) \leftrightarrow {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = seq 1 (+ H) (k + 1))$
58	53 57	anbi12d	$⊢ z = k + 1 \to ((⋃_{n = 1}^{z} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z)) \leftrightarrow (⋃_{n = 1}^{k + 1} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = seq 1 (+ H) (k + 1)))$
59	58	imbi2d	$⊢ z = k + 1 \to ((φ \to (⋃_{n = 1}^{z} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{z} F (n)) = seq 1 (+ H) (z))) \leftrightarrow (φ \to (⋃_{n = 1}^{k + 1} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = seq 1 (+ H) (k + 1))))$
60		1z	$⊢ 1 \in ℤ$
61		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
62		iuneq1	$⊢ (1 \dots 1) = \{1\} \to ⋃_{n = 1}^{1} F (n) = ⋃_{n \in \{1\}} F (n)$
63	60 61 62	mp2b	$⊢ ⋃_{n = 1}^{1} F (n) = ⋃_{n \in \{1\}} F (n)$
64		1ex	$⊢ 1 \in V$
65		fveq2	$⊢ n = 1 \to F (n) = F (1)$
66	64 65	iunxsn	$⊢ ⋃_{n \in \{1\}} F (n) = F (1)$
67	63 66	eqtri	$⊢ ⋃_{n = 1}^{1} F (n) = F (1)$
68		1nn	$⊢ 1 \in ℕ$
69		ffvelrn	$⊢ (F : ℕ ⟶ dom vol \land 1 \in ℕ) \to F (1) \in dom vol$
70	1 68 69	sylancl	$⊢ φ \to F (1) \in dom vol$
71	67 70	eqeltrid	$⊢ φ \to ⋃_{n = 1}^{1} F (n) \in dom vol$
72	65	ineq2d	$⊢ n = 1 \to E \cap F (n) = E \cap F (1)$
73	72	fveq2d	$⊢ n = 1 \to {vol}^{} (E \cap F (n)) = {vol}^{} (E \cap F (1))$
74		fvex	$⊢ {vol}^{*} (E \cap F (1)) \in V$
75	73 3 74	fvmpt	$⊢ 1 \in ℕ \to H (1) = {vol}^{*} (E \cap F (1))$
76	68 75	ax-mp	$⊢ H (1) = {vol}^{*} (E \cap F (1))$
77		seq1	$⊢ 1 \in ℤ \to seq 1 (+ H) (1) = H (1)$
78	60 77	ax-mp	$⊢ seq 1 (+ H) (1) = H (1)$
79	67	ineq2i	$⊢ E \cap ⋃_{n = 1}^{1} F (n) = E \cap F (1)$
80	79	fveq2i	$⊢ {vol}^{} (E \cap ⋃_{n = 1}^{1} F (n)) = {vol}^{} (E \cap F (1))$
81	76 78 80	3eqtr4ri	$⊢ {vol}^{*} (E \cap ⋃_{n = 1}^{1} F (n)) = seq 1 (+ H) (1)$
82	71 81	jctir	$⊢ φ \to (⋃_{n = 1}^{1} F (n) \in dom vol \land {vol}^{*} (E \cap ⋃_{n = 1}^{1} F (n)) = seq 1 (+ H) (1))$
83		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
84		ffvelrn	$⊢ (F : ℕ ⟶ dom vol \land k + 1 \in ℕ) \to F (k + 1) \in dom vol$
85	1 83 84	syl2an	$⊢ (φ \land k \in ℕ) \to F (k + 1) \in dom vol$
86		unmbl	$⊢ (⋃_{n = 1}^{k} F (n) \in dom vol \land F (k + 1) \in dom vol) \to ⋃_{n = 1}^{k} F (n) \cup F (k + 1) \in dom vol$
87	86	ex	$⊢ ⋃_{n = 1}^{k} F (n) \in dom vol \to (F (k + 1) \in dom vol \to ⋃_{n = 1}^{k} F (n) \cup F (k + 1) \in dom vol)$
88	85 87	syl5com	$⊢ (φ \land k \in ℕ) \to (⋃_{n = 1}^{k} F (n) \in dom vol \to ⋃_{n = 1}^{k} F (n) \cup F (k + 1) \in dom vol)$
89		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
90		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
91	89 90	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
92		fzsuc	$⊢ k \in ℤ_{\geq 1} \to (1 \dots k + 1) = (1 \dots k) \cup \{k + 1\}$
93		iuneq1	$⊢ (1 \dots k + 1) = (1 \dots k) \cup \{k + 1\} \to ⋃_{n = 1}^{k + 1} F (n) = ⋃_{n \in (1 \dots k) \cup \{k + 1\}} F (n)$
94	91 92 93	3syl	$⊢ (φ \land k \in ℕ) \to ⋃_{n = 1}^{k + 1} F (n) = ⋃_{n \in (1 \dots k) \cup \{k + 1\}} F (n)$
95		iunxun	$⊢ ⋃_{n \in (1 \dots k) \cup \{k + 1\}} F (n) = ⋃_{n = 1}^{k} F (n) \cup ⋃_{n \in \{k + 1\}} F (n)$
96		ovex	$⊢ k + 1 \in V$
97		fveq2	$⊢ n = k + 1 \to F (n) = F (k + 1)$
98	96 97	iunxsn	$⊢ ⋃_{n \in \{k + 1\}} F (n) = F (k + 1)$
99	98	uneq2i	$⊢ ⋃_{n = 1}^{k} F (n) \cup ⋃_{n \in \{k + 1\}} F (n) = ⋃_{n = 1}^{k} F (n) \cup F (k + 1)$
100	95 99	eqtri	$⊢ ⋃_{n \in (1 \dots k) \cup \{k + 1\}} F (n) = ⋃_{n = 1}^{k} F (n) \cup F (k + 1)$
101	94 100	eqtrdi	$⊢ (φ \land k \in ℕ) \to ⋃_{n = 1}^{k + 1} F (n) = ⋃_{n = 1}^{k} F (n) \cup F (k + 1)$
102	101	eleq1d	$⊢ (φ \land k \in ℕ) \to (⋃_{n = 1}^{k + 1} F (n) \in dom vol \leftrightarrow ⋃_{n = 1}^{k} F (n) \cup F (k + 1) \in dom vol)$
103	88 102	sylibrd	$⊢ (φ \land k \in ℕ) \to (⋃_{n = 1}^{k} F (n) \in dom vol \to ⋃_{n = 1}^{k + 1} F (n) \in dom vol)$
104		oveq1	$⊢ {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k) \to {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{} (E \cap F (k + 1)) = seq 1 (+ H) (k) + {vol}^{} (E \cap F (k + 1))$
105		inss1	$⊢ E \cap ⋃_{n = 1}^{k + 1} F (n) \subseteq E$
106	105 28	sstrid	$⊢ (φ \land k \in ℕ) \to E \cap ⋃_{n = 1}^{k + 1} F (n) \subseteq ℝ$
107		ovolsscl	$⊢ (E \cap ⋃_{n = 1}^{k + 1} F (n) \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) \in ℝ$
108	105 4 7 107	mp3an2ani	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E \cap ⋃_{n = 1}^{k + 1} F (n)) \in ℝ$
109		mblsplit	$⊢ (F (k + 1) \in dom vol \land E \cap ⋃_{n = 1}^{k + 1} F (n) \subseteq ℝ \land {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) \in ℝ) \to {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = {vol}^{} ((E \cap ⋃_{n = 1}^{k + 1} F (n)) \cap F (k + 1)) + {vol}^{} ((E \cap ⋃_{n = 1}^{k + 1} F (n)) ∖ F (k + 1))$
110	85 106 108 109	syl3anc	$⊢ (φ \land k \in ℕ) \to {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = {vol}^{} ((E \cap ⋃_{n = 1}^{k + 1} F (n)) \cap F (k + 1)) + {vol}^{*} ((E \cap ⋃_{n = 1}^{k + 1} F (n)) ∖ F (k + 1))$
111		in32	$⊢ (E \cap ⋃_{n = 1}^{k + 1} F (n)) \cap F (k + 1) = (E \cap F (k + 1)) \cap ⋃_{n = 1}^{k + 1} F (n)$
112		inss2	$⊢ E \cap F (k + 1) \subseteq F (k + 1)$
113	83	adantl	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℕ$
114	113 90	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k + 1 \in ℤ_{\geq 1}$
115		eluzfz2	$⊢ k + 1 \in ℤ_{\geq 1} \to k + 1 \in (1 \dots k + 1)$
116	97	ssiun2s	$⊢ k + 1 \in (1 \dots k + 1) \to F (k + 1) \subseteq ⋃_{n = 1}^{k + 1} F (n)$
117	114 115 116	3syl	$⊢ (φ \land k \in ℕ) \to F (k + 1) \subseteq ⋃_{n = 1}^{k + 1} F (n)$
118	112 117	sstrid	$⊢ (φ \land k \in ℕ) \to E \cap F (k + 1) \subseteq ⋃_{n = 1}^{k + 1} F (n)$
119		df-ss	$⊢ E \cap F (k + 1) \subseteq ⋃_{n = 1}^{k + 1} F (n) \leftrightarrow (E \cap F (k + 1)) \cap ⋃_{n = 1}^{k + 1} F (n) = E \cap F (k + 1)$
120	118 119	sylib	$⊢ (φ \land k \in ℕ) \to (E \cap F (k + 1)) \cap ⋃_{n = 1}^{k + 1} F (n) = E \cap F (k + 1)$
121	111 120	eqtrid	$⊢ (φ \land k \in ℕ) \to (E \cap ⋃_{n = 1}^{k + 1} F (n)) \cap F (k + 1) = E \cap F (k + 1)$
122	121	fveq2d	$⊢ (φ \land k \in ℕ) \to {vol}^{} ((E \cap ⋃_{n = 1}^{k + 1} F (n)) \cap F (k + 1)) = {vol}^{} (E \cap F (k + 1))$
123		indif2	$⊢ E \cap (⋃_{n = 1}^{k + 1} F (n) ∖ F (k + 1)) = (E \cap ⋃_{n = 1}^{k + 1} F (n)) ∖ F (k + 1)$
124		uncom	$⊢ ⋃_{n = 1}^{k} F (n) \cup F (k + 1) = F (k + 1) \cup ⋃_{n = 1}^{k} F (n)$
125	101 124	eqtr2di	$⊢ (φ \land k \in ℕ) \to F (k + 1) \cup ⋃_{n = 1}^{k} F (n) = ⋃_{n = 1}^{k + 1} F (n)$
126	2	ad2antrr	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to \underset{i \in ℕ}{Disj} F (i)$
127	113	adantr	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to k + 1 \in ℕ$
128	16	adantl	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n \in ℕ$
129	128	nnred	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n \in ℝ$
130		elfzle2	$⊢ n \in (1 \dots k) \to n \leq k$
131	130	adantl	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n \leq k$
132	89	adantr	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to k \in ℕ$
133		nnleltp1	$⊢ (n \in ℕ \land k \in ℕ) \to (n \leq k \leftrightarrow n < k + 1)$
134	128 132 133	syl2anc	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to (n \leq k \leftrightarrow n < k + 1)$
135	131 134	mpbid	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to n < k + 1$
136	129 135	gtned	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to k + 1 \neq n$
137		fveq2	$⊢ i = k + 1 \to F (i) = F (k + 1)$
138		fveq2	$⊢ i = n \to F (i) = F (n)$
139	137 138	disji2	$⊢ (\underset{i \in ℕ}{Disj} F (i) \land (k + 1 \in ℕ \land n \in ℕ) \land k + 1 \neq n) \to F (k + 1) \cap F (n) = \emptyset$
140	126 127 128 136 139	syl121anc	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to F (k + 1) \cap F (n) = \emptyset$
141	140	iuneq2dv	$⊢ (φ \land k \in ℕ) \to ⋃_{n = 1}^{k} (F (k + 1) \cap F (n)) = ⋃_{n = 1}^{k} \emptyset$
142		iunin2	$⊢ ⋃_{n = 1}^{k} (F (k + 1) \cap F (n)) = F (k + 1) \cap ⋃_{n = 1}^{k} F (n)$
143		iun0	$⊢ ⋃_{n = 1}^{k} \emptyset = \emptyset$
144	141 142 143	3eqtr3g	$⊢ (φ \land k \in ℕ) \to F (k + 1) \cap ⋃_{n = 1}^{k} F (n) = \emptyset$
145		uneqdifeq	$⊢ (F (k + 1) \subseteq ⋃_{n = 1}^{k + 1} F (n) \land F (k + 1) \cap ⋃_{n = 1}^{k} F (n) = \emptyset) \to (F (k + 1) \cup ⋃_{n = 1}^{k} F (n) = ⋃_{n = 1}^{k + 1} F (n) \leftrightarrow ⋃_{n = 1}^{k + 1} F (n) ∖ F (k + 1) = ⋃_{n = 1}^{k} F (n))$
146	117 144 145	syl2anc	$⊢ (φ \land k \in ℕ) \to (F (k + 1) \cup ⋃_{n = 1}^{k} F (n) = ⋃_{n = 1}^{k + 1} F (n) \leftrightarrow ⋃_{n = 1}^{k + 1} F (n) ∖ F (k + 1) = ⋃_{n = 1}^{k} F (n))$
147	125 146	mpbid	$⊢ (φ \land k \in ℕ) \to ⋃_{n = 1}^{k + 1} F (n) ∖ F (k + 1) = ⋃_{n = 1}^{k} F (n)$
148	147	ineq2d	$⊢ (φ \land k \in ℕ) \to E \cap (⋃_{n = 1}^{k + 1} F (n) ∖ F (k + 1)) = E \cap ⋃_{n = 1}^{k} F (n)$
149	123 148	eqtr3id	$⊢ (φ \land k \in ℕ) \to (E \cap ⋃_{n = 1}^{k + 1} F (n)) ∖ F (k + 1) = E \cap ⋃_{n = 1}^{k} F (n)$
150	149	fveq2d	$⊢ (φ \land k \in ℕ) \to {vol}^{} ((E \cap ⋃_{n = 1}^{k + 1} F (n)) ∖ F (k + 1)) = {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n))$
151	122 150	oveq12d	$⊢ (φ \land k \in ℕ) \to {vol}^{} ((E \cap ⋃_{n = 1}^{k + 1} F (n)) \cap F (k + 1)) + {vol}^{} ((E \cap ⋃_{n = 1}^{k + 1} F (n)) ∖ F (k + 1)) = {vol}^{} (E \cap F (k + 1)) + {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n))$
152		inss1	$⊢ E \cap F (k + 1) \subseteq E$
153		ovolsscl	$⊢ (E \cap F (k + 1) \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E \cap F (k + 1)) \in ℝ$
154	152 4 7 153	mp3an2ani	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E \cap F (k + 1)) \in ℝ$
155	154	recnd	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E \cap F (k + 1)) \in ℂ$
156	15	recnd	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E \cap ⋃_{n = 1}^{k} F (n)) \in ℂ$
157	155 156	addcomd	$⊢ (φ \land k \in ℕ) \to {vol}^{} (E \cap F (k + 1)) + {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{} (E \cap F (k + 1))$
158	110 151 157	3eqtrd	$⊢ (φ \land k \in ℕ) \to {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{*} (E \cap F (k + 1))$
159		seqp1	$⊢ k \in ℤ_{\geq 1} \to seq 1 (+ H) (k + 1) = seq 1 (+ H) (k) + H (k + 1)$
160	91 159	syl	$⊢ (φ \land k \in ℕ) \to seq 1 (+ H) (k + 1) = seq 1 (+ H) (k) + H (k + 1)$
161	97	ineq2d	$⊢ n = k + 1 \to E \cap F (n) = E \cap F (k + 1)$
162	161	fveq2d	$⊢ n = k + 1 \to {vol}^{} (E \cap F (n)) = {vol}^{} (E \cap F (k + 1))$
163		fvex	$⊢ {vol}^{*} (E \cap F (k + 1)) \in V$
164	162 3 163	fvmpt	$⊢ k + 1 \in ℕ \to H (k + 1) = {vol}^{*} (E \cap F (k + 1))$
165	113 164	syl	$⊢ (φ \land k \in ℕ) \to H (k + 1) = {vol}^{*} (E \cap F (k + 1))$
166	165	oveq2d	$⊢ (φ \land k \in ℕ) \to seq 1 (+ H) (k) + H (k + 1) = seq 1 (+ H) (k) + {vol}^{*} (E \cap F (k + 1))$
167	160 166	eqtrd	$⊢ (φ \land k \in ℕ) \to seq 1 (+ H) (k + 1) = seq 1 (+ H) (k) + {vol}^{*} (E \cap F (k + 1))$
168	158 167	eqeq12d	$⊢ (φ \land k \in ℕ) \to ({vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = seq 1 (+ H) (k + 1) \leftrightarrow {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{} (E \cap F (k + 1)) = seq 1 (+ H) (k) + {vol}^{} (E \cap F (k + 1)))$
169	104 168	syl5ibr	$⊢ (φ \land k \in ℕ) \to ({vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k) \to {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = seq 1 (+ H) (k + 1))$
170	103 169	anim12d	$⊢ (φ \land k \in ℕ) \to ((⋃_{n = 1}^{k} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k)) \to (⋃_{n = 1}^{k + 1} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = seq 1 (+ H) (k + 1)))$
171	170	expcom	$⊢ k \in ℕ \to (φ \to ((⋃_{n = 1}^{k} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k)) \to (⋃_{n = 1}^{k + 1} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = seq 1 (+ H) (k + 1))))$
172	171	a2d	$⊢ k \in ℕ \to ((φ \to (⋃_{n = 1}^{k} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k))) \to (φ \to (⋃_{n = 1}^{k + 1} F (n) \in dom vol \land {vol}^{} (E \cap ⋃_{n = 1}^{k + 1} F (n)) = seq 1 (+ H) (k + 1))))$
173	41 50 59 50 82 172	nnind	$⊢ k \in ℕ \to (φ \to (⋃_{n = 1}^{k} F (n) \in dom vol \land {vol}^{*} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k)))$
174	173	impcom	$⊢ (φ \land k \in ℕ) \to (⋃_{n = 1}^{k} F (n) \in dom vol \land {vol}^{*} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k))$
175	174	simprd	$⊢ (φ \land k \in ℕ) \to {vol}^{*} (E \cap ⋃_{n = 1}^{k} F (n)) = seq 1 (+ H) (k)$
176	175	eqcomd	$⊢ (φ \land k \in ℕ) \to seq 1 (+ H) (k) = {vol}^{*} (E \cap ⋃_{n = 1}^{k} F (n))$
177	176	oveq1d	$⊢ (φ \land k \in ℕ) \to seq 1 (+ H) (k) + {vol}^{} (E ∖ ⋃ ran F) = {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{*} (E ∖ ⋃ ran F)$
178	174	simpld	$⊢ (φ \land k \in ℕ) \to ⋃_{n = 1}^{k} F (n) \in dom vol$
179		mblsplit	$⊢ (⋃_{n = 1}^{k} F (n) \in dom vol \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E) = {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{} (E ∖ ⋃_{n = 1}^{k} F (n))$
180	178 28 7 179	syl3anc	$⊢ (φ \land k \in ℕ) \to {vol}^{} (E) = {vol}^{} (E \cap ⋃_{n = 1}^{k} F (n)) + {vol}^{*} (E ∖ ⋃_{n = 1}^{k} F (n))$
181	32 177 180	3brtr4d	$⊢ (φ \land k \in ℕ) \to seq 1 (+ H) (k) + {vol}^{} (E ∖ ⋃ ran F) \leq {vol}^{} (E)$

Metamath Proof Explorer

Theorem voliunlem1

Proof