uniioombllem3 - Metamath Proof Explorer

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

Theorem uniioombllem3 25649

Description: Lemma for uniioombl 25653. (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...𝑀))

**Assertion**
Ref	Expression
uniioombllem3	⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))

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

Proof of Theorem uniioombllem3 Dummy variables 𝑗 𝑘 𝑛 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 4190	. . . . 5 ⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸
2	1	a1i 11	. . . 4 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸)
3		uniioombl.s	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))
4		uniioombl.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	uniiccdif 25642	. . . . . . 7 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
6	5	simpld 498	. . . . . 6 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
7		ovolficcss 25533	. . . . . . 7 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
8	4, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
9	6, 8	sstrd 3948	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
10	3, 9	sstrd 3948	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
11		uniioombl.e	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
12		ovolsscl 25550	. . . 4 ⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∩ 𝐴)) ∈ ℝ)
13	2, 10, 11, 12	syl3anc 1392	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ)
14		difssd 4092	. . . 4 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸)
15		ovolsscl 25550	. . . 4 ⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∖ 𝐴)) ∈ ℝ)
16	14, 10, 11, 15	syl3anc 1392	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ)
17		inss1 4190	. . . . . 6 ⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾
18	17	a1i 11	. . . . 5 ⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ 𝐾)
19		uniioombl.1	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
20		uniioombl.2	. . . . . . . 8 ⊢ (𝜑 → Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)))
21		uniioombl.3	. . . . . . . 8 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
22		uniioombl.a	. . . . . . . 8 ⊢ 𝐴 = ∪ ran ((,) ∘ 𝐹)
23		uniioombl.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
24		uniioombl.t	. . . . . . . 8 ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
25		uniioombl.v	. . . . . . . 8 ⊢ (𝜑 → sup(ran 𝑇, ℝ^, < ) ≤ ((vol‘𝐸) + 𝐶))
26		uniioombl.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
27		uniioombl.m2	. . . . . . . 8 ⊢ (𝜑 → (abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ^*, < ))) < 𝐶)
28		uniioombl.k	. . . . . . . 8 ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))
29	19, 20, 21, 22, 11, 23, 4, 3, 24, 25, 26, 27, 28	uniioombllem3a 25648	. . . . . . 7 ⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ))
30	29	simpld 498	. . . . . 6 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
31		inss2 4191	. . . . . . . . . . . . 13 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
32		elfznn 13560	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
33		ffvelcdm 7064	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
34	4, 32, 33	syl2an 605	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
35	31, 34	sselid 3936	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
36		1st2nd2 8011	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
38	37	fveq2d 6873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩))
39		df-ov 7401	. . . . . . . . . 10 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
40	38, 39	eqtr4di 2817	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))))
41		ioossre 13413	. . . . . . . . 9 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ⊆ ℝ
42	40, 41	eqsstrdi 3982	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
43	42	ralrimiva 3156	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
44		iunss 5004	. . . . . . 7 ⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
45	43, 44	sylibr 236	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
46	30, 45	eqsstrd 3972	. . . . 5 ⊢ (𝜑 → 𝐾 ⊆ ℝ)
47	29	simprd 499	. . . . 5 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
48		ovolsscl 25550	. . . . 5 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ)
49	18, 46, 47, 48	syl3anc 1392	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
50	23	rpred 13039	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
51	49, 50	readdcld 11213	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ)
52		difssd 4092	. . . . 5 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾)
53		ovolsscl 25550	. . . . 5 ⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∖ 𝐴)) ∈ ℝ)
54	52, 46, 47, 53	syl3anc 1392	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ)
55	54, 50	readdcld 11213	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ)
56		ssun2 4133	. . . . . . 7 ⊢ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
57		ioof 13453	. . . . . . . . . . . . . . 15 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
58		rexpssxrxp 11229	. . . . . . . . . . . . . . . . 17 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
59	31, 58	sstri 3947	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
60		fss 6710	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐺:ℕ⟶(ℝ^ × ℝ^*))
61	4, 59, 60	sylancl 595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ^* × ℝ^*))
62		fco 6718	. . . . . . . . . . . . . . 15 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
63	57, 61, 62	sylancr 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
64	63	ffnd 6694	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
65		fnima 6653	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺) Fn ℕ → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
66	64, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
67		nnuz 12880	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
68	26	peano2nnd 12229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
69	68, 67	eleqtrdi 2874	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
70		uzsplit 13603	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
71	69, 70	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℤ_≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
72	67, 71	eqtrid 2811	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
73	26	nncnd 12228	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
74		ax-1cn 11133	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
75		pncan 11438	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
76	73, 74, 75	sylancl 595	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
77	76	oveq2d 7414	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀))
78	77	uneq1d 4122	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1))))
79	72, 78	eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1))))
80	79	imaeq2d 6051	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))))
81	66, 80	eqtr3d 2801	. . . . . . . . . . 11 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))))
82		imaundi 6136	. . . . . . . . . . 11 ⊢ (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
83	81, 82	eqtrdi 2815	. . . . . . . . . 10 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
84	83	unieqd 4880	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
85		uniun 4890	. . . . . . . . 9 ⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
86	84, 85	eqtrdi 2815	. . . . . . . 8 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
87	28	uneq1i 4119	. . . . . . . 8 ⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
88	86, 87	eqtr4di 2817	. . . . . . 7 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
89	56, 88	sseqtrrid 3981	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺))
90	19, 20, 21, 22, 11, 23, 4, 3, 24, 25	uniioombllem1 25645	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
91		ssid 3960	. . . . . . . 8 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
92	24	ovollb 25543	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
93	4, 91, 92	sylancl 595	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
94		ovollecl 25547	. . . . . . 7 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ^, < ) ∈ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < )) → (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
95	9, 90, 93, 94	syl3anc 1392	. . . . . 6 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
96		ovolsscl 25550	. . . . . 6 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)
97	89, 9, 95, 96	syl3anc 1392	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)
98	49, 97	readdcld 11213	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
99		unss1 4139	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
100	17, 99	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
101	100, 88	sseqtrrid 3981	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
102		ovolsscl 25550	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
103	101, 9, 95, 102	syl3anc 1392	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
104	3, 88	sseqtrd 3974	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
105	104	ssrind 4197	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴))
106		indir 4240	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴))
107		inss1 4190	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))
108		unss2 4141	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
109	107, 108	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
110	106, 109	eqsstri 3984	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
111	105, 110	sstrdi 3950	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
112	101, 9	sstrd 3948	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ)
113		ovolss 25549	. . . . . 6 ⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol‘(𝐸 ∩ 𝐴)) ≤ (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
114	111, 112, 113	syl2anc 593	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) ≤ (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
115	18, 46	sstrd 3948	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ)
116	89, 9	sstrd 3948	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ)
117		ovolun 25563	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
118	115, 49, 116, 97, 117	syl22anc 849	. . . . 5 ⊢ (𝜑 → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
119	13, 103, 98, 114, 118	letrd 11342	. . . 4 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
120		rge0ssre 13462	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
121		eqid 2764	. . . . . . . . . . 11 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
122	121, 24	ovolsf 25536	. . . . . . . . . 10 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
123	4, 122	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
124	123, 26	ffvelcdmd 7068	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞))
125	120, 124	sselid 3936	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ)
126	90, 125	resubcld 11617	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)) ∈ ℝ)
127	97	rexrd 11234	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ^)
128		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
129		nnaddcl 12235	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
130	128, 26, 129	syl2anr 606	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
131	4	ffvelcdmda 7067	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
132	130, 131	syldan 600	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
133	132	fmpttd 7098	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
134		eqid 2764	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
135		eqid 2764	. . . . . . . . . . . 12 ⊢ seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
136	134, 135	ovolsf 25536	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
137	133, 136	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
138	137	frnd 6702	. . . . . . . . 9 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ (0[,)+∞))
139		icossxr 13438	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ^*
140	138, 139	sstrdi 3950	. . . . . . . 8 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^*)
141		supxrcl 13320	. . . . . . . 8 ⊢ (ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^* → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ∈ ℝ^)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ∈ ℝ^)
143	126	rexrd 11234	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ∈ ℝ^)
144		1zzd 12604	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 1 ∈ ℤ)
145	26	nnzd 12596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℤ)
146	145	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ)
147		addcom 11371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + 1) = (1 + 𝑀))
148	73, 74, 147	sylancl 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀))
149	148	fveq2d 6873	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) = (ℤ_≥‘(1 + 𝑀)))
150	149	eleq2d 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ_≥‘(1 + 𝑀))))
151	150	biimpa 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ_≥‘(1 + 𝑀)))
152		eluzsub 12871	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ (ℤ_≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈ (ℤ_≥‘1))
153	144, 146, 151, 152	syl3anc 1392	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ (ℤ_≥‘1))
154	153, 67	eleqtrrdi 2875	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ)
155		eluzelz 12851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ)
156	155	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ℤ)
157	156	zcnd 12680	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ℂ)
158	73	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ)
159	157, 158	npcand 11548	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
160	159	eqcomd 2770	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀))
161		oveq1 7405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
162	161	rspceeqv 3606	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
163	154, 160, 162	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
164		eqid 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))
165	164	elrnmpt 5936	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)))
166	165	elv 3461	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
167	163, 166	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
168	167	ex 416	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
169	168	ssrdv 3944	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
170		imass2 6093	. . . . . . . . . . . . 13 ⊢ ((ℤ_≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
171	169, 170	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
172		rnco2 6243	. . . . . . . . . . . . 13 ⊢ ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
173	4, 130	cofmpt 7116	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
174	173	rneqd 5916	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
175	172, 174	eqtr3id 2813	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
176	171, 175	sseqtrd 3974	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
177		imass2 6093	. . . . . . . . . . 11 ⊢ ((𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
178	176, 177	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
179		imaco 6240	. . . . . . . . . 10 ⊢ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) = ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1))))
180		rnco2 6243	. . . . . . . . . 10 ⊢ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
181	178, 179, 180	3sstr4g 3991	. . . . . . . . 9 ⊢ (𝜑 → (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
182	181	unissd 4877	. . . . . . . 8 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
183	135	ovollb 25543	. . . . . . . 8 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ))
184	133, 182, 183	syl2anc 593	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ))
185	123	frnd 6702	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
186	185, 139	sstrdi 3950	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
187	24	fveq1i 6870	. . . . . . . . . . . . . 14 ⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛))
188	26	nnred 12227	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ)
189	188	ltp1d 12124	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
190		fzdisj 13558	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
191	189, 190	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
192	191	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
193		nnnn0 12490	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
194		nn0addge1 12529	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → 𝑀 ≤ (𝑀 + 𝑛))
195	188, 193, 194	syl2an 605	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛))
196	26	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ)
197	196, 67	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (ℤ_≥‘1))
198		nnaddcl 12235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
199	26, 198	sylan 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
200	199	nnzd 12596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ)
201		elfz5 13523	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ (ℤ_≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
202	197, 200, 201	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
203	195, 202	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛)))
204		fzsplit 13557	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
205	203, 204	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
206		fzfid 13988	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin)
207	4	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
208		elfznn 13560	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ)
209		ovolfcl 25530	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
210	207, 208, 209	syl2an 605	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
211	210	simp2d 1157	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
212	210	simp1d 1156	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
213	211, 212	resubcld 11617	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
214	213	recnd 11212	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
215	192, 205, 206, 214	fsumsplit 15770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗)))))
216	121	ovolfsval 25534	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
217	207, 208, 216	syl2an 605	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
218	199, 67	eleqtrdi 2874	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ (ℤ_≥‘1))
219	217, 218, 214	fsumser 15759	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)))
220	4	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
221	32	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
222	220, 221, 216	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
223	4, 32, 209	syl2an 605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
224	223	simp2d 1157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
225	223	simp1d 1156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
226	224, 225	resubcld 11617	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
227	226	adantlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
228	227	recnd 11212	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
229	222, 197, 228	fsumser 15759	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀))
230	24	fveq1i 6870	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀)
231	229, 230	eqtr4di 2817	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (𝑇‘𝑀))
232	196	nnzd 12596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ)
233	232	peano2zd 12682	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
234	4	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
235	196	peano2nnd 12229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ)
236		elfzuz 13527	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ_≥‘(𝑀 + 1)))
237		eluznn 12921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ)
238	235, 236, 237	syl2an 605	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ)
239	234, 238, 209	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
240	239	simp2d 1157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
241	239	simp1d 1156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
242	240, 241	resubcld 11617	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
243	242	recnd 11212	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
244		2fveq3 6874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (2^nd ‘(𝐺‘𝑗)) = (2^nd ‘(𝐺‘(𝑘 + 𝑀))))
245		2fveq3 6874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (1^st ‘(𝐺‘𝑗)) = (1^st ‘(𝐺‘(𝑘 + 𝑀))))
246	244, 245	oveq12d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑘 + 𝑀) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
247	232, 233, 200, 243, 246	fsumshftm 15810	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
248	196	nncnd 12228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ)
249		pncan2 11439	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 𝑀) = 1)
250	248, 74, 249	sylancl 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1)
251		nncn 12220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
252	251	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
253	248, 252	pncan2d 11546	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛)
254	250, 253	oveq12d 7416	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛))
255	254	sumeq1d 15729	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
256	133	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
257		elfznn 13560	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
258	134	ovolfsval 25534	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
259	256, 257, 258	syl2an 605	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
260	257	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
261		fvoveq1 7421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀)))
262		eqid 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))
263		fvex 6882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V
264	261, 262, 263	fvmpt 6977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
265	260, 264	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
266	265	fveq2d 6873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2^nd ‘(𝐺‘(𝑘 + 𝑀))))
267	265	fveq2d 6873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1^st ‘(𝐺‘(𝑘 + 𝑀))))
268	266, 267	oveq12d 7416	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
269	259, 268	eqtrd 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
270		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
271	270, 67	eleqtrdi 2874	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
272	4	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
273		nnaddcl 12235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ)
274	257, 196, 273	syl2anr 606	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ)
275		ovolfcl 25530	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1^st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2^nd ‘(𝐺‘(𝑘 + 𝑀)))))
276	272, 274, 275	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1^st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2^nd ‘(𝐺‘(𝑘 + 𝑀)))))
277	276	simp2d 1157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
278	276	simp1d 1156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
279	277, 278	resubcld 11617	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ)
280	279	recnd 11212	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ)
281	269, 271, 280	fsumser 15759	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
282	247, 255, 281	3eqtrd 2803	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
283	231, 282	oveq12d 7416	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
284	215, 219, 283	3eqtr3d 2807	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
285	187, 284	eqtrid 2811	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
286	123	ffnd 6694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn ℕ)
287		fnfvelrn 7063	. . . . . . . . . . . . . 14 ⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
288	286, 199, 287	syl2an2r 695	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
289	285, 288	eqeltrrd 2865	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇)
290		supxrub 13329	. . . . . . . . . . . 12 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^*, < ))
291	186, 289, 290	syl2an2r 695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^*, < ))
292	125	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ)
293	137	ffvelcdmda 7067	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞))
294	120, 293	sselid 3936	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ)
295	90	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
296	292, 294, 295	leaddsub2d 11791	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^, < ) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
297	291, 296	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
298	297	ralrimiva 3156	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
299	137	ffnd 6694	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ)
300		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
301	300	ralrn 7071	. . . . . . . . . 10 ⊢ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ → (∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
302	299, 301	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
303	298, 302	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
304		supxrleub 13331	. . . . . . . . 9 ⊢ ((ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^* ∧ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ∈ ℝ^) → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀))))
305	140, 143, 304	syl2anc 593	. . . . . . . 8 ⊢ (𝜑 → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀))))
306	303, 305	mpbird 259	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)))
307	127, 142, 143, 184, 306	xrletrd 13166	. . . . . 6 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)))
308	125, 90, 50	absdifltd 15465	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ^, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ^, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ^*, < ) + 𝐶))))
309	27, 308	mpbid 234	. . . . . . . 8 ⊢ (𝜑 → ((sup(ran 𝑇, ℝ^, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ^, < ) + 𝐶)))
310	309	simpld 498	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − 𝐶) < (𝑇‘𝑀))
311	90, 50, 125, 310	ltsub23d 11794	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)) < 𝐶)
312	97, 126, 50, 307, 311	lelttrd 11343	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) < 𝐶)
313	97, 50, 49, 312	ltadd2dd 11344	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶))
314	13, 98, 51, 119, 313	lelttrd 11343	. . 3 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) < ((vol‘(𝐾 ∩ 𝐴)) + 𝐶))
315	54, 97	readdcld 11213	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∖ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
316		difss 4091	. . . . . . . 8 ⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾
317		unss1 4139	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
318	316, 317	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
319	318, 88	sseqtrrid 3981	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
320		ovolsscl 25550	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
321	319, 9, 95, 320	syl3anc 1392	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
322	104	ssdifd 4100	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴))
323		difundir 4245	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴))
324		difss 4091	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))
325		unss2 4141	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
326	324, 325	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
327	323, 326	eqsstri 3984	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
328	322, 327	sstrdi 3950	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
329	319, 9	sstrd 3948	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ)
330		ovolss 25549	. . . . . 6 ⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol‘(𝐸 ∖ 𝐴)) ≤ (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
331	328, 329, 330	syl2anc 593	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) ≤ (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
332	52, 46	sstrd 3948	. . . . . 6 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ)
333		ovolun 25563	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
334	332, 54, 116, 97, 333	syl22anc 849	. . . . 5 ⊢ (𝜑 → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
335	16, 321, 315, 331, 334	letrd 11342	. . . 4 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
336	97, 50, 54, 312	ltadd2dd 11344	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∖ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))
337	16, 315, 55, 335, 336	lelttrd 11343	. . 3 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) < ((vol‘(𝐾 ∖ 𝐴)) + 𝐶))
338	13, 16, 51, 55, 314, 337	lt2addd 11812	. 2 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol‘(𝐾 ∖ 𝐴)) + 𝐶)))
339	49	recnd 11212	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ)
340	50	recnd 11212	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
341	54	recnd 11212	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ)
342	339, 340, 341, 340	add4d 11414	. 2 ⊢ (𝜑 → (((vol‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))
343	338, 342	breqtrd 5128	1 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1099 = wceq 1562 ∈ wcel 2144 ∀wral 3078 ∃wrex 3088 Vcvv 3456 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 𝒫 cpw 4557 ⟨cop 4590 ∪ cuni 4867 ∪ ciun 4951 Disj wdisj 5069 class class class wbr 5102 ↦ cmpt 5183 × cxp 5647 ran crn 5650 “ cima 5652 ∘ ccom 5653 Fn wfn 6518 ⟶wf 6519 ‘cfv 6523 (class class class)co 7398 1^st c1st 7970 2^nd c2nd 7971 supcsup 9388 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 +∞cpnf 11215 ℝ^*cxr 11217 < clt 11218 ≤ cle 11219 − cmin 11416 ℕcn 12212 ℕ₀cn0 12483 ℤcz 12570 ℤ_≥cuz 12841 ℝ⁺crp 12995 (,)cioo 13351 [,)cico 13353 [,]cicc 13354 ...cfz 13514 seqcseq 14016 abscabs 15263 Σcsu 15715 vol*covol 25526

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720 ax-inf2 9598 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-se 5603 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-isom 6532 df-riota 7355 df-ov 7401 df-oprab 7402 df-mpo 7403 df-of 7662 df-om 7849 df-1st 7972 df-2nd 7973 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-1o 8439 df-2o 8440 df-er 8680 df-map 8812 df-pm 8813 df-en 8930 df-dom 8931 df-sdom 8932 df-fin 8933 df-fi 9359 df-sup 9390 df-inf 9391 df-oi 9460 df-dju 9861 df-card 9899 df-acn 9902 df-pnf 11220 df-mnf 11221 df-xr 11222 df-ltxr 11223 df-le 11224 df-sub 11418 df-neg 11419 df-div 11847 df-nn 12213 df-2 12282 df-3 12283 df-n0 12484 df-z 12571 df-uz 12842 df-q 12952 df-rp 12996 df-xneg 13116 df-xadd 13117 df-xmul 13118 df-ioo 13355 df-ico 13357 df-icc 13358 df-fz 13515 df-fzo 13662 df-fl 13804 df-seq 14017 df-exp 14077 df-hash 14346 df-cj 15128 df-re 15129 df-im 15130 df-sqrt 15264 df-abs 15265 df-clim 15517 df-rlim 15518 df-sum 15716 df-rest 17453 df-topgen 17474 df-psmet 21418 df-xmet 21419 df-met 21420 df-bl 21421 df-mopn 21422 df-top 22956 df-topon 22973 df-bases 23008 df-cmp 23449 df-ovol 25528 df-vol 25529

This theorem is referenced by: uniioombllem5 25651

W3C validator