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 25519

Description: Lemma for uniioombl 25523. (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 4196	. . . . 5 ⊢ (𝐸 ∩ 𝐴) ⊆ 𝐸
2	1	a1i 11	. . . 4 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ 𝐸)
3		uniioombl.s	. . . . 5 ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐺))
4		uniioombl.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
5	4	uniiccdif 25512	. . . . . . 7 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
6	5	simpld 494	. . . . . 6 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
7		ovolficcss 25403	. . . . . . 7 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
8	4, 7	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
9	6, 8	sstrd 3954	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
10	3, 9	sstrd 3954	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
11		uniioombl.e	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
12		ovolsscl 25420	. . . 4 ⊢ (((𝐸 ∩ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∩ 𝐴)) ∈ ℝ)
13	2, 10, 11, 12	syl3anc 1373	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐴)) ∈ ℝ)
14		difssd 4096	. . . 4 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ 𝐸)
15		ovolsscl 25420	. . . 4 ⊢ (((𝐸 ∖ 𝐴) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∖ 𝐴)) ∈ ℝ)
16	14, 10, 11, 15	syl3anc 1373	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐴)) ∈ ℝ)
17		inss1 4196	. . . . . 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 25518	. . . . . . 7 ⊢ (𝜑 → (𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ∧ (vol*‘𝐾) ∈ ℝ))
30	29	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
31		inss2 4197	. . . . . . . . . . . . 13 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
32		elfznn 13490	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
33		ffvelcdm 7035	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
34	4, 32, 33	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
35	31, 34	sselid 3941	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
36		1st2nd2 7986	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
37	35, 36	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
38	37	fveq2d 6844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩))
39		df-ov 7372	. . . . . . . . . 10 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
40	38, 39	eqtr4di 2782	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))))
41		ioossre 13344	. . . . . . . . 9 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ⊆ ℝ
42	40, 41	eqsstrdi 3988	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
43	42	ralrimiva 3125	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
44		iunss 5004	. . . . . . 7 ⊢ (∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ ↔ ∀𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
45	43, 44	sylibr 234	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)) ⊆ ℝ)
46	30, 45	eqsstrd 3978	. . . . 5 ⊢ (𝜑 → 𝐾 ⊆ ℝ)
47	29	simprd 495	. . . . 5 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
48		ovolsscl 25420	. . . . 5 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ)
49	18, 46, 47, 48	syl3anc 1373	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
50	23	rpred 12971	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ)
51	49, 50	readdcld 11179	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶) ∈ ℝ)
52		difssd 4096	. . . . 5 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ 𝐾)
53		ovolsscl 25420	. . . . 5 ⊢ (((𝐾 ∖ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∖ 𝐴)) ∈ ℝ)
54	52, 46, 47, 53	syl3anc 1373	. . . 4 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℝ)
55	54, 50	readdcld 11179	. . 3 ⊢ (𝜑 → ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶) ∈ ℝ)
56		ssun2 4138	. . . . . . 7 ⊢ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
57		ioof 13384	. . . . . . . . . . . . . . 15 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
58		rexpssxrxp 11195	. . . . . . . . . . . . . . . . 17 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
59	31, 58	sstri 3953	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
60		fss 6686	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐺:ℕ⟶(ℝ^ × ℝ^*))
61	4, 59, 60	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ^* × ℝ^*))
62		fco 6694	. . . . . . . . . . . . . . 15 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
63	57, 61, 62	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
64	63	ffnd 6671	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
65		fnima 6630	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺) Fn ℕ → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
66	64, 65	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = ran ((,) ∘ 𝐺))
67		nnuz 12812	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ_≥‘1)
68	26	peano2nnd 12179	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ)
69	68, 67	eleqtrdi 2838	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ_≥‘1))
70		uzsplit 13533	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
71	69, 70	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℤ_≥‘1) = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
72	67, 71	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℕ = ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))))
73	26	nncnd 12178	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℂ)
74		ax-1cn 11102	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
75		pncan 11403	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
76	73, 74, 75	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
77	76	oveq2d 7385	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...((𝑀 + 1) − 1)) = (1...𝑀))
78	77	uneq1d 4126	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1...((𝑀 + 1) − 1)) ∪ (ℤ_≥‘(𝑀 + 1))) = ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1))))
79	72, 78	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1))))
80	79	imaeq2d 6020	. . . . . . . . . . . 12 ⊢ (𝜑 → (((,) ∘ 𝐺) “ ℕ) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))))
81	66, 80	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))))
82		imaundi 6110	. . . . . . . . . . 11 ⊢ (((,) ∘ 𝐺) “ ((1...𝑀) ∪ (ℤ_≥‘(𝑀 + 1)))) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
83	81, 82	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝜑 → ran ((,) ∘ 𝐺) = ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
84	83	unieqd 4880	. . . . . . . . 9 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
85		uniun 4890	. . . . . . . . 9 ⊢ ∪ ((((,) ∘ 𝐺) “ (1...𝑀)) ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
86	84, 85	eqtrdi 2780	. . . . . . . 8 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
87	28	uneq1i 4123	. . . . . . . 8 ⊢ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) = (∪ (((,) ∘ 𝐺) “ (1...𝑀)) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
88	86, 87	eqtr4di 2782	. . . . . . 7 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
89	56, 88	sseqtrrid 3987	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺))
90	19, 20, 21, 22, 11, 23, 4, 3, 24, 25	uniioombllem1 25515	. . . . . . 7 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
91		ssid 3966	. . . . . . . 8 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
92	24	ovollb 25413	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
93	4, 91, 92	sylancl 586	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
94		ovollecl 25417	. . . . . . 7 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ^, < ) ∈ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < )) → (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
95	9, 90, 93, 94	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
96		ovolsscl 25420	. . . . . 6 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)
97	89, 9, 95, 96	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)
98	49, 97	readdcld 11179	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
99		unss1 4144	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ⊆ 𝐾 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
100	17, 99	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
101	100, 88	sseqtrrid 3987	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
102		ovolsscl 25420	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
103	101, 9, 95, 102	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
104	3, 88	sseqtrd 3980	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
105	104	ssrind 4203	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴))
106		indir 4245	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴) = ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴))
107		inss1 4196	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))
108		unss2 4146	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) → ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
109	107, 108	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∩ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∩ 𝐴)) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
110	106, 109	eqsstri 3990	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
111	105, 110	sstrdi 3956	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
112	101, 9	sstrd 3954	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ)
113		ovolss 25419	. . . . . 6 ⊢ (((𝐸 ∩ 𝐴) ⊆ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∧ ((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol‘(𝐸 ∩ 𝐴)) ≤ (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
114	111, 112, 113	syl2anc 584	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) ≤ (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
115	18, 46	sstrd 3954	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) ⊆ ℝ)
116	89, 9	sstrd 3954	. . . . . 6 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ)
117		ovolun 25433	. . . . . 6 ⊢ ((((𝐾 ∩ 𝐴) ⊆ ℝ ∧ (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
118	115, 49, 116, 97, 117	syl22anc 838	. . . . 5 ⊢ (𝜑 → (vol‘((𝐾 ∩ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
119	13, 103, 98, 114, 118	letrd 11307	. . . 4 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
120		rge0ssre 13393	. . . . . . . 8 ⊢ (0[,)+∞) ⊆ ℝ
121		eqid 2729	. . . . . . . . . . 11 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
122	121, 24	ovolsf 25406	. . . . . . . . . 10 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
123	4, 122	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
124	123, 26	ffvelcdmd 7039	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘𝑀) ∈ (0[,)+∞))
125	120, 124	sselid 3941	. . . . . . 7 ⊢ (𝜑 → (𝑇‘𝑀) ∈ ℝ)
126	90, 125	resubcld 11582	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)) ∈ ℝ)
127	97	rexrd 11200	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ^)
128		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ℕ → 𝑧 ∈ ℕ)
129		nnaddcl 12185	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
130	128, 26, 129	syl2anr 597	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝑧 + 𝑀) ∈ ℕ)
131	4	ffvelcdmda 7038	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 + 𝑀) ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
132	130, 131	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (𝐺‘(𝑧 + 𝑀)) ∈ ( ≤ ∩ (ℝ × ℝ)))
133	132	fmpttd 7069	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
134		eqid 2729	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
135		eqid 2729	. . . . . . . . . . . 12 ⊢ seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) = seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
136	134, 135	ovolsf 25406	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
137	133, 136	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))):ℕ⟶(0[,)+∞))
138	137	frnd 6678	. . . . . . . . 9 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ (0[,)+∞))
139		icossxr 13369	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ^*
140	138, 139	sstrdi 3956	. . . . . . . 8 ⊢ (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^*)
141		supxrcl 13251	. . . . . . . 8 ⊢ (ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) ⊆ ℝ^* → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ∈ ℝ^)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ∈ ℝ^)
143	126	rexrd 11200	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ∈ ℝ^)
144		1zzd 12540	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 1 ∈ ℤ)
145	26	nnzd 12532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℤ)
146	145	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ ℤ)
147		addcom 11336	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + 1) = (1 + 𝑀))
148	73, 74, 147	sylancl 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 + 1) = (1 + 𝑀))
149	148	fveq2d 6844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) = (ℤ_≥‘(1 + 𝑀)))
150	149	eleq2d 2814	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) ↔ 𝑥 ∈ (ℤ_≥‘(1 + 𝑀))))
151	150	biimpa 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ (ℤ_≥‘(1 + 𝑀)))
152		eluzsub 12799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ (ℤ_≥‘(1 + 𝑀))) → (𝑥 − 𝑀) ∈ (ℤ_≥‘1))
153	144, 146, 151, 152	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ (ℤ_≥‘1))
154	153, 67	eleqtrrdi 2839	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → (𝑥 − 𝑀) ∈ ℕ)
155		eluzelz 12779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑥 ∈ ℤ)
156	155	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ℤ)
157	156	zcnd 12615	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ℂ)
158	73	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑀 ∈ ℂ)
159	157, 158	npcand 11513	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → ((𝑥 − 𝑀) + 𝑀) = 𝑥)
160	159	eqcomd 2735	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 = ((𝑥 − 𝑀) + 𝑀))
161		oveq1 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = (𝑥 − 𝑀) → (𝑧 + 𝑀) = ((𝑥 − 𝑀) + 𝑀))
162	161	rspceeqv 3608	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 − 𝑀) ∈ ℕ ∧ 𝑥 = ((𝑥 − 𝑀) + 𝑀)) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
163	154, 160, 162	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
164		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) = (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))
165	164	elrnmpt 5911	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀)))
166	165	elv 3449	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) ↔ ∃𝑧 ∈ ℕ 𝑥 = (𝑧 + 𝑀))
167	163, 166	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ_≥‘(𝑀 + 1))) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
168	167	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (ℤ_≥‘(𝑀 + 1)) → 𝑥 ∈ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
169	168	ssrdv 3949	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
170		imass2 6062	. . . . . . . . . . . . 13 ⊢ ((ℤ_≥‘(𝑀 + 1)) ⊆ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)) → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
171	169, 170	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))))
172		rnco2 6214	. . . . . . . . . . . . 13 ⊢ ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀)))
173	4, 130	cofmpt 7086	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
174	173	rneqd 5891	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran (𝐺 ∘ (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
175	172, 174	eqtr3id 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 “ ran (𝑧 ∈ ℕ ↦ (𝑧 + 𝑀))) = ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
176	171, 175	sseqtrd 3980	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
177		imass2 6062	. . . . . . . . . . 11 ⊢ ((𝐺 “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) → ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
178	176, 177	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
179		imaco 6212	. . . . . . . . . 10 ⊢ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) = ((,) “ (𝐺 “ (ℤ_≥‘(𝑀 + 1))))
180		rnco2 6214	. . . . . . . . . 10 ⊢ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))) = ((,) “ ran (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))
181	178, 179, 180	3sstr4g 3997	. . . . . . . . 9 ⊢ (𝜑 → (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
182	181	unissd 4877	. . . . . . . 8 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ∪ ran ((,) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))
183	135	ovollb 25413	. . . . . . . 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 6678	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
186	185, 139	sstrdi 3956	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ^*)
187	24	fveq1i 6841	. . . . . . . . . . . . . 14 ⊢ (𝑇‘(𝑀 + 𝑛)) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛))
188	26	nnred 12177	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ ℝ)
189	188	ltp1d 12089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
190		fzdisj 13488	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
191	189, 190	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
192	191	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1...𝑀) ∩ ((𝑀 + 1)...(𝑀 + 𝑛))) = ∅)
193		nnnn0 12425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ₀)
194		nn0addge1 12464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℝ ∧ 𝑛 ∈ ℕ₀) → 𝑀 ≤ (𝑀 + 𝑛))
195	188, 193, 194	syl2an 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ≤ (𝑀 + 𝑛))
196	26	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℕ)
197	196, 67	eleqtrdi 2838	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (ℤ_≥‘1))
198		nnaddcl 12185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
199	26, 198	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℕ)
200	199	nnzd 12532	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ ℤ)
201		elfz5 13453	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ (ℤ_≥‘1) ∧ (𝑀 + 𝑛) ∈ ℤ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
202	197, 200, 201	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 ∈ (1...(𝑀 + 𝑛)) ↔ 𝑀 ≤ (𝑀 + 𝑛)))
203	195, 202	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ (1...(𝑀 + 𝑛)))
204		fzsplit 13487	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ (1...(𝑀 + 𝑛)) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
205	203, 204	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) = ((1...𝑀) ∪ ((𝑀 + 1)...(𝑀 + 𝑛))))
206		fzfid 13914	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...(𝑀 + 𝑛)) ∈ Fin)
207	4	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
208		elfznn 13490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (1...(𝑀 + 𝑛)) → 𝑗 ∈ ℕ)
209		ovolfcl 25400	. . . . . . . . . . . . . . . . . . . 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 11582	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
214	213	recnd 11178	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
215	192, 205, 206, 214	fsumsplit 15683	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗)))))
216	121	ovolfsval 25404	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
217	207, 208, 216	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...(𝑀 + 𝑛))) → (((abs ∘ − ) ∘ 𝐺)‘𝑗) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
218	199, 67	eleqtrdi 2838	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 𝑛) ∈ (ℤ_≥‘1))
219	217, 218, 214	fsumser 15672	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)))
220	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
221	32	adantl 481	. . . . . . . . . . . . . . . . . . 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 11582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
227	226	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
228	227	recnd 11178	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
229	222, 197, 228	fsumser 15672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀))
230	24	fveq1i 6841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇‘𝑀) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑀)
231	229, 230	eqtr4di 2782	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (𝑇‘𝑀))
232	196	nnzd 12532	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℤ)
233	232	peano2zd 12617	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℤ)
234	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
235	196	peano2nnd 12179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀 + 1) ∈ ℕ)
236		elfzuz 13457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛)) → 𝑗 ∈ (ℤ_≥‘(𝑀 + 1)))
237		eluznn 12853	. . . . . . . . . . . . . . . . . . . . . . 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 11582	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
243	242	recnd 11178	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℂ)
244		2fveq3 6845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (2^nd ‘(𝐺‘𝑗)) = (2^nd ‘(𝐺‘(𝑘 + 𝑀))))
245		2fveq3 6845	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑘 + 𝑀) → (1^st ‘(𝐺‘𝑗)) = (1^st ‘(𝐺‘(𝑘 + 𝑀))))
246	244, 245	oveq12d 7387	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑘 + 𝑀) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
247	232, 233, 200, 243, 246	fsumshftm 15723	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
248	196	nncnd 12178	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀 ∈ ℂ)
249		pncan2 11404	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 𝑀) = 1)
250	248, 74, 249	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 1) − 𝑀) = 1)
251		nncn 12170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
252	251	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
253	248, 252	pncan2d 11511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀 + 𝑛) − 𝑀) = 𝑛)
254	250, 253	oveq12d 7387	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀)) = (1...𝑛))
255	254	sumeq1d 15642	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (((𝑀 + 1) − 𝑀)...((𝑀 + 𝑛) − 𝑀))((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) = Σ𝑘 ∈ (1...𝑛)((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
256	133	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
257		elfznn 13490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ)
258	134	ovolfsval 25404	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑘 ∈ ℕ) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
259	256, 257, 258	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))))
260	257	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
261		fvoveq1 7392	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑘 → (𝐺‘(𝑧 + 𝑀)) = (𝐺‘(𝑘 + 𝑀)))
262		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))) = (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))
263		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺‘(𝑘 + 𝑀)) ∈ V
264	261, 262, 263	fvmpt 6950	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
265	260, 264	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘) = (𝐺‘(𝑘 + 𝑀)))
266	265	fveq2d 6844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (2^nd ‘(𝐺‘(𝑘 + 𝑀))))
267	265	fveq2d 6844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) = (1^st ‘(𝐺‘(𝑘 + 𝑀))))
268	266, 267	oveq12d 7387	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘)) − (1^st ‘((𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))‘𝑘))) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
269	259, 268	eqtrd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))‘𝑘) = ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))))
270		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
271	270, 67	eleqtrdi 2838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
272	4	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
273		nnaddcl 12185	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑘 + 𝑀) ∈ ℕ)
274	257, 196, 273	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑘 + 𝑀) ∈ ℕ)
275		ovolfcl 25400	. . . . . . . . . . . . . . . . . . . . . 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 11582	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℝ)
280	279	recnd 11178	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → ((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) ∈ ℂ)
281	269, 271, 280	fsumser 15672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑘 ∈ (1...𝑛)((2^nd ‘(𝐺‘(𝑘 + 𝑀))) − (1^st ‘(𝐺‘(𝑘 + 𝑀)))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
282	247, 255, 281	3eqtrd 2768	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛))
283	231, 282	oveq12d 7387	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑗 ∈ (1...𝑀)((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) + Σ𝑗 ∈ ((𝑀 + 1)...(𝑀 + 𝑛))((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗)))) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
284	215, 219, 283	3eqtr3d 2772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
285	187, 284	eqtrid 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) = ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)))
286	123	ffnd 6671	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn ℕ)
287		fnfvelrn 7034	. . . . . . . . . . . . . 14 ⊢ ((𝑇 Fn ℕ ∧ (𝑀 + 𝑛) ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
288	286, 199, 287	syl2an2r 685	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘(𝑀 + 𝑛)) ∈ ran 𝑇)
289	285, 288	eqeltrrd 2829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇)
290		supxrub 13260	. . . . . . . . . . . 12 ⊢ ((ran 𝑇 ⊆ ℝ^* ∧ ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ∈ ran 𝑇) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^*, < ))
291	186, 289, 290	syl2an2r 685	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^*, < ))
292	125	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑀) ∈ ℝ)
293	137	ffvelcdmda 7038	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ (0[,)+∞))
294	120, 293	sselid 3941	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ∈ ℝ)
295	90	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
296	292, 294, 295	leaddsub2d 11756	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑇‘𝑀) + (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛)) ≤ sup(ran 𝑇, ℝ^, < ) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
297	291, 296	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
298	297	ralrimiva 3125	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
299	137	ffnd 6671	. . . . . . . . . 10 ⊢ (𝜑 → seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))) Fn ℕ)
300		breq1 5105	. . . . . . . . . . 11 ⊢ (𝑥 = (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) → (𝑥 ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)) ↔ (seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))‘𝑛) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀))))
301	300	ralrn 7042	. . . . . . . . . 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 257	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀)))))𝑥 ≤ (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)))
304		supxrleub 13262	. . . . . . . . 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 257	. . . . . . 7 ⊢ (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ (𝑧 ∈ ℕ ↦ (𝐺‘(𝑧 + 𝑀))))), ℝ^, < ) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)))
307	127, 142, 143, 184, 306	xrletrd 13098	. . . . . 6 ⊢ (𝜑 → (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ≤ (sup(ran 𝑇, ℝ^, < ) − (𝑇‘𝑀)))
308	125, 90, 50	absdifltd 15378	. . . . . . . . 9 ⊢ (𝜑 → ((abs‘((𝑇‘𝑀) − sup(ran 𝑇, ℝ^, < ))) < 𝐶 ↔ ((sup(ran 𝑇, ℝ^, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ^*, < ) + 𝐶))))
309	27, 308	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((sup(ran 𝑇, ℝ^, < ) − 𝐶) < (𝑇‘𝑀) ∧ (𝑇‘𝑀) < (sup(ran 𝑇, ℝ^, < ) + 𝐶)))
310	309	simpld 494	. . . . . . 7 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − 𝐶) < (𝑇‘𝑀))
311	90, 50, 125, 310	ltsub23d 11759	. . . . . 6 ⊢ (𝜑 → (sup(ran 𝑇, ℝ^*, < ) − (𝑇‘𝑀)) < 𝐶)
312	97, 126, 50, 307, 311	lelttrd 11308	. . . . 5 ⊢ (𝜑 → (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) < 𝐶)
313	97, 50, 49, 312	ltadd2dd 11309	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∩ 𝐴)) + 𝐶))
314	13, 98, 51, 119, 313	lelttrd 11308	. . 3 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐴)) < ((vol‘(𝐾 ∩ 𝐴)) + 𝐶))
315	54, 97	readdcld 11179	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∖ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
316		difss 4095	. . . . . . . 8 ⊢ (𝐾 ∖ 𝐴) ⊆ 𝐾
317		unss1 4144	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ⊆ 𝐾 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
318	316, 317	ax-mp 5	. . . . . . 7 ⊢ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ (𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
319	318, 88	sseqtrrid 3987	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺))
320		ovolsscl 25420	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
321	319, 9, 95, 320	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (vol*‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ∈ ℝ)
322	104	ssdifd 4104	. . . . . . 7 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴))
323		difundir 4250	. . . . . . . 8 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴) = ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴))
324		difss 4095	. . . . . . . . 9 ⊢ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))
325		unss2 4146	. . . . . . . . 9 ⊢ ((∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴) ⊆ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) → ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
326	324, 325	ax-mp 5	. . . . . . . 8 ⊢ ((𝐾 ∖ 𝐴) ∪ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ∖ 𝐴)) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
327	323, 326	eqsstri 3990	. . . . . . 7 ⊢ ((𝐾 ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))
328	322, 327	sstrdi 3956	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))))
329	319, 9	sstrd 3954	. . . . . 6 ⊢ (𝜑 → ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ)
330		ovolss 25419	. . . . . 6 ⊢ (((𝐸 ∖ 𝐴) ⊆ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∧ ((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ⊆ ℝ) → (vol‘(𝐸 ∖ 𝐴)) ≤ (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
331	328, 329, 330	syl2anc 584	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) ≤ (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
332	52, 46	sstrd 3954	. . . . . 6 ⊢ (𝜑 → (𝐾 ∖ 𝐴) ⊆ ℝ)
333		ovolun 25433	. . . . . 6 ⊢ ((((𝐾 ∖ 𝐴) ⊆ ℝ ∧ (vol‘(𝐾 ∖ 𝐴)) ∈ ℝ) ∧ (∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))) ⊆ ℝ ∧ (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1)))) ∈ ℝ)) → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
334	332, 54, 116, 97, 333	syl22anc 838	. . . . 5 ⊢ (𝜑 → (vol‘((𝐾 ∖ 𝐴) ∪ ∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
335	16, 321, 315, 331, 334	letrd 11307	. . . 4 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) ≤ ((vol‘(𝐾 ∖ 𝐴)) + (vol*‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))))
336	97, 50, 54, 312	ltadd2dd 11309	. . . 4 ⊢ (𝜑 → ((vol‘(𝐾 ∖ 𝐴)) + (vol‘∪ (((,) ∘ 𝐺) “ (ℤ_≥‘(𝑀 + 1))))) < ((vol*‘(𝐾 ∖ 𝐴)) + 𝐶))
337	16, 315, 55, 335, 336	lelttrd 11308	. . 3 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐴)) < ((vol‘(𝐾 ∖ 𝐴)) + 𝐶))
338	13, 16, 51, 55, 314, 337	lt2addd 11777	. 2 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol‘(𝐾 ∖ 𝐴)) + 𝐶)))
339	49	recnd 11178	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℂ)
340	50	recnd 11178	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ)
341	54	recnd 11178	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∖ 𝐴)) ∈ ℂ)
342	339, 340, 341, 340	add4d 11379	. 2 ⊢ (𝜑 → (((vol‘(𝐾 ∩ 𝐴)) + 𝐶) + ((vol‘(𝐾 ∖ 𝐴)) + 𝐶)) = (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))
343	338, 342	breqtrd 5128	1 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐴)) + (vol‘(𝐸 ∖ 𝐴))) < (((vol‘(𝐾 ∩ 𝐴)) + (vol‘(𝐾 ∖ 𝐴))) + (𝐶 + 𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3444 ∖ cdif 3908 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ∅c0 4292 𝒫 cpw 4559 ⟨cop 4591 ∪ cuni 4867 ∪ ciun 4951 Disj wdisj 5069 class class class wbr 5102 ↦ cmpt 5183 × cxp 5629 ran crn 5632 “ cima 5634 ∘ ccom 5635 Fn wfn 6494 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 1^st c1st 7945 2^nd c2nd 7946 supcsup 9367 ℂcc 11042 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 +∞cpnf 11181 ℝ^*cxr 11183 < clt 11184 ≤ cle 11185 − cmin 11381 ℕcn 12162 ℕ₀cn0 12418 ℤcz 12505 ℤ_≥cuz 12769 ℝ⁺crp 12927 (,)cioo 13282 [,)cico 13284 [,]cicc 13285 ...cfz 13444 seqcseq 13942 abscabs 15176 Σcsu 15628 vol*covol 25396

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-of 7633 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-er 8648 df-map 8778 df-pm 8779 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fi 9338 df-sup 9369 df-inf 9370 df-oi 9439 df-dju 9830 df-card 9868 df-acn 9871 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-z 12506 df-uz 12770 df-q 12884 df-rp 12928 df-xneg 13048 df-xadd 13049 df-xmul 13050 df-ioo 13286 df-ico 13288 df-icc 13289 df-fz 13445 df-fzo 13592 df-fl 13730 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-rlim 15431 df-sum 15629 df-rest 17361 df-topgen 17382 df-psmet 21288 df-xmet 21289 df-met 21290 df-bl 21291 df-mopn 21292 df-top 22814 df-topon 22831 df-bases 22866 df-cmp 23307 df-ovol 25398 df-vol 25399

This theorem is referenced by: uniioombllem5 25521

W3C validator