Theorem uniioombllem3 23159

Description: Lemma for uniioombl 23163. (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 3795	. . . . 5 ⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸
2	1	a1i 11	. . . 4 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸)
3		uniioombl.s	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))
4		uniioombl.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	uniiccdif 23152	. . . . . . 7 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
6	5	simpld 474	. . . . . 6 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
7		ovolficcss 23045	. . . . . . 7 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
8	4, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
9	6, 8	sstrd 3578	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
10	3, 9	sstrd 3578	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
11		uniioombl.e	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
12		ovolsscl 23061	. . . 4 ⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ)
13	2, 10, 11, 12	syl3anc 1318	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ)
14		difssd 3700	. . . 4 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸)
15		ovolsscl 23061	. . . 4 ⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ)
16	14, 10, 11, 15	syl3anc 1318	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ)
17		inss1 3795	. . . . . 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 23158	. . . . . . 7 ⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ))
30	29	simpld 474	. . . . . 6 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
31		inss2 3796	. . . . . . . . . . . . 13 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
32		elfznn 12241	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
33		ffvelrn 6265	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
34	4, 32, 33	syl2an 493	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
35	31, 34	sseldi 3566	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
36		1st2nd2 7096	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))⟩)
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))⟩)
38	37	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))⟩))
39		df-ov 6552	. . . . . . . . . 10 ⊢ ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1st ‘(𝐺‘𝑗)), (2nd ‘(𝐺‘𝑗))⟩)
40	38, 39	syl6eqr 2662	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))))
41		ioossre 12106	. . . . . . . . 9 ⊢ ((1st ‘(𝐺‘𝑗))(,)(2nd ‘(𝐺‘𝑗))) ⊆ ℝ
42	40, 41	syl6eqss 3618	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
43	42	ralrimiva 2949	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
44		iunss 4497	. . . . . . 7 ⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
45	43, 44	sylibr 223	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
46	30, 45	eqsstrd 3602	. . . . 5 ⊢ (𝜑 → 𝐾 ⊆ ℝ)
47	29	simprd 478	. . . . 5 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
48		ovolsscl 23061	. . . . 5 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
49	18, 46, 47, 48	syl3anc 1318	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
50	23	rpred 11748	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
51	49, 50	readdcld 9948	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ)
52		difssd 3700	. . . . 5 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾)
53		ovolsscl 23061	. . . . 5 ⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ)
54	52, 46, 47, 53	syl3anc 1318	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ)
55	54, 50	readdcld 9948	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ)
56		ssun2 3739	. . . . . . 7 ⊢ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
57		ioof 12142	. . . . . . . . . . . . . . 15 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
58		rexpssxrxp 9963	. . . . . . . . . . . . . . . . 17 ⊢ (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
59	31, 58	sstri 3577	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
60		fss 5969	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
61	4, 59, 60	sylancl 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* × ℝ*))
62		fco 5971	. . . . . . . . . . . . . . 15 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
63	57, 61, 62	sylancr 694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
64		ffn 5958	. . . . . . . . . . . . . 14 ⊢ (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐺) Fn ℕ)
65	63, 64	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
66		fnima 5923	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺) Fn ℕ → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
67	65, 66	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
68		nnuz 11599	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ≥‘1)
69	26	peano2nnd 10914	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
70	69, 68	syl6eleq 2698	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ≥‘1))
71		uzsplit 12281	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘1) → (ℤ≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1))))
72	70, 71	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℤ≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1))))
73	68, 72	syl5eq 2656	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1))))
74	26	nncnd 10913	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
75		ax-1cn 9873	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
76		pncan 10166	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
77	74, 75, 76	sylancl 693	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
78	77	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀))
79	78	uneq1d 3728	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
80	73, 79	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
81	80	imaeq2d 5385	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))))
82	67, 81	eqtr3d 2646	. . . . . . . . . . 11 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))))
83		imaundi 5464	. . . . . . . . . . 11 ⊢ (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
84	82, 83	syl6eq 2660	. . . . . . . . . 10 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
85	84	unieqd 4382	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
86		uniun 4392	. . . . . . . . 9 ⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
87	85, 86	syl6eq 2660	. . . . . . . 8 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
88	28	uneq1i 3725	. . . . . . . 8 ⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
89	87, 88	syl6eqr 2662	. . . . . . 7 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
90	56, 89	syl5sseqr 3617	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺))
91	19, 20, 21, 22, 11, 23, 4, 3, 24, 25	uniioombllem1 23155	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
92		ssid 3587	. . . . . . . 8 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
93	24	ovollb 23054	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
94	4, 92, 93	sylancl 693	. . . . . . 7 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
95		ovollecl 23058	. . . . . . 7 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < )) → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
96	9, 91, 94, 95	syl3anc 1318	. . . . . 6 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
97		ovolsscl 23061	. . . . . 6 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∈ ℝ)
98	90, 9, 96, 97	syl3anc 1318	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∈ ℝ)
99	49, 98	readdcld 9948	. . . 4 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ∈ ℝ)
100		unss1 3744	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
101	17, 100	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
102	101, 89	syl5sseqr 3617	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
103		ovolsscl 23061	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ∈ ℝ)
104	102, 9, 96, 103	syl3anc 1318	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ∈ ℝ)
105	3, 89	sseqtrd 3604	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
106		ssrin 3800	. . . . . . . 8 ⊢ (𝐸 ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∩ 𝐴))
107	105, 106	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∩ 𝐴))
108		indir 3834	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∩ 𝐴))
109		inss1 3795	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))
110		unss2 3746	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
111	109, 110	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
112	108, 111	eqsstri 3598	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
113	107, 112	syl6ss 3580	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
114	102, 9	sstrd 3578	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ ℝ)
115		ovolss 23060	. . . . . 6 ⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
116	113, 114, 115	syl2anc 691	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
117	18, 46	sstrd 3578	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ)
118	90, 9	sstrd 3578	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ ℝ)
119		ovolun 23074	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
120	117, 49, 118, 98, 119	syl22anc 1319	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
121	13, 104, 99, 116, 120	letrd 10073	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ≤ ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
122		rge0ssre 12151	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
123		eqid 2610	. . . . . . . . . . 11 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
124	123, 24	ovolsf 23048	. . . . . . . . . 10 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
125	4, 124	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
126	125, 26	ffvelrnd 6268	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞))
127	122, 126	sseldi 3566	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ)
128	91, 127	resubcld 10337	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ)
129	98	rexrd 9968	. . . . . . 7 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∈ ℝ*)
130		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
131		nnaddcl 10919	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
132	130, 26, 131	syl2anr 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
133	4	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
134	132, 133	syldan 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
135		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))
136	134, 135	fmptd 6292	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
137		eqid 2610	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
138		eqid 2610	. . . . . . . . . . . 12 ⊢ seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
139	137, 138	ovolsf 23048	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
140	136, 139	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
141		frn 5966	. . . . . . . . . 10 ⊢ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞) → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ (0[,)+∞))
142	140, 141	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ (0[,)+∞))
143		icossxr 12129	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ*
144	142, 143	syl6ss 3580	. . . . . . . 8 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ*)
145		supxrcl 12017	. . . . . . . 8 ⊢ (ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈ ℝ*)
146	144, 145	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ∈ ℝ*)
147	128	rexrd 9968	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ*)
148		1zzd 11285	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 1 ∈ ℤ)
149	26	nnzd 11357	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℤ)
150	149	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ)
151		addcom 10101	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + 1) = (1 + 𝑀))
152	74, 75, 151	sylancl 693	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀))
153	152	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(1 + 𝑀)))
154	153	eleq2d 2673	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ≥‘(1 + 𝑀))))
155	154	biimpa 500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ≥‘(1 + 𝑀)))
156		eluzsub 11593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ (ℤ≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈ (ℤ≥‘1))
157	148, 150, 155, 156	syl3anc 1318	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ (ℤ≥‘1))
158	157, 68	syl6eleqr 2699	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ)
159		eluzelz 11573	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ)
160	159	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ℤ)
161	160	zcnd 11359	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ℂ)
162	74	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ)
163	161, 162	npcand 10275	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
164	163	eqcomd 2616	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀))
165		oveq1 6556	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
166	165	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑥 − 𝑀) → (𝑥 = (𝑧 + 𝑀) ↔ 𝑥 = ((𝑥 − 𝑀) + 𝑀)))
167	166	rspcev 3282	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
168	158, 164, 167	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
169		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
170		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))
171	170	elrnmpt 5293	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)))
172	169, 171	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
173	168, 172	sylibr 223	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
174	173	ex 449	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
175	174	ssrdv 3574	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
176		imass2 5420	. . . . . . . . . . . . 13 ⊢ ((ℤ≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “ (ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
177	175, 176	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ (ℤ≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
178		rnco2 5559	. . . . . . . . . . . . 13 ⊢ ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
179		eqidd 2611	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
180	4	feqmptd 6159	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 = (𝑤 ∈ ℕ ↦ (𝐺‘𝑤)))
181		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑧 + 𝑀) → (𝐺‘𝑤) = (𝐺‘(𝑧 + 𝑀)))
182	132, 179, 180, 181	fmptco 6303	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
183	182	rneqd 5274	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
184	178, 183	syl5eqr 2658	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
185	177, 184	sseqtrd 3604	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
186		imass2 5420	. . . . . . . . . . 11 ⊢ ((𝐺 “ (ℤ≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “ (ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
187	185, 186	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((,) “ (𝐺 “ (ℤ≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
188		imaco 5557	. . . . . . . . . 10 ⊢ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) = ((,) “ (𝐺 “ (ℤ≥‘(𝑀 + 1))))
189		rnco2 5559	. . . . . . . . . 10 ⊢ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
190	187, 188, 189	3sstr4g 3609	. . . . . . . . 9 ⊢ (𝜑 → (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
191	190	unissd 4398	. . . . . . . 8 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
192	138	ovollb 23054	. . . . . . . 8 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ))
193	136, 191, 192	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ))
194		frn 5966	. . . . . . . . . . . . . . 15 ⊢ (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
195	125, 194	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
196	195, 143	syl6ss 3580	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ*)
197	196	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝑇 ⊆ ℝ*)
198	24	fveq1i 6104	. . . . . . . . . . . . . 14 ⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛))
199	26	nnred 10912	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ)
200	199	ltp1d 10833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
201		fzdisj 12239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
202	200, 201	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
203	202	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
204		nnnn0 11176	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
205		nn0addge1 11216	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ0) → 𝑀 ≤ (𝑀 + 𝑛))
206	199, 204, 205	syl2an 493	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛))
207	26	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ)
208	207, 68	syl6eleq 2698	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (ℤ≥‘1))
209		nnaddcl 10919	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
210	26, 209	sylan 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
211	210	nnzd 11357	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ)
212		elfz5 12205	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ (ℤ≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
213	208, 211, 212	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
214	206, 213	mpbird 246	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛)))
215		fzsplit 12238	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
216	214, 215	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
217		fzfid 12634	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin)
218	4	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
219		elfznn 12241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ)
220		ovolfcl 23042	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))))
221	218, 219, 220	syl2an 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))))
222	221	simp2d 1067	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ)
223	221	simp1d 1066	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ)
224	222, 223	resubcld 10337	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ)
225	224	recnd 9947	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ)
226	203, 216, 217, 225	fsumsplit 14318	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))))
227	123	ovolfsval 23046	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))))
228	218, 219, 227	syl2an 493	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))))
229	210, 68	syl6eleq 2698	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ (ℤ≥‘1))
230	228, 229, 225	fsumser 14308	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)))
231	4	ad2antrr 758	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
232	32	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
233	231, 232, 227	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))))
234	4, 32, 220	syl2an 493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))))
235	234	simp2d 1067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ)
236	234	simp1d 1066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺‘𝑗)) ∈ ℝ)
237	235, 236	resubcld 10337	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ)
238	237	adantlr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ)
239	238	recnd 9947	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ)
240	233, 208, 239	fsumser 14308	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀))
241	24	fveq1i 6104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀)
242	240, 241	syl6eqr 2662	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (𝑇‘𝑀))
243	207	nnzd 11357	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ)
244	243	peano2zd 11361	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
245	4	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
246	207	peano2nnd 10914	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ)
247		elfzuz 12209	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ≥‘(𝑀 + 1)))
248		eluznn 11634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ)
249	246, 247, 248	syl2an 493	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ)
250	245, 249, 220	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1st ‘(𝐺‘𝑗)) ≤ (2nd ‘(𝐺‘𝑗))))
251	250	simp2d 1067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2nd ‘(𝐺‘𝑗)) ∈ ℝ)
252	250	simp1d 1066	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1st ‘(𝐺‘𝑗)) ∈ ℝ)
253	251, 252	resubcld 10337	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℝ)
254	253	recnd 9947	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) ∈ ℂ)
255		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑘 + 𝑀) → (𝐺‘𝑗) = (𝐺‘(𝑘 + 𝑀)))
256	255	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (2nd ‘(𝐺‘𝑗)) = (2nd ‘(𝐺‘(𝑘 + 𝑀))))
257	255	fveq2d 6107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (1st ‘(𝐺‘𝑗)) = (1st ‘(𝐺‘(𝑘 + 𝑀))))
258	256, 257	oveq12d 6567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑘 + 𝑀) → ((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
259	243, 244, 211, 254, 258	fsumshftm 14355	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
260	207	nncnd 10913	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ)
261		pncan2 10167	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 𝑀) = 1)
262	260, 75, 261	sylancl 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1)
263		nncn 10905	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
264	263	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
265	260, 264	pncan2d 10273	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛)
266	262, 265	oveq12d 6567	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛))
267	266	sumeq1d 14279	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
268	136	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
269		elfznn 12241	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
270	137	ovolfsval 23046	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
271	268, 269, 270	syl2an 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
272	269	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
273		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = 𝑘 → (𝑧 + 𝑀) = (𝑘 + 𝑀))
274	273	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀)))
275		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V
276	274, 135, 275	fvmpt 6191	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
277	272, 276	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
278	277	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2nd ‘(𝐺‘(𝑘 + 𝑀))))
279	277	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1st ‘(𝐺‘(𝑘 + 𝑀))))
280	278, 279	oveq12d 6567	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
281	271, 280	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))))
282		simpr 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
283	282, 68	syl6eleq 2698	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ≥‘1))
284	4	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
285		nnaddcl 10919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ)
286	269, 207, 285	syl2anr 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ)
287		ovolfcl 23042	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀)))))
288	284, 286, 287	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2nd ‘(𝐺‘(𝑘 + 𝑀)))))
289	288	simp2d 1067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
290	288	simp1d 1066	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
291	289, 290	resubcld 10337	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ)
292	291	recnd 9947	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ)
293	281, 283, 292	fsumser 14308	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2nd ‘(𝐺‘(𝑘 + 𝑀))) − (1st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
294	259, 267, 293	3eqtrd 2648	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
295	242, 294	oveq12d 6567	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2nd ‘(𝐺‘𝑗)) − (1st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
296	226, 230, 295	3eqtr3d 2652	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
297	198, 296	syl5eq 2656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
298		ffn 5958	. . . . . . . . . . . . . . . 16 ⊢ (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
299	125, 298	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 Fn ℕ)
300	299	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑇 Fn ℕ)
301		fnfvelrn 6264	. . . . . . . . . . . . . 14 ⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
302	300, 210, 301	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
303	297, 302	eqeltrrd 2689	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇)
304		supxrub 12026	. . . . . . . . . . . 12 ⊢ ((ran 𝑇 ⊆ ℝ* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ))
305	197, 303, 304	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ))
306	127	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ)
307	140	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞))
308	122, 307	sseldi 3566	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ)
309	91	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
310	306, 308, 309	leaddsub2d 10508	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ*, < ) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))))
311	305, 310	mpbid 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))
312	311	ralrimiva 2949	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))
313		ffn 5958	. . . . . . . . . . 11 ⊢ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ)
314	140, 313	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ)
315		breq1 4586	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))))
316	315	ralrn 6270	. . . . . . . . . 10 ⊢ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ → (∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))))
317	314, 316	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))))
318	312, 317	mpbird 246	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))
319		supxrleub 12028	. . . . . . . . 9 ⊢ ((ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ* ∧ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ∈ ℝ*) → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))))
320	144, 147, 319	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀))))
321	318, 320	mpbird 246	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ*, < ) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))
322	129, 146, 147, 193, 321	xrletrd 11869	. . . . . 6 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)))
323	127, 91, 50	absdifltd 14020	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶))))
324	27, 323	mpbid 221	. . . . . . . 8 ⊢ (𝜑 → ((sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ*, < ) + 𝐶)))
325	324	simpld 474	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − 𝐶) < (𝑇‘𝑀))
326	91, 50, 127, 325	ltsub23d 10511	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) − (𝑇‘𝑀)) < 𝐶)
327	98, 128, 50, 322, 326	lelttrd 10074	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) < 𝐶)
328	98, 50, 49, 327	ltadd2dd 10075	. . . 4 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶))
329	13, 99, 51, 121, 328	lelttrd 10074	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶))
330	54, 98	readdcld 9948	. . . 4 ⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ∈ ℝ)
331		difss 3699	. . . . . . . 8 ⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾
332		unss1 3744	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
333	331, 332	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
334	333, 89	syl5sseqr 3617	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
335		ovolsscl 23061	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ∈ ℝ)
336	334, 9, 96, 335	syl3anc 1318	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ∈ ℝ)
337	105	ssdifd 3708	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∖ 𝐴))
338		difundir 3839	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∖ 𝐴))
339		difss 3699	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))
340		unss2 3746	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
341	339, 340	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
342	338, 341	eqsstri 3598	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))
343	337, 342	syl6ss 3580	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))))
344	334, 9	sstrd 3578	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ ℝ)
345		ovolss 23060	. . . . . 6 ⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol*‘(𝐸 ∖ 𝐴)) ≤ (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
346	343, 344, 345	syl2anc 691	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
347	52, 46	sstrd 3578	. . . . . 6 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ)
348		ovolun 23074	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
349	347, 54, 118, 98, 348	syl22anc 1319	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
350	16, 336, 330, 346, 349	letrd 10073	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ≤ ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))))
351	98, 50, 54, 327	ltadd2dd 10075	. . . 4 ⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))
352	16, 330, 55, 350, 351	lelttrd 10074	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))
353	13, 16, 51, 55, 329, 352	lt2addd 10529	. 2 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)))
354	49	recnd 9947	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ)
355	50	recnd 9947	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
356	54	recnd 9947	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ)
357	354, 355, 356, 355	add4d 10143	. 2 ⊢ (𝜑 → (((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))
358	353, 357	breqtrd 4609	1 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐴)) + (vol*‘(𝐸 ∖ 𝐴))) < (((vol*‘(𝐾 ∩ 𝐴)) + (vol*‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  ⟨cop 4131  ∪ cuni 4372  ∪ ciun 4455  Disj wdisj 4553   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ran crn 5039   “ cima 5041   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  1^st c1st 7057  2^nd c2nd 7058  supcsup 8229  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818  +∞cpnf 9950  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ₀cn0 11169  ℤcz 11254  ℤ_≥cuz 11563  ℝ⁺crp 11708  (,)cioo 12046  [,)cico 12048  [,]cicc 12049  ...cfz 12197  seqcseq 12663  abscabs 13822  Σcsu 14264  vol*covol 23038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-acn 8651  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041

This theorem is referenced by:  uniioombllem5  23161