Theorem ioombl1lem4 25735

Description: Lemma for ioombl1 25736. (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 4192	. . . 4 ⊢ (𝐸 ∩ 𝐵) ⊆ 𝐸
2		ioombl1.e	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
3		ioombl1.v	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
4		ovolsscl 25660	. . . 4 ⊢ (((𝐸 ∩ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
5	1, 2, 3, 4	mp3an2i 1495	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
6		difss 4093	. . . 4 ⊢ (𝐸 ∖ 𝐵) ⊆ 𝐸
7		ovolsscl 25660	. . . 4 ⊢ (((𝐸 ∖ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol*‘𝐸) ∈ ℝ) → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
8	6, 2, 3, 7	mp3an2i 1495	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
9	5, 8	readdcld 11248	. 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 25733	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
24	12	rpred 13070	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
25	3, 24	readdcld 11248	. 2 ⊢ (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ)
26	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem1 25732	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
27	26	simpld 500	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
28		eqid 2766	. . . . . . . . 9 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
29	28, 14	ovolsf 25646	. . . . . . . 8 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
30	27, 29	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
31	30	frnd 6718	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
32		rge0ssre 13493	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
33	31, 32	sstrdi 3952	. . . . 5 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
34		1nn 12254	. . . . . . . 8 ⊢ 1 ∈ ℕ
35	30	fdmd 6720	. . . . . . . 8 ⊢ (𝜑 → dom 𝑇 = ℕ)
36	34, 35	eleqtrrid 2873	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑇)
37	36	ne0d 4298	. . . . . 6 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
38		dm0rn0 5917	. . . . . . 7 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
39	38	necon3bii 3013	. . . . . 6 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
40	37, 39	sylib 221	. . . . 5 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
41	30	ffvelcdmda 7083	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ (0[,)+∞))
42	32, 41	sselid 3938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℝ)
43		eqid 2766	. . . . . . . . . . . . 13 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
44	43, 13	ovolsf 25646	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
45	16, 44	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
46	45	ffvelcdmda 7083	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ (0[,)+∞))
47	32, 46	sselid 3938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ ℝ)
48	23	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
49		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
50		nnuz 12911	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
51	49, 50	eleqtrdi 2876	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ≥‘1))
52		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑)
53		elfznn 13592	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
54	28	ovolfsf 25645	. . . . . . . . . . . . . . 15 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
55	27, 54	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
56	55	ffvelcdmda 7083	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞))
57	32, 56	sselid 3938	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
58	52, 53, 57	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
59	43	ovolfsf 25645	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
60	16, 59	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
61	60	ffvelcdmda 7083	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞))
62		elrege0 13491	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
63	61, 62	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
64	63	simpld 500	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
65	52, 53, 64	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
66	26	simprd 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
67		eqid 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
68	67	ovolfsf 25645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
69	66, 68	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
70	69	ffvelcdmda 7083	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞))
71		elrege0 13491	. . . . . . . . . . . . . . . 16 ⊢ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
72	70, 71	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
73	72	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛))
74	72	simpld 500	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
75	57, 74	addge01d 11812	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
76	73, 75	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
77	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem3 25734	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
78	76, 77	breqtrd 5140	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
79	52, 53, 78	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
80	51, 58, 65, 79	serle 14104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
81	14	fveq1i 6886	. . . . . . . . . 10 ⊢ (𝑇‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗)
82	13	fveq1i 6886	. . . . . . . . . 10 ⊢ (𝑆‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗)
83	80, 81, 82	3brtr4g 5148	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ (𝑆‘𝑗))
84		1zzd 12635	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℤ)
85		eqidd 2767	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
86	63	simprd 501	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
87	45	frnd 6718	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
88		icossxr 13469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0[,)+∞) ⊆ ℝ*
89	87, 88	sstrdi 3952	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ*)
90	89	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
91	45	ffnd 6710	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑆 Fn ℕ)
92		fnfvelrn 7079	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
93	91, 92	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
94		supxrub 13360	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑆 ⊆ ℝ* ∧ (𝑆‘𝑘) ∈ ran 𝑆) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
95	90, 93, 94	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
96	95	ralrimiva 3160	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
97		brralrspcev 5174	. . . . . . . . . . . . . . . 16 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
98	23, 96, 97	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
99	50, 13, 84, 85, 64, 86, 98	isumsup2 15911	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
100	87, 32	sstrdi 3952	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
101	45	fdmd 6720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom 𝑆 = ℕ)
102	34, 101	eleqtrrid 2873	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ dom 𝑆)
103	102	ne0d 4298	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
104		dm0rn0 5917	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
105	104	necon3bii 3013	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
106	103, 105	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
107		breq1 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑆‘𝑘) ≤ 𝑥))
108	107	ralrn 7087	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
109	91, 108	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
110	109	rexbidv 3192	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
111	98, 110	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥)
112		supxrre 13363	. . . . . . . . . . . . . . 15 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
113	100, 106, 111, 112	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
114	99, 113	breqtrrd 5142	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
115	114	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ⇝ sup(ran 𝑆, ℝ*, < ))
116	13, 115	eqbrtrrid 5150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇝ sup(ran 𝑆, ℝ*, < ))
117	64	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
118	86	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
119	50, 49, 116, 117, 118	climserle 15725	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
120	82, 119	eqbrtrid 5149	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
121	42, 47, 48, 83, 120	letrd 11377	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
122	121	ralrimiva 3160	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
123		brralrspcev 5174	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
124	23, 122, 123	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
125	30	ffnd 6710	. . . . . . . 8 ⊢ (𝜑 → 𝑇 Fn ℕ)
126		breq1 5115	. . . . . . . . 9 ⊢ (𝑧 = (𝑇‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑇‘𝑗) ≤ 𝑥))
127	126	ralrn 7087	. . . . . . . 8 ⊢ (𝑇 Fn ℕ → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
128	125, 127	syl 18	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
129	128	rexbidv 3192	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
130	124, 129	mpbird 260	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥)
131	33, 40, 130	suprcld 12188	. . . 4 ⊢ (𝜑 → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
132	67, 15	ovolsf 25646	. . . . . . . 8 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
133	66, 132	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
134	133	frnd 6718	. . . . . 6 ⊢ (𝜑 → ran 𝑈 ⊆ (0[,)+∞))
135	134, 32	sstrdi 3952	. . . . 5 ⊢ (𝜑 → ran 𝑈 ⊆ ℝ)
136	133	fdmd 6720	. . . . . . . 8 ⊢ (𝜑 → dom 𝑈 = ℕ)
137	34, 136	eleqtrrid 2873	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑈)
138	137	ne0d 4298	. . . . . 6 ⊢ (𝜑 → dom 𝑈 ≠ ∅)
139		dm0rn0 5917	. . . . . . 7 ⊢ (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
140	139	necon3bii 3013	. . . . . 6 ⊢ (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
141	138, 140	sylib 221	. . . . 5 ⊢ (𝜑 → ran 𝑈 ≠ ∅)
142	133	ffvelcdmda 7083	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ (0[,)+∞))
143	32, 142	sselid 3938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℝ)
144	52, 53, 74	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
145		elrege0 13491	. . . . . . . . . . . . . . . 16 ⊢ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
146	56, 145	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
147	146	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛))
148	74, 57	addge02d 11813	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
149	147, 148	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
150	149, 77	breqtrd 5140	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
151	52, 53, 150	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
152	51, 144, 65, 151	serle 14104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
153	15	fveq1i 6886	. . . . . . . . . 10 ⊢ (𝑈‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)
154	152, 153, 82	3brtr4g 5148	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ (𝑆‘𝑗))
155	143, 47, 48, 154, 120	letrd 11377	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
156	155	ralrimiva 3160	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < ))
157		brralrspcev 5174	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
158	23, 156, 157	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
159	133	ffnd 6710	. . . . . . . 8 ⊢ (𝜑 → 𝑈 Fn ℕ)
160		breq1 5115	. . . . . . . . 9 ⊢ (𝑧 = (𝑈‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑈‘𝑗) ≤ 𝑥))
161	160	ralrn 7087	. . . . . . . 8 ⊢ (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
162	159, 161	syl 18	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
163	162	rexbidv 3192	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
164	158, 163	mpbird 260	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥)
165	135, 141, 164	suprcld 12188	. . . 4 ⊢ (𝜑 → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
166		ssralv 4009	. . . . . . . . . 10 ⊢ ((𝐸 ∩ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
167	1, 166	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))
168	19	breq1i 5119	. . . . . . . . . . . . 13 ⊢ (𝑃 < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < 𝑥)
169		ovolfcl 25640	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
170	16, 169	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
171	170	simp1d 1160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ)
172	19, 171	eqeltrid 2870	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
173	172	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
174	1, 2	sstrid 3951	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ℝ)
175	174	sselda 3940	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → 𝑥 ∈ ℝ)
176	175	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
177		ltle 11308	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
178	173, 176, 177	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
179		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
180		opex 5448	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V
181	21	fvmpt2 7005	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
182	179, 180, 181	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
183	182	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺‘𝑛)) = (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
184	11	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
185	184, 172	ifcld 4537	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
186	170	simp2d 1161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ)
187	20, 186	eqeltrid 2870	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
188	185, 187	ifcld 4537	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
189		op1stg 8000	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
190	188, 187, 189	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
191	183, 190	eqtrd 2801	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
192	191	ad2ant2r 760	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (1st ‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
193	188	ad2ant2r 760	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
194	185	ad2ant2r 760	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
195	174	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (𝐸 ∩ 𝐵) ⊆ ℝ)
196		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ (𝐸 ∩ 𝐵))
197	195, 196	sseldd 3941	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ ℝ)
198	187	ad2ant2r 760	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑄 ∈ ℝ)
199		min1 13225	. . . . . . . . . . . . . . . . . 18 ⊢ ((if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
200	194, 198, 199	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
201	11	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ∈ ℝ)
202		elinel2 4158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∩ 𝐵) → 𝑥 ∈ 𝐵)
203	202	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ 𝐵)
204	11	rexrd 11269	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
205		pnfxr 11273	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ +∞ ∈ ℝ*
206		elioo2 13423	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
207	204, 205, 206	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
208	10	eleq2i 2858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (𝐴(,)+∞))
209		ltpnf 13155	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
210	209	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝑥 < +∞)
211	210	pm4.71i 569	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
212		df-3an 1105	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
213	211, 212	bitr4i 281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞))
214	207, 208, 213	3bitr4g 317	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
215		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝐴 < 𝑥)
216	214, 215	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝐴 < 𝑥))
217	216	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (𝑥 ∈ 𝐵 → 𝐴 < 𝑥))
218	203, 217	mpd 16	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 < 𝑥)
219	201, 197, 218	ltled 11368	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ≤ 𝑥)
220		simprr 785	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑃 ≤ 𝑥)
221		breq1 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝐴 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
222		breq1 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝑃 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
223	221, 222	ifboth 4530	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≤ 𝑥 ∧ 𝑃 ≤ 𝑥) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
224	219, 220, 223	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
225	193, 194, 197, 200, 224	letrd 11377	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑥)
226	192, 225	eqbrtrd 5136	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (1st ‘(𝐺‘𝑛)) ≤ 𝑥)
227	226	expr 462	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 ≤ 𝑥 → (1st ‘(𝐺‘𝑛)) ≤ 𝑥))
228	178, 227	syld 48	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → (1st ‘(𝐺‘𝑛)) ≤ 𝑥))
229	168, 228	biimtrrid 246	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → (1st ‘(𝐺‘𝑛)) ≤ 𝑥))
230	20	breq2i 5120	. . . . . . . . . . . . . 14 ⊢ (𝑥 < 𝑄 ↔ 𝑥 < (2nd ‘(𝐹‘𝑛)))
231	187	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
232		ltle 11308	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
233	176, 231, 232	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
234	230, 233	biimtrrid 246	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ 𝑄))
235	182	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
236		op2ndg 8001	. . . . . . . . . . . . . . . . 17 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
237	188, 187, 236	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
238	235, 237	eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = 𝑄)
239	238	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺‘𝑛)) = 𝑄)
240	239	breq2d 5124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ (2nd ‘(𝐺‘𝑛)) ↔ 𝑥 ≤ 𝑄))
241	234, 240	sylibrd 262	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ (2nd ‘(𝐺‘𝑛))))
242	229, 241	anim12d 621	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
243	242	reximdva 3181	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
244	243	ralimdva 3180	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
245	167, 244	syl5 35	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
246		ovolfioo 25641	. . . . . . . . 9 ⊢ ((𝐸 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
247	2, 16, 246	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
248		ovolficc 25642	. . . . . . . . 9 ⊢ (((𝐸 ∩ 𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
249	174, 27, 248	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐺‘𝑛)))))
250	245, 247, 249	3imtr4d 297	. . . . . . 7 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) → (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)))
251	17, 250	mpd 16	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺))
252	14	ovollb2 25663	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)) → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
253	27, 251, 252	syl2anc 596	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ*, < ))
254		supxrre 13363	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
255	33, 40, 130, 254	syl3anc 1398	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
256	253, 255	breqtrd 5140	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ, < ))
257		ssralv 4009	. . . . . . . . . 10 ⊢ ((𝐸 ∖ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))))
258	6, 257	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))
259	172	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
260	6, 2	sstrid 3951	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ℝ)
261	260	sselda 3940	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → 𝑥 ∈ ℝ)
262	261	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
263	259, 262, 177	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
264	168, 263	biimtrrid 246	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → 𝑃 ≤ 𝑥))
265		opex 5448	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V
266	22	fvmpt2 7005	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
267	179, 265, 266	sylancl 598	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
268	267	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
269		op1stg 8000	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
270	172, 188, 269	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
271	268, 270	eqtrd 2801	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = 𝑃)
272	271	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐻‘𝑛)) = 𝑃)
273	272	breq1d 5122	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ↔ 𝑃 ≤ 𝑥))
274	264, 273	sylibrd 262	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛)) < 𝑥 → (1st ‘(𝐻‘𝑛)) ≤ 𝑥))
275	187	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
276	262, 275, 232	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
277	260	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐸 ∖ 𝐵) ⊆ ℝ)
278		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ (𝐸 ∖ 𝐵))
279	277, 278	sseldd 3941	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ ℝ)
280	11	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ∈ ℝ)
281	172	ad2ant2r 760	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑃 ∈ ℝ)
282	280, 281	ifcld 4537	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
283		eldifn 4089	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
284	283	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → ¬ 𝑥 ∈ 𝐵)
285	279	biantrurd 542	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐴 < 𝑥 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
286	214	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
287	285, 286	bitr4d 285	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐴 < 𝑥 ↔ 𝑥 ∈ 𝐵))
288	284, 287	mtbird 328	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → ¬ 𝐴 < 𝑥)
289	279, 280, 288	nltled 11370	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝐴)
290		max2 13223	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
291	281, 280, 290	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
292	279, 280, 282, 289, 291	letrd 11377	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
293		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝑄)
294		breq2 5116	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑃 ≤ 𝐴, 𝐴, 𝑃) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
295		breq2 5116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑄 = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ 𝑄 ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
296	294, 295	ifboth 4530	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∧ 𝑥 ≤ 𝑄) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
297	292, 293, 296	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
298	267	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐻‘𝑛)) = (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
299		op2ndg 8001	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
300	172, 188, 299	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
301	298, 300	eqtrd 2801	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
302	301	ad2ant2r 760	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (2nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
303	297, 302	breqtrrd 5142	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))
304	303	expr 462	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ 𝑄 → 𝑥 ≤ (2nd ‘(𝐻‘𝑛))))
305	276, 304	syld 48	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ (2nd ‘(𝐻‘𝑛))))
306	230, 305	biimtrrid 246	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2nd ‘(𝐹‘𝑛)) → 𝑥 ≤ (2nd ‘(𝐻‘𝑛))))
307	274, 306	anim12d 621	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
308	307	reximdva 3181	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
309	308	ralimdva 3180	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
310	258, 309	syl5 35	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
311		ovolficc 25642	. . . . . . . . 9 ⊢ (((𝐸 ∖ 𝐵) ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
312	260, 66, 311	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2nd ‘(𝐻‘𝑛)))))
313	310, 247, 312	3imtr4d 297	. . . . . . 7 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) → (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)))
314	17, 313	mpd 16	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻))
315	15	ovollb2 25663	. . . . . 6 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)) → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
316	66, 314, 315	syl2anc 596	. . . . 5 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ*, < ))
317		supxrre 13363	. . . . . 6 ⊢ ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥) → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
318	135, 141, 164, 317	syl3anc 1398	. . . . 5 ⊢ (𝜑 → sup(ran 𝑈, ℝ*, < ) = sup(ran 𝑈, ℝ, < ))
319	316, 318	breqtrd 5140	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ, < ))
320	5, 8, 131, 165, 256, 319	le2addd 11843	. . 3 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
321		eqidd 2767	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐺)‘𝑛))
322	50, 14, 84, 321, 57, 147, 124	isumsup2 15911	. . . . 5 ⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
323		seqex 14050	. . . . . . 7 ⊢ seq1( + , ((abs ∘ − ) ∘ 𝐹)) ∈ V
324	13, 323	eqeltri 2862	. . . . . 6 ⊢ 𝑆 ∈ V
325	324	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ V)
326		eqidd 2767	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) = (((abs ∘ − ) ∘ 𝐻)‘𝑛))
327	50, 15, 84, 326, 74, 73, 158	isumsup2 15911	. . . . 5 ⊢ (𝜑 → 𝑈 ⇝ sup(ran 𝑈, ℝ, < ))
328	42	recnd 11247	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℂ)
329	143	recnd 11247	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℂ)
330	57	recnd 11247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
331	52, 53, 330	syl2an 608	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
332	74	recnd 11247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
333	52, 53, 332	syl2an 608	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
334	77	eqcomd 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
335	52, 53, 334	syl2an 608	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
336	51, 331, 333, 335	seradd 14091	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)))
337	81, 153	oveq12i 7428	. . . . . 6 ⊢ ((𝑇‘𝑗) + (𝑈‘𝑗)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗))
338	336, 82, 337	3eqtr4g 2826	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) = ((𝑇‘𝑗) + (𝑈‘𝑗)))
339	50, 84, 322, 325, 327, 328, 329, 338	climadd 15694	. . . 4 ⊢ (𝜑 → 𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
340		climuni 15614	. . . 4 ⊢ ((𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) ∧ 𝑆 ⇝ sup(ran 𝑆, ℝ*, < )) → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
341	339, 114, 340	syl2anc 596	. . 3 ⊢ (𝜑 → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ*, < ))
342	320, 341	breqtrd 5140	. 2 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ sup(ran 𝑆, ℝ*, < ))
343	9, 23, 25, 342, 18	letrd 11377	1 ⊢ (𝜑 → ((vol*‘(𝐸 ∩ 𝐵)) + (vol*‘(𝐸 ∖ 𝐵))) ≤ ((vol*‘𝐸) + 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2961  ∀wral 3082  ∃wrex 3092  Vcvv 3458   ∖ cdif 3905   ∩ cin 3907   ⊆ wss 3908  ∅c0 4289  ifcif 4490  ⟨cop 4598  ∪ cuni 4875   class class class wbr 5112   ↦ cmpt 5195   × cxp 5662  dom cdm 5664  ran crn 5665   ∘ ccom 5668   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540  (class class class)co 7416  1^st c1st 7986  2^nd c2nd 7987  supcsup 9402  ℂcc 11108  ℝcr 11109  0cc0 11110  1c1 11111   + caddc 11113  +∞cpnf 11250  ℝ^*cxr 11252   < clt 11253   ≤ cle 11254   − cmin 11451  ℕcn 12243  ℤ_≥cuz 12872  ℝ⁺crp 13026  (,)cioo 13382  [,)cico 13384  [,]cicc 13385  ...cfz 13545  seqcseq 14048  abscabs 15296   ⇝ cli 15546  vol*covol 25636

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5241  ax-sep 5260  ax-nul 5272  ax-pow 5339  ax-pr 5407  ax-un 7738  ax-inf2 9612  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-int 4916  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-tr 5222  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-er 8696  df-map 8828  df-pm 8829  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-sup 9404  df-inf 9405  df-oi 9474  df-card 9936  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11453  df-neg 11454  df-div 11882  df-nn 12244  df-2 12313  df-3 12314  df-n0 12515  df-z 12602  df-uz 12873  df-q 12983  df-rp 13027  df-ioo 13386  df-ico 13388  df-icc 13389  df-fz 13546  df-fzo 13694  df-fl 13836  df-seq 14049  df-exp 14109  df-hash 14378  df-cj 15161  df-re 15162  df-im 15163  df-sqrt 15297  df-abs 15298  df-clim 15550  df-rlim 15551  df-sum 15749  df-ovol 25638

This theorem is used by:  ioombl1  25736