Theorem ioombl1lem4 25610

Description: Lemma for ioombl1 25611. (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 4245	. . . 4 ⊢ (𝐸 ∩ 𝐵) ⊆ 𝐸
2		ioombl1.e	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
3		ioombl1.v	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
4		ovolsscl 25535	. . . 4 ⊢ (((𝐸 ∩ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
5	1, 2, 3, 4	mp3an2i 1465	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
6		difss 4146	. . . 4 ⊢ (𝐸 ∖ 𝐵) ⊆ 𝐸
7		ovolsscl 25535	. . . 4 ⊢ (((𝐸 ∖ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
8	6, 2, 3, 7	mp3an2i 1465	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
9	5, 8	readdcld 11288	. 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 25608	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
24	12	rpred 13075	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
25	3, 24	readdcld 11288	. 2 ⊢ (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ)
26	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem1 25607	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
27	26	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
28		eqid 2735	. . . . . . . . 9 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
29	28, 14	ovolsf 25521	. . . . . . . 8 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
30	27, 29	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
31	30	frnd 6745	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
32		rge0ssre 13493	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
33	31, 32	sstrdi 4008	. . . . 5 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
34		1nn 12275	. . . . . . . 8 ⊢ 1 ∈ ℕ
35	30	fdmd 6747	. . . . . . . 8 ⊢ (𝜑 → dom 𝑇 = ℕ)
36	34, 35	eleqtrrid 2846	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑇)
37	36	ne0d 4348	. . . . . 6 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
38		dm0rn0 5938	. . . . . . 7 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
39	38	necon3bii 2991	. . . . . 6 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
40	37, 39	sylib 218	. . . . 5 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
41	30	ffvelcdmda 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ (0[,)+∞))
42	32, 41	sselid 3993	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℝ)
43		eqid 2735	. . . . . . . . . . . . 13 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
44	43, 13	ovolsf 25521	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
45	16, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
46	45	ffvelcdmda 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ (0[,)+∞))
47	32, 46	sselid 3993	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ ℝ)
48	23	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
49		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
50		nnuz 12919	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
51	49, 50	eleqtrdi 2849	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ≥‘1))
52		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑)
53		elfznn 13590	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
54	28	ovolfsf 25520	. . . . . . . . . . . . . . 15 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
55	27, 54	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
56	55	ffvelcdmda 7104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞))
57	32, 56	sselid 3993	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
58	52, 53, 57	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
59	43	ovolfsf 25520	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
60	16, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
61	60	ffvelcdmda 7104	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞))
62		elrege0 13491	. . . . . . . . . . . . . 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 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
66	26	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
67		eqid 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
68	67	ovolfsf 25520	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
69	66, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
70	69	ffvelcdmda 7104	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞))
71		elrege0 13491	. . . . . . . . . . . . . . . 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 11849	. . . . . . . . . . . . . 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 25609	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
78	76, 77	breqtrd 5174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
79	52, 53, 78	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
80	51, 58, 65, 79	serle 14095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
81	14	fveq1i 6908	. . . . . . . . . 10 ⊢ (𝑇‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗)
82	13	fveq1i 6908	. . . . . . . . . 10 ⊢ (𝑆‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗)
83	80, 81, 82	3brtr4g 5182	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ (𝑆‘𝑗))
84		1zzd 12646	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℤ)
85		eqidd 2736	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
86	63	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
87	45	frnd 6745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
88		icossxr 13469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0[,)+∞) ⊆ ℝ*
89	87, 88	sstrdi 4008	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ*)
90	89	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
91	45	ffnd 6738	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑆 Fn ℕ)
92		fnfvelrn 7100	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
93	91, 92	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
94		supxrub 13363	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘𝑘) ∈ ran 𝑆) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
95	90, 93, 94	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
96	95	ralrimiva 3144	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
97		brralrspcev 5208	. . . . . . . . . . . . . . . 16 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
98	23, 96, 97	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
99	50, 13, 84, 85, 64, 86, 98	isumsup2 15879	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
100	87, 32	sstrdi 4008	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
101	45	fdmd 6747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom 𝑆 = ℕ)
102	34, 101	eleqtrrid 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ dom 𝑆)
103	102	ne0d 4348	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
104		dm0rn0 5938	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
105	104	necon3bii 2991	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
106	103, 105	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
107		breq1 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑆‘𝑘) ≤ 𝑥))
108	107	ralrn 7108	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
109	91, 108	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
110	109	rexbidv 3177	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
111	98, 110	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥)
112		supxrre 13366	. . . . . . . . . . . . . . 15 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
113	100, 106, 111, 112	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
114	99, 113	breqtrrd 5176	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
115	114	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
116	13, 115	eqbrtrrid 5184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇝ sup(ran 𝑆, ℝ*, < ))
117	64	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
118	86	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
119	50, 49, 116, 117, 118	climserle 15696	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
120	82, 119	eqbrtrid 5183	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
121	42, 47, 48, 83, 120	letrd 11416	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
122	121	ralrimiva 3144	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
123		brralrspcev 5208	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
124	23, 122, 123	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
125	30	ffnd 6738	. . . . . . . 8 ⊢ (𝜑 → 𝑇 Fn ℕ)
126		breq1 5151	. . . . . . . . 9 ⊢ (𝑧 = (𝑇‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑇‘𝑗) ≤ 𝑥))
127	126	ralrn 7108	. . . . . . . 8 ⊢ (𝑇 Fn ℕ → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
128	125, 127	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
129	128	rexbidv 3177	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
130	124, 129	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥)
131	33, 40, 130	suprcld 12229	. . . 4 ⊢ (𝜑 → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
132	67, 15	ovolsf 25521	. . . . . . . 8 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
133	66, 132	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
134	133	frnd 6745	. . . . . 6 ⊢ (𝜑 → ran 𝑈 ⊆ (0[,)+∞))
135	134, 32	sstrdi 4008	. . . . 5 ⊢ (𝜑 → ran 𝑈 ⊆ ℝ)
136	133	fdmd 6747	. . . . . . . 8 ⊢ (𝜑 → dom 𝑈 = ℕ)
137	34, 136	eleqtrrid 2846	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑈)
138	137	ne0d 4348	. . . . . 6 ⊢ (𝜑 → dom 𝑈 ≠ ∅)
139		dm0rn0 5938	. . . . . . 7 ⊢ (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
140	139	necon3bii 2991	. . . . . 6 ⊢ (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
141	138, 140	sylib 218	. . . . 5 ⊢ (𝜑 → ran 𝑈 ≠ ∅)
142	133	ffvelcdmda 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ (0[,)+∞))
143	32, 142	sselid 3993	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℝ)
144	52, 53, 74	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
145		elrege0 13491	. . . . . . . . . . . . . . . 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 11850	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
149	147, 148	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
150	149, 77	breqtrd 5174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
151	52, 53, 150	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
152	51, 144, 65, 151	serle 14095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
153	15	fveq1i 6908	. . . . . . . . . 10 ⊢ (𝑈‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)
154	152, 153, 82	3brtr4g 5182	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ (𝑆‘𝑗))
155	143, 47, 48, 154, 120	letrd 11416	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
156	155	ralrimiva 3144	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
157		brralrspcev 5208	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
158	23, 156, 157	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
159	133	ffnd 6738	. . . . . . . 8 ⊢ (𝜑 → 𝑈 Fn ℕ)
160		breq1 5151	. . . . . . . . 9 ⊢ (𝑧 = (𝑈‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑈‘𝑗) ≤ 𝑥))
161	160	ralrn 7108	. . . . . . . 8 ⊢ (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
162	159, 161	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
163	162	rexbidv 3177	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
164	158, 163	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥)
165	135, 141, 164	suprcld 12229	. . . 4 ⊢ (𝜑 → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
166		ssralv 4064	. . . . . . . . . 10 ⊢ ((𝐸 ∩ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
167	1, 166	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))
168	19	breq1i 5155	. . . . . . . . . . . . 13 ⊢ (𝑃 < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < 𝑥)
169		ovolfcl 25515	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
170	16, 169	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
171	170	simp1d 1141	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ)
172	19, 171	eqeltrid 2843	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
173	172	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
174	1, 2	sstrid 4007	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ℝ)
175	174	sselda 3995	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → 𝑥 ∈ ℝ)
176	175	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
177		ltle 11347	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
178	173, 176, 177	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
179		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
180		opex 5475	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V
181	21	fvmpt2 7027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
182	179, 180, 181	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
183	182	fveq2d 6911	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺‘𝑛)) = (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
184	11	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
185	184, 172	ifcld 4577	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
186	170	simp2d 1142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ)
187	20, 186	eqeltrid 2843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
188	185, 187	ifcld 4577	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
189		op1stg 8025	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
190	188, 187, 189	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
191	183, 190	eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
192	191	ad2ant2r 747	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (1st ‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
193	188	ad2ant2r 747	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
194	185	ad2ant2r 747	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
195	174	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (𝐸 ∩ 𝐵) ⊆ ℝ)
196		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ (𝐸 ∩ 𝐵))
197	195, 196	sseldd 3996	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ ℝ)
198	187	ad2ant2r 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑄 ∈ ℝ)
199		min1 13228	. . . . . . . . . . . . . . . . . 18 ⊢ ((if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
200	194, 198, 199	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
201	11	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ∈ ℝ)
202		elinel2 4212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∩ 𝐵) → 𝑥 ∈ 𝐵)
203	202	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ 𝐵)
204	11	rexrd 11309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
205		pnfxr 11313	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ +∞ ∈ ℝ*
206		elioo2 13425	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
207	204, 205, 206	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
208	10	eleq2i 2831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (𝐴(,)+∞))
209		ltpnf 13160	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝑥 < +∞)
211	210	pm4.71i 559	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
212		df-3an 1088	. . . . . . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (𝑥 ∈ 𝐵 → 𝐴 < 𝑥))
218	203, 217	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 < 𝑥)
219	201, 197, 218	ltled 11407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ≤ 𝑥)
220		simprr 773	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑃 ≤ 𝑥)
221		breq1 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝐴 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
222		breq1 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝑃 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
223	221, 222	ifboth 4570	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≤ 𝑥 ∧ 𝑃 ≤ 𝑥) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
224	219, 220, 223	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
225	193, 194, 197, 200, 224	letrd 11416	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑥)
226	192, 225	eqbrtrd 5170	. . . . . . . . . . . . . . 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 5156	. . . . . . . . . . . . . 14 ⊢ (𝑥 < 𝑄 ↔ 𝑥 < (2nd ‘(𝐹‘𝑛)))
231	187	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
232		ltle 11347	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
233	176, 231, 232	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
234	230, 233	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ 𝑄))
235	182	fveq2d 6911	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
236		op2ndg 8026	. . . . . . . . . . . . . . . . 17 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
237	188, 187, 236	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
238	235, 237	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = 𝑄)
239	238	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = 𝑄)
240	239	breq2d 5160	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ (2nd ‘(𝐺‘𝑛)) ↔ 𝑥 ≤ 𝑄))
241	234, 240	sylibrd 259	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ (2nd ‘(𝐺‘𝑛))))
242	229, 241	anim12d 609	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
243	242	reximdva 3166	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
244	243	ralimdva 3165	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
245	167, 244	syl5 34	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
246		ovolfioo 25516	. . . . . . . . 9 ⊢ ((𝐸 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
247	2, 16, 246	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
248		ovolficc 25517	. . . . . . . . 9 ⊢ (((𝐸 ∩ 𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
249	174, 27, 248	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
250	245, 247, 249	3imtr4d 294	. . . . . . 7 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) → (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)))
251	17, 250	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺))
252	14	ovollb2 25538	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)) → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
253	27, 251, 252	syl2anc 584	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
254		supxrre 13366	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
255	33, 40, 130, 254	syl3anc 1370	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
256	253, 255	breqtrd 5174	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ, < ))
257		ssralv 4064	. . . . . . . . . 10 ⊢ ((𝐸 ∖ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
258	6, 257	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))
259	172	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
260	6, 2	sstrid 4007	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ℝ)
261	260	sselda 3995	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → 𝑥 ∈ ℝ)
262	261	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
263	259, 262, 177	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
264	168, 263	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → 𝑃 ≤ 𝑥))
265		opex 5475	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V
266	22	fvmpt2 7027	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
267	179, 265, 266	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
268	267	fveq2d 6911	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
269		op1stg 8025	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
270	172, 188, 269	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
271	268, 270	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = 𝑃)
272	271	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = 𝑃)
273	272	breq1d 5158	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ↔ 𝑃 ≤ 𝑥))
274	264, 273	sylibrd 259	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → (1st ‘(𝐻‘𝑛)) ≤ 𝑥))
275	187	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
276	262, 275, 232	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
277	260	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐸 ∖ 𝐵) ⊆ ℝ)
278		simplr 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ (𝐸 ∖ 𝐵))
279	277, 278	sseldd 3996	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ ℝ)
280	11	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ∈ ℝ)
281	172	ad2ant2r 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑃 ∈ ℝ)
282	280, 281	ifcld 4577	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
283		eldifn 4142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
284	283	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → ¬ 𝑥 ∈ 𝐵)
285	279	biantrurd 532	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐴 < 𝑥 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
286	214	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
287	285, 286	bitr4d 282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐴 < 𝑥 ↔ 𝑥 ∈ 𝐵))
288	284, 287	mtbird 325	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → ¬ 𝐴 < 𝑥)
289	279, 280, 288	nltled 11409	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝐴)
290		max2 13226	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
291	281, 280, 290	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
292	279, 280, 282, 289, 291	letrd 11416	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
293		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝑄)
294		breq2 5152	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑃 ≤ 𝐴, 𝐴, 𝑃) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
295		breq2 5152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑄 = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ 𝑄 ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
296	294, 295	ifboth 4570	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∧ 𝑥 ≤ 𝑄) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
297	292, 293, 296	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
298	267	fveq2d 6911	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐻‘𝑛)) = (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
299		op2ndg 8026	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
300	172, 188, 299	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
301	298, 300	eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
302	301	ad2ant2r 747	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (2nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
303	297, 302	breqtrrd 5176	. . . . . . . . . . . . . . 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 609	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
308	307	reximdva 3166	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
309	308	ralimdva 3165	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
310	258, 309	syl5 34	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
311		ovolficc 25517	. . . . . . . . 9 ⊢ (((𝐸 ∖ 𝐵) ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
312	260, 66, 311	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
313	310, 247, 312	3imtr4d 294	. . . . . . 7 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) → (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)))
314	17, 313	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻))
315	15	ovollb2 25538	. . . . . 6 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)) → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
316	66, 314, 315	syl2anc 584	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
317		supxrre 13366	. . . . . 6 ⊢ ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥) → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
318	135, 141, 164, 317	syl3anc 1370	. . . . 5 ⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
319	316, 318	breqtrd 5174	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ, < ))
320	5, 8, 131, 165, 256, 319	le2addd 11880	. . 3 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
321		eqidd 2736	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐺)‘𝑛))
322	50, 14, 84, 321, 57, 147, 124	isumsup2 15879	. . . . 5 ⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
323		seqex 14041	. . . . . . 7 ⊢ seq1( + , ((abs ∘ − ) ∘ 𝐹)) ∈ V
324	13, 323	eqeltri 2835	. . . . . 6 ⊢ 𝑆 ∈ V
325	324	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ V)
326		eqidd 2736	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) = (((abs ∘ − ) ∘ 𝐻)‘𝑛))
327	50, 15, 84, 326, 74, 73, 158	isumsup2 15879	. . . . 5 ⊢ (𝜑 → 𝑈 ⇝ sup(ran 𝑈, ℝ, < ))
328	42	recnd 11287	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℂ)
329	143	recnd 11287	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℂ)
330	57	recnd 11287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
331	52, 53, 330	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
332	74	recnd 11287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
333	52, 53, 332	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
334	77	eqcomd 2741	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
335	52, 53, 334	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
336	51, 331, 333, 335	seradd 14082	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)))
337	81, 153	oveq12i 7443	. . . . . 6 ⊢ ((𝑇‘𝑗) + (𝑈‘𝑗)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗))
338	336, 82, 337	3eqtr4g 2800	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) = ((𝑇‘𝑗) + (𝑈‘𝑗)))
339	50, 84, 322, 325, 327, 328, 329, 338	climadd 15665	. . . 4 ⊢ (𝜑 → 𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
340		climuni 15585	. . . 4 ⊢ ((𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) ∧ 𝑆 ⇝ sup(ran 𝑆, ℝ*, < )) → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
341	339, 114, 340	syl2anc 584	. . 3 ⊢ (𝜑 → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
342	320, 341	breqtrd 5174	. 2 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ sup(ran 𝑆, ℝ*, < ))
343	9, 23, 25, 342, 18	letrd 11416	1 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ ((vol*‘𝐸) + 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  Vcvv 3478   ∖ cdif 3960   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339  ifcif 4531  ⟨cop 4637  ∪ cuni 4912   class class class wbr 5148   ↦ cmpt 5231   × cxp 5687  dom cdm 5689  ran crn 5690   ∘ ccom 5693   Fn wfn 6558  ⟶wf 6559  ‘cfv 6563  (class class class)co 7431  1^st c1st 8011  2^nd c2nd 8012  supcsup 9478  ℂcc 11151  ℝcr 11152  0cc0 11153  1c1 11154   + caddc 11156  +∞cpnf 11290  ℝ^*cxr 11292   < clt 11293   ≤ cle 11294   − cmin 11490  ℕcn 12264  ℤ_≥cuz 12876  ℝ⁺crp 13032  (,)cioo 13384  [,)cico 13386  [,]cicc 13387  ...cfz 13544  seqcseq 14039  abscabs 15270   ⇝ cli 15517  vol*covol 25511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-map 8867  df-pm 8868  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-sup 9480  df-inf 9481  df-oi 9548  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12612  df-uz 12877  df-q 12989  df-rp 13033  df-ioo 13388  df-ico 13390  df-icc 13391  df-fz 13545  df-fzo 13692  df-fl 13829  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-clim 15521  df-rlim 15522  df-sum 15720  df-ovol 25513

This theorem is referenced by:  ioombl1  25611