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 46629

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 4025	. . . . . . . . 9 ⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ⊆ (𝐴[,]𝐵)
6	4, 5	eqsstri 3976	. . . . . . . 8 ⊢ 𝑈 ⊆ (𝐴[,]𝐵)
7	6	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))
8	2	rexrd 11157	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
9	3	rexrd 11157	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
10		hoidmv1lelem1.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 < 𝐵)
11	2, 3, 10	ltled 11256	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
12		lbicc2 13359	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
13	8, 9, 11, 12	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
14	2	recnd 11135	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	subidd 11455	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
16		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝜑
17		nnex 12126	. . . . . . . . . . . . . 14 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ ∈ V)
19		volf 25452	. . . . . . . . . . . . . . 15 ⊢ vol:dom vol⟶(0[,]+∞)
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
21		hoidmv1lelem1.c	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶:ℕ⟶ℝ)
22	21	ffvelcdmda 7012	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ)
23		hoidmv1lelem1.d	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:ℕ⟶ℝ)
24	23	ffvelcdmda 7012	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ)
25	2	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ ℝ)
26	24, 25	ifcld 4517	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ)
27	26	rexrd 11157	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ^*)
28		icombl 25487	. . . . . . . . . . . . . . 15 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol)
29	22, 27, 28	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol)
30	20, 29	ffvelcdmd 7013	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))) ∈ (0[,]+∞))
31	16, 18, 30	sge0ge0mpt 46476	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
32	15, 31	eqbrtrd 5108	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
33	13, 32	jca 511	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
34		oveq1 7348	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (𝑧 − 𝐴) = (𝐴 − 𝐴))
35		breq2 5090	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝐴 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝐴))
36		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝐴 → 𝑧 = 𝐴)
37	35, 36	ifbieq2d 4497	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝐴 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))
38	37	oveq2d 7357	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝐴 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))
39	38	fveq2d 6821	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐴 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))
40	39	mpteq2dv 5180	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐴 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))
41	40	fveq2d 6821	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
42	34, 41	breq12d 5099	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐴 → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
43	42	elrab 3642	. . . . . . . . . 10 ⊢ (𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
44	33, 43	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
45	44, 4	eleqtrrdi 2842	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
46	45	ne0d 4287	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≠ ∅)
47	2, 3, 7, 46	supicc 13396	. . . . . 6 ⊢ (𝜑 → sup(𝑈, ℝ, < ) ∈ (𝐴[,]𝐵))
48	1, 47	eqeltrid 2835	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (𝐴[,]𝐵))
49	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑆 = sup(𝑈, ℝ, < ))
50		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑧𝜑
51	2, 3	iccssred 13329	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
52	7, 51	sstrd 3940	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ⊆ ℝ)
53	52	sselda 3929	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℝ)
54		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ 𝑈)
55	17	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ℕ ∈ V)
56	19	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
57	22	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ)
58	24	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ)
59	53	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → 𝑧 ∈ ℝ)
60	58, 59	ifcld 4517	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ)
61	60	rexrd 11157	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ^*)
62		icombl 25487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol)
63	57, 61, 62	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol)
64	56, 63	ffvelcdmd 7013	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ∈ (0[,]+∞))
65	54, 55, 64	sge0xrclmpt 46466	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ^*)
66		pnfxr 11161	. . . . . . . . . . . . . . . 16 ⊢ +∞ ∈ ℝ^*
67	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → +∞ ∈ ℝ^*)
68		hoidmv1lelem1.r	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ)
69	68	rexrd 11157	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ^*)
70	69	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ^*)
71	24	rexrd 11157	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ^*)
72		icombl 25487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ^*) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
73	22, 71, 72	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
74	20, 73	ffvelcdmd 7013	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞))
75	74	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞))
76	73	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
77	22	rexrd 11157	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ^*)
78	77	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ^*)
79	71	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ^*)
80	22	leidd 11678	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗))
81	80	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗))
82		min1 13083	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑧 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))
83	58, 59, 82	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))
84		icossico 13311	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ (𝐷‘𝑗) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
85	78, 79, 81, 83, 84	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
86		volss 25456	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))
87	63, 76, 85, 86	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))
88	54, 55, 64, 75, 87	sge0lempt 46448	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))))
89	68	ltpnfd 13015	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞)
90	89	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞)
91	65, 70, 67, 88, 90	xrlelttrd 13054	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) < +∞)
92	65, 67, 91	xrltned 45396	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≠ +∞)
93	92	neneqd 2933	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞)
94		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))
95	64, 94	fmptd 7042	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))):ℕ⟶(0[,]+∞))
96	55, 95	sge0repnf 46424	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞))
97	93, 96	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ)
98	2	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝐴 ∈ ℝ)
99	97, 98	readdcld 11136	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ∈ ℝ)
100	51, 48	sseldd 3930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑆 ∈ ℝ)
101	100	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
102	24, 101	ifcld 4517	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ)
103	102	rexrd 11157	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*)
104		icombl 25487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
105	22, 103, 104	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
106	20, 105	ffvelcdmd 7013	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞))
107	16, 18, 106	sge0xrclmpt 46466	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ^*)
108	66	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → +∞ ∈ ℝ^*)
109		min1 13083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))
110	24, 101, 109	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))
111		icossico 13311	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ (𝐷‘𝑗) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
112	77, 71, 80, 110, 111	syl22anc 838	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
113		volss 25456	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))
114	105, 73, 112, 113	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ≤ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))
115	16, 18, 106, 74, 114	sge0lempt 46448	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))))
116	107, 69, 108, 115, 89	xrlelttrd 13054	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) < +∞)
117	107, 108, 116	xrltned 45396	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≠ +∞)
118	117	neneqd 2933	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞)
119		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
120	106, 119	fmptd 7042	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
121	18, 120	sge0repnf 46424	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞))
122	118, 121	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ)
123	122, 2	readdcld 11136	. . . . . . . . . . . 12 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ)
124	123	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ)
125	4	eleq2i 2823	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
126	125	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑈 → 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
127	126	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
128		rabid 3416	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑧 ∈ (𝐴[,]𝐵) ∧ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))))
129	127, 128	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑧 ∈ (𝐴[,]𝐵) ∧ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))))
130	129	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))))
131	53, 98, 97	lesubaddd 11709	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴)))
132	130, 131	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴))
133	122	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ)
134	106	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞))
135	105	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
136	103	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*)
137	60	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ)
138		eqidd 2732	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) = (𝐷‘𝑗))
139		iftrue 4476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷‘𝑗) ≤ 𝑧 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = (𝐷‘𝑗))
140	139	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = (𝐷‘𝑗))
141	58	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ∈ ℝ)
142	59	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ∈ ℝ)
143	100	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑆 ∈ ℝ)
144		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ≤ 𝑧)
145	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑈 ⊆ ℝ)
146	46	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑈 ≠ ∅)
147	2, 3	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ))
148		iccsupr 13337	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝑈 ⊆ (𝐴[,]𝐵) ∧ 𝐴 ∈ 𝑈) → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥))
149	147, 7, 45, 148	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥))
150	149	simp3d 1144	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)
151	150	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥)
152	127, 125	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈)
153		suprub 12078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < ))
154	145, 146, 151, 152, 153	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < ))
155	154, 1	breqtrrdi 5128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ 𝑆)
156	155	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ 𝑆)
157	141, 142, 143, 144, 156	letrd 11265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ≤ 𝑆)
158	157	iftrued 4478	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
159	138, 140, 158	3eqtr4d 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
160	137, 159	eqled 11211	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
161	59	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ∈ ℝ)
162	58	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ∈ ℝ)
163		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → ¬ (𝐷‘𝑗) ≤ 𝑧)
164	161, 162	ltnled 11255	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝑧 < (𝐷‘𝑗) ↔ ¬ (𝐷‘𝑗) ≤ 𝑧))
165	163, 164	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 < (𝐷‘𝑗))
166	161, 162, 165	ltled 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ (𝐷‘𝑗))
167	166	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ (𝐷‘𝑗))
168		iffalse 4479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐷‘𝑗) ≤ 𝑧 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
169	168	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
170		iftrue 4476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
171	170	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
172	169, 171	breq12d 5099	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → (if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ↔ 𝑧 ≤ (𝐷‘𝑗)))
173	167, 172	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
174	155	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ 𝑆)
175	168	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
176		iffalse 4479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆)
177	176	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆)
178	175, 177	breq12d 5099	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → (if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ↔ 𝑧 ≤ 𝑆))
179	174, 178	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
180	173, 179	pm2.61dan 812	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
181	160, 180	pm2.61dan 812	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
182		icossico 13311	. . . . . . . . . . . . . . 15 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
183	78, 136, 81, 181, 182	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
184		volss 25456	. . . . . . . . . . . . . 14 ⊢ ((((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol ∧ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
185	63, 135, 183, 184	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ≤ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
186	54, 55, 64, 134, 185	sge0lempt 46448	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
187	97, 133, 98, 186	leadd1dd 11726	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
188	53, 99, 124, 132, 187	letrd 11265	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
189	188	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ 𝑈 → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
190	50, 189	ralrimi 3230	. . . . . . . 8 ⊢ (𝜑 → ∀𝑧 ∈ 𝑈 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
191		suprleub 12083	. . . . . . . . 9 ⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ) → (sup(𝑈, ℝ, < ) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ↔ ∀𝑧 ∈ 𝑈 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
192	52, 46, 150, 123, 191	syl31anc 1375	. . . . . . . 8 ⊢ (𝜑 → (sup(𝑈, ℝ, < ) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ↔ ∀𝑧 ∈ 𝑈 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
193	190, 192	mpbird 257	. . . . . . 7 ⊢ (𝜑 → sup(𝑈, ℝ, < ) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
194	49, 193	eqbrtrd 5108	. . . . . 6 ⊢ (𝜑 → 𝑆 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
195	100, 2, 122	lesubaddd 11709	. . . . . 6 ⊢ (𝜑 → ((𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ↔ 𝑆 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
196	194, 195	mpbird 257	. . . . 5 ⊢ (𝜑 → (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
197	48, 196	jca 511	. . . 4 ⊢ (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
198		oveq1 7348	. . . . . 6 ⊢ (𝑧 = 𝑆 → (𝑧 − 𝐴) = (𝑆 − 𝐴))
199		breq2 5090	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑆))
200		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → 𝑧 = 𝑆)
201	199, 200	ifbieq2d 4497	. . . . . . . . . 10 ⊢ (𝑧 = 𝑆 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
202	201	oveq2d 7357	. . . . . . . . 9 ⊢ (𝑧 = 𝑆 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
203	202	fveq2d 6821	. . . . . . . 8 ⊢ (𝑧 = 𝑆 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
204	203	mpteq2dv 5180	. . . . . . 7 ⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))
205	204	fveq2d 6821	. . . . . 6 ⊢ (𝑧 = 𝑆 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
206	198, 205	breq12d 5099	. . . . 5 ⊢ (𝑧 = 𝑆 → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
207	206	elrab 3642	. . . 4 ⊢ (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
208	197, 207	sylibr 234	. . 3 ⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
209	208, 4	eleqtrrdi 2842	. 2 ⊢ (𝜑 → 𝑆 ∈ 𝑈)
210	209, 45, 150	3jca 1128	1 ⊢ (𝜑 → (𝑆 ∈ 𝑈 ∧ 𝐴 ∈ 𝑈 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 {crab 3395 Vcvv 3436 ⊆ wss 3897 ∅c0 4278 ifcif 4470 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5611 ⟶wf 6472 ‘cfv 6476 (class class class)co 7341 supcsup 9319 ℝcr 11000 0cc0 11001 + caddc 11004 +∞cpnf 11138 ℝ^*cxr 11140 < clt 11141 ≤ cle 11142 − cmin 11339 ℕcn 12120 [,)cico 13242 [,]cicc 13243 volcvol 25386 Σ^{^}csumge0 46400

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-inf2 9526 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-pre-sup 11079

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-se 5565 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-isom 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-er 8617 df-map 8747 df-pm 8748 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-sup 9321 df-inf 9322 df-oi 9391 df-dju 9789 df-card 9827 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-div 11770 df-nn 12121 df-2 12183 df-3 12184 df-n0 12377 df-z 12464 df-uz 12728 df-q 12842 df-rp 12886 df-xadd 13007 df-ioo 13244 df-ico 13246 df-icc 13247 df-fz 13403 df-fzo 13550 df-fl 13691 df-seq 13904 df-exp 13964 df-hash 14233 df-cj 15001 df-re 15002 df-im 15003 df-sqrt 15137 df-abs 15138 df-clim 15390 df-rlim 15391 df-sum 15589 df-xmet 21279 df-met 21280 df-ovol 25387 df-vol 25388 df-sumge0 46401

This theorem is referenced by: hoidmv1lelem3 46631

W3C validator