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 46596

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 4046	. . . . . . . . 9 ⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ⊆ (𝐴[,]𝐵)
6	4, 5	eqsstri 3996	. . . . . . . 8 ⊢ 𝑈 ⊆ (𝐴[,]𝐵)
7	6	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))
8	2	rexrd 11231	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
9	3	rexrd 11231	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
10		hoidmv1lelem1.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 < 𝐵)
11	2, 3, 10	ltled 11329	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
12		lbicc2 13432	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
13	8, 9, 11, 12	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
14	2	recnd 11209	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	subidd 11528	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
16		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝜑
17		nnex 12199	. . . . . . . . . . . . . 14 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ ∈ V)
19		volf 25437	. . . . . . . . . . . . . . 15 ⊢ vol:dom vol⟶(0[,]+∞)
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
21		hoidmv1lelem1.c	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶:ℕ⟶ℝ)
22	21	ffvelcdmda 7059	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ)
23		hoidmv1lelem1.d	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:ℕ⟶ℝ)
24	23	ffvelcdmda 7059	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ)
25	2	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ ℝ)
26	24, 25	ifcld 4538	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ)
27	26	rexrd 11231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ^*)
28		icombl 25472	. . . . . . . . . . . . . . 15 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol)
29	22, 27, 28	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol)
30	20, 29	ffvelcdmd 7060	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))) ∈ (0[,]+∞))
31	16, 18, 30	sge0ge0mpt 46443	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
32	15, 31	eqbrtrd 5132	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
33	13, 32	jca 511	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
34		oveq1 7397	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (𝑧 − 𝐴) = (𝐴 − 𝐴))
35		breq2 5114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝐴 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝐴))
36		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝐴 → 𝑧 = 𝐴)
37	35, 36	ifbieq2d 4518	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝐴 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))
38	37	oveq2d 7406	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝐴 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))
39	38	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐴 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))
40	39	mpteq2dv 5204	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐴 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))
41	40	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
42	34, 41	breq12d 5123	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐴 → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
43	42	elrab 3662	. . . . . . . . . 10 ⊢ (𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
44	33, 43	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
45	44, 4	eleqtrrdi 2840	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
46	45	ne0d 4308	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≠ ∅)
47	2, 3, 7, 46	supicc 13469	. . . . . 6 ⊢ (𝜑 → sup(𝑈, ℝ, < ) ∈ (𝐴[,]𝐵))
48	1, 47	eqeltrid 2833	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (𝐴[,]𝐵))
49	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑆 = sup(𝑈, ℝ, < ))
50		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑧𝜑
51	2, 3	iccssred 13402	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
52	7, 51	sstrd 3960	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ⊆ ℝ)
53	52	sselda 3949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℝ)
54		nfv 1914	. . . . . . . . . . . . . . . 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 4538	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ)
61	60	rexrd 11231	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ^*)
62		icombl 25472	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol)
63	57, 61, 62	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol)
64	56, 63	ffvelcdmd 7060	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ∈ (0[,]+∞))
65	54, 55, 64	sge0xrclmpt 46433	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ^*)
66		pnfxr 11235	. . . . . . . . . . . . . . . 16 ⊢ +∞ ∈ ℝ^*
67	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → +∞ ∈ ℝ^*)
68		hoidmv1lelem1.r	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ)
69	68	rexrd 11231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ^*)
70	69	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ^*)
71	24	rexrd 11231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ^*)
72		icombl 25472	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ^*) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
73	22, 71, 72	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
74	20, 73	ffvelcdmd 7060	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞))
75	74	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞))
76	73	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
77	22	rexrd 11231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ^*)
78	77	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ^*)
79	71	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ^*)
80	22	leidd 11751	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗))
81	80	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗))
82		min1 13156	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑧 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))
83	58, 59, 82	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))
84		icossico 13384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ (𝐷‘𝑗) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
85	78, 79, 81, 83, 84	syl22anc 838	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
86		volss 25441	. . . . . . . . . . . . . . . . . 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 46415	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))))
89	68	ltpnfd 13088	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞)
90	89	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞)
91	65, 70, 67, 88, 90	xrlelttrd 13127	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) < +∞)
92	65, 67, 91	xrltned 45360	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≠ +∞)
93	92	neneqd 2931	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞)
94		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))
95	64, 94	fmptd 7089	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))):ℕ⟶(0[,]+∞))
96	55, 95	sge0repnf 46391	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞))
97	93, 96	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ)
98	2	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝐴 ∈ ℝ)
99	97, 98	readdcld 11210	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ∈ ℝ)
100	51, 48	sseldd 3950	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑆 ∈ ℝ)
101	100	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
102	24, 101	ifcld 4538	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ)
103	102	rexrd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*)
104		icombl 25472	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
105	22, 103, 104	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
106	20, 105	ffvelcdmd 7060	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞))
107	16, 18, 106	sge0xrclmpt 46433	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ^*)
108	66	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → +∞ ∈ ℝ^*)
109		min1 13156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))
110	24, 101, 109	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))
111		icossico 13384	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ (𝐷‘𝑗) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
112	77, 71, 80, 110, 111	syl22anc 838	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
113		volss 25441	. . . . . . . . . . . . . . . . . . 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 46415	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))))
116	107, 69, 108, 115, 89	xrlelttrd 13127	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) < +∞)
117	107, 108, 116	xrltned 45360	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≠ +∞)
118	117	neneqd 2931	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞)
119		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
120	106, 119	fmptd 7089	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
121	18, 120	sge0repnf 46391	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞))
122	118, 121	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ)
123	122, 2	readdcld 11210	. . . . . . . . . . . 12 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ)
124	123	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ)
125	4	eleq2i 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
126	125	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑈 → 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
127	126	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
128		rabid 3430	. . . . . . . . . . . . . 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 11782	. . . . . . . . . . . 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 2731	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) = (𝐷‘𝑗))
139		iftrue 4497	. . . . . . . . . . . . . . . . . . 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 13410	. . . . . . . . . . . . . . . . . . . . . . . . . 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 12151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < ))
154	145, 146, 151, 152, 153	syl31anc 1375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < ))
155	154, 1	breqtrrdi 5152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ 𝑆)
156	155	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ 𝑆)
157	141, 142, 143, 144, 156	letrd 11338	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ≤ 𝑆)
158	157	iftrued 4499	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
159	138, 140, 158	3eqtr4d 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
160	137, 159	eqled 11284	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
161	59	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ∈ ℝ)
162	58	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ∈ ℝ)
163		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → ¬ (𝐷‘𝑗) ≤ 𝑧)
164	161, 162	ltnled 11328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝑧 < (𝐷‘𝑗) ↔ ¬ (𝐷‘𝑗) ≤ 𝑧))
165	163, 164	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 < (𝐷‘𝑗))
166	161, 162, 165	ltled 11329	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ (𝐷‘𝑗))
167	166	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ (𝐷‘𝑗))
168		iffalse 4500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐷‘𝑗) ≤ 𝑧 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
169	168	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
170		iftrue 4497	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
171	170	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
172	169, 171	breq12d 5123	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → (if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ↔ 𝑧 ≤ (𝐷‘𝑗)))
173	167, 172	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
174	155	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ 𝑆)
175	168	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
176		iffalse 4500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆)
177	176	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆)
178	175, 177	breq12d 5123	. . . . . . . . . . . . . . . . . 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 13384	. . . . . . . . . . . . . . 15 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
183	78, 136, 81, 181, 182	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
184		volss 25441	. . . . . . . . . . . . . 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 46415	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
187	97, 133, 98, 186	leadd1dd 11799	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
188	53, 99, 124, 132, 187	letrd 11338	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
189	188	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ 𝑈 → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
190	50, 189	ralrimi 3236	. . . . . . . 8 ⊢ (𝜑 → ∀𝑧 ∈ 𝑈 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
191		suprleub 12156	. . . . . . . . 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 5132	. . . . . 6 ⊢ (𝜑 → 𝑆 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
195	100, 2, 122	lesubaddd 11782	. . . . . 6 ⊢ (𝜑 → ((𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ↔ 𝑆 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
196	194, 195	mpbird 257	. . . . 5 ⊢ (𝜑 → (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
197	48, 196	jca 511	. . . 4 ⊢ (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
198		oveq1 7397	. . . . . 6 ⊢ (𝑧 = 𝑆 → (𝑧 − 𝐴) = (𝑆 − 𝐴))
199		breq2 5114	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑆))
200		id 22	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → 𝑧 = 𝑆)
201	199, 200	ifbieq2d 4518	. . . . . . . . . 10 ⊢ (𝑧 = 𝑆 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
202	201	oveq2d 7406	. . . . . . . . 9 ⊢ (𝑧 = 𝑆 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
203	202	fveq2d 6865	. . . . . . . 8 ⊢ (𝑧 = 𝑆 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
204	203	mpteq2dv 5204	. . . . . . 7 ⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))
205	204	fveq2d 6865	. . . . . 6 ⊢ (𝑧 = 𝑆 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
206	198, 205	breq12d 5123	. . . . 5 ⊢ (𝑧 = 𝑆 → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
207	206	elrab 3662	. . . 4 ⊢ (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
208	197, 207	sylibr 234	. . 3 ⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
209	208, 4	eleqtrrdi 2840	. 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 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {crab 3408 Vcvv 3450 ⊆ wss 3917 ∅c0 4299 ifcif 4491 class class class wbr 5110 ↦ cmpt 5191 dom cdm 5641 ⟶wf 6510 ‘cfv 6514 (class class class)co 7390 supcsup 9398 ℝcr 11074 0cc0 11075 + caddc 11078 +∞cpnf 11212 ℝ^*cxr 11214 < clt 11215 ≤ cle 11216 − cmin 11412 ℕcn 12193 [,)cico 13315 [,]cicc 13316 volcvol 25371 Σ^{^}csumge0 46367

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8674 df-map 8804 df-pm 8805 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9861 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-n0 12450 df-z 12537 df-uz 12801 df-q 12915 df-rp 12959 df-xadd 13080 df-ioo 13317 df-ico 13319 df-icc 13320 df-fz 13476 df-fzo 13623 df-fl 13761 df-seq 13974 df-exp 14034 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-rlim 15462 df-sum 15660 df-xmet 21264 df-met 21265 df-ovol 25372 df-vol 25373 df-sumge0 46368

This theorem is referenced by: hoidmv1lelem3 46598

W3C validator