Theorem ioombl1lem4 25519

Description: Lemma for ioombl1 25520. (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 4217	. . . 4 ⊢ (𝐸 ∩ 𝐵) ⊆ 𝐸
2		ioombl1.e	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
3		ioombl1.v	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
4		ovolsscl 25444	. . . 4 ⊢ (((𝐸 ∩ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
5	1, 2, 3, 4	mp3an2i 1468	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
6		difss 4116	. . . 4 ⊢ (𝐸 ∖ 𝐵) ⊆ 𝐸
7		ovolsscl 25444	. . . 4 ⊢ (((𝐸 ∖ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
8	6, 2, 3, 7	mp3an2i 1468	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
9	5, 8	readdcld 11269	. 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 25517	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
24	12	rpred 13056	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
25	3, 24	readdcld 11269	. 2 ⊢ (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ)
26	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem1 25516	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
27	26	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
28		eqid 2736	. . . . . . . . 9 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
29	28, 14	ovolsf 25430	. . . . . . . 8 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
30	27, 29	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
31	30	frnd 6719	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
32		rge0ssre 13478	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
33	31, 32	sstrdi 3976	. . . . 5 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
34		1nn 12256	. . . . . . . 8 ⊢ 1 ∈ ℕ
35	30	fdmd 6721	. . . . . . . 8 ⊢ (𝜑 → dom 𝑇 = ℕ)
36	34, 35	eleqtrrid 2842	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑇)
37	36	ne0d 4322	. . . . . 6 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
38		dm0rn0 5909	. . . . . . 7 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
39	38	necon3bii 2985	. . . . . 6 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
40	37, 39	sylib 218	. . . . 5 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
41	30	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ (0[,)+∞))
42	32, 41	sselid 3961	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℝ)
43		eqid 2736	. . . . . . . . . . . . 13 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
44	43, 13	ovolsf 25430	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
45	16, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
46	45	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ (0[,)+∞))
47	32, 46	sselid 3961	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ ℝ)
48	23	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
49		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
50		nnuz 12900	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
51	49, 50	eleqtrdi 2845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ≥‘1))
52		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑)
53		elfznn 13575	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
54	28	ovolfsf 25429	. . . . . . . . . . . . . . 15 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
55	27, 54	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
56	55	ffvelcdmda 7079	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞))
57	32, 56	sselid 3961	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
58	52, 53, 57	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
59	43	ovolfsf 25429	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
60	16, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
61	60	ffvelcdmda 7079	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞))
62		elrege0 13476	. . . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
68	67	ovolfsf 25429	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
69	66, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
70	69	ffvelcdmda 7079	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞))
71		elrege0 13476	. . . . . . . . . . . . . . . 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 11830	. . . . . . . . . . . . . 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 25518	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
78	76, 77	breqtrd 5150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
79	52, 53, 78	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
80	51, 58, 65, 79	serle 14080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
81	14	fveq1i 6882	. . . . . . . . . 10 ⊢ (𝑇‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗)
82	13	fveq1i 6882	. . . . . . . . . 10 ⊢ (𝑆‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗)
83	80, 81, 82	3brtr4g 5158	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ (𝑆‘𝑗))
84		1zzd 12628	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℤ)
85		eqidd 2737	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
86	63	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
87	45	frnd 6719	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
88		icossxr 13454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0[,)+∞) ⊆ ℝ*
89	87, 88	sstrdi 3976	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ*)
90	89	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
91	45	ffnd 6712	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑆 Fn ℕ)
92		fnfvelrn 7075	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
93	91, 92	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
94		supxrub 13345	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘𝑘) ∈ ran 𝑆) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
95	90, 93, 94	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
96	95	ralrimiva 3133	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
97		brralrspcev 5184	. . . . . . . . . . . . . . . 16 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
98	23, 96, 97	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
99	50, 13, 84, 85, 64, 86, 98	isumsup2 15867	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
100	87, 32	sstrdi 3976	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
101	45	fdmd 6721	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom 𝑆 = ℕ)
102	34, 101	eleqtrrid 2842	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ dom 𝑆)
103	102	ne0d 4322	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
104		dm0rn0 5909	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
105	104	necon3bii 2985	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
106	103, 105	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
107		breq1 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑆‘𝑘) ≤ 𝑥))
108	107	ralrn 7083	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
109	91, 108	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
110	109	rexbidv 3165	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
111	98, 110	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥)
112		supxrre 13348	. . . . . . . . . . . . . . 15 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
113	100, 106, 111, 112	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
114	99, 113	breqtrrd 5152	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
115	114	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
116	13, 115	eqbrtrrid 5160	. . . . . . . . . . 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 15684	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
120	82, 119	eqbrtrid 5159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
121	42, 47, 48, 83, 120	letrd 11397	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
122	121	ralrimiva 3133	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
123		brralrspcev 5184	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
124	23, 122, 123	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
125	30	ffnd 6712	. . . . . . . 8 ⊢ (𝜑 → 𝑇 Fn ℕ)
126		breq1 5127	. . . . . . . . 9 ⊢ (𝑧 = (𝑇‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑇‘𝑗) ≤ 𝑥))
127	126	ralrn 7083	. . . . . . . 8 ⊢ (𝑇 Fn ℕ → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
128	125, 127	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
129	128	rexbidv 3165	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
130	124, 129	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥)
131	33, 40, 130	suprcld 12210	. . . 4 ⊢ (𝜑 → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
132	67, 15	ovolsf 25430	. . . . . . . 8 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
133	66, 132	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
134	133	frnd 6719	. . . . . 6 ⊢ (𝜑 → ran 𝑈 ⊆ (0[,)+∞))
135	134, 32	sstrdi 3976	. . . . 5 ⊢ (𝜑 → ran 𝑈 ⊆ ℝ)
136	133	fdmd 6721	. . . . . . . 8 ⊢ (𝜑 → dom 𝑈 = ℕ)
137	34, 136	eleqtrrid 2842	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑈)
138	137	ne0d 4322	. . . . . 6 ⊢ (𝜑 → dom 𝑈 ≠ ∅)
139		dm0rn0 5909	. . . . . . 7 ⊢ (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
140	139	necon3bii 2985	. . . . . 6 ⊢ (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
141	138, 140	sylib 218	. . . . 5 ⊢ (𝜑 → ran 𝑈 ≠ ∅)
142	133	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ (0[,)+∞))
143	32, 142	sselid 3961	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℝ)
144	52, 53, 74	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
145		elrege0 13476	. . . . . . . . . . . . . . . 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 11831	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
149	147, 148	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
150	149, 77	breqtrd 5150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
151	52, 53, 150	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
152	51, 144, 65, 151	serle 14080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
153	15	fveq1i 6882	. . . . . . . . . 10 ⊢ (𝑈‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)
154	152, 153, 82	3brtr4g 5158	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ (𝑆‘𝑗))
155	143, 47, 48, 154, 120	letrd 11397	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
156	155	ralrimiva 3133	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
157		brralrspcev 5184	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
158	23, 156, 157	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
159	133	ffnd 6712	. . . . . . . 8 ⊢ (𝜑 → 𝑈 Fn ℕ)
160		breq1 5127	. . . . . . . . 9 ⊢ (𝑧 = (𝑈‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑈‘𝑗) ≤ 𝑥))
161	160	ralrn 7083	. . . . . . . 8 ⊢ (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
162	159, 161	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
163	162	rexbidv 3165	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
164	158, 163	mpbird 257	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥)
165	135, 141, 164	suprcld 12210	. . . 4 ⊢ (𝜑 → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
166		ssralv 4032	. . . . . . . . . 10 ⊢ ((𝐸 ∩ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
167	1, 166	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))
168	19	breq1i 5131	. . . . . . . . . . . . 13 ⊢ (𝑃 < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < 𝑥)
169		ovolfcl 25424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
170	16, 169	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
171	170	simp1d 1142	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ)
172	19, 171	eqeltrid 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
173	172	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
174	1, 2	sstrid 3975	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ℝ)
175	174	sselda 3963	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → 𝑥 ∈ ℝ)
176	175	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
177		ltle 11328	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
178	173, 176, 177	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
179		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
180		opex 5444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V
181	21	fvmpt2 7002	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
182	179, 180, 181	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
183	182	fveq2d 6885	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺‘𝑛)) = (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
184	11	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
185	184, 172	ifcld 4552	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
186	170	simp2d 1143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ)
187	20, 186	eqeltrid 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
188	185, 187	ifcld 4552	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
189		op1stg 8005	. . . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ (𝐸 ∩ 𝐵))
197	195, 196	sseldd 3964	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ ℝ)
198	187	ad2ant2r 747	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑄 ∈ ℝ)
199		min1 13210	. . . . . . . . . . . . . . . . . 18 ⊢ ((if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
200	194, 198, 199	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
201	11	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ∈ ℝ)
202		elinel2 4182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∩ 𝐵) → 𝑥 ∈ 𝐵)
203	202	ad2antlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ 𝐵)
204	11	rexrd 11290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
205		pnfxr 11294	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ +∞ ∈ ℝ*
206		elioo2 13408	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
207	204, 205, 206	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
208	10	eleq2i 2827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (𝐴(,)+∞))
209		ltpnf 13141	. . . . . . . . . . . . . . . . . . . . . . . . . 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 11388	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ≤ 𝑥)
220		simprr 772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑃 ≤ 𝑥)
221		breq1 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝐴 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
222		breq1 5127	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝑃 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
223	221, 222	ifboth 4545	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≤ 𝑥 ∧ 𝑃 ≤ 𝑥) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
224	219, 220, 223	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
225	193, 194, 197, 200, 224	letrd 11397	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑥)
226	192, 225	eqbrtrd 5146	. . . . . . . . . . . . . . 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 5132	. . . . . . . . . . . . . 14 ⊢ (𝑥 < 𝑄 ↔ 𝑥 < (2nd ‘(𝐹‘𝑛)))
231	187	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
232		ltle 11328	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
233	176, 231, 232	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
234	230, 233	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ 𝑄))
235	182	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
236		op2ndg 8006	. . . . . . . . . . . . . . . . 17 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
237	188, 187, 236	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
238	235, 237	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = 𝑄)
239	238	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = 𝑄)
240	239	breq2d 5136	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ (2nd ‘(𝐺‘𝑛)) ↔ 𝑥 ≤ 𝑄))
241	234, 240	sylibrd 259	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ (2nd ‘(𝐺‘𝑛))))
242	229, 241	anim12d 609	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
243	242	reximdva 3154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
244	243	ralimdva 3153	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
245	167, 244	syl5 34	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
246		ovolfioo 25425	. . . . . . . . 9 ⊢ ((𝐸 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
247	2, 16, 246	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
248		ovolficc 25426	. . . . . . . . 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 25447	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)) → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
253	27, 251, 252	syl2anc 584	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
254		supxrre 13348	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
255	33, 40, 130, 254	syl3anc 1373	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
256	253, 255	breqtrd 5150	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ, < ))
257		ssralv 4032	. . . . . . . . . 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 3975	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ℝ)
261	260	sselda 3963	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → 𝑥 ∈ ℝ)
262	261	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
263	259, 262, 177	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
264	168, 263	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → 𝑃 ≤ 𝑥))
265		opex 5444	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V
266	22	fvmpt2 7002	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
267	179, 265, 266	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
268	267	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
269		op1stg 8005	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
270	172, 188, 269	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
271	268, 270	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = 𝑃)
272	271	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = 𝑃)
273	272	breq1d 5134	. . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ (𝐸 ∖ 𝐵))
279	277, 278	sseldd 3964	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ ℝ)
280	11	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ∈ ℝ)
281	172	ad2ant2r 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑃 ∈ ℝ)
282	280, 281	ifcld 4552	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
283		eldifn 4112	. . . . . . . . . . . . . . . . . . . . 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 11390	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝐴)
290		max2 13208	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
291	281, 280, 290	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
292	279, 280, 282, 289, 291	letrd 11397	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
293		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝑄)
294		breq2 5128	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑃 ≤ 𝐴, 𝐴, 𝑃) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
295		breq2 5128	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑄 = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ 𝑄 ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
296	294, 295	ifboth 4545	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∧ 𝑥 ≤ 𝑄) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
297	292, 293, 296	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
298	267	fveq2d 6885	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐻‘𝑛)) = (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
299		op2ndg 8006	. . . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
302	301	ad2ant2r 747	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (2nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
303	297, 302	breqtrrd 5152	. . . . . . . . . . . . . . 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 3154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
309	308	ralimdva 3153	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
310	258, 309	syl5 34	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
311		ovolficc 25426	. . . . . . . . 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 25447	. . . . . 6 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)) → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
316	66, 314, 315	syl2anc 584	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
317		supxrre 13348	. . . . . 6 ⊢ ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥) → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
318	135, 141, 164, 317	syl3anc 1373	. . . . 5 ⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
319	316, 318	breqtrd 5150	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ, < ))
320	5, 8, 131, 165, 256, 319	le2addd 11861	. . 3 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
321		eqidd 2737	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐺)‘𝑛))
322	50, 14, 84, 321, 57, 147, 124	isumsup2 15867	. . . . 5 ⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
323		seqex 14026	. . . . . . 7 ⊢ seq1( + , ((abs ∘ − ) ∘ 𝐹)) ∈ V
324	13, 323	eqeltri 2831	. . . . . 6 ⊢ 𝑆 ∈ V
325	324	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ V)
326		eqidd 2737	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) = (((abs ∘ − ) ∘ 𝐻)‘𝑛))
327	50, 15, 84, 326, 74, 73, 158	isumsup2 15867	. . . . 5 ⊢ (𝜑 → 𝑈 ⇝ sup(ran 𝑈, ℝ, < ))
328	42	recnd 11268	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℂ)
329	143	recnd 11268	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℂ)
330	57	recnd 11268	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
331	52, 53, 330	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
332	74	recnd 11268	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
333	52, 53, 332	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
334	77	eqcomd 2742	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
335	52, 53, 334	syl2an 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
336	51, 331, 333, 335	seradd 14067	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)))
337	81, 153	oveq12i 7422	. . . . . 6 ⊢ ((𝑇‘𝑗) + (𝑈‘𝑗)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗))
338	336, 82, 337	3eqtr4g 2796	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) = ((𝑇‘𝑗) + (𝑈‘𝑗)))
339	50, 84, 322, 325, 327, 328, 329, 338	climadd 15653	. . . 4 ⊢ (𝜑 → 𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
340		climuni 15573	. . . 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 5150	. 2 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ sup(ran 𝑆, ℝ*, < ))
343	9, 23, 25, 342, 18	letrd 11397	1 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ ((vol*‘𝐸) + 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  Vcvv 3464   ∖ cdif 3928   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  ifcif 4505  ⟨cop 4612  ∪ cuni 4888   class class class wbr 5124   ↦ cmpt 5206   × cxp 5657  dom cdm 5659  ran crn 5660   ∘ ccom 5663   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410  1^st c1st 7991  2^nd c2nd 7992  supcsup 9457  ℂcc 11132  ℝcr 11133  0cc0 11134  1c1 11135   + caddc 11137  +∞cpnf 11271  ℝ^*cxr 11273   < clt 11274   ≤ cle 11275   − cmin 11471  ℕcn 12245  ℤ_≥cuz 12857  ℝ⁺crp 13013  (,)cioo 13367  [,)cico 13369  [,]cicc 13370  ...cfz 13529  seqcseq 14024  abscabs 15258   ⇝ cli 15505  vol*covol 25420

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 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-inf2 9660  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211  ax-pre-sup 11212

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8724  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9459  df-inf 9460  df-oi 9529  df-card 9958  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900  df-nn 12246  df-2 12308  df-3 12309  df-n0 12507  df-z 12594  df-uz 12858  df-q 12970  df-rp 13014  df-ioo 13371  df-ico 13373  df-icc 13374  df-fz 13530  df-fzo 13677  df-fl 13814  df-seq 14025  df-exp 14085  df-hash 14354  df-cj 15123  df-re 15124  df-im 15125  df-sqrt 15259  df-abs 15260  df-clim 15509  df-rlim 15510  df-sum 15708  df-ovol 25422

This theorem is referenced by:  ioombl1  25520