hoidmv1lelem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hoidmv1lelem1		Structured version Visualization version GIF version

Theorem hoidmv1lelem1 47645

Description: The supremum of 𝑈 belongs to 𝑈. This is the last part of step (a) and the whole step (b) in the proof of Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)

**Hypotheses**
Ref	Expression
hoidmv1lelem1.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
hoidmv1lelem1.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
hoidmv1lelem1.l	⊢ (𝜑 → 𝐴 < 𝐵)
hoidmv1lelem1.c	⊢ (𝜑 → 𝐶:ℕ⟶ℝ)
hoidmv1lelem1.d	⊢ (𝜑 → 𝐷:ℕ⟶ℝ)
hoidmv1lelem1.r	⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ)
hoidmv1lelem1.u	⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}
hoidmv1lelem1.s	⊢ 𝑆 = sup(𝑈, ℝ, < )

**Assertion**
Ref	Expression
hoidmv1lelem1	⊢ (𝜑 → (𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥))

Distinct variable groups: 𝐴,𝑗,𝑧 𝑦,𝐴 𝑥,𝐵,𝑦 𝑧,𝐵 𝑧,𝐶 𝑧,𝐷 𝑆,𝑗,𝑧 𝑈,𝑗,𝑧 𝑥,𝑈,𝑦 𝜑,𝑗,𝑧 Allowed substitution hints: 𝜑(𝑥, 𝑦) 𝐴(𝑥) 𝐵(𝑗) 𝐶(𝑥, 𝑦, 𝑗) 𝐷(𝑥, 𝑦, 𝑗) 𝑆(𝑥, 𝑦)

**Proof of Theorem hoidmv1lelem1**
Step	Hyp	Ref	Expression
1		hoidmv1lelem1.s	. . . . . 6 ⊢ 𝑆 = sup(𝑈, ℝ, < )
2		hoidmv1lelem1.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		hoidmv1lelem1.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		hoidmv1lelem1.u	. . . . . . . . 9 ⊢ 𝑈 = {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))}
5		ssrab2 4005	. . . . . . . . 9 ⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ⊆ (𝐴[,]𝐵)
6	4, 5	eqsstri 3954	. . . . . . . 8 ⊢ 𝑈 ⊆ (𝐴[,]𝐵)
7	6	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))
8	2	rexrd 11360	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
9	3	rexrd 11360	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
10		hoidmv1lelem1.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 < 𝐵)
11	2, 3, 10	ltled 11459	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
12		lbicc2 13596	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
13	8, 9, 11, 12	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
14	2	recnd 11338	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	subidd 11658	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
16		nfv 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝜑
17		nnex 12342	. . . . . . . . . . . . . 14 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ ∈ V)
19		volf 25851	. . . . . . . . . . . . . . 15 ⊢ vol:dom vol⟶(0[,]+∞)
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
21		hoidmv1lelem1.c	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶:ℕ⟶ℝ)
22	21	ffvelcdmda 7084	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ)
23		hoidmv1lelem1.d	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:ℕ⟶ℝ)
24	23	ffvelcdmda 7084	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ)
25	2	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ ℝ)
26	24, 25	ifcld 4528	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ)
27	26	rexrd 11360	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ^*)
28		icombl 25886	. . . . . . . . . . . . . . 15 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol)
29	22, 27, 28	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol)
30	20, 29	ffvelcdmd 7085	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))) ∈ (0[,]+∞))
31	16, 18, 30	sge0ge0mpt 47492	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
32	15, 31	eqbrtrd 5126	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
33	13, 32	jca 521	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
34		oveq1 7427	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (𝑧 − 𝐴) = (𝐴 − 𝐴))
35		breq2 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝐴 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝐴))
36		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝐴 → 𝑧 = 𝐴)
37	35, 36	ifbieq2d 4508	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝐴 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))
38	37	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝐴 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))
39	38	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐴 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))
40	39	mpteq2dv 5198	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐴 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))
41	40	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
42	34, 41	breq12d 5115	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐴 → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
43	42	elrab 3644	. . . . . . . . . 10 ⊢ (𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
44	33, 43	sylibr 237	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
45	44, 4	eleqtrrdi 2871	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
46	45	ne0d 4287	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≠ ∅)
47	2, 3, 7, 46	supicc 13633	. . . . . 6 ⊢ (𝜑 → sup(𝑈, ℝ, < ) ∈ (𝐴[,]𝐵))
48	1, 47	eqeltrid 2864	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (𝐴[,]𝐵))
49	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑆 = sup(𝑈, ℝ, < ))
50		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑧𝜑
51	2, 3	iccssred 13566	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
52	7, 51	sstrd 3918	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ⊆ ℝ)
53	52	sselda 3908	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℝ)
54		nfv 1946	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ 𝑈)
55	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ℕ ∈ V)
56	19	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
57	22	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ)
58	24	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ)
59	53	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → 𝑧 ∈ ℝ)
60	58, 59	ifcld 4528	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ)
61	60	rexrd 11360	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ^*)
62		icombl 25886	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol)
63	57, 61, 62	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol)
64	56, 63	ffvelcdmd 7085	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ∈ (0[,]+∞))
65	54, 55, 64	sge0xrclmpt 47482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ^*)
66		pnfxr 11364	. . . . . . . . . . . . . . . 16 ⊢ +∞ ∈ ℝ^*
67	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → +∞ ∈ ℝ^*)
68		hoidmv1lelem1.r	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ)
69	68	rexrd 11360	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ^*)
70	69	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ^*)
71	24	rexrd 11360	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ^*)
72		icombl 25886	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ^*) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
73	22, 71, 72	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
74	20, 73	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞))
75	74	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞))
76	73	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
77	22	rexrd 11360	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ^*)
78	77	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ^*)
79	71	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ^*)
80	22	leidd 11883	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗))
81	80	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗))
82		min1 13320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑧 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))
83	58, 59, 82	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))
84		icossico 13548	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ (𝐷‘𝑗) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
85	78, 79, 81, 83, 84	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
86		volss 25855	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))
87	63, 76, 85, 86	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))
88	54, 55, 64, 75, 87	sge0lempt 47464	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))))
89	68	ltpnfd 13251	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞)
90	89	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞)
91	65, 70, 67, 88, 90	xrlelttrd 13290	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) < +∞)
92	65, 67, 91	xrltned 46413	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≠ +∞)
93	92	neneqd 2960	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞)
94		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))
95	64, 94	fmptd 7114	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))):ℕ⟶(0[,]+∞))
96	55, 95	sge0repnf 47440	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞))
97	93, 96	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ)
98	2	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝐴 ∈ ℝ)
99	97, 98	readdcld 11339	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ∈ ℝ)
100	51, 48	sseldd 3909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑆 ∈ ℝ)
101	100	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
102	24, 101	ifcld 4528	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ)
103	102	rexrd 11360	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*)
104		icombl 25886	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
105	22, 103, 104	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
106	20, 105	ffvelcdmd 7085	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞))
107	16, 18, 106	sge0xrclmpt 47482	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ^*)
108	66	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → +∞ ∈ ℝ^*)
109		min1 13320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))
110	24, 101, 109	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))
111		icossico 13548	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ (𝐷‘𝑗) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
112	77, 71, 80, 110, 111	syl22anc 852	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
113		volss 25855	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))
114	105, 73, 112, 113	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))
115	16, 18, 106, 74, 114	sge0lempt 47464	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))))
116	107, 69, 108, 115, 89	xrlelttrd 13290	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) < +∞)
117	107, 108, 116	xrltned 46413	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≠ +∞)
118	117	neneqd 2960	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞)
119		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
120	106, 119	fmptd 7114	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
121	18, 120	sge0repnf 47440	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞))
122	118, 121	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ)
123	122, 2	readdcld 11339	. . . . . . . . . . . 12 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ)
124	123	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ)
125	4	eleq2i 2852	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
126	125	bilani 510	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
127		rabid 3432	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑧 ∈ (𝐴[,]𝐵) ∧ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))))
128	126, 127	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑧 ∈ (𝐴[,]𝐵) ∧ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))))
129	128	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))))
130	53, 98, 97	lesubaddd 11914	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴)))
131	129, 130	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴))
132	122	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ)
133	106	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞))
134	105	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
135	103	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*)
136	60	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ)
137		eqidd 2761	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) = (𝐷‘𝑗))
138		iftrue 4487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷‘𝑗) ≤ 𝑧 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = (𝐷‘𝑗))
139	138	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = (𝐷‘𝑗))
140	58	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ∈ ℝ)
141	59	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ∈ ℝ)
142	100	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑆 ∈ ℝ)
143		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ≤ 𝑧)
144	52	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑈 ⊆ ℝ)
145	46	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑈 ≠ ∅)
146	2, 3	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
147		iccsupr 13574	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑈 ⊆ (𝐴[,]𝐵) ∧ 𝐴 ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥))
148	146, 7, 45, 147	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥))
149	148	simp3d 1162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)
150	149	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)
151	126, 125	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈)
152		suprub 12279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < ))
153	144, 145, 150, 151, 152	syl31anc 1400	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < ))
154	153, 1	breqtrrdi 5146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ 𝑆)
155	154	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ 𝑆)
156	140, 141, 142, 143, 155	letrd 11468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ≤ 𝑆)
157	156	iftrued 4489	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
158	137, 139, 157	3eqtr4d 2805	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
159	136, 158	eqled 11414	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
160	59	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ∈ ℝ)
161	58	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ∈ ℝ)
162		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → ¬ (𝐷‘𝑗) ≤ 𝑧)
163	160, 161	ltnled 11458	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝑧 < (𝐷‘𝑗) ↔ ¬ (𝐷‘𝑗) ≤ 𝑧))
164	162, 163	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 < (𝐷‘𝑗))
165	160, 161, 164	ltled 11459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ (𝐷‘𝑗))
166	165	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ (𝐷‘𝑗))
167		iffalse 4490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐷‘𝑗) ≤ 𝑧 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
168	167	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
169		iftrue 4487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
170	169	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
171	168, 170	breq12d 5115	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → (if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ↔ 𝑧 ≤ (𝐷‘𝑗)))
172	166, 171	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
173	154	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ 𝑆)
174	167	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
175		iffalse 4490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆)
176	175	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆)
177	174, 176	breq12d 5115	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → (if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ↔ 𝑧 ≤ 𝑆))
178	173, 177	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
179	172, 178	pm2.61dan 825	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
180	159, 179	pm2.61dan 825	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
181		icossico 13548	. . . . . . . . . . . . . . 15 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
182	78, 135, 81, 180, 181	syl22anc 852	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
183		volss 25855	. . . . . . . . . . . . . 14 ⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
184	63, 134, 182, 183	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
185	54, 55, 64, 133, 184	sge0lempt 47464	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
186	97, 132, 98, 185	leadd1dd 11931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
187	53, 99, 124, 131, 186	letrd 11468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
188	187	ex 418	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ 𝑈 → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
189	50, 188	ralrimi 3260	. . . . . . . 8 ⊢ (𝜑 → ∀𝑧 ∈ 𝑈 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
190		suprleub 12284	. . . . . . . . 9 ⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ) → (sup(𝑈, ℝ, < ) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ↔ ∀𝑧 ∈ 𝑈 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
191	52, 46, 149, 123, 190	syl31anc 1400	. . . . . . . 8 ⊢ (𝜑 → (sup(𝑈, ℝ, < ) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ↔ ∀𝑧 ∈ 𝑈 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
192	189, 191	mpbird 260	. . . . . . 7 ⊢ (𝜑 → sup(𝑈, ℝ, < ) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
193	49, 192	eqbrtrd 5126	. . . . . 6 ⊢ (𝜑 → 𝑆 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
194	100, 2, 122	lesubaddd 11914	. . . . . 6 ⊢ (𝜑 → ((𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ↔ 𝑆 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
195	193, 194	mpbird 260	. . . . 5 ⊢ (𝜑 → (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
196	48, 195	jca 521	. . . 4 ⊢ (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
197		oveq1 7427	. . . . . 6 ⊢ (𝑧 = 𝑆 → (𝑧 − 𝐴) = (𝑆 − 𝐴))
198		breq2 5106	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑆))
199		id 23	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → 𝑧 = 𝑆)
200	198, 199	ifbieq2d 4508	. . . . . . . . . 10 ⊢ (𝑧 = 𝑆 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
201	200	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑧 = 𝑆 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
202	201	fveq2d 6889	. . . . . . . 8 ⊢ (𝑧 = 𝑆 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
203	202	mpteq2dv 5198	. . . . . . 7 ⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))
204	203	fveq2d 6889	. . . . . 6 ⊢ (𝑧 = 𝑆 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
205	197, 204	breq12d 5115	. . . . 5 ⊢ (𝑧 = 𝑆 → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
206	205	elrab 3644	. . . 4 ⊢ (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
207	196, 206	sylibr 237	. . 3 ⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
208	207, 4	eleqtrrdi 2871	. 2 ⊢ (𝜑 → 𝑆 ∈ 𝑈)
209	208, 45, 149	3jca 1146	1 ⊢ (𝜑 → (𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ⊆ wss 3895 ∅c0 4278 ifcif 4481 class class class wbr 5102 ↦ cmpt 5185 dom cdm 5650 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 supcsup 9433 ℝcr 11200 0cc0 11201 + caddc 11204 +∞cpnf 11341 ℝ^*cxr 11343 < clt 11344 ≤ cle 11345 − cmin 11542 ℕcn 12336 [,)cico 13479 [,]cicc 13480 volcvol 25785 Σ^{^}csumge0 47416

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9643 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278 ax-pre-sup 11279

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-2o 8478 df-er 8718 df-map 8850 df-pm 8851 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-sup 9435 df-inf 9436 df-oi 9505 df-dju 9983 df-card 10021 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-div 11975 df-nn 12337 df-2 12406 df-3 12407 df-n0 12608 df-z 12695 df-uz 12967 df-q 13077 df-rp 13122 df-xadd 13243 df-ioo 13481 df-ico 13483 df-icc 13484 df-fz 13641 df-fzo 13790 df-fl 13933 df-seq 14146 df-exp 14206 df-hash 14476 df-cj 15267 df-re 15268 df-im 15269 df-sqrt 15403 df-abs 15404 df-clim 15656 df-rlim 15657 df-sum 15855 df-xmet 21672 df-met 21673 df-ovol 25786 df-vol 25787 df-sumge0 47417

This theorem is used by: hoidmv1lelem3 47647

W3C validator