Theorem ioombl1lem4 25541

Description: Lemma for ioombl1 25542. (Contributed by Mario Carneiro, 16-Jun-2014.)

Hypotheses

Ref	Expression
ioombl1.b	⊢ 𝐵 = (𝐴(,)+∞)
ioombl1.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ioombl1.e	⊢ (𝜑 → 𝐸 ⊆ ℝ)
ioombl1.v	⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
ioombl1.c	⊢ (𝜑 → 𝐶 ∈ ℝ+)
ioombl1.s	⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ioombl1.t	⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
ioombl1.u	⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
ioombl1.f1	⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ioombl1.f2	⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))
ioombl1.f3	⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
ioombl1.p	⊢ 𝑃 = (1st ‘(𝐹‘𝑛))
ioombl1.q	⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))
ioombl1.g	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
ioombl1.h	⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)

Assertion

Ref	Expression
ioombl1lem4	⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ ((vol*‘𝐸) + 𝐶))

Distinct variable groups:   𝐵,𝑛   𝐶,𝑛   𝑛,𝐸   𝑛,𝐹   𝑛,𝐺   𝑛,𝐻   𝜑,𝑛   𝑆,𝑛

Allowed substitution hints:   𝐴(𝑛)   𝑃(𝑛)   𝑄(𝑛)   𝑇(𝑛)   𝑈(𝑛)

Proof of Theorem ioombl1lem4

Dummy variables 𝑥 𝑗 𝑘 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 4178	. . . 4 ⊢ (𝐸 ∩ 𝐵) ⊆ 𝐸
2		ioombl1.e	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
3		ioombl1.v	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
4		ovolsscl 25466	. . . 4 ⊢ (((𝐸 ∩ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
5	1, 2, 3, 4	mp3an2i 1469	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
6		difss 4077	. . . 4 ⊢ (𝐸 ∖ 𝐵) ⊆ 𝐸
7		ovolsscl 25466	. . . 4 ⊢ (((𝐸 ∖ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
8	6, 2, 3, 7	mp3an2i 1469	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
9	5, 8	readdcld 11168	. 2 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ∈ ℝ)
10		ioombl1.b	. . 3 ⊢ 𝐵 = (𝐴(,)+∞)
11		ioombl1.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
12		ioombl1.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ+)
13		ioombl1.s	. . 3 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
14		ioombl1.t	. . 3 ⊢ 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
15		ioombl1.u	. . 3 ⊢ 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
16		ioombl1.f1	. . 3 ⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
17		ioombl1.f2	. . 3 ⊢ (𝜑 → 𝐸 ⊆ ∪ ran ((,) ∘ 𝐹))
18		ioombl1.f3	. . 3 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
19		ioombl1.p	. . 3 ⊢ 𝑃 = (1st ‘(𝐹‘𝑛))
20		ioombl1.q	. . 3 ⊢ 𝑄 = (2nd ‘(𝐹‘𝑛))
21		ioombl1.g	. . 3 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
22		ioombl1.h	. . 3 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
23	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem2 25539	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
24	12	rpred 12980	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
25	3, 24	readdcld 11168	. 2 ⊢ (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ)
26	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem1 25538	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
27	26	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
28		eqid 2737	. . . . . . . . 9 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
29	28, 14	ovolsf 25452	. . . . . . . 8 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
30	27, 29	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
31	30	frnd 6671	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
32		rge0ssre 13403	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
33	31, 32	sstrdi 3935	. . . . 5 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
34		1nn 12179	. . . . . . . 8 ⊢ 1 ∈ ℕ
35	30	fdmd 6673	. . . . . . . 8 ⊢ (𝜑 → dom 𝑇 = ℕ)
36	34, 35	eleqtrrid 2844	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑇)
37	36	ne0d 4283	. . . . . 6 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
38		dm0rn0 5874	. . . . . . 7 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
39	38	necon3bii 2985	. . . . . 6 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
40	37, 39	sylib 218	. . . . 5 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
41	30	ffvelcdmda 7031	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ (0[,)+∞))
42	32, 41	sselid 3920	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℝ)
43		eqid 2737	. . . . . . . . . . . . 13 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
44	43, 13	ovolsf 25452	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
45	16, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
46	45	ffvelcdmda 7031	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ (0[,)+∞))
47	32, 46	sselid 3920	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ ℝ)
48	23	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
49		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
50		nnuz 12821	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
51	49, 50	eleqtrdi 2847	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ≥‘1))
52		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑)
53		elfznn 13501	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
54	28	ovolfsf 25451	. . . . . . . . . . . . . . 15 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
55	27, 54	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
56	55	ffvelcdmda 7031	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞))
57	32, 56	sselid 3920	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
58	52, 53, 57	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
59	43	ovolfsf 25451	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
60	16, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
61	60	ffvelcdmda 7031	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞))
62		elrege0 13401	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
63	61, 62	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
64	63	simpld 494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
65	52, 53, 64	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
66	26	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
67		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
68	67	ovolfsf 25451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
69	66, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
70	69	ffvelcdmda 7031	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞))
71		elrege0 13401	. . . . . . . . . . . . . . . 16 ⊢ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
72	70, 71	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
73	72	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛))
74	72	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
75	57, 74	addge01d 11732	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
76	73, 75	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
77	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem3 25540	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
78	76, 77	breqtrd 5112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
79	52, 53, 78	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
80	51, 58, 65, 79	serle 14013	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
81	14	fveq1i 6836	. . . . . . . . . 10 ⊢ (𝑇‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗)
82	13	fveq1i 6836	. . . . . . . . . 10 ⊢ (𝑆‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗)
83	80, 81, 82	3brtr4g 5120	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ (𝑆‘𝑗))
84		1zzd 12552	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℤ)
85		eqidd 2738	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
86	63	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
87	45	frnd 6671	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
88		icossxr 13379	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0[,)+∞) ⊆ ℝ*
89	87, 88	sstrdi 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ*)
90	89	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
91	45	ffnd 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑆 Fn ℕ)
92		fnfvelrn 7027	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
93	91, 92	sylan 581	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
94		supxrub 13270	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘𝑘) ∈ ran 𝑆) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
95	90, 93, 94	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
96	95	ralrimiva 3130	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
97		brralrspcev 5146	. . . . . . . . . . . . . . . 16 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
98	23, 96, 97	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
99	50, 13, 84, 85, 64, 86, 98	isumsup2 15805	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
100	87, 32	sstrdi 3935	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
101	45	fdmd 6673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom 𝑆 = ℕ)
102	34, 101	eleqtrrid 2844	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ dom 𝑆)
103	102	ne0d 4283	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
104		dm0rn0 5874	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
105	104	necon3bii 2985	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
106	103, 105	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
107		breq1 5089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑆‘𝑘) ≤ 𝑥))
108	107	ralrn 7035	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
109	91, 108	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
110	109	rexbidv 3162	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
111	98, 110	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥)
112		supxrre 13273	. . . . . . . . . . . . . . 15 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
113	100, 106, 111, 112	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
114	99, 113	breqtrrd 5114	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
115	114	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
116	13, 115	eqbrtrrid 5122	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇝ sup(ran 𝑆, ℝ*, < ))
117	64	adantlr 716	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
118	86	adantlr 716	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
119	50, 49, 116, 117, 118	climserle 15619	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
120	82, 119	eqbrtrid 5121	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
121	42, 47, 48, 83, 120	letrd 11297	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
122	121	ralrimiva 3130	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
123		brralrspcev 5146	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
124	23, 122, 123	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
125	30	ffnd 6664	. . . . . . . 8 ⊢ (𝜑 → 𝑇 Fn ℕ)
126		breq1 5089	. . . . . . . . 9 ⊢ (𝑧 = (𝑇‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑇‘𝑗) ≤ 𝑥))
127	126	ralrn 7035	. . . . . . . 8 ⊢ (𝑇 Fn ℕ → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
128	125, 127	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
129	128	rexbidv 3162	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
130	124, 129	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥)
131	33, 40, 130	suprcld 12113	. . . 4 ⊢ (𝜑 → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
132	67, 15	ovolsf 25452	. . . . . . . 8 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
133	66, 132	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
134	133	frnd 6671	. . . . . 6 ⊢ (𝜑 → ran 𝑈 ⊆ (0[,)+∞))
135	134, 32	sstrdi 3935	. . . . 5 ⊢ (𝜑 → ran 𝑈 ⊆ ℝ)
136	133	fdmd 6673	. . . . . . . 8 ⊢ (𝜑 → dom 𝑈 = ℕ)
137	34, 136	eleqtrrid 2844	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑈)
138	137	ne0d 4283	. . . . . 6 ⊢ (𝜑 → dom 𝑈 ≠ ∅)
139		dm0rn0 5874	. . . . . . 7 ⊢ (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
140	139	necon3bii 2985	. . . . . 6 ⊢ (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
141	138, 140	sylib 218	. . . . 5 ⊢ (𝜑 → ran 𝑈 ≠ ∅)
142	133	ffvelcdmda 7031	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ (0[,)+∞))
143	32, 142	sselid 3920	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℝ)
144	52, 53, 74	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
145		elrege0 13401	. . . . . . . . . . . . . . . 16 ⊢ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
146	56, 145	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
147	146	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛))
148	74, 57	addge02d 11733	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
149	147, 148	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
150	149, 77	breqtrd 5112	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
151	52, 53, 150	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
152	51, 144, 65, 151	serle 14013	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
153	15	fveq1i 6836	. . . . . . . . . 10 ⊢ (𝑈‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)
154	152, 153, 82	3brtr4g 5120	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ (𝑆‘𝑗))
155	143, 47, 48, 154, 120	letrd 11297	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
156	155	ralrimiva 3130	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
157		brralrspcev 5146	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
158	23, 156, 157	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
159	133	ffnd 6664	. . . . . . . 8 ⊢ (𝜑 → 𝑈 Fn ℕ)
160		breq1 5089	. . . . . . . . 9 ⊢ (𝑧 = (𝑈‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑈‘𝑗) ≤ 𝑥))
161	160	ralrn 7035	. . . . . . . 8 ⊢ (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
162	159, 161	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
163	162	rexbidv 3162	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
164	158, 163	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥)
165	135, 141, 164	suprcld 12113	. . . 4 ⊢ (𝜑 → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
166		ssralv 3991	. . . . . . . . . 10 ⊢ ((𝐸 ∩ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
167	1, 166	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))
168	19	breq1i 5093	. . . . . . . . . . . . 13 ⊢ (𝑃 < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < 𝑥)
169		ovolfcl 25446	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
170	16, 169	sylan 581	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
171	170	simp1d 1143	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ)
172	19, 171	eqeltrid 2841	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
173	172	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
174	1, 2	sstrid 3934	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ℝ)
175	174	sselda 3922	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → 𝑥 ∈ ℝ)
176	175	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
177		ltle 11228	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
178	173, 176, 177	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
179		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
180		opex 5412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V
181	21	fvmpt2 6954	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
182	179, 180, 181	sylancl 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
183	182	fveq2d 6839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺‘𝑛)) = (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
184	11	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
185	184, 172	ifcld 4514	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
186	170	simp2d 1144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ)
187	20, 186	eqeltrid 2841	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
188	185, 187	ifcld 4514	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
189		op1stg 7948	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
190	188, 187, 189	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
191	183, 190	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
192	191	ad2ant2r 748	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (1st ‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
193	188	ad2ant2r 748	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
194	185	ad2ant2r 748	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
195	174	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (𝐸 ∩ 𝐵) ⊆ ℝ)
196		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ (𝐸 ∩ 𝐵))
197	195, 196	sseldd 3923	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ ℝ)
198	187	ad2ant2r 748	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑄 ∈ ℝ)
199		min1 13135	. . . . . . . . . . . . . . . . . 18 ⊢ ((if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
200	194, 198, 199	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
201	11	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ∈ ℝ)
202		elinel2 4143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∩ 𝐵) → 𝑥 ∈ 𝐵)
203	202	ad2antlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ 𝐵)
204	11	rexrd 11189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
205		pnfxr 11193	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ +∞ ∈ ℝ*
206		elioo2 13333	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
207	204, 205, 206	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
208	10	eleq2i 2829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (𝐴(,)+∞))
209		ltpnf 13065	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝑥 < +∞)
211	210	pm4.71i 559	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
212		df-3an 1089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
213	211, 212	bitr4i 278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞))
214	207, 208, 213	3bitr4g 314	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
215		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝐴 < 𝑥)
216	214, 215	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝐴 < 𝑥))
217	216	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (𝑥 ∈ 𝐵 → 𝐴 < 𝑥))
218	203, 217	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 < 𝑥)
219	201, 197, 218	ltled 11288	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ≤ 𝑥)
220		simprr 773	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑃 ≤ 𝑥)
221		breq1 5089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝐴 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
222		breq1 5089	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝑃 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
223	221, 222	ifboth 4507	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≤ 𝑥 ∧ 𝑃 ≤ 𝑥) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
224	219, 220, 223	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
225	193, 194, 197, 200, 224	letrd 11297	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑥)
226	192, 225	eqbrtrd 5108	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (1st ‘(𝐺‘𝑛)) ≤ 𝑥)
227	226	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 ≤ 𝑥 → (1st ‘(𝐺‘𝑛)) ≤ 𝑥))
228	178, 227	syld 47	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → (1st ‘(𝐺‘𝑛)) ≤ 𝑥))
229	168, 228	biimtrrid 243	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → (1st ‘(𝐺‘𝑛)) ≤ 𝑥))
230	20	breq2i 5094	. . . . . . . . . . . . . 14 ⊢ (𝑥 < 𝑄 ↔ 𝑥 < (2nd ‘(𝐹‘𝑛)))
231	187	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
232		ltle 11228	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
233	176, 231, 232	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
234	230, 233	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ 𝑄))
235	182	fveq2d 6839	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
236		op2ndg 7949	. . . . . . . . . . . . . . . . 17 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
237	188, 187, 236	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
238	235, 237	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = 𝑄)
239	238	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = 𝑄)
240	239	breq2d 5098	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ (2nd ‘(𝐺‘𝑛)) ↔ 𝑥 ≤ 𝑄))
241	234, 240	sylibrd 259	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ (2nd ‘(𝐺‘𝑛))))
242	229, 241	anim12d 610	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
243	242	reximdva 3151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
244	243	ralimdva 3150	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
245	167, 244	syl5 34	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
246		ovolfioo 25447	. . . . . . . . 9 ⊢ ((𝐸 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
247	2, 16, 246	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
248		ovolficc 25448	. . . . . . . . 9 ⊢ (((𝐸 ∩ 𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
249	174, 27, 248	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
250	245, 247, 249	3imtr4d 294	. . . . . . 7 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) → (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)))
251	17, 250	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺))
252	14	ovollb2 25469	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)) → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
253	27, 251, 252	syl2anc 585	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
254		supxrre 13273	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
255	33, 40, 130, 254	syl3anc 1374	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
256	253, 255	breqtrd 5112	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ, < ))
257		ssralv 3991	. . . . . . . . . 10 ⊢ ((𝐸 ∖ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
258	6, 257	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))
259	172	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
260	6, 2	sstrid 3934	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ℝ)
261	260	sselda 3922	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → 𝑥 ∈ ℝ)
262	261	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
263	259, 262, 177	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
264	168, 263	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → 𝑃 ≤ 𝑥))
265		opex 5412	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V
266	22	fvmpt2 6954	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
267	179, 265, 266	sylancl 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
268	267	fveq2d 6839	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
269		op1stg 7948	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
270	172, 188, 269	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
271	268, 270	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = 𝑃)
272	271	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = 𝑃)
273	272	breq1d 5096	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ↔ 𝑃 ≤ 𝑥))
274	264, 273	sylibrd 259	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → (1st ‘(𝐻‘𝑛)) ≤ 𝑥))
275	187	adantlr 716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
276	262, 275, 232	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
277	260	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐸 ∖ 𝐵) ⊆ ℝ)
278		simplr 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ (𝐸 ∖ 𝐵))
279	277, 278	sseldd 3923	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ ℝ)
280	11	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ∈ ℝ)
281	172	ad2ant2r 748	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑃 ∈ ℝ)
282	280, 281	ifcld 4514	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
283		eldifn 4073	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
284	283	ad2antlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → ¬ 𝑥 ∈ 𝐵)
285	279	biantrurd 532	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐴 < 𝑥 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
286	214	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
287	285, 286	bitr4d 282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐴 < 𝑥 ↔ 𝑥 ∈ 𝐵))
288	284, 287	mtbird 325	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → ¬ 𝐴 < 𝑥)
289	279, 280, 288	nltled 11290	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝐴)
290		max2 13133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
291	281, 280, 290	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
292	279, 280, 282, 289, 291	letrd 11297	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
293		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝑄)
294		breq2 5090	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑃 ≤ 𝐴, 𝐴, 𝑃) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
295		breq2 5090	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑄 = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ 𝑄 ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
296	294, 295	ifboth 4507	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∧ 𝑥 ≤ 𝑄) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
297	292, 293, 296	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
298	267	fveq2d 6839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐻‘𝑛)) = (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
299		op2ndg 7949	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
300	172, 188, 299	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
301	298, 300	eqtrd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
302	301	ad2ant2r 748	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (2nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
303	297, 302	breqtrrd 5114	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))
304	303	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ 𝑄 → 𝑥 ≤ (2nd ‘(𝐻‘𝑛))))
305	276, 304	syld 47	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ (2nd ‘(𝐻‘𝑛))))
306	230, 305	biimtrrid 243	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ (2nd ‘(𝐻‘𝑛))))
307	274, 306	anim12d 610	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
308	307	reximdva 3151	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
309	308	ralimdva 3150	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
310	258, 309	syl5 34	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
311		ovolficc 25448	. . . . . . . . 9 ⊢ (((𝐸 ∖ 𝐵) ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
312	260, 66, 311	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
313	310, 247, 312	3imtr4d 294	. . . . . . 7 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) → (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)))
314	17, 313	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻))
315	15	ovollb2 25469	. . . . . 6 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)) → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
316	66, 314, 315	syl2anc 585	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
317		supxrre 13273	. . . . . 6 ⊢ ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥) → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
318	135, 141, 164, 317	syl3anc 1374	. . . . 5 ⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
319	316, 318	breqtrd 5112	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ, < ))
320	5, 8, 131, 165, 256, 319	le2addd 11763	. . 3 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
321		eqidd 2738	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐺)‘𝑛))
322	50, 14, 84, 321, 57, 147, 124	isumsup2 15805	. . . . 5 ⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
323		seqex 13959	. . . . . . 7 ⊢ seq1( + , ((abs ∘ − ) ∘ 𝐹)) ∈ V
324	13, 323	eqeltri 2833	. . . . . 6 ⊢ 𝑆 ∈ V
325	324	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ V)
326		eqidd 2738	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) = (((abs ∘ − ) ∘ 𝐻)‘𝑛))
327	50, 15, 84, 326, 74, 73, 158	isumsup2 15805	. . . . 5 ⊢ (𝜑 → 𝑈 ⇝ sup(ran 𝑈, ℝ, < ))
328	42	recnd 11167	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℂ)
329	143	recnd 11167	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℂ)
330	57	recnd 11167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
331	52, 53, 330	syl2an 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
332	74	recnd 11167	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
333	52, 53, 332	syl2an 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
334	77	eqcomd 2743	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
335	52, 53, 334	syl2an 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
336	51, 331, 333, 335	seradd 14000	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)))
337	81, 153	oveq12i 7373	. . . . . 6 ⊢ ((𝑇‘𝑗) + (𝑈‘𝑗)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗))
338	336, 82, 337	3eqtr4g 2797	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) = ((𝑇‘𝑗) + (𝑈‘𝑗)))
339	50, 84, 322, 325, 327, 328, 329, 338	climadd 15588	. . . 4 ⊢ (𝜑 → 𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
340		climuni 15508	. . . 4 ⊢ ((𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) ∧ 𝑆 ⇝ sup(ran 𝑆, ℝ*, < )) → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
341	339, 114, 340	syl2anc 585	. . 3 ⊢ (𝜑 → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
342	320, 341	breqtrd 5112	. 2 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ sup(ran 𝑆, ℝ*, < ))
343	9, 23, 25, 342, 18	letrd 11297	1 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ ((vol*‘𝐸) + 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ∖ cdif 3887   ∩ cin 3889   ⊆ wss 3890  ∅c0 4274  ifcif 4467  ⟨cop 4574  ∪ cuni 4851   class class class wbr 5086   ↦ cmpt 5167   × cxp 5623  dom cdm 5625  ran crn 5626   ∘ ccom 5629   Fn wfn 6488  ⟶wf 6489  ‘cfv 6493  (class class class)co 7361  1^st c1st 7934  2^nd c2nd 7935  supcsup 9347  ℂcc 11030  ℝcr 11031  0cc0 11032  1c1 11033   + caddc 11035  +∞cpnf 11170  ℝ^*cxr 11172   < clt 11173   ≤ cle 11174   − cmin 11371  ℕcn 12168  ℤ_≥cuz 12782  ℝ⁺crp 12936  (,)cioo 13292  [,)cico 13294  [,]cicc 13295  ...cfz 13455  seqcseq 13957  abscabs 15190   ⇝ cli 15440  vol*covol 25442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-inf2 9556  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109  ax-pre-sup 11110

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-1st 7936  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-map 8769  df-pm 8770  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-sup 9349  df-inf 9350  df-oi 9419  df-card 9857  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-div 11802  df-nn 12169  df-2 12238  df-3 12239  df-n0 12432  df-z 12519  df-uz 12783  df-q 12893  df-rp 12937  df-ioo 13296  df-ico 13298  df-icc 13299  df-fz 13456  df-fzo 13603  df-fl 13745  df-seq 13958  df-exp 14018  df-hash 14287  df-cj 15055  df-re 15056  df-im 15057  df-sqrt 15191  df-abs 15192  df-clim 15444  df-rlim 15445  df-sum 15643  df-ovol 25444

This theorem is referenced by:  ioombl1  25542