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 47570

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 4028	. . . . . . . . 9 ⊢ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ⊆ (𝐴[,]𝐵)
6	4, 5	eqsstri 3977	. . . . . . . 8 ⊢ 𝑈 ⊆ (𝐴[,]𝐵)
7	6	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (𝐴[,]𝐵))
8	2	rexrd 11352	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
9	3	rexrd 11352	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
10		hoidmv1lelem1.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 < 𝐵)
11	2, 3, 10	ltled 11451	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
12		lbicc2 13588	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
13	8, 9, 11, 12	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
14	2	recnd 11330	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ ℂ)
15	14	subidd 11650	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 − 𝐴) = 0)
16		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗𝜑
17		nnex 12334	. . . . . . . . . . . . . 14 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ ∈ V)
19		volf 25843	. . . . . . . . . . . . . . 15 ⊢ vol:dom vol⟶(0[,]+∞)
20	19	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → vol:dom vol⟶(0[,]+∞))
21		hoidmv1lelem1.c	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶:ℕ⟶ℝ)
22	21	ffvelcdmda 7082	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ)
23		hoidmv1lelem1.d	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷:ℕ⟶ℝ)
24	23	ffvelcdmda 7082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ)
25	2	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝐴 ∈ ℝ)
26	24, 25	ifcld 4529	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ)
27	26	rexrd 11352	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ^*)
28		icombl 25878	. . . . . . . . . . . . . . 15 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol)
29	22, 27, 28	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)) ∈ dom vol)
30	20, 29	ffvelcdmd 7083	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))) ∈ (0[,]+∞))
31	16, 18, 30	sge0ge0mpt 47417	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
32	15, 31	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
33	13, 32	jca 521	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
34		oveq1 7425	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (𝑧 − 𝐴) = (𝐴 − 𝐴))
35		breq2 5107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝐴 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝐴))
36		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝐴 → 𝑧 = 𝐴)
37	35, 36	ifbieq2d 4509	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝐴 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))
38	37	oveq2d 7434	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝐴 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))
39	38	fveq2d 6887	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐴 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))
40	39	mpteq2dv 5199	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐴 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))
41	40	fveq2d 6887	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴))))))
42	34, 41	breq12d 5116	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐴 → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
43	42	elrab 3645	. . . . . . . . . 10 ⊢ (𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐴 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝐴, (𝐷‘𝑗), 𝐴)))))))
44	33, 43	sylibr 237	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
45	44, 4	eleqtrrdi 2872	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
46	45	ne0d 4288	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≠ ∅)
47	2, 3, 7, 46	supicc 13625	. . . . . 6 ⊢ (𝜑 → sup(𝑈, ℝ, < ) ∈ (𝐴[,]𝐵))
48	1, 47	eqeltrid 2865	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ (𝐴[,]𝐵))
49	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝑆 = sup(𝑈, ℝ, < ))
50		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑧𝜑
51	2, 3	iccssred 13558	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
52	7, 51	sstrd 3941	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ⊆ ℝ)
53	52	sselda 3931	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ ℝ)
54		nfv 1947	. . . . . . . . . . . . . . . 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 4529	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ)
61	60	rexrd 11352	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ^*)
62		icombl 25878	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol)
63	57, 61, 62	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ∈ dom vol)
64	56, 63	ffvelcdmd 7083	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) ∈ (0[,]+∞))
65	54, 55, 64	sge0xrclmpt 47407	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ^*)
66		pnfxr 11356	. . . . . . . . . . . . . . . 16 ⊢ +∞ ∈ ℝ^*
67	66	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → +∞ ∈ ℝ^*)
68		hoidmv1lelem1.r	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ)
69	68	rexrd 11352	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ^*)
70	69	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) ∈ ℝ^*)
71	24	rexrd 11352	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ^*)
72		icombl 25878	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ (𝐷‘𝑗) ∈ ℝ^*) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
73	22, 71, 72	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
74	20, 73	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞))
75	74	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∈ (0[,]+∞))
76	73	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)(𝐷‘𝑗)) ∈ dom vol)
77	22	rexrd 11352	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ^*)
78	77	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ ℝ^*)
79	71	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ ℝ^*)
80	22	leidd 11875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗))
81	80	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ≤ (𝐶‘𝑗))
82		min1 13312	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑧 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))
83	58, 59, 82	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))
84		icossico 13540	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ (𝐷‘𝑗) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
85	78, 79, 81, 83, 84	syl22anc 852	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
86		volss 25847	. . . . . . . . . . . . . . . . . 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 47389	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))))
89	68	ltpnfd 13243	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞)
90	89	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))) < +∞)
91	65, 70, 67, 88, 90	xrlelttrd 13282	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) < +∞)
92	65, 67, 91	xrltned 46338	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≠ +∞)
93	92	neneqd 2961	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞)
94		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))
95	64, 94	fmptd 7112	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))):ℕ⟶(0[,]+∞))
96	55, 95	sge0repnf 47365	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = +∞))
97	93, 96	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ∈ ℝ)
98	2	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝐴 ∈ ℝ)
99	97, 98	readdcld 11331	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ∈ ℝ)
100	51, 48	sseldd 3932	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑆 ∈ ℝ)
101	100	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ)
102	24, 101	ifcld 4529	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ)
103	102	rexrd 11352	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*)
104		icombl 25878	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶‘𝑗) ∈ ℝ ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
105	22, 103, 104	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ∈ dom vol)
106	20, 105	ffvelcdmd 7083	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) ∈ (0[,]+∞))
107	16, 18, 106	sge0xrclmpt 47407	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ^*)
108	66	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → +∞ ∈ ℝ^*)
109		min1 13312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐷‘𝑗) ∈ ℝ ∧ 𝑆 ∈ ℝ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))
110	24, 101, 109	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))
111		icossico 13540	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ (𝐷‘𝑗) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ≤ (𝐷‘𝑗))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
112	77, 71, 80, 110, 111	syl22anc 852	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)) ⊆ ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
113		volss 25847	. . . . . . . . . . . . . . . . . . 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 47389	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)(𝐷‘𝑗))))))
116	107, 69, 108, 115, 89	xrlelttrd 13282	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) < +∞)
117	107, 108, 116	xrltned 46338	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ≠ +∞)
118	117	neneqd 2961	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞)
119		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
120	106, 119	fmptd 7112	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))):ℕ⟶(0[,]+∞))
121	18, 120	sge0repnf 47365	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) = +∞))
122	118, 121	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ∈ ℝ)
123	122, 2	readdcld 11331	. . . . . . . . . . . 12 ⊢ (𝜑 → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ)
124	123	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴) ∈ ℝ)
125	4	eleq2i 2853	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝑈 ↔ 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
126	125	bilani 510	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
127		rabid 3433	. . . . . . . . . . . . . 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 11906	. . . . . . . . . . . 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 2762	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) = (𝐷‘𝑗))
138		iftrue 4488	. . . . . . . . . . . . . . . . . . 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 13566	. . . . . . . . . . . . . . . . . . . . . . . . . 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 12271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑈 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < ))
153	144, 145, 150, 151, 152	syl31anc 1400	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ sup(𝑈, ℝ, < ))
154	153, 1	breqtrrdi 5147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ 𝑆)
155	154	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ 𝑆)
156	140, 141, 142, 143, 155	letrd 11460	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ≤ 𝑆)
157	156	iftrued 4490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
158	137, 139, 157	3eqtr4d 2806	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
159	136, 158	eqled 11406	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ (𝐷‘𝑗) ≤ 𝑧) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
160	59	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ∈ ℝ)
161	58	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝐷‘𝑗) ∈ ℝ)
162		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → ¬ (𝐷‘𝑗) ≤ 𝑧)
163	160, 161	ltnled 11450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → (𝑧 < (𝐷‘𝑗) ↔ ¬ (𝐷‘𝑗) ≤ 𝑧))
164	162, 163	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 < (𝐷‘𝑗))
165	160, 161, 164	ltled 11451	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) → 𝑧 ≤ (𝐷‘𝑗))
166	165	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ (𝐷‘𝑗))
167		iffalse 4491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐷‘𝑗) ≤ 𝑧 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
168	167	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
169		iftrue 4488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
170	169	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = (𝐷‘𝑗))
171	168, 170	breq12d 5116	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → (if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ↔ 𝑧 ≤ (𝐷‘𝑗)))
172	166, 171	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
173	154	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → 𝑧 ≤ 𝑆)
174	167	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = 𝑧)
175		iffalse 4491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝐷‘𝑗) ≤ 𝑆 → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆)
176	175	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) ∧ ¬ (𝐷‘𝑗) ≤ 𝑧) ∧ ¬ (𝐷‘𝑗) ≤ 𝑆) → if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) = 𝑆)
177	174, 176	breq12d 5116	. . . . . . . . . . . . . . . . . 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 13540	. . . . . . . . . . . . . . 15 ⊢ ((((𝐶‘𝑗) ∈ ℝ^* ∧ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆) ∈ ℝ^*) ∧ ((𝐶‘𝑗) ≤ (𝐶‘𝑗) ∧ if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) ≤ if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
182	78, 135, 81, 180, 181	syl22anc 852	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑈) ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) ⊆ ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
183		volss 25847	. . . . . . . . . . . . . 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 47389	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
186	97, 132, 98, 185	leadd1dd 11923	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) + 𝐴) ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
187	53, 99, 124, 131, 186	letrd 11460	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑈) → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
188	187	ex 418	. . . . . . . . 9 ⊢ (𝜑 → (𝑧 ∈ 𝑈 → 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
189	50, 188	ralrimi 3261	. . . . . . . 8 ⊢ (𝜑 → ∀𝑧 ∈ 𝑈 𝑧 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
190		suprleub 12276	. . . . . . . . 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 5127	. . . . . 6 ⊢ (𝜑 → 𝑆 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴))
194	100, 2, 122	lesubaddd 11906	. . . . . 6 ⊢ (𝜑 → ((𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) ↔ 𝑆 ≤ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))) + 𝐴)))
195	193, 194	mpbird 260	. . . . 5 ⊢ (𝜑 → (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
196	48, 195	jca 521	. . . 4 ⊢ (𝜑 → (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
197		oveq1 7425	. . . . . 6 ⊢ (𝑧 = 𝑆 → (𝑧 − 𝐴) = (𝑆 − 𝐴))
198		breq2 5107	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → ((𝐷‘𝑗) ≤ 𝑧 ↔ (𝐷‘𝑗) ≤ 𝑆))
199		id 23	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑆 → 𝑧 = 𝑆)
200	198, 199	ifbieq2d 4509	. . . . . . . . . 10 ⊢ (𝑧 = 𝑆 → if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧) = if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))
201	200	oveq2d 7434	. . . . . . . . 9 ⊢ (𝑧 = 𝑆 → ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)) = ((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))
202	201	fveq2d 6887	. . . . . . . 8 ⊢ (𝑧 = 𝑆 → (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))) = (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))
203	202	mpteq2dv 5199	. . . . . . 7 ⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))) = (𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))
204	203	fveq2d 6887	. . . . . 6 ⊢ (𝑧 = 𝑆 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆))))))
205	197, 204	breq12d 5116	. . . . 5 ⊢ (𝑧 = 𝑆 → ((𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧))))) ↔ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
206	205	elrab 3645	. . . 4 ⊢ (𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))} ↔ (𝑆 ∈ (𝐴[,]𝐵) ∧ (𝑆 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑆, (𝐷‘𝑗), 𝑆)))))))
207	196, 206	sylibr 237	. . 3 ⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ (𝐴[,]𝐵) ∣ (𝑧 − 𝐴) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ (vol‘((𝐶‘𝑗)[,)if((𝐷‘𝑗) ≤ 𝑧, (𝐷‘𝑗), 𝑧)))))})
208	207, 4	eleqtrrdi 2872	. 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 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 Vcvv 3451 ⊆ wss 3899 ∅c0 4279 ifcif 4482 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 supcsup 9425 ℝcr 11192 0cc0 11193 + caddc 11196 +∞cpnf 11333 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 − cmin 11534 ℕcn 12328 [,)cico 13471 [,]cicc 13472 volcvol 25777 Σ^{^}csumge0 47341

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-sup 9427 df-inf 9428 df-oi 9497 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-z 12687 df-uz 12959 df-q 13069 df-rp 13114 df-xadd 13235 df-ioo 13473 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-clim 15648 df-rlim 15649 df-sum 15847 df-xmet 21664 df-met 21665 df-ovol 25778 df-vol 25779 df-sumge0 47342

This theorem is used by: hoidmv1lelem3 47572

W3C validator