hoidmvlelem5 - Mathbox for Glauco Siliprandi

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

Theorem hoidmvlelem5 44027

Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)

**Hypotheses**
Ref	Expression
hoidmvlelem5.l	⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
hoidmvlelem5.f	⊢ (𝜑 → 𝑋 ∈ Fin)
hoidmvlelem5.y	⊢ (𝜑 → 𝑌 ⊆ 𝑋)
hoidmvlelem5.z	⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌))
hoidmvlelem5.w	⊢ 𝑊 = (𝑌 ∪ {𝑍})
hoidmvlelem5.a	⊢ (𝜑 → 𝐴:𝑊⟶ℝ)
hoidmvlelem5.b	⊢ (𝜑 → 𝐵:𝑊⟶ℝ)
hoidmvlelem5.c	⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
hoidmvlelem5.d	⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
hoidmvlelem5.i	⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑_m 𝑌)∀𝑓 ∈ (ℝ ↑_m 𝑌)∀𝑔 ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)∀ℎ ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗))))))
hoidmvlelem5.s	⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
hoidmvlelem5.n	⊢ (𝜑 → 𝑌 ≠ ∅)

**Assertion**
Ref	Expression
hoidmvlelem5	⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))

Distinct variable groups: 𝐴,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 𝐴,𝑒,𝑓,𝑔,ℎ,𝑗,𝑘 𝐵,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 𝐵,𝑓,𝑔 𝐶,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 𝐶,𝑔 𝐷,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 𝐷,𝑔 𝐿,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 𝑒,𝐿,𝑓,𝑔 𝑊,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 𝑔,𝑊 𝑌,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 𝑒,𝑌,𝑓,𝑔 𝑍,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 𝑔,𝑍 𝜑,𝑎,𝑏,ℎ,𝑗,𝑘,𝑥 Allowed substitution hints: 𝜑(𝑒,𝑓,𝑔) 𝐵(𝑒) 𝐶(𝑒,𝑓) 𝐷(𝑒,𝑓) 𝑊(𝑒,𝑓) 𝑋(𝑥,𝑒,𝑓,𝑔,ℎ,𝑗,𝑘,𝑎,𝑏) 𝑍(𝑒,𝑓)

Proof of Theorem hoidmvlelem5 Dummy variables 𝑟 𝑠 𝑐 𝑤 𝑧 𝑖 𝑙 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1918	. . . . 5 ⊢ Ⅎ𝑠𝜑
2		nfre1 3234	. . . . 5 ⊢ Ⅎ𝑠∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)
3	1, 2	nfan 1903	. . . 4 ⊢ Ⅎ𝑠(𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
4		hoidmvlelem5.l	. . . 4 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
5		hoidmvlelem5.w	. . . . . 6 ⊢ 𝑊 = (𝑌 ∪ {𝑍})
6		hoidmvlelem5.f	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ Fin)
7		hoidmvlelem5.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
8		ssfi 8918	. . . . . . . 8 ⊢ ((𝑋 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ Fin)
9	6, 7, 8	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Fin)
10		snfi 8788	. . . . . . . 8 ⊢ {𝑍} ∈ Fin
11	10	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑍} ∈ Fin)
12		unfi 8917	. . . . . . 7 ⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
13	9, 11, 12	syl2anc 583	. . . . . 6 ⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
14	5, 13	eqeltrid 2843	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Fin)
15	14	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝑊 ∈ Fin)
16		hoidmvlelem5.a	. . . . 5 ⊢ (𝜑 → 𝐴:𝑊⟶ℝ)
17	16	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝐴:𝑊⟶ℝ)
18		hoidmvlelem5.b	. . . . 5 ⊢ (𝜑 → 𝐵:𝑊⟶ℝ)
19	18	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝐵:𝑊⟶ℝ)
20		simpr 484	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
21	3, 4, 15, 17, 19, 20	hoidmvval0 44015	. . 3 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) = 0)
22		nnex 11909	. . . . . 6 ⊢ ℕ ∈ V
23	22	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ ∈ V)
24		icossicc 13097	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
25	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
26		hoidmvlelem5.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
27	26	ffvelrnda 6943	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_m 𝑊))
28		elmapi 8595	. . . . . . . . 9 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_m 𝑊) → (𝐶‘𝑗):𝑊⟶ℝ)
29	27, 28	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ)
30		hoidmvlelem5.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
31	30	ffvelrnda 6943	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_m 𝑊))
32		elmapi 8595	. . . . . . . . 9 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_m 𝑊) → (𝐷‘𝑗):𝑊⟶ℝ)
33	31, 32	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ)
34	4, 25, 29, 33	hoidmvcl 44010	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,)+∞))
35	24, 34	sselid 3915	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,]+∞))
36	35	fmpttd 6971	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
37	23, 36	sge0ge0 43812	. . . 4 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
38	37	adantr 480	. . 3 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
39	21, 38	eqbrtrd 5092	. 2 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
40		icossxr 13093	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ^*
41	4, 14, 16, 18	hoidmvcl 44010	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ (0[,)+∞))
42	40, 41	sselid 3915	. . . . . 6 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
43	42	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
44	23, 36	sge0xrcl 43813	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
45	44	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
46		rge0ssre 13117	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ
47	46, 41	sselid 3915	. . . . . . . 8 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ)
48		ltpnf 12785	. . . . . . . 8 ⊢ ((𝐴(𝐿‘𝑊)𝐵) ∈ ℝ → (𝐴(𝐿‘𝑊)𝐵) < +∞)
49	47, 48	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) < +∞)
50	49	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < +∞)
51		id 22	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞)
52	51	eqcomd 2744	. . . . . . 7 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
53	52	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
54	50, 53	breqtrd 5096	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
55	43, 45, 54	xrltled 12813	. . . 4 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
56	55	adantlr 711	. . 3 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
57		simpll 763	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → 𝜑)
58		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
59	16	ffvelrnda 6943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐴‘𝑠) ∈ ℝ)
60	18	ffvelrnda 6943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐵‘𝑠) ∈ ℝ)
61	59, 60	ltnled 11052	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
62	61	ralbidva 3119	. . . . . . . 8 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
63		ralnex 3163	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
65	62, 64	bitrd 278	. . . . . . 7 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
66	65	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
67	58, 66	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠))
68	67	adantr 480	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠))
69		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞)
70	22	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ℕ ∈ V)
71	36	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
72	70, 71	sge0repnf 43814	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞))
73	69, 72	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
74	73	adantlr 711	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
75		simpll 763	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)))
76		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
77		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
78	76, 77	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) = ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))
79	78	cbvmptv 5183	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) = (𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))
80	79	fveq2i 6759	. . . . . . . . . 10 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖))))
81	80	eleq1i 2829	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
82	81	biimpi 215	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ → (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
83	82	ad2antlr 723	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
84		simpr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
85	6	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑋 ∈ Fin)
86	7	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑌 ⊆ 𝑋)
87		hoidmvlelem5.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ≠ ∅)
88	87	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑌 ≠ ∅)
89		hoidmvlelem5.z	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌))
90	89	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑍 ∈ (𝑋 ∖ 𝑌))
91	16	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐴:𝑊⟶ℝ)
92	18	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐵:𝑊⟶ℝ)
93		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑘 → (𝐴‘𝑠) = (𝐴‘𝑘))
94		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑘 → (𝐵‘𝑠) = (𝐵‘𝑘))
95	93, 94	breq12d 5083	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑘 → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ (𝐴‘𝑘) < (𝐵‘𝑘)))
96	95	cbvralvw 3372	. . . . . . . . . . . 12 ⊢ (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
97	96	biimpi 215	. . . . . . . . . . 11 ⊢ (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
98	97	adantr 480	. . . . . . . . . 10 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
99		simpr 484	. . . . . . . . . 10 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑊)
100		rspa 3130	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
101	98, 99, 100	syl2anc 583	. . . . . . . . 9 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
102	101	ad5ant25 758	. . . . . . . 8 ⊢ (((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
103	26	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
104	30	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
105	81	biimpri 227	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
106	105	ad2antlr 723	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
107		fveq1 6755	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑐 → (𝑑‘𝑖) = (𝑐‘𝑖))
108	107	breq1d 5080	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑐 → ((𝑑‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑖) ≤ 𝑥))
109	108, 107	ifbieq1d 4480	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑐 → if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥) = if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))
110	107, 109	ifeq12d 4477	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑐 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)) = if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)))
111	110	mpteq2dv 5172	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))))
112		eleq1w 2821	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ 𝑌 ↔ 𝑗 ∈ 𝑌))
113		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑐‘𝑖) = (𝑐‘𝑗))
114	113	breq1d 5080	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑐‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑗) ≤ 𝑥))
115	114, 113	ifbieq1d 4480	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥) = if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))
116	112, 113, 115	ifbieq12d 4484	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)) = if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))
117	116	cbvmptv 5183	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
119	111, 118	eqtrd 2778	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
120	119	cbvmptv 5183	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))) = (𝑐 ∈ (ℝ ↑_m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
121	120	mpteq2i 5175	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))))
122		eqid 2738	. . . . . . . 8 ⊢ ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌))
123		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
124		oveq1 7262	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍)))
125	124	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) = (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))))
126		breq2 5074	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑑‘𝑖) ≤ 𝑤 ↔ (𝑑‘𝑖) ≤ 𝑥))
127		eqidd 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → (𝑑‘𝑖) = (𝑑‘𝑖))
128		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → 𝑤 = 𝑥)
129	126, 127, 128	ifbieq12d 4484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑥 → if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤) = if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))
130	129	ifeq2d 4476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑥 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)) = if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))
131	130	mpteq2dv 5172	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))
132	131	mpteq2dv 5172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑥 → (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))) = (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))
133	132	cbvmptv 5183	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))))) = (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))
134	133	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → (𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))))) = (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))))
135		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
136	134, 135	fveq12d 6763	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤) = ((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧))
137	136	fveq1d 6758	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → (((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))
138	137	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))) = ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))))
139	138	mpteq2dv 5172	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))))
140		fveq2 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑗 → (𝐶‘𝑙) = (𝐶‘𝑗))
141		2fveq3 6761	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑗 → (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))
142	140, 141	oveq12d 7273	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑗 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))) = ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))
143	142	cbvmptv 5183	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))
144	143	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))
145	139, 144	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))
146	145	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))
147	146	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) = ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))))
148	125, 147	breq12d 5083	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → ((((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) ↔ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))))
149	148	cbvrabv 3416	. . . . . . . 8 ⊢ {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))}
150		eqid 2738	. . . . . . . 8 ⊢ sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))}, ℝ, < )
151		hoidmvlelem5.i	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑_m 𝑌)∀𝑓 ∈ (ℝ ↑_m 𝑌)∀𝑔 ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)∀ℎ ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗))))))
152	151	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑒 ∈ (ℝ ↑_m 𝑌)∀𝑓 ∈ (ℝ ↑_m 𝑌)∀𝑔 ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)∀ℎ ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗))))))
153		hoidmvlelem5.s	. . . . . . . . 9 ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
154	153	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
155	4, 85, 86, 88, 90, 5, 91, 92, 102, 103, 104, 106, 121, 122, 123, 149, 150, 152, 154	hoidmvlelem4 44026	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
156	75, 83, 84, 155	syl21anc 834	. . . . . 6 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
157	156	ralrimiva 3107	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ∀𝑟 ∈ ℝ⁺ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
158		nfv 1918	. . . . . 6 ⊢ Ⅎ𝑟((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
159	42	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
160		0xr 10953	. . . . . . . 8 ⊢ 0 ∈ ℝ^*
161	160	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ∈ ℝ^*)
162		pnfxr 10960	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
163	162	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → +∞ ∈ ℝ^*)
164	44	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
165	37	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
166		ltpnf 12785	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞)
167	166	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞)
168	161, 163, 164, 165, 167	elicod 13058	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ (0[,)+∞))
169	158, 159, 168	xralrple2 42783	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ((𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ↔ ∀𝑟 ∈ ℝ⁺ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))))
170	157, 169	mpbird 256	. . . 4 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
171	57, 68, 74, 170	syl21anc 834	. . 3 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
172	56, 171	pm2.61dan 809	. 2 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
173	39, 172	pm2.61dan 809	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 {crab 3067 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ⊆ wss 3883 ∅c0 4253 ifcif 4456 {csn 4558 ∪ ciun 4921 class class class wbr 5070 ↦ cmpt 5153 ↾ cres 5582 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ∈ cmpo 7257 ↑_m cmap 8573 Xcixp 8643 Fincfn 8691 supcsup 9129 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 +∞cpnf 10937 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 ℕcn 11903 ℝ⁺crp 12659 [,)cico 13010 [,]cicc 13011 ∏cprod 15543 volcvol 24532 Σ^{^}csumge0 43790

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

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

This theorem is referenced by: hoidmvle 44028

W3C validator