ioombl1lem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ioombl1lem4		Structured version Visualization version GIF version

Theorem ioombl1lem4 24630

Description: Lemma for ioombl1 24631. (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	⊢ 𝑃 = (1^st ‘(𝐹‘𝑛))
ioombl1.q	⊢ 𝑄 = (2^nd ‘(𝐹‘𝑛))
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 4159	. . . 4 ⊢ (𝐸 ∩ 𝐵) ⊆ 𝐸
2		ioombl1.e	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
3		ioombl1.v	. . . 4 ⊢ (𝜑 → (vol*‘𝐸) ∈ ℝ)
4		ovolsscl 24555	. . . 4 ⊢ (((𝐸 ∩ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∩ 𝐵)) ∈ ℝ)
5	1, 2, 3, 4	mp3an2i 1464	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ∈ ℝ)
6		difss 4062	. . . 4 ⊢ (𝐸 ∖ 𝐵) ⊆ 𝐸
7		ovolsscl 24555	. . . 4 ⊢ (((𝐸 ∖ 𝐵) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ (vol‘𝐸) ∈ ℝ) → (vol‘(𝐸 ∖ 𝐵)) ∈ ℝ)
8	6, 2, 3, 7	mp3an2i 1464	. . 3 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ∈ ℝ)
9	5, 8	readdcld 10935	. 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 ⊢ 𝑃 = (1^st ‘(𝐹‘𝑛))
20		ioombl1.q	. . 3 ⊢ 𝑄 = (2^nd ‘(𝐹‘𝑛))
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 24628	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
24	12	rpred 12701	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
25	3, 24	readdcld 10935	. 2 ⊢ (𝜑 → ((vol*‘𝐸) + 𝐶) ∈ ℝ)
26	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem1 24627	. . . . . . . . 9 ⊢ (𝜑 → (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))))
27	26	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
28		eqid 2738	. . . . . . . . 9 ⊢ ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
29	28, 14	ovolsf 24541	. . . . . . . 8 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
30	27, 29	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑇:ℕ⟶(0[,)+∞))
31	30	frnd 6592	. . . . . 6 ⊢ (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
32		rge0ssre 13117	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
33	31, 32	sstrdi 3929	. . . . 5 ⊢ (𝜑 → ran 𝑇 ⊆ ℝ)
34		1nn 11914	. . . . . . . 8 ⊢ 1 ∈ ℕ
35	30	fdmd 6595	. . . . . . . 8 ⊢ (𝜑 → dom 𝑇 = ℕ)
36	34, 35	eleqtrrid 2846	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑇)
37	36	ne0d 4266	. . . . . 6 ⊢ (𝜑 → dom 𝑇 ≠ ∅)
38		dm0rn0 5823	. . . . . . 7 ⊢ (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
39	38	necon3bii 2995	. . . . . 6 ⊢ (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
40	37, 39	sylib 217	. . . . 5 ⊢ (𝜑 → ran 𝑇 ≠ ∅)
41	30	ffvelrnda 6943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ (0[,)+∞))
42	32, 41	sselid 3915	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℝ)
43		eqid 2738	. . . . . . . . . . . . 13 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
44	43, 13	ovolsf 24541	. . . . . . . . . . . 12 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
45	16, 44	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞))
46	45	ffvelrnda 6943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ (0[,)+∞))
47	32, 46	sselid 3915	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ∈ ℝ)
48	23	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → sup(ran 𝑆, ℝ^*, < ) ∈ ℝ)
49		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ)
50		nnuz 12550	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ_≥‘1)
51	49, 50	eleqtrdi 2849	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ_≥‘1))
52		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝜑)
53		elfznn 13214	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ)
54	28	ovolfsf 24540	. . . . . . . . . . . . . . 15 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
55	27, 54	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
56	55	ffvelrnda 6943	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞))
57	32, 56	sselid 3915	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
58	52, 53, 57	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ)
59	43	ovolfsf 24540	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
60	16, 59	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
61	60	ffvelrnda 6943	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞))
62		elrege0 13115	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
63	61, 62	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛)))
64	63	simpld 494	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
65	52, 53, 64	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
66	26	simprd 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
67		eqid 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
68	67	ovolfsf 24540	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
69	66, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs ∘ − ) ∘ 𝐻):ℕ⟶(0[,)+∞))
70	69	ffvelrnda 6943	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞))
71		elrege0 13115	. . . . . . . . . . . . . . . 16 ⊢ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
72	70, 71	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
73	72	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛))
74	72	simpld 494	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
75	57, 74	addge01d 11493	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
76	73, 75	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
77	10, 11, 2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	ioombl1lem3 24629	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
78	76, 77	breqtrd 5096	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
79	52, 53, 78	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
80	51, 58, 65, 79	serle 13706	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
81	14	fveq1i 6757	. . . . . . . . . 10 ⊢ (𝑇‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗)
82	13	fveq1i 6757	. . . . . . . . . 10 ⊢ (𝑆‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗)
83	80, 81, 82	3brtr4g 5104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ (𝑆‘𝑗))
84		1zzd 12281	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 1 ∈ ℤ)
85		eqidd 2739	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
86	63	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
87	45	frnd 6592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
88		icossxr 13093	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0[,)+∞) ⊆ ℝ^*
89	87, 88	sstrdi 3929	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ^*)
90	89	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ^*)
91	45	ffnd 6585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑆 Fn ℕ)
92		fnfvelrn 6940	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
93	91, 92	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ∈ ran 𝑆)
94		supxrub 12987	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑆 ⊆ ℝ^* ∧ (𝑆‘𝑘) ∈ ran 𝑆) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ^*, < ))
95	90, 93, 94	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ^*, < ))
96	95	ralrimiva 3107	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ^*, < ))
97		brralrspcev 5130	. . . . . . . . . . . . . . . 16 ⊢ ((sup(ran 𝑆, ℝ^, < ) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ sup(ran 𝑆, ℝ^, < )) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
98	23, 96, 97	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)
99	50, 13, 84, 85, 64, 86, 98	isumsup2 15486	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
100	87, 32	sstrdi 3929	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ⊆ ℝ)
101	45	fdmd 6595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom 𝑆 = ℕ)
102	34, 101	eleqtrrid 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ dom 𝑆)
103	102	ne0d 4266	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → dom 𝑆 ≠ ∅)
104		dm0rn0 5823	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
105	104	necon3bii 2995	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
106	103, 105	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝑆 ≠ ∅)
107		breq1 5073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑆‘𝑘) ≤ 𝑥))
108	107	ralrn 6946	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
109	91, 108	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
110	109	rexbidv 3225	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥))
111	98, 110	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥)
112		supxrre 12990	. . . . . . . . . . . . . . 15 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) → sup(ran 𝑆, ℝ^*, < ) = sup(ran 𝑆, ℝ, < ))
113	100, 106, 111, 112	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (𝜑 → sup(ran 𝑆, ℝ^*, < ) = sup(ran 𝑆, ℝ, < ))
114	99, 113	breqtrrd 5098	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ^*, < ))
115	114	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ⇝ sup(ran 𝑆, ℝ^*, < ))
116	13, 115	eqbrtrrid 5106	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → seq1( + , ((abs ∘ − ) ∘ 𝐹)) ⇝ sup(ran 𝑆, ℝ^*, < ))
117	64	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) ∈ ℝ)
118	86	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
119	50, 49, 116, 117, 118	climserle 15302	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) ≤ sup(ran 𝑆, ℝ^*, < ))
120	82, 119	eqbrtrid 5105	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) ≤ sup(ran 𝑆, ℝ^*, < ))
121	42, 47, 48, 83, 120	letrd 11062	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ^*, < ))
122	121	ralrimiva 3107	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ^*, < ))
123		brralrspcev 5130	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ^, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ sup(ran 𝑆, ℝ^, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
124	23, 122, 123	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥)
125	30	ffnd 6585	. . . . . . . 8 ⊢ (𝜑 → 𝑇 Fn ℕ)
126		breq1 5073	. . . . . . . . 9 ⊢ (𝑧 = (𝑇‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑇‘𝑗) ≤ 𝑥))
127	126	ralrn 6946	. . . . . . . 8 ⊢ (𝑇 Fn ℕ → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
128	125, 127	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
129	128	rexbidv 3225	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑇‘𝑗) ≤ 𝑥))
130	124, 129	mpbird 256	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥)
131	33, 40, 130	suprcld 11868	. . . 4 ⊢ (𝜑 → sup(ran 𝑇, ℝ, < ) ∈ ℝ)
132	67, 15	ovolsf 24541	. . . . . . . 8 ⊢ (𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑈:ℕ⟶(0[,)+∞))
133	66, 132	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈:ℕ⟶(0[,)+∞))
134	133	frnd 6592	. . . . . 6 ⊢ (𝜑 → ran 𝑈 ⊆ (0[,)+∞))
135	134, 32	sstrdi 3929	. . . . 5 ⊢ (𝜑 → ran 𝑈 ⊆ ℝ)
136	133	fdmd 6595	. . . . . . . 8 ⊢ (𝜑 → dom 𝑈 = ℕ)
137	34, 136	eleqtrrid 2846	. . . . . . 7 ⊢ (𝜑 → 1 ∈ dom 𝑈)
138	137	ne0d 4266	. . . . . 6 ⊢ (𝜑 → dom 𝑈 ≠ ∅)
139		dm0rn0 5823	. . . . . . 7 ⊢ (dom 𝑈 = ∅ ↔ ran 𝑈 = ∅)
140	139	necon3bii 2995	. . . . . 6 ⊢ (dom 𝑈 ≠ ∅ ↔ ran 𝑈 ≠ ∅)
141	138, 140	sylib 217	. . . . 5 ⊢ (𝜑 → ran 𝑈 ≠ ∅)
142	133	ffvelrnda 6943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ (0[,)+∞))
143	32, 142	sselid 3915	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℝ)
144	52, 53, 74	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℝ)
145		elrege0 13115	. . . . . . . . . . . . . . . 16 ⊢ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
146	56, 145	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛)))
147	146	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛))
148	74, 57	addge02d 11494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑛) ↔ (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛))))
149	147, 148	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
150	149, 77	breqtrd 5096	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
151	52, 53, 150	syl2an 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ≤ (((abs ∘ − ) ∘ 𝐹)‘𝑛))
152	51, 144, 65, 151	serle 13706	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗) ≤ (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗))
153	15	fveq1i 6757	. . . . . . . . . 10 ⊢ (𝑈‘𝑗) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)
154	152, 153, 82	3brtr4g 5104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ (𝑆‘𝑗))
155	143, 47, 48, 154, 120	letrd 11062	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ^*, < ))
156	155	ralrimiva 3107	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ^*, < ))
157		brralrspcev 5130	. . . . . . 7 ⊢ ((sup(ran 𝑆, ℝ^, < ) ∈ ℝ ∧ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ sup(ran 𝑆, ℝ^, < )) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
158	23, 156, 157	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥)
159	133	ffnd 6585	. . . . . . . 8 ⊢ (𝜑 → 𝑈 Fn ℕ)
160		breq1 5073	. . . . . . . . 9 ⊢ (𝑧 = (𝑈‘𝑗) → (𝑧 ≤ 𝑥 ↔ (𝑈‘𝑗) ≤ 𝑥))
161	160	ralrn 6946	. . . . . . . 8 ⊢ (𝑈 Fn ℕ → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
162	159, 161	syl 17	. . . . . . 7 ⊢ (𝜑 → (∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
163	162	rexbidv 3225	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑗 ∈ ℕ (𝑈‘𝑗) ≤ 𝑥))
164	158, 163	mpbird 256	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥)
165	135, 141, 164	suprcld 11868	. . . 4 ⊢ (𝜑 → sup(ran 𝑈, ℝ, < ) ∈ ℝ)
166		ssralv 3983	. . . . . . . . . 10 ⊢ ((𝐸 ∩ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛)))))
167	1, 166	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))))
168	19	breq1i 5077	. . . . . . . . . . . . 13 ⊢ (𝑃 < 𝑥 ↔ (1^st ‘(𝐹‘𝑛)) < 𝑥)
169		ovolfcl 24535	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1^st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑛)) ≤ (2^nd ‘(𝐹‘𝑛))))
170	16, 169	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1^st ‘(𝐹‘𝑛)) ∈ ℝ ∧ (2^nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1^st ‘(𝐹‘𝑛)) ≤ (2^nd ‘(𝐹‘𝑛))))
171	170	simp1d 1140	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1^st ‘(𝐹‘𝑛)) ∈ ℝ)
172	19, 171	eqeltrid 2843	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
173	172	adantlr 711	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
174	1, 2	sstrid 3928	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ℝ)
175	174	sselda 3917	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → 𝑥 ∈ ℝ)
176	175	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
177		ltle 10994	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
178	173, 176, 177	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
179		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
180		opex 5373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V
181	21	fvmpt2 6868	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩ ∈ V) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
182	179, 180, 181	sylancl 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩)
183	182	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1^st ‘(𝐺‘𝑛)) = (1^st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
184	11	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℝ)
185	184, 172	ifcld 4502	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
186	170	simp2d 1141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2^nd ‘(𝐹‘𝑛)) ∈ ℝ)
187	20, 186	eqeltrid 2843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
188	185, 187	ifcld 4502	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
189		op1stg 7816	. . . . . . . . . . . . . . . . . . 19 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (1^st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
190	188, 187, 189	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1^st ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
191	183, 190	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1^st ‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
192	191	ad2ant2r 743	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (1^st ‘(𝐺‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
193	188	ad2ant2r 743	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ)
194	185	ad2ant2r 743	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
195	174	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (𝐸 ∩ 𝐵) ⊆ ℝ)
196		simplr 765	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ (𝐸 ∩ 𝐵))
197	195, 196	sseldd 3918	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ ℝ)
198	187	ad2ant2r 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑄 ∈ ℝ)
199		min1 12852	. . . . . . . . . . . . . . . . . 18 ⊢ ((if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ ∧ 𝑄 ∈ ℝ) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
200	194, 198, 199	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
201	11	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ∈ ℝ)
202		elinel2 4126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∩ 𝐵) → 𝑥 ∈ 𝐵)
203	202	ad2antlr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑥 ∈ 𝐵)
204	11	rexrd 10956	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
205		pnfxr 10960	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ +∞ ∈ ℝ^*
206		elioo2 13049	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
207	204, 205, 206	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞)))
208	10	eleq2i 2830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (𝐴(,)+∞))
209		ltpnf 12785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝑥 < +∞)
211	210	pm4.71i 559	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
212		df-3an 1087	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞) ↔ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ∧ 𝑥 < +∞))
213	211, 212	bitr4i 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞))
214	207, 208, 213	3bitr4g 313	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
215		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 < 𝑥) → 𝐴 < 𝑥)
216	214, 215	syl6bi 252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝐴 < 𝑥))
217	216	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (𝑥 ∈ 𝐵 → 𝐴 < 𝑥))
218	203, 217	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 < 𝑥)
219	201, 197, 218	ltled 11053	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝐴 ≤ 𝑥)
220		simprr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → 𝑃 ≤ 𝑥)
221		breq1 5073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝐴 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
222		breq1 5073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 = if(𝑃 ≤ 𝐴, 𝐴, 𝑃) → (𝑃 ≤ 𝑥 ↔ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥))
223	221, 222	ifboth 4495	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ≤ 𝑥 ∧ 𝑃 ≤ 𝑥) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
224	219, 220, 223	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑥)
225	193, 194, 197, 200, 224	letrd 11062	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ≤ 𝑥)
226	192, 225	eqbrtrd 5092	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑃 ≤ 𝑥)) → (1^st ‘(𝐺‘𝑛)) ≤ 𝑥)
227	226	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 ≤ 𝑥 → (1^st ‘(𝐺‘𝑛)) ≤ 𝑥))
228	178, 227	syld 47	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → (1^st ‘(𝐺‘𝑛)) ≤ 𝑥))
229	168, 228	syl5bir 242	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1^st ‘(𝐹‘𝑛)) < 𝑥 → (1^st ‘(𝐺‘𝑛)) ≤ 𝑥))
230	20	breq2i 5078	. . . . . . . . . . . . . 14 ⊢ (𝑥 < 𝑄 ↔ 𝑥 < (2^nd ‘(𝐹‘𝑛)))
231	187	adantlr 711	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
232		ltle 10994	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ ∧ 𝑄 ∈ ℝ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
233	176, 231, 232	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
234	230, 233	syl5bir 242	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2^nd ‘(𝐹‘𝑛)) → 𝑥 ≤ 𝑄))
235	182	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2^nd ‘(𝐺‘𝑛)) = (2^nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩))
236		op2ndg 7817	. . . . . . . . . . . . . . . . 17 ⊢ ((if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (2^nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
237	188, 187, 236	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2^nd ‘⟨if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄), 𝑄⟩) = 𝑄)
238	235, 237	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2^nd ‘(𝐺‘𝑛)) = 𝑄)
239	238	adantlr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (2^nd ‘(𝐺‘𝑛)) = 𝑄)
240	239	breq2d 5082	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ (2^nd ‘(𝐺‘𝑛)) ↔ 𝑥 ≤ 𝑄))
241	234, 240	sylibrd 258	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2^nd ‘(𝐹‘𝑛)) → 𝑥 ≤ (2^nd ‘(𝐺‘𝑛))))
242	229, 241	anim12d 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ((1^st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐺‘𝑛)))))
243	242	reximdva 3202	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∩ 𝐵)) → (∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1^st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐺‘𝑛)))))
244	243	ralimdva 3102	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐺‘𝑛)))))
245	167, 244	syl5 34	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐺‘𝑛)))))
246		ovolfioo 24536	. . . . . . . . 9 ⊢ ((𝐸 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛)))))
247	2, 16, 246	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) ↔ ∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛)))))
248		ovolficc 24537	. . . . . . . . 9 ⊢ (((𝐸 ∩ 𝐵) ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐺‘𝑛)))))
249	174, 27, 248	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺) ↔ ∀𝑥 ∈ (𝐸 ∩ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐺‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐺‘𝑛)))))
250	245, 247, 249	3imtr4d 293	. . . . . . 7 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) → (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)))
251	17, 250	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺))
252	14	ovollb2 24558	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∩ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐺)) → (vol‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ^, < ))
253	27, 251, 252	syl2anc 583	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ^, < ))
254		supxrre 12990	. . . . . 6 ⊢ ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑇 𝑧 ≤ 𝑥) → sup(ran 𝑇, ℝ^*, < ) = sup(ran 𝑇, ℝ, < ))
255	33, 40, 130, 254	syl3anc 1369	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) = sup(ran 𝑇, ℝ, < ))
256	253, 255	breqtrd 5096	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∩ 𝐵)) ≤ sup(ran 𝑇, ℝ, < ))
257		ssralv 3983	. . . . . . . . . 10 ⊢ ((𝐸 ∖ 𝐵) ⊆ 𝐸 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛)))))
258	6, 257	ax-mp 5	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))))
259	172	adantlr 711	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑃 ∈ ℝ)
260	6, 2	sstrid 3928	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ℝ)
261	260	sselda 3917	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → 𝑥 ∈ ℝ)
262	261	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑥 ∈ ℝ)
263	259, 262, 177	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑃 < 𝑥 → 𝑃 ≤ 𝑥))
264	168, 263	syl5bir 242	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1^st ‘(𝐹‘𝑛)) < 𝑥 → 𝑃 ≤ 𝑥))
265		opex 5373	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V
266	22	fvmpt2 6868	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩ ∈ V) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
267	179, 265, 266	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐻‘𝑛) = ⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩)
268	267	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1^st ‘(𝐻‘𝑛)) = (1^st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
269		op1stg 7816	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (1^st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
270	172, 188, 269	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1^st ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = 𝑃)
271	268, 270	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1^st ‘(𝐻‘𝑛)) = 𝑃)
272	271	adantlr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (1^st ‘(𝐻‘𝑛)) = 𝑃)
273	272	breq1d 5080	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1^st ‘(𝐻‘𝑛)) ≤ 𝑥 ↔ 𝑃 ≤ 𝑥))
274	264, 273	sylibrd 258	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → ((1^st ‘(𝐹‘𝑛)) < 𝑥 → (1^st ‘(𝐻‘𝑛)) ≤ 𝑥))
275	187	adantlr 711	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → 𝑄 ∈ ℝ)
276	262, 275, 232	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ 𝑄))
277	260	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐸 ∖ 𝐵) ⊆ ℝ)
278		simplr 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ (𝐸 ∖ 𝐵))
279	277, 278	sseldd 3918	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ∈ ℝ)
280	11	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ∈ ℝ)
281	172	ad2ant2r 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑃 ∈ ℝ)
282	280, 281	ifcld 4502	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∈ ℝ)
283		eldifn 4058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐸 ∖ 𝐵) → ¬ 𝑥 ∈ 𝐵)
284	283	ad2antlr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → ¬ 𝑥 ∈ 𝐵)
285	279	biantrurd 532	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐴 < 𝑥 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
286	214	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ ℝ ∧ 𝐴 < 𝑥)))
287	285, 286	bitr4d 281	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (𝐴 < 𝑥 ↔ 𝑥 ∈ 𝐵))
288	284, 287	mtbird 324	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → ¬ 𝐴 < 𝑥)
289	279, 280, 288	nltled 11055	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝐴)
290		max2 12850	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ 𝐴 ∈ ℝ) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
291	281, 280, 290	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝐴 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
292	279, 280, 282, 289, 291	letrd 11062	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃))
293		simprr 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ 𝑄)
294		breq2 5074	. . . . . . . . . . . . . . . . . 18 ⊢ (if(𝑃 ≤ 𝐴, 𝐴, 𝑃) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
295		breq2 5074	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑄 = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) → (𝑥 ≤ 𝑄 ↔ 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)))
296	294, 295	ifboth 4495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ≤ if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ∧ 𝑥 ≤ 𝑄) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
297	292, 293, 296	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
298	267	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2^nd ‘(𝐻‘𝑛)) = (2^nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩))
299		op2ndg 7817	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄) ∈ ℝ) → (2^nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
300	172, 188, 299	syl2anc 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2^nd ‘⟨𝑃, if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄)⟩) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
301	298, 300	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2^nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
302	301	ad2ant2r 743	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → (2^nd ‘(𝐻‘𝑛)) = if(if(𝑃 ≤ 𝐴, 𝐴, 𝑃) ≤ 𝑄, if(𝑃 ≤ 𝐴, 𝐴, 𝑃), 𝑄))
303	297, 302	breqtrrd 5098	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ (𝑛 ∈ ℕ ∧ 𝑥 ≤ 𝑄)) → 𝑥 ≤ (2^nd ‘(𝐻‘𝑛)))
304	303	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 ≤ 𝑄 → 𝑥 ≤ (2^nd ‘(𝐻‘𝑛))))
305	276, 304	syld 47	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < 𝑄 → 𝑥 ≤ (2^nd ‘(𝐻‘𝑛))))
306	230, 305	syl5bir 242	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (𝑥 < (2^nd ‘(𝐹‘𝑛)) → 𝑥 ≤ (2^nd ‘(𝐻‘𝑛))))
307	274, 306	anim12d 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) ∧ 𝑛 ∈ ℕ) → (((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ((1^st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐻‘𝑛)))))
308	307	reximdva 3202	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 ∖ 𝐵)) → (∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1^st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐻‘𝑛)))))
309	308	ralimdva 3102	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐻‘𝑛)))))
310	258, 309	syl5 34	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥 ∈ 𝐸 ∃𝑛 ∈ ℕ ((1^st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2^nd ‘(𝐹‘𝑛))) → ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐻‘𝑛)))))
311		ovolficc 24537	. . . . . . . . 9 ⊢ (((𝐸 ∖ 𝐵) ⊆ ℝ ∧ 𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → ((𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐻‘𝑛)))))
312	260, 66, 311	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻) ↔ ∀𝑥 ∈ (𝐸 ∖ 𝐵)∃𝑛 ∈ ℕ ((1^st ‘(𝐻‘𝑛)) ≤ 𝑥 ∧ 𝑥 ≤ (2^nd ‘(𝐻‘𝑛)))))
313	310, 247, 312	3imtr4d 293	. . . . . . 7 ⊢ (𝜑 → (𝐸 ⊆ ∪ ran ((,) ∘ 𝐹) → (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)))
314	17, 313	mpd 15	. . . . . 6 ⊢ (𝜑 → (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻))
315	15	ovollb2 24558	. . . . . 6 ⊢ ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ (𝐸 ∖ 𝐵) ⊆ ∪ ran ([,] ∘ 𝐻)) → (vol‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ^, < ))
316	66, 314, 315	syl2anc 583	. . . . 5 ⊢ (𝜑 → (vol‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ^, < ))
317		supxrre 12990	. . . . . 6 ⊢ ((ran 𝑈 ⊆ ℝ ∧ ran 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑈 𝑧 ≤ 𝑥) → sup(ran 𝑈, ℝ^*, < ) = sup(ran 𝑈, ℝ, < ))
318	135, 141, 164, 317	syl3anc 1369	. . . . 5 ⊢ (𝜑 → sup(ran 𝑈, ℝ^*, < ) = sup(ran 𝑈, ℝ, < ))
319	316, 318	breqtrd 5096	. . . 4 ⊢ (𝜑 → (vol*‘(𝐸 ∖ 𝐵)) ≤ sup(ran 𝑈, ℝ, < ))
320	5, 8, 131, 165, 256, 319	le2addd 11524	. . 3 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐵)) + (vol‘(𝐸 ∖ 𝐵))) ≤ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
321		eqidd 2739	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐺)‘𝑛))
322	50, 14, 84, 321, 57, 147, 124	isumsup2 15486	. . . . 5 ⊢ (𝜑 → 𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
323		seqex 13651	. . . . . . 7 ⊢ seq1( + , ((abs ∘ − ) ∘ 𝐹)) ∈ V
324	13, 323	eqeltri 2835	. . . . . 6 ⊢ 𝑆 ∈ V
325	324	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ V)
326		eqidd 2739	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) = (((abs ∘ − ) ∘ 𝐻)‘𝑛))
327	50, 15, 84, 326, 74, 73, 158	isumsup2 15486	. . . . 5 ⊢ (𝜑 → 𝑈 ⇝ sup(ran 𝑈, ℝ, < ))
328	42	recnd 10934	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑇‘𝑗) ∈ ℂ)
329	143	recnd 10934	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑈‘𝑗) ∈ ℂ)
330	57	recnd 10934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
331	52, 53, 330	syl2an 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) ∈ ℂ)
332	74	recnd 10934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
333	52, 53, 332	syl2an 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐻)‘𝑛) ∈ ℂ)
334	77	eqcomd 2744	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
335	52, 53, 334	syl2an 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((((abs ∘ − ) ∘ 𝐺)‘𝑛) + (((abs ∘ − ) ∘ 𝐻)‘𝑛)))
336	51, 331, 333, 335	seradd 13693	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑗) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗)))
337	81, 153	oveq12i 7267	. . . . . 6 ⊢ ((𝑇‘𝑗) + (𝑈‘𝑗)) = ((seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑗) + (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝑗))
338	336, 82, 337	3eqtr4g 2804	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆‘𝑗) = ((𝑇‘𝑗) + (𝑈‘𝑗)))
339	50, 84, 322, 325, 327, 328, 329, 338	climadd 15269	. . . 4 ⊢ (𝜑 → 𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )))
340		climuni 15189	. . . 4 ⊢ ((𝑆 ⇝ (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) ∧ 𝑆 ⇝ sup(ran 𝑆, ℝ^, < )) → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ^, < ))
341	339, 114, 340	syl2anc 583	. . 3 ⊢ (𝜑 → (sup(ran 𝑇, ℝ, < ) + sup(ran 𝑈, ℝ, < )) = sup(ran 𝑆, ℝ^*, < ))
342	320, 341	breqtrd 5096	. 2 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐵)) + (vol‘(𝐸 ∖ 𝐵))) ≤ sup(ran 𝑆, ℝ^*, < ))
343	9, 23, 25, 342, 18	letrd 11062	1 ⊢ (𝜑 → ((vol‘(𝐸 ∩ 𝐵)) + (vol‘(𝐸 ∖ 𝐵))) ≤ ((vol*‘𝐸) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ∖ cdif 3880 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 ifcif 4456 ⟨cop 4564 ∪ cuni 4836 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 dom cdm 5580 ran crn 5581 ∘ ccom 5584 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 1^st c1st 7802 2^nd c2nd 7803 supcsup 9129 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 +∞cpnf 10937 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 ℕcn 11903 ℤ_≥cuz 12511 ℝ⁺crp 12659 (,)cioo 13008 [,)cico 13010 [,]cicc 13011 ...cfz 13168 seqcseq 13649 abscabs 14873 ⇝ cli 15121 vol*covol 24531

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-oi 9199 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-ioo 13012 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-rlim 15126 df-sum 15326 df-ovol 24533

This theorem is referenced by: ioombl1 24631

W3C validator