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 25101

Description: Lemma for uniioombl 25105. (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 4228	. . . . 5 ⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸
2	1	a1i 11	. . . 4 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸)
3		uniioombl.s	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))
4		uniioombl.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	uniiccdif 25094	. . . . . . 7 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
6	5	simpld 495	. . . . . 6 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
7		ovolficcss 24985	. . . . . . 7 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
8	4, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
9	6, 8	sstrd 3992	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
10	3, 9	sstrd 3992	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
11		uniioombl.e	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
12		ovolsscl 25002	. . . 4 ⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∩ 𝐴)) ∈ ℝ)
13	2, 10, 11, 12	syl3anc 1371	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ)
14		difssd 4132	. . . 4 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸)
15		ovolsscl 25002	. . . 4 ⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∖ 𝐴)) ∈ ℝ)
16	14, 10, 11, 15	syl3anc 1371	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ)
17		inss1 4228	. . . . . 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 25100	. . . . . . 7 ⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ))
30	29	simpld 495	. . . . . 6 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
31		inss2 4229	. . . . . . . . . . . . 13 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
32		elfznn 13529	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
33		ffvelcdm 7083	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
34	4, 32, 33	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
35	31, 34	sselid 3980	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
36		1st2nd2 8013	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
38	37	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩))
39		df-ov 7411	. . . . . . . . . 10 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
40	38, 39	eqtr4di 2790	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))))
41		ioossre 13384	. . . . . . . . 9 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ⊆ ℝ
42	40, 41	eqsstrdi 4036	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
43	42	ralrimiva 3146	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
44		iunss 5048	. . . . . . 7 ⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
45	43, 44	sylibr 233	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
46	30, 45	eqsstrd 4020	. . . . 5 ⊢ (𝜑 → 𝐾 ⊆ ℝ)
47	29	simprd 496	. . . . 5 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
48		ovolsscl 25002	. . . . 5 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ)
49	18, 46, 47, 48	syl3anc 1371	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
50	23	rpred 13015	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
51	49, 50	readdcld 11242	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ)
52		difssd 4132	. . . . 5 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾)
53		ovolsscl 25002	. . . . 5 ⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∖ 𝐴)) ∈ ℝ)
54	52, 46, 47, 53	syl3anc 1371	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ)
55	54, 50	readdcld 11242	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ)
56		ssun2 4173	. . . . . . 7 ⊢ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
57		ioof 13423	. . . . . . . . . . . . . . 15 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
58		rexpssxrxp 11258	. . . . . . . . . . . . . . . . 17 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
59	31, 58	sstri 3991	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
60		fss 6734	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐺:ℕ⟶(ℝ^ × ℝ^*))
61	4, 59, 60	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ^* × ℝ^*))
62		fco 6741	. . . . . . . . . . . . . . 15 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
63	57, 61, 62	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
64	63	ffnd 6718	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
65		fnima 6680	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺) Fn ℕ → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
66	64, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
67		nnuz 12864	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
68	26	peano2nnd 12228	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
69	68, 67	eleqtrdi 2843	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
70		uzsplit 13572	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
71	69, 70	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℤ_≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
72	67, 71	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
73	26	nncnd 12227	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
74		ax-1cn 11167	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
75		pncan 11465	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
76	73, 74, 75	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
77	76	oveq2d 7424	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀))
78	77	uneq1d 4162	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1))))
79	72, 78	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1))))
80	79	imaeq2d 6059	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))))
81	66, 80	eqtr3d 2774	. . . . . . . . . . 11 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))))
82		imaundi 6149	. . . . . . . . . . 11 ⊢ (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
83	81, 82	eqtrdi 2788	. . . . . . . . . 10 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
84	83	unieqd 4922	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
85		uniun 4934	. . . . . . . . 9 ⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
86	84, 85	eqtrdi 2788	. . . . . . . 8 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
87	28	uneq1i 4159	. . . . . . . 8 ⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
88	86, 87	eqtr4di 2790	. . . . . . 7 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
89	56, 88	sseqtrrid 4035	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺))
90	19, 20, 21, 22, 11, 23, 4, 3, 24, 25	uniioombllem1 25097	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
91		ssid 4004	. . . . . . . 8 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
92	24	ovollb 24995	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
93	4, 91, 92	sylancl 586	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
94		ovollecl 24999	. . . . . . 7 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ^, < ) ∈ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < )) → (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
95	9, 90, 93, 94	syl3anc 1371	. . . . . 6 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
96		ovolsscl 25002	. . . . . 6 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)
97	89, 9, 95, 96	syl3anc 1371	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)
98	49, 97	readdcld 11242	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
99		unss1 4179	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
100	17, 99	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
101	100, 88	sseqtrrid 4035	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
102		ovolsscl 25002	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
103	101, 9, 95, 102	syl3anc 1371	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
104	3, 88	sseqtrd 4022	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
105	104	ssrind 4235	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴))
106		indir 4275	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴))
107		inss1 4228	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))
108		unss2 4181	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
109	107, 108	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
110	106, 109	eqsstri 4016	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
111	105, 110	sstrdi 3994	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
112	101, 9	sstrd 3992	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ)
113		ovolss 25001	. . . . . 6 ⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol‘(𝐸 ∩ 𝐴)) ≤ (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
114	111, 112, 113	syl2anc 584	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) ≤ (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
115	18, 46	sstrd 3992	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ)
116	89, 9	sstrd 3992	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ)
117		ovolun 25015	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
118	115, 49, 116, 97, 117	syl22anc 837	. . . . 5 ⊢ (𝜑 → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
119	13, 103, 98, 114, 118	letrd 11370	. . . 4 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
120		rge0ssre 13432	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
121		eqid 2732	. . . . . . . . . . 11 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
122	121, 24	ovolsf 24988	. . . . . . . . . 10 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
123	4, 122	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
124	123, 26	ffvelcdmd 7087	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞))
125	120, 124	sselid 3980	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ)
126	90, 125	resubcld 11641	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)) ∈ ℝ)
127	97	rexrd 11263	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ^)
128		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
129		nnaddcl 12234	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
130	128, 26, 129	syl2anr 597	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
131	4	ffvelcdmda 7086	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
132	130, 131	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
133	132	fmpttd 7114	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
134		eqid 2732	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
135		eqid 2732	. . . . . . . . . . . 12 ⊢ seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
136	134, 135	ovolsf 24988	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
137	133, 136	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
138	137	frnd 6725	. . . . . . . . 9 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ (0[,)+∞))
139		icossxr 13408	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ^*
140	138, 139	sstrdi 3994	. . . . . . . 8 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^*)
141		supxrcl 13293	. . . . . . . 8 ⊢ (ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^* → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ∈ ℝ^)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ∈ ℝ^)
143	126	rexrd 11263	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ∈ ℝ^)
144		1zzd 12592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 1 ∈ ℤ)
145	26	nnzd 12584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℤ)
146	145	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ)
147		addcom 11399	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + 1) = (1 + 𝑀))
148	73, 74, 147	sylancl 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀))
149	148	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) = (ℤ_≥‘(1 + 𝑀)))
150	149	eleq2d 2819	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ_≥‘(1 + 𝑀))))
151	150	biimpa 477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ_≥‘(1 + 𝑀)))
152		eluzsub 12851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ (ℤ_≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈ (ℤ_≥‘1))
153	144, 146, 151, 152	syl3anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ (ℤ_≥‘1))
154	153, 67	eleqtrrdi 2844	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ)
155		eluzelz 12831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ)
156	155	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ℤ)
157	156	zcnd 12666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ℂ)
158	73	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ)
159	157, 158	npcand 11574	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
160	159	eqcomd 2738	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀))
161		oveq1 7415	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
162	161	rspceeqv 3633	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
163	154, 160, 162	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
164		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))
165	164	elrnmpt 5955	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)))
166	165	elv 3480	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
167	163, 166	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
168	167	ex 413	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
169	168	ssrdv 3988	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
170		imass2 6101	. . . . . . . . . . . . 13 ⊢ ((ℤ_≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
171	169, 170	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
172		rnco2 6252	. . . . . . . . . . . . 13 ⊢ ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
173	4, 130	cofmpt 7129	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
174	173	rneqd 5937	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
175	172, 174	eqtr3id 2786	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
176	171, 175	sseqtrd 4022	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
177		imass2 6101	. . . . . . . . . . 11 ⊢ ((𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
178	176, 177	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
179		imaco 6250	. . . . . . . . . 10 ⊢ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) = ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1))))
180		rnco2 6252	. . . . . . . . . 10 ⊢ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
181	178, 179, 180	3sstr4g 4027	. . . . . . . . 9 ⊢ (𝜑 → (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
182	181	unissd 4918	. . . . . . . 8 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
183	135	ovollb 24995	. . . . . . . 8 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ))
184	133, 182, 183	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ))
185	123	frnd 6725	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
186	185, 139	sstrdi 3994	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
187	24	fveq1i 6892	. . . . . . . . . . . . . 14 ⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛))
188	26	nnred 12226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ)
189	188	ltp1d 12143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
190		fzdisj 13527	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
191	189, 190	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
192	191	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
193		nnnn0 12478	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
194		nn0addge1 12517	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → 𝑀 ≤ (𝑀 + 𝑛))
195	188, 193, 194	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛))
196	26	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ)
197	196, 67	eleqtrdi 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (ℤ_≥‘1))
198		nnaddcl 12234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
199	26, 198	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
200	199	nnzd 12584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ)
201		elfz5 13492	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ (ℤ_≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
202	197, 200, 201	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
203	195, 202	mpbird 256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛)))
204		fzsplit 13526	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
205	203, 204	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
206		fzfid 13937	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin)
207	4	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
208		elfznn 13529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ)
209		ovolfcl 24982	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
210	207, 208, 209	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
211	210	simp2d 1143	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
212	210	simp1d 1142	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
213	211, 212	resubcld 11641	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
214	213	recnd 11241	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
215	192, 205, 206, 214	fsumsplit 15686	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗)))))
216	121	ovolfsval 24986	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
217	207, 208, 216	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
218	199, 67	eleqtrdi 2843	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ (ℤ_≥‘1))
219	217, 218, 214	fsumser 15675	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)))
220	4	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
221	32	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
222	220, 221, 216	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
223	4, 32, 209	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
224	223	simp2d 1143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
225	223	simp1d 1142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
226	224, 225	resubcld 11641	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
227	226	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
228	227	recnd 11241	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
229	222, 197, 228	fsumser 15675	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀))
230	24	fveq1i 6892	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀)
231	229, 230	eqtr4di 2790	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (𝑇‘𝑀))
232	196	nnzd 12584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ)
233	232	peano2zd 12668	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
234	4	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
235	196	peano2nnd 12228	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ)
236		elfzuz 13496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ_≥‘(𝑀 + 1)))
237		eluznn 12901	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ)
238	235, 236, 237	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ)
239	234, 238, 209	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
240	239	simp2d 1143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
241	239	simp1d 1142	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
242	240, 241	resubcld 11641	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
243	242	recnd 11241	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
244		2fveq3 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (2^nd ‘(𝐺‘𝑗)) = (2^nd ‘(𝐺‘(𝑘 + 𝑀))))
245		2fveq3 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (1^st ‘(𝐺‘𝑗)) = (1^st ‘(𝐺‘(𝑘 + 𝑀))))
246	244, 245	oveq12d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑘 + 𝑀) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
247	232, 233, 200, 243, 246	fsumshftm 15726	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
248	196	nncnd 12227	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ)
249		pncan2 11466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 𝑀) = 1)
250	248, 74, 249	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1)
251		nncn 12219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
252	251	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
253	248, 252	pncan2d 11572	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛)
254	250, 253	oveq12d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛))
255	254	sumeq1d 15646	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
256	133	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
257		elfznn 13529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
258	134	ovolfsval 24986	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
259	256, 257, 258	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
260	257	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
261		fvoveq1 7431	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀)))
262		eqid 2732	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))
263		fvex 6904	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V
264	261, 262, 263	fvmpt 6998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
265	260, 264	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
266	265	fveq2d 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2^nd ‘(𝐺‘(𝑘 + 𝑀))))
267	265	fveq2d 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1^st ‘(𝐺‘(𝑘 + 𝑀))))
268	266, 267	oveq12d 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
269	259, 268	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
270		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
271	270, 67	eleqtrdi 2843	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
272	4	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
273		nnaddcl 12234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ)
274	257, 196, 273	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ)
275		ovolfcl 24982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1^st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2^nd ‘(𝐺‘(𝑘 + 𝑀)))))
276	272, 274, 275	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1^st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2^nd ‘(𝐺‘(𝑘 + 𝑀)))))
277	276	simp2d 1143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
278	276	simp1d 1142	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
279	277, 278	resubcld 11641	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ)
280	279	recnd 11241	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ)
281	269, 271, 280	fsumser 15675	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
282	247, 255, 281	3eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
283	231, 282	oveq12d 7426	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
284	215, 219, 283	3eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
285	187, 284	eqtrid 2784	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
286	123	ffnd 6718	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn ℕ)
287		fnfvelrn 7082	. . . . . . . . . . . . . 14 ⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
288	286, 199, 287	syl2an2r 683	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
289	285, 288	eqeltrrd 2834	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇)
290		supxrub 13302	. . . . . . . . . . . 12 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^*, < ))
291	186, 289, 290	syl2an2r 683	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^*, < ))
292	125	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ)
293	137	ffvelcdmda 7086	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞))
294	120, 293	sselid 3980	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ)
295	90	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
296	292, 294, 295	leaddsub2d 11815	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^, < ) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
297	291, 296	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
298	297	ralrimiva 3146	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
299	137	ffnd 6718	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ)
300		breq1 5151	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
301	300	ralrn 7089	. . . . . . . . . 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 256	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
304		supxrleub 13304	. . . . . . . . 9 ⊢ ((ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^* ∧ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ∈ ℝ^) → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀))))
305	140, 143, 304	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀))))
306	303, 305	mpbird 256	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)))
307	127, 142, 143, 184, 306	xrletrd 13140	. . . . . 6 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)))
308	125, 90, 50	absdifltd 15379	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ^, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ^, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ^*, < ) + 𝐶))))
309	27, 308	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → ((sup(ran 𝑇, ℝ^, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ^, < ) + 𝐶)))
310	309	simpld 495	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − 𝐶) < (𝑇‘𝑀))
311	90, 50, 125, 310	ltsub23d 11818	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)) < 𝐶)
312	97, 126, 50, 307, 311	lelttrd 11371	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) < 𝐶)
313	97, 50, 49, 312	ltadd2dd 11372	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶))
314	13, 98, 51, 119, 313	lelttrd 11371	. . 3 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) < ((vol‘(𝐾 ∩ 𝐴)) + 𝐶))
315	54, 97	readdcld 11242	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∖ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
316		difss 4131	. . . . . . . 8 ⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾
317		unss1 4179	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
318	316, 317	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
319	318, 88	sseqtrrid 4035	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
320		ovolsscl 25002	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
321	319, 9, 95, 320	syl3anc 1371	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
322	104	ssdifd 4140	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴))
323		difundir 4280	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴))
324		difss 4131	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))
325		unss2 4181	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
326	324, 325	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
327	323, 326	eqsstri 4016	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
328	322, 327	sstrdi 3994	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
329	319, 9	sstrd 3992	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ)
330		ovolss 25001	. . . . . 6 ⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol‘(𝐸 ∖ 𝐴)) ≤ (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
331	328, 329, 330	syl2anc 584	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) ≤ (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
332	52, 46	sstrd 3992	. . . . . 6 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ)
333		ovolun 25015	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
334	332, 54, 116, 97, 333	syl22anc 837	. . . . 5 ⊢ (𝜑 → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
335	16, 321, 315, 331, 334	letrd 11370	. . . 4 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
336	97, 50, 54, 312	ltadd2dd 11372	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∖ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))
337	16, 315, 55, 335, 336	lelttrd 11371	. . 3 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) < ((vol‘(𝐾 ∖ 𝐴)) + 𝐶))
338	13, 16, 51, 55, 314, 337	lt2addd 11836	. 2 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol‘(𝐾 ∖ 𝐴)) + 𝐶)))
339	49	recnd 11241	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ)
340	50	recnd 11241	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
341	54	recnd 11241	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ)
342	339, 340, 341, 340	add4d 11441	. 2 ⊢ (𝜑 → (((vol‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))
343	338, 342	breqtrd 5174	1 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3061 ∃wrex 3070 Vcvv 3474 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 𝒫 cpw 4602 ⟨cop 4634 ∪ cuni 4908 ∪ ciun 4997 Disj wdisj 5113 class class class wbr 5148 ↦ cmpt 5231 × cxp 5674 ran crn 5677 “ cima 5679 ∘ ccom 5680 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7408 1^st c1st 7972 2^nd c2nd 7973 supcsup 9434 ℂcc 11107 ℝcr 11108 0cc0 11109 1c1 11110 + caddc 11112 +∞cpnf 11244 ℝ^*cxr 11246 < clt 11247 ≤ cle 11248 − cmin 11443 ℕcn 12211 ℕ₀cn0 12471 ℤcz 12557 ℤ_≥cuz 12821 ℝ⁺crp 12973 (,)cioo 13323 [,)cico 13325 [,]cicc 13326 ...cfz 13483 seqcseq 13965 abscabs 15180 Σcsu 15631 vol*covol 24978

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7724 ax-inf2 9635 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186 ax-pre-sup 11187

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7364 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7669 df-om 7855 df-1st 7974 df-2nd 7975 df-frecs 8265 df-wrecs 8296 df-recs 8370 df-rdg 8409 df-1o 8465 df-2o 8466 df-er 8702 df-map 8821 df-pm 8822 df-en 8939 df-dom 8940 df-sdom 8941 df-fin 8942 df-fi 9405 df-sup 9436 df-inf 9437 df-oi 9504 df-dju 9895 df-card 9933 df-acn 9936 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11445 df-neg 11446 df-div 11871 df-nn 12212 df-2 12274 df-3 12275 df-n0 12472 df-z 12558 df-uz 12822 df-q 12932 df-rp 12974 df-xneg 13091 df-xadd 13092 df-xmul 13093 df-ioo 13327 df-ico 13329 df-icc 13330 df-fz 13484 df-fzo 13627 df-fl 13756 df-seq 13966 df-exp 14027 df-hash 14290 df-cj 15045 df-re 15046 df-im 15047 df-sqrt 15181 df-abs 15182 df-clim 15431 df-rlim 15432 df-sum 15632 df-rest 17367 df-topgen 17388 df-psmet 20935 df-xmet 20936 df-met 20937 df-bl 20938 df-mopn 20939 df-top 22395 df-topon 22412 df-bases 22448 df-cmp 22890 df-ovol 24980 df-vol 24981

This theorem is referenced by: uniioombllem5 25103

W3C validator