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 23693

Description: Lemma for uniioombl 23697. (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 4028	. . . . 5 ⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸
2	1	a1i 11	. . . 4 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸)
3		uniioombl.s	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))
4		uniioombl.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	uniiccdif 23686	. . . . . . 7 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
6	5	simpld 489	. . . . . 6 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
7		ovolficcss 23577	. . . . . . 7 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
8	4, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
9	6, 8	sstrd 3808	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
10	3, 9	sstrd 3808	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
11		uniioombl.e	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
12		ovolsscl 23594	. . . 4 ⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∩ 𝐴)) ∈ ℝ)
13	2, 10, 11, 12	syl3anc 1491	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ)
14		difssd 3936	. . . 4 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸)
15		ovolsscl 23594	. . . 4 ⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∖ 𝐴)) ∈ ℝ)
16	14, 10, 11, 15	syl3anc 1491	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ)
17		inss1 4028	. . . . . 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 23692	. . . . . . 7 ⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ))
30	29	simpld 489	. . . . . 6 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
31		inss2 4029	. . . . . . . . . . . . 13 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
32		elfznn 12624	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
33		ffvelrn 6583	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
34	4, 32, 33	syl2an 590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
35	31, 34	sseldi 3796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
36		1st2nd2 7440	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
38	37	fveq2d 6415	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩))
39		df-ov 6881	. . . . . . . . . 10 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
40	38, 39	syl6eqr 2851	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))))
41		ioossre 12484	. . . . . . . . 9 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ⊆ ℝ
42	40, 41	syl6eqss 3851	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
43	42	ralrimiva 3147	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
44		iunss 4751	. . . . . . 7 ⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
45	43, 44	sylibr 226	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
46	30, 45	eqsstrd 3835	. . . . 5 ⊢ (𝜑 → 𝐾 ⊆ ℝ)
47	29	simprd 490	. . . . 5 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
48		ovolsscl 23594	. . . . 5 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ)
49	18, 46, 47, 48	syl3anc 1491	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
50	23	rpred 12117	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
51	49, 50	readdcld 10358	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ)
52		difssd 3936	. . . . 5 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾)
53		ovolsscl 23594	. . . . 5 ⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∖ 𝐴)) ∈ ℝ)
54	52, 46, 47, 53	syl3anc 1491	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ)
55	54, 50	readdcld 10358	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ)
56		ssun2 3975	. . . . . . 7 ⊢ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
57		ioof 12521	. . . . . . . . . . . . . . 15 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
58		rexpssxrxp 10373	. . . . . . . . . . . . . . . . 17 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
59	31, 58	sstri 3807	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
60		fss 6269	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐺:ℕ⟶(ℝ^ × ℝ^*))
61	4, 59, 60	sylancl 581	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ^* × ℝ^*))
62		fco 6273	. . . . . . . . . . . . . . 15 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
63	57, 61, 62	sylancr 582	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
64	63	ffnd 6257	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
65		fnima 6221	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺) Fn ℕ → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
66	64, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
67		nnuz 11967	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
68	26	peano2nnd 11331	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
69	68, 67	syl6eleq 2888	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
70		uzsplit 12666	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
71	69, 70	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℤ_≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
72	67, 71	syl5eq 2845	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
73	26	nncnd 11330	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
74		ax-1cn 10282	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
75		pncan 10578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
76	73, 74, 75	sylancl 581	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
77	76	oveq2d 6894	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀))
78	77	uneq1d 3964	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1))))
79	72, 78	eqtrd 2833	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1))))
80	79	imaeq2d 5683	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))))
81	66, 80	eqtr3d 2835	. . . . . . . . . . 11 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))))
82		imaundi 5762	. . . . . . . . . . 11 ⊢ (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
83	81, 82	syl6eq 2849	. . . . . . . . . 10 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
84	83	unieqd 4638	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
85		uniun 4649	. . . . . . . . 9 ⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
86	84, 85	syl6eq 2849	. . . . . . . 8 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
87	28	uneq1i 3961	. . . . . . . 8 ⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
88	86, 87	syl6eqr 2851	. . . . . . 7 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
89	56, 88	syl5sseqr 3850	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺))
90	19, 20, 21, 22, 11, 23, 4, 3, 24, 25	uniioombllem1 23689	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
91		ssid 3819	. . . . . . . 8 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
92	24	ovollb 23587	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
93	4, 91, 92	sylancl 581	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
94		ovollecl 23591	. . . . . . 7 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ^, < ) ∈ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < )) → (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
95	9, 90, 93, 94	syl3anc 1491	. . . . . 6 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
96		ovolsscl 23594	. . . . . 6 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)
97	89, 9, 95, 96	syl3anc 1491	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)
98	49, 97	readdcld 10358	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
99		unss1 3980	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
100	17, 99	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
101	100, 88	syl5sseqr 3850	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
102		ovolsscl 23594	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
103	101, 9, 95, 102	syl3anc 1491	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
104	3, 88	sseqtrd 3837	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
105	104	ssrind 4035	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴))
106		indir 4076	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴))
107		inss1 4028	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))
108		unss2 3982	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
109	107, 108	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
110	106, 109	eqsstri 3831	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
111	105, 110	syl6ss 3810	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
112	101, 9	sstrd 3808	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ)
113		ovolss 23593	. . . . . 6 ⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol‘(𝐸 ∩ 𝐴)) ≤ (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
114	111, 112, 113	syl2anc 580	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) ≤ (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
115	18, 46	sstrd 3808	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ)
116	89, 9	sstrd 3808	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ)
117		ovolun 23607	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
118	115, 49, 116, 97, 117	syl22anc 868	. . . . 5 ⊢ (𝜑 → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
119	13, 103, 98, 114, 118	letrd 10484	. . . 4 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
120		rge0ssre 12531	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
121		eqid 2799	. . . . . . . . . . 11 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
122	121, 24	ovolsf 23580	. . . . . . . . . 10 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
123	4, 122	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
124	123, 26	ffvelrnd 6586	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞))
125	120, 124	sseldi 3796	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ)
126	90, 125	resubcld 10750	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)) ∈ ℝ)
127	97	rexrd 10378	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ^)
128		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
129		nnaddcl 11336	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
130	128, 26, 129	syl2anr 591	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
131	4	ffvelrnda 6585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
132	130, 131	syldan 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
133	132	fmpttd 6611	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
134		eqid 2799	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
135		eqid 2799	. . . . . . . . . . . 12 ⊢ seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
136	134, 135	ovolsf 23580	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
137	133, 136	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
138	137	frnd 6263	. . . . . . . . 9 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ (0[,)+∞))
139		icossxr 12507	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ^*
140	138, 139	syl6ss 3810	. . . . . . . 8 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^*)
141		supxrcl 12394	. . . . . . . 8 ⊢ (ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^* → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ∈ ℝ^)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ∈ ℝ^)
143	126	rexrd 10378	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ∈ ℝ^)
144		1zzd 11698	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 1 ∈ ℤ)
145	26	nnzd 11771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℤ)
146	145	adantr 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ)
147		addcom 10512	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + 1) = (1 + 𝑀))
148	73, 74, 147	sylancl 581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀))
149	148	fveq2d 6415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) = (ℤ_≥‘(1 + 𝑀)))
150	149	eleq2d 2864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ_≥‘(1 + 𝑀))))
151	150	biimpa 469	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ_≥‘(1 + 𝑀)))
152		eluzsub 11960	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ (ℤ_≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈ (ℤ_≥‘1))
153	144, 146, 151, 152	syl3anc 1491	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ (ℤ_≥‘1))
154	153, 67	syl6eleqr 2889	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ)
155		eluzelz 11940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ)
156	155	adantl 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ℤ)
157	156	zcnd 11773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ℂ)
158	73	adantr 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ)
159	157, 158	npcand 10688	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
160	159	eqcomd 2805	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀))
161		oveq1 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
162	161	rspceeqv 3515	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
163	154, 160, 162	syl2anc 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
164		vex 3388	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
165		eqid 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))
166	165	elrnmpt 5576	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)))
167	164, 166	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
168	163, 167	sylibr 226	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
169	168	ex 402	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
170	169	ssrdv 3804	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
171		imass2 5718	. . . . . . . . . . . . 13 ⊢ ((ℤ_≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
172	170, 171	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
173		rnco2 5861	. . . . . . . . . . . . 13 ⊢ ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
174		eqidd 2800	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
175	4	feqmptd 6474	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 = (𝑤 ∈ ℕ ↦ (𝐺‘𝑤)))
176		fveq2 6411	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝑧 + 𝑀) → (𝐺‘𝑤) = (𝐺‘(𝑧 + 𝑀)))
177	130, 174, 175, 176	fmptco 6623	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
178	177	rneqd 5556	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
179	173, 178	syl5eqr 2847	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
180	172, 179	sseqtrd 3837	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
181		imass2 5718	. . . . . . . . . . 11 ⊢ ((𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
182	180, 181	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
183		imaco 5859	. . . . . . . . . 10 ⊢ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) = ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1))))
184		rnco2 5861	. . . . . . . . . 10 ⊢ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
185	182, 183, 184	3sstr4g 3842	. . . . . . . . 9 ⊢ (𝜑 → (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
186	185	unissd 4654	. . . . . . . 8 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
187	135	ovollb 23587	. . . . . . . 8 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ))
188	133, 186, 187	syl2anc 580	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ))
189	123	frnd 6263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
190	189, 139	syl6ss 3810	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
191	190	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝑇 ⊆ ℝ^*)
192	24	fveq1i 6412	. . . . . . . . . . . . . 14 ⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛))
193	26	nnred 11329	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ)
194	193	ltp1d 11246	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
195		fzdisj 12622	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
196	194, 195	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
197	196	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
198		nnnn0 11588	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
199		nn0addge1 11628	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → 𝑀 ≤ (𝑀 + 𝑛))
200	193, 198, 199	syl2an 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛))
201	26	adantr 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ)
202	201, 67	syl6eleq 2888	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (ℤ_≥‘1))
203		nnaddcl 11336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
204	26, 203	sylan 576	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
205	204	nnzd 11771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ)
206		elfz5 12588	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ (ℤ_≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
207	202, 205, 206	syl2anc 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
208	200, 207	mpbird 249	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛)))
209		fzsplit 12621	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
210	208, 209	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
211		fzfid 13027	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin)
212	4	adantr 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
213		elfznn 12624	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ)
214		ovolfcl 23574	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
215	212, 213, 214	syl2an 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
216	215	simp2d 1174	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
217	215	simp1d 1173	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
218	216, 217	resubcld 10750	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
219	218	recnd 10357	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
220	197, 210, 211, 219	fsumsplit 14812	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗)))))
221	121	ovolfsval 23578	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
222	212, 213, 221	syl2an 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
223	204, 67	syl6eleq 2888	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ (ℤ_≥‘1))
224	222, 223, 219	fsumser 14802	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)))
225	4	ad2antrr 718	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
226	32	adantl 474	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ)
227	225, 226, 221	syl2anc 580	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
228	4, 32, 214	syl2an 590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
229	228	simp2d 1174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
230	228	simp1d 1173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
231	229, 230	resubcld 10750	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
232	231	adantlr 707	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
233	232	recnd 10357	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
234	227, 202, 233	fsumser 14802	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀))
235	24	fveq1i 6412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀)
236	234, 235	syl6eqr 2851	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (𝑇‘𝑀))
237	201	nnzd 11771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ)
238	237	peano2zd 11775	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
239	4	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
240	201	peano2nnd 11331	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ)
241		elfzuz 12592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ_≥‘(𝑀 + 1)))
242		eluznn 12003	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑀 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑗 ∈ ℕ)
243	240, 241, 242	syl2an 590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝑗 ∈ ℕ)
244	239, 243, 214	syl2anc 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
245	244	simp2d 1174	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
246	244	simp1d 1173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
247	245, 246	resubcld 10750	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
248	247	recnd 10357	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
249		2fveq3 6416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (2^nd ‘(𝐺‘𝑗)) = (2^nd ‘(𝐺‘(𝑘 + 𝑀))))
250		2fveq3 6416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (1^st ‘(𝐺‘𝑗)) = (1^st ‘(𝐺‘(𝑘 + 𝑀))))
251	249, 250	oveq12d 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑘 + 𝑀) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
252	237, 238, 205, 248, 251	fsumshftm 14851	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
253	201	nncnd 11330	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ)
254		pncan2 10579	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 𝑀) = 1)
255	253, 74, 254	sylancl 581	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1)
256		nncn 11321	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
257	256	adantl 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
258	253, 257	pncan2d 10686	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛)
259	255, 258	oveq12d 6896	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛))
260	259	sumeq1d 14772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
261	133	adantr 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
262		elfznn 12624	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
263	134	ovolfsval 23578	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
264	261, 262, 263	syl2an 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
265	262	adantl 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
266		fvoveq1 6901	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀)))
267		eqid 2799	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))
268		fvex 6424	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V
269	266, 267, 268	fvmpt 6507	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
270	265, 269	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
271	270	fveq2d 6415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2^nd ‘(𝐺‘(𝑘 + 𝑀))))
272	270	fveq2d 6415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1^st ‘(𝐺‘(𝑘 + 𝑀))))
273	271, 272	oveq12d 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
274	264, 273	eqtrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
275		simpr 478	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
276	275, 67	syl6eleq 2888	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
277	4	ad2antrr 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
278		nnaddcl 11336	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ)
279	262, 201, 278	syl2anr 591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ)
280		ovolfcl 23574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝑘 + 𝑀) ∈ ℕ) → ((1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1^st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2^nd ‘(𝐺‘(𝑘 + 𝑀)))))
281	277, 279, 280	syl2anc 580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ ∧ (1^st ‘(𝐺‘(𝑘 + 𝑀))) ≤ (2^nd ‘(𝐺‘(𝑘 + 𝑀)))))
282	281	simp2d 1174	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2^nd ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
283	281	simp1d 1173	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1^st ‘(𝐺‘(𝑘 + 𝑀))) ∈ ℝ)
284	282, 283	resubcld 10750	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ)
285	284	recnd 10357	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ)
286	274, 276, 285	fsumser 14802	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
287	252, 260, 286	3eqtrd 2837	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
288	236, 287	oveq12d 6896	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
289	220, 224, 288	3eqtr3d 2841	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
290	192, 289	syl5eq 2845	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
291	123	ffnd 6257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 Fn ℕ)
292	291	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑇 Fn ℕ)
293		fnfvelrn 6582	. . . . . . . . . . . . . 14 ⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
294	292, 204, 293	syl2anc 580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
295	290, 294	eqeltrrd 2879	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇)
296		supxrub 12403	. . . . . . . . . . . 12 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^*, < ))
297	191, 295, 296	syl2anc 580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^*, < ))
298	125	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ)
299	137	ffvelrnda 6585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞))
300	120, 299	sseldi 3796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ)
301	90	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
302	298, 300, 301	leaddsub2d 10921	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^, < ) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
303	297, 302	mpbid 224	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
304	303	ralrimiva 3147	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
305	137	ffnd 6257	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ)
306		breq1 4846	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
307	306	ralrn 6588	. . . . . . . . . 10 ⊢ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ → (∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
308	305, 307	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
309	304, 308	mpbird 249	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
310		supxrleub 12405	. . . . . . . . 9 ⊢ ((ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^* ∧ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ∈ ℝ^) → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀))))
311	140, 143, 310	syl2anc 580	. . . . . . . 8 ⊢ (𝜑 → (sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀))))
312	309, 311	mpbird 249	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)))
313	127, 142, 143, 188, 312	xrletrd 12242	. . . . . 6 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)))
314	125, 90, 50	absdifltd 14513	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ^, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ^, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ^*, < ) + 𝐶))))
315	27, 314	mpbid 224	. . . . . . . 8 ⊢ (𝜑 → ((sup(ran 𝑇, ℝ^, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ^, < ) + 𝐶)))
316	315	simpld 489	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − 𝐶) < (𝑇‘𝑀))
317	90, 50, 125, 316	ltsub23d 10924	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)) < 𝐶)
318	97, 126, 50, 313, 317	lelttrd 10485	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) < 𝐶)
319	97, 50, 49, 318	ltadd2dd 10486	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶))
320	13, 98, 51, 119, 319	lelttrd 10485	. . 3 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) < ((vol‘(𝐾 ∩ 𝐴)) + 𝐶))
321	54, 97	readdcld 10358	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∖ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
322		difss 3935	. . . . . . . 8 ⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾
323		unss1 3980	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
324	322, 323	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
325	324, 88	syl5sseqr 3850	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
326		ovolsscl 23594	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
327	325, 9, 95, 326	syl3anc 1491	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
328	104	ssdifd 3944	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴))
329		difundir 4081	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴))
330		difss 3935	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))
331		unss2 3982	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
332	330, 331	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
333	329, 332	eqsstri 3831	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
334	328, 333	syl6ss 3810	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
335	325, 9	sstrd 3808	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ)
336		ovolss 23593	. . . . . 6 ⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol‘(𝐸 ∖ 𝐴)) ≤ (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
337	334, 335, 336	syl2anc 580	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) ≤ (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
338	52, 46	sstrd 3808	. . . . . 6 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ)
339		ovolun 23607	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
340	338, 54, 116, 97, 339	syl22anc 868	. . . . 5 ⊢ (𝜑 → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
341	16, 327, 321, 337, 340	letrd 10484	. . . 4 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
342	97, 50, 54, 318	ltadd2dd 10486	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∖ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))
343	16, 321, 55, 341, 342	lelttrd 10485	. . 3 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) < ((vol‘(𝐾 ∖ 𝐴)) + 𝐶))
344	13, 16, 51, 55, 320, 343	lt2addd 10942	. 2 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol‘(𝐾 ∖ 𝐴)) + 𝐶)))
345	49	recnd 10357	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ)
346	50	recnd 10357	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
347	54	recnd 10357	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ)
348	345, 346, 347, 346	add4d 10554	. 2 ⊢ (𝜑 → (((vol‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))
349	344, 348	breqtrd 4869	1 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 = wceq 1653 ∈ wcel 2157 ∀wral 3089 ∃wrex 3090 Vcvv 3385 ∖ cdif 3766 ∪ cun 3767 ∩ cin 3768 ⊆ wss 3769 ∅c0 4115 𝒫 cpw 4349 ⟨cop 4374 ∪ cuni 4628 ∪ ciun 4710 Disj wdisj 4811 class class class wbr 4843 ↦ cmpt 4922 × cxp 5310 ran crn 5313 “ cima 5315 ∘ ccom 5316 Fn wfn 6096 ⟶wf 6097 ‘cfv 6101 (class class class)co 6878 1^st c1st 7399 2^nd c2nd 7400 supcsup 8588 ℂcc 10222 ℝcr 10223 0cc0 10224 1c1 10225 + caddc 10227 +∞cpnf 10360 ℝ^*cxr 10362 < clt 10363 ≤ cle 10364 − cmin 10556 ℕcn 11312 ℕ₀cn0 11580 ℤcz 11666 ℤ_≥cuz 11930 ℝ⁺crp 12074 (,)cioo 12424 [,)cico 12426 [,]cicc 12427 ...cfz 12580 seqcseq 13055 abscabs 14315 Σcsu 14757 vol*covol 23570

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-inf2 8788 ax-cnex 10280 ax-resscn 10281 ax-1cn 10282 ax-icn 10283 ax-addcl 10284 ax-addrcl 10285 ax-mulcl 10286 ax-mulrcl 10287 ax-mulcom 10288 ax-addass 10289 ax-mulass 10290 ax-distr 10291 ax-i2m1 10292 ax-1ne0 10293 ax-1rid 10294 ax-rnegex 10295 ax-rrecex 10296 ax-cnre 10297 ax-pre-lttri 10298 ax-pre-lttrn 10299 ax-pre-ltadd 10300 ax-pre-mulgt0 10301 ax-pre-sup 10302

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-fal 1667 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rmo 3097 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-tp 4373 df-op 4375 df-uni 4629 df-int 4668 df-iun 4712 df-br 4844 df-opab 4906 df-mpt 4923 df-tr 4946 df-id 5220 df-eprel 5225 df-po 5233 df-so 5234 df-fr 5271 df-se 5272 df-we 5273 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-pred 5898 df-ord 5944 df-on 5945 df-lim 5946 df-suc 5947 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-isom 6110 df-riota 6839 df-ov 6881 df-oprab 6882 df-mpt2 6883 df-of 7131 df-om 7300 df-1st 7401 df-2nd 7402 df-wrecs 7645 df-recs 7707 df-rdg 7745 df-1o 7799 df-2o 7800 df-oadd 7803 df-er 7982 df-map 8097 df-pm 8098 df-en 8196 df-dom 8197 df-sdom 8198 df-fin 8199 df-fi 8559 df-sup 8590 df-inf 8591 df-oi 8657 df-card 9051 df-acn 9054 df-cda 9278 df-pnf 10365 df-mnf 10366 df-xr 10367 df-ltxr 10368 df-le 10369 df-sub 10558 df-neg 10559 df-div 10977 df-nn 11313 df-2 11376 df-3 11377 df-n0 11581 df-z 11667 df-uz 11931 df-q 12034 df-rp 12075 df-xneg 12193 df-xadd 12194 df-xmul 12195 df-ioo 12428 df-ico 12430 df-icc 12431 df-fz 12581 df-fzo 12721 df-fl 12848 df-seq 13056 df-exp 13115 df-hash 13371 df-cj 14180 df-re 14181 df-im 14182 df-sqrt 14316 df-abs 14317 df-clim 14560 df-rlim 14561 df-sum 14758 df-rest 16398 df-topgen 16419 df-psmet 20060 df-xmet 20061 df-met 20062 df-bl 20063 df-mopn 20064 df-top 21027 df-topon 21044 df-bases 21079 df-cmp 21519 df-ovol 23572 df-vol 23573

This theorem is referenced by: uniioombllem5 23695

W3C validator