uniioombllem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > uniioombllem4		Structured version Visualization version GIF version

Theorem uniioombllem4 25485

Description: Lemma for uniioombl 25488. (Contributed by Mario Carneiro, 26-Mar-2015.)

**Hypotheses**
Ref	Expression
uniioombl.1	⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.2	⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))
uniioombl.3	⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
uniioombl.a	⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)
uniioombl.e	⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
uniioombl.c	⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
uniioombl.g	⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.s	⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))
uniioombl.t	⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
uniioombl.v	⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐸) + 𝐶))
uniioombl.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
uniioombl.m2	⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ^*, < ))) < 𝐶)
uniioombl.k	⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))
uniioombl.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
uniioombl.n2	⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
uniioombl.l	⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))

**Assertion**
Ref	Expression
uniioombllem4	⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + 𝐶))

Distinct variable groups: 𝑖,𝑗,𝑥,𝐹 𝑖,𝐺,𝑗,𝑥 𝑗,𝐾,𝑥 𝐴,𝑗,𝑥 𝐶,𝑖,𝑗,𝑥 𝑖,𝑀,𝑗,𝑥 𝑖,𝑁,𝑗 𝜑,𝑖,𝑗,𝑥 𝑇,𝑖,𝑗,𝑥 Allowed substitution hints: 𝐴(𝑖) 𝑆(𝑥,𝑖,𝑗) 𝐸(𝑥,𝑖,𝑗) 𝐾(𝑖) 𝐿(𝑥,𝑖,𝑗) 𝑁(𝑥)

**Proof of Theorem uniioombllem4**
Step	Hyp	Ref	Expression
1		inss1 4188	. . 3 ⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾
2		uniioombl.k	. . . . 5 ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))
3		imassrn 6022	. . . . . 6 ⊢ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
4	3	unissi 4867	. . . . 5 ⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ∪ ran ((,) ∘ 𝐺)
5	2, 4	eqsstri 3982	. . . 4 ⊢ 𝐾 ⊆ ∪ ran ((,) ∘ 𝐺)
6		uniioombl.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
7	6	uniiccdif 25477	. . . . . 6 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
8	7	simpld 494	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
9		ovolficcss 25368	. . . . . 6 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
10	6, 9	syl 17	. . . . 5 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
11	8, 10	sstrd 3946	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
12	5, 11	sstrid 3947	. . 3 ⊢ (𝜑 → 𝐾 ⊆ ℝ)
13		uniioombl.1	. . . . . 6 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
14		uniioombl.2	. . . . . 6 ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))
15		uniioombl.3	. . . . . 6 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
16		uniioombl.a	. . . . . 6 ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)
17		uniioombl.e	. . . . . 6 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
18		uniioombl.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
19		uniioombl.s	. . . . . 6 ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))
20		uniioombl.t	. . . . . 6 ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
21		uniioombl.v	. . . . . 6 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐸) + 𝐶))
22	13, 14, 15, 16, 17, 18, 6, 19, 20, 21	uniioombllem1 25480	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
23		ssid 3958	. . . . . 6 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
24	20	ovollb 25378	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
25	6, 23, 24	sylancl 586	. . . . 5 ⊢ (𝜑 → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
26		ovollecl 25382	. . . . 5 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ^, < ) ∈ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < )) → (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
27	11, 22, 25, 26	syl3anc 1373	. . . 4 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
28		ovolsscl 25385	. . . 4 ⊢ ((𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘𝐾) ∈ ℝ)
29	5, 11, 27, 28	mp3an2i 1468	. . 3 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
30		ovolsscl 25385	. . 3 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ)
31	1, 12, 29, 30	mp3an2i 1468	. 2 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
32		inss1 4188	. . . 4 ⊢ (𝐾 ∩ 𝐿) ⊆ 𝐾
33		ovolsscl 25385	. . . 4 ⊢ (((𝐾 ∩ 𝐿) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐿)) ∈ ℝ)
34	32, 12, 29, 33	mp3an2i 1468	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ)
35		ssun2 4130	. . . . . 6 ⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
36		nnuz 12778	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
37		uniioombl.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ)
38	37	peano2nnd 12145	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
39	38, 36	eleqtrdi 2838	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
40		uzsplit 13499	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
41	39, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤ_≥‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
42	36, 41	eqtrid 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
43	37	nncnd 12144	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℂ)
44		ax-1cn 11067	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
45		pncan 11369	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
46	43, 44, 45	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
47	46	oveq2d 7365	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁))
48	47	uneq1d 4118	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
49	42, 48	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (𝜑 → ℕ = ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
50	49	iuneq1d 4969	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)))
51		iunxun 5043	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
52	50, 51	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
53		ioof 13350	. . . . . . . . . . . . . 14 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
54		inss2 4189	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
55		rexpssxrxp 11160	. . . . . . . . . . . . . . . 16 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
56	54, 55	sstri 3945	. . . . . . . . . . . . . . 15 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
57		fss 6668	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐹:ℕ⟶(ℝ^ × ℝ^*))
58	13, 56, 57	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ^* × ℝ^*))
59		fco 6676	. . . . . . . . . . . . . 14 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
60	53, 58, 59	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
61		ffn 6652	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
62		fniunfv 7183	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,) ∘ 𝐹))
63	60, 61, 62	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,) ∘ 𝐹))
64		fvco3 6922	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
65	13, 64	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
66	65	iuneq2dv 4966	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
67	63, 66	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
68	16, 67	eqtrid 2776	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
69		uniioombl.l	. . . . . . . . . . . 12 ⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))
70		ffun 6655	. . . . . . . . . . . . . 14 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐹))
71		funiunfv 7184	. . . . . . . . . . . . . 14 ⊢ (Fun ((,) ∘ 𝐹) → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,) ∘ 𝐹) “ (1...𝑁)))
72	60, 70, 71	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,) ∘ 𝐹) “ (1...𝑁)))
73		elfznn 13456	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ)
74	13, 73, 64	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
75	74	iuneq2dv 4966	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
76	72, 75	eqtr3d 2766	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (((,) ∘ 𝐹) “ (1...𝑁)) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
77	69, 76	eqtrid 2776	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
78	77	uneq1d 4118	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
79	52, 68, 78	3eqtr4d 2774	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
80	79	ineq2d 4171	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = (𝐾 ∩ (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))))
81		indi 4235	. . . . . . . 8 ⊢ (𝐾 ∩ (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
82	80, 81	eqtrdi 2780	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))))
83		fss 6668	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐺:ℕ⟶(ℝ^ × ℝ^*))
84	6, 56, 83	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ^* × ℝ^*))
85		fco 6676	. . . . . . . . . . . . . 14 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
86	53, 84, 85	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
87		ffun 6655	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐺))
88		funiunfv 7184	. . . . . . . . . . . . 13 ⊢ (Fun ((,) ∘ 𝐺) → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,) ∘ 𝐺) “ (1...𝑀)))
89	86, 87, 88	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,) ∘ 𝐺) “ (1...𝑀)))
90		elfznn 13456	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
91		fvco3 6922	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗)))
92	6, 90, 91	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗)))
93	92	iuneq2dv 4966	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
94	89, 93	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (1...𝑀)) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
95	2, 94	eqtrid 2776	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
96	95	ineq2d 4171	. . . . . . . . 9 ⊢ (𝜑 → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))))
97		incom 4160	. . . . . . . . 9 ⊢ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾)
98		iunin2 5020	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
99		incom 4160	. . . . . . . . . . . . . . 15 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
100	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ_≥‘(𝑁 + 1)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))))
101	100	iuneq2i 4963	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
102		incom 4160	. . . . . . . . . . . . 13 ⊢ (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
103	98, 101, 102	3eqtr4ri 2763	. . . . . . . . . . . 12 ⊢ (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))
104	103	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑀) → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
105	104	iuneq2i 4963	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))
106		iunin2 5020	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
107	105, 106	eqtr3i 2754	. . . . . . . . 9 ⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
108	96, 97, 107	3eqtr4g 2789	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
109	108	uneq2d 4119	. . . . . . 7 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
110	82, 109	eqtrd 2764	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
111	35, 110	sseqtrrid 3979	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ (𝐾 ∩ 𝐴))
112	111, 1	sstrdi 3948	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
113		ovolsscl 25385	. . . 4 ⊢ ((∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
114	112, 12, 29, 113	syl3anc 1373	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
115	34, 114	readdcld 11144	. 2 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐿)) + (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ∈ ℝ)
116	18	rpred 12937	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
117	34, 116	readdcld 11144	. 2 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) ∈ ℝ)
118	110	fveq2d 6826	. . 3 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) = (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
119	32, 12	sstrid 3947	. . . 4 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ ℝ)
120	112, 12	sstrd 3946	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ)
121		ovolun 25398	. . . 4 ⊢ ((((𝐾 ∩ 𝐿) ⊆ ℝ ∧ (vol‘(𝐾 ∩ 𝐿)) ∈ ℝ) ∧ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) → (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
122	119, 34, 120, 114, 121	syl22anc 838	. . 3 ⊢ (𝜑 → (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
123	118, 122	eqbrtrd 5114	. 2 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
124		fzfid 13880	. . . . 5 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
125		iunss 4994	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
126	112, 125	sylib 218	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
127	126	r19.21bi 3221	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
128	12	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ)
129	29	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ)
130		ovolsscl 25385	. . . . . 6 ⊢ ((∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
131	127, 128, 129, 130	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
132	124, 131	fsumrecl 15641	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
133	127, 128	sstrd 3946	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ)
134	133, 131	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
135	134	ralrimiva 3121	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
136		ovolfiniun 25400	. . . . 5 ⊢ (((1...𝑀) ∈ Fin ∧ ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
137	124, 135, 136	syl2anc 584	. . . 4 ⊢ (𝜑 → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
138		uniioombl.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
139	116, 138	nndivred 12182	. . . . . . 7 ⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℝ)
140	139	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ)
141	77	ineq2d 4171	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))))
142	141	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))))
143	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))))
144	143	iuneq2i 4963	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
145		iunin2 5020	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
146	144, 145	eqtri 2752	. . . . . . . . . . . 12 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
147	142, 146	eqtr4di 2782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
148		fzfid 13880	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin)
149		ffvelcdm 7015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
150	13, 73, 149	syl2an 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
151	150	elin2d 4156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ (ℝ × ℝ))
152		1st2nd2 7963	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑖) ∈ (ℝ × ℝ) → (𝐹‘𝑖) = ⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
153	151, 152	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) = ⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
154	153	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((,)‘⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩))
155		df-ov 7352	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))) = ((,)‘⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
156	154, 155	eqtr4di 2782	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))))
157		ioombl 25464	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))) ∈ dom vol
158	156, 157	eqeltrdi 2836	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol)
159	158	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol)
160		ffvelcdm 7015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
161	6, 90, 160	syl2an 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
162	161	elin2d 4156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
163		1st2nd2 7963	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
165	164	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩))
166		df-ov 7352	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
167	165, 166	eqtr4di 2782	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))))
168		ioombl 25464	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ∈ dom vol
169	167, 168	eqeltrdi 2836	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol)
170	169	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol)
171		inmbl 25441	. . . . . . . . . . . . . 14 ⊢ ((((,)‘(𝐹‘𝑖)) ∈ dom vol ∧ ((,)‘(𝐺‘𝑗)) ∈ dom vol) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
172	159, 170, 171	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
173	172	ralrimiva 3121	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
174		finiunmbl 25443	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
175	148, 173, 174	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
176	147, 175	eqeltrd 2828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol)
177		inss2 4189	. . . . . . . . . . 11 ⊢ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ 𝐴
178	13	uniiccdif 25477	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹) ∧ (vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran ((,) ∘ 𝐹))) = 0))
179	178	simpld 494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹))
180		ovolficcss 25368	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
181	13, 180	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
182	179, 181	sstrd 3946	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
183	16, 182	eqsstrid 3974	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
184	183	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ)
185	177, 184	sstrid 3947	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ)
186		inss1 4188	. . . . . . . . . . 11 ⊢ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗))
187		ioossre 13310	. . . . . . . . . . . 12 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ⊆ ℝ
188	167, 187	eqsstrdi 3980	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
189	167	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((,)‘(𝐺‘𝑗))) = (vol‘((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗)))))
190		ovolfcl 25365	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
191	6, 90, 190	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
192		ovolioo 25467	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))) → (vol*‘((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗)))) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
193	191, 192	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗)))) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
194	189, 193	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
195	191	simp2d 1143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
196	191	simp1d 1142	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
197	195, 196	resubcld 11548	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
198	194, 197	eqeltrd 2828	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)
199		ovolsscl 25385	. . . . . . . . . . 11 ⊢ (((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧ (vol‘((,)‘(𝐺‘𝑗))) ∈ ℝ) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ)
200	186, 188, 198, 199	mp3an2i 1468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ)
201		mblsplit 25431	. . . . . . . . . 10 ⊢ (((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ ∧ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))))
202	176, 185, 200, 201	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))))
203		imassrn 6022	. . . . . . . . . . . . . . 15 ⊢ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
204	203	unissi 4867	. . . . . . . . . . . . . 14 ⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ∪ ran ((,) ∘ 𝐹)
205	204, 69, 16	3sstr4i 3987	. . . . . . . . . . . . 13 ⊢ 𝐿 ⊆ 𝐴
206		sslin 4194	. . . . . . . . . . . . 13 ⊢ (𝐿 ⊆ 𝐴 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴))
207	205, 206	mp1i 13	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴))
208		sseqin2 4174	. . . . . . . . . . . 12 ⊢ ((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
209	207, 208	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
210	209	fveq2d 6826	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)))
211		indifdir 4246	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗))))
212		incom 4160	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐴)
213		incom 4160	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿)
214	212, 213	difeq12i 4075	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗)))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
215	211, 214	eqtri 2752	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
216	79	eqcomd 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴)
217	77	ineq1d 4170	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
218		2fveq3 6827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑖 → ((,)‘(𝐹‘𝑥)) = ((,)‘(𝐹‘𝑖)))
219	218	cbvdisjv 5070	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
220	14, 219	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
221		fz1ssnn 13458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ⊆ ℕ
222	221	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
223		uzss 12758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘(𝑁 + 1)) ⊆ (ℤ_≥‘1))
224	39, 223	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ⊆ (ℤ_≥‘1))
225	224, 36	sseqtrrdi 3977	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ⊆ ℕ)
226	47	ineq1d 4170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))))
227		uzdisj 13500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅
228	226, 227	eqtr3di 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)
229		disjiun 5080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧ (ℤ_≥‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)) → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
230	220, 222, 225, 228, 229	syl13anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
231	217, 230	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
232		uneqdifeq 4444	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ⊆ 𝐴 ∧ (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) → ((𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
233	205, 231, 232	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
234	216, 233	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
235	234	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
236	235	ineq2d 4171	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
237		incom 4160	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿))
238	101, 98	eqtri 2752	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
239	236, 237, 238	3eqtr4g 2789	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
240	215, 239	eqtr3id 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
241	240	fveq2d 6826	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
242	210, 241	oveq12d 7367	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))) = ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
243	202, 242	eqtrd 2764	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
244	200, 140	resubcld 11548	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ)
245		inss2 4189	. . . . . . . . . . . . 13 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗))
246	188	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
247	198	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)
248		ovolsscl 25385	. . . . . . . . . . . . 13 ⊢ (((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧ (vol‘((,)‘(𝐺‘𝑗))) ∈ ℝ) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
249	245, 246, 247, 248	mp3an2i 1468	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
250	148, 249	fsumrecl 15641	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
251		uniioombl.n2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
252	251	r19.21bi 3221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
253	250, 200, 140	absdifltd 15343	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀) ↔ (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀)))))
254	252, 253	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀))))
255	254	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
256	244, 250, 255	ltled 11264	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
257	147	fveq2d 6826	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
258		mblvol 25429	. . . . . . . . . . . . . . . . 17 ⊢ ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
259	172, 258	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
260	259, 249	eqeltrd 2828	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
261	172, 260	jca 511	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
262	261	ralrimiva 3121	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
263		inss1 4188	. . . . . . . . . . . . . . . 16 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖))
264	263	rgenw 3048	. . . . . . . . . . . . . . 15 ⊢ ∀𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖))
265	220	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
266		disjss2 5062	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
267	264, 265, 266	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
268		disjss1 5065	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ⊆ ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
269	221, 267, 268	mpsyl 68	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
270		volfiniun 25446	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
271	148, 262, 269, 270	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
272		mblvol 25429	. . . . . . . . . . . . 13 ⊢ (∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
273	175, 272	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
274	259	sumeq2dv 15609	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
275	271, 273, 274	3eqtr3d 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
276	257, 275	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
277	256, 276	breqtrrd 5120	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)))
278	276, 250	eqeltrd 2828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ∈ ℝ)
279	200, 140, 278	lesubaddd 11717	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ↔ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
280	277, 279	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
281	243, 280	eqbrtrrd 5116	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
282	131, 140, 278	leadd2d 11715	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
283	281, 282	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀))
284	124, 131, 140, 283	fsumle 15706	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀))
285	139	recnd 11143	. . . . . . 7 ⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℂ)
286		fsumconst 15697	. . . . . . 7 ⊢ (((1...𝑀) ∈ Fin ∧ (𝐶 / 𝑀) ∈ ℂ) → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
287	124, 285, 286	syl2anc 584	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
288		nnnn0 12391	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
289		hashfz1 14253	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
290	138, 288, 289	3syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
291	290	oveq1d 7364	. . . . . 6 ⊢ (𝜑 → ((♯‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀)))
292	116	recnd 11143	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
293	138	nncnd 12144	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
294	138	nnne0d 12178	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
295	292, 293, 294	divcan2d 11902	. . . . . 6 ⊢ (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶)
296	287, 291, 295	3eqtrd 2768	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶)
297	284, 296	breqtrd 5118	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶)
298	114, 132, 116, 137, 297	letrd 11273	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶)
299	114, 116, 34, 298	leadd2dd 11735	. 2 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐿)) + (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶))
300	31, 115, 117, 123, 299	letrd 11273	1 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ∅c0 4284 𝒫 cpw 4551 ⟨cop 4583 ∪ cuni 4858 ∪ ciun 4941 Disj wdisj 5059 class class class wbr 5092 × cxp 5617 dom cdm 5619 ran crn 5620 “ cima 5622 ∘ ccom 5623 Fun wfun 6476 Fn wfn 6477 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 1^st c1st 7922 2^nd c2nd 7923 Fincfn 8872 supcsup 9330 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 ℝ^*cxr 11148 < clt 11149 ≤ cle 11150 − cmin 11347 / cdiv 11777 ℕcn 12128 ℕ₀cn0 12384 ℤ_≥cuz 12735 ℝ⁺crp 12893 (,)cioo 13248 [,]cicc 13251 ...cfz 13410 seqcseq 13908 ♯chash 14237 abscabs 15141 Σcsu 15593 vol*covol 25361 volcvol 25362

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-inf2 9537 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-disj 5060 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-map 8755 df-pm 8756 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-dju 9797 df-card 9835 df-acn 9838 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-n0 12385 df-z 12472 df-uz 12736 df-q 12850 df-rp 12894 df-xneg 13014 df-xadd 13015 df-xmul 13016 df-ioo 13252 df-ico 13254 df-icc 13255 df-fz 13411 df-fzo 13558 df-fl 13696 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-rlim 15396 df-sum 15594 df-rest 17326 df-topgen 17347 df-psmet 21253 df-xmet 21254 df-met 21255 df-bl 21256 df-mopn 21257 df-top 22779 df-topon 22796 df-bases 22831 df-cmp 23272 df-ovol 25363 df-vol 25364

This theorem is referenced by: uniioombllem5 25486

W3C validator