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 46595

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 1914	. . . . 5 ⊢ Ⅎ𝑠𝜑
2		nfre1 3271	. . . . 5 ⊢ Ⅎ𝑠∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)
3	1, 2	nfan 1899	. . . 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 9192	. . . . . . . 8 ⊢ ((𝑋 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ Fin)
9	6, 7, 8	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Fin)
10		snfi 9062	. . . . . . . 8 ⊢ {𝑍} ∈ Fin
11	10	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑍} ∈ Fin)
12		unfi 9190	. . . . . . 7 ⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
13	9, 11, 12	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
14	5, 13	eqeltrid 2839	. . . . 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 46583	. . 3 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) = 0)
22		nnex 12251	. . . . . 6 ⊢ ℕ ∈ V
23	22	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ ∈ V)
24		icossicc 13458	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
25	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
26		hoidmvlelem5.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
27	26	ffvelcdmda 7079	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_m 𝑊))
28		elmapi 8868	. . . . . . . . 9 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_m 𝑊) → (𝐶‘𝑗):𝑊⟶ℝ)
29	27, 28	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ)
30		hoidmvlelem5.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
31	30	ffvelcdmda 7079	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_m 𝑊))
32		elmapi 8868	. . . . . . . . 9 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_m 𝑊) → (𝐷‘𝑗):𝑊⟶ℝ)
33	31, 32	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ)
34	4, 25, 29, 33	hoidmvcl 46578	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,)+∞))
35	24, 34	sselid 3961	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,]+∞))
36	35	fmpttd 7110	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
37	23, 36	sge0ge0 46380	. . . 4 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
38	37	adantr 480	. . 3 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
39	21, 38	eqbrtrd 5146	. 2 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
40		icossxr 13454	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ^*
41	4, 14, 16, 18	hoidmvcl 46578	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ (0[,)+∞))
42	40, 41	sselid 3961	. . . . . 6 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
43	42	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
44	23, 36	sge0xrcl 46381	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
45	44	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
46		rge0ssre 13478	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ
47	46, 41	sselid 3961	. . . . . . . 8 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ)
48		ltpnf 13141	. . . . . . . 8 ⊢ ((𝐴(𝐿‘𝑊)𝐵) ∈ ℝ → (𝐴(𝐿‘𝑊)𝐵) < +∞)
49	47, 48	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) < +∞)
50	49	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < +∞)
51		id 22	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞)
52	51	eqcomd 2742	. . . . . . 7 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
53	52	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
54	50, 53	breqtrd 5150	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
55	43, 45, 54	xrltled 13171	. . . 4 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
56	55	adantlr 715	. . 3 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
57		simpll 766	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → 𝜑)
58		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
59	16	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐴‘𝑠) ∈ ℝ)
60	18	ffvelcdmda 7079	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐵‘𝑠) ∈ ℝ)
61	59, 60	ltnled 11387	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
62	61	ralbidva 3162	. . . . . . . 8 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
63		ralnex 3063	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
65	62, 64	bitrd 279	. . . . . . 7 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
66	65	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
67	58, 66	mpbird 257	. . . . 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 46382	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞))
73	69, 72	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
74	73	adantlr 715	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
75		simpll 766	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)))
76		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
77		fveq2 6881	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
78	76, 77	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) = ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))
79	78	cbvmptv 5230	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) = (𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))
80	79	fveq2i 6884	. . . . . . . . . 10 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖))))
81	80	eleq1i 2826	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
82	81	biimpi 216	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ → (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
83	82	ad2antlr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
84		simpr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
85	6	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑋 ∈ Fin)
86	7	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑌 ⊆ 𝑋)
87		hoidmvlelem5.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ≠ ∅)
88	87	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑌 ≠ ∅)
89		hoidmvlelem5.z	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌))
90	89	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑍 ∈ (𝑋 ∖ 𝑌))
91	16	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐴:𝑊⟶ℝ)
92	18	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐵:𝑊⟶ℝ)
93		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑘 → (𝐴‘𝑠) = (𝐴‘𝑘))
94		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑘 → (𝐵‘𝑠) = (𝐵‘𝑘))
95	93, 94	breq12d 5137	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑘 → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ (𝐴‘𝑘) < (𝐵‘𝑘)))
96	95	cbvralvw 3224	. . . . . . . . . . . 12 ⊢ (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
97	96	biimpi 216	. . . . . . . . . . 11 ⊢ (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
98	97	adantr 480	. . . . . . . . . 10 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
99		simpr 484	. . . . . . . . . 10 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑊)
100		rspa 3235	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
101	98, 99, 100	syl2anc 584	. . . . . . . . 9 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
102	101	ad5ant25 761	. . . . . . . 8 ⊢ (((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
103	26	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
104	30	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
105	81	biimpri 228	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
106	105	ad2antlr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
107		fveq1 6880	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑐 → (𝑑‘𝑖) = (𝑐‘𝑖))
108	107	breq1d 5134	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑐 → ((𝑑‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑖) ≤ 𝑥))
109	108, 107	ifbieq1d 4530	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑐 → if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥) = if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))
110	107, 109	ifeq12d 4527	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑐 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)) = if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)))
111	110	mpteq2dv 5220	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))))
112		eleq1w 2818	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ 𝑌 ↔ 𝑗 ∈ 𝑌))
113		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑐‘𝑖) = (𝑐‘𝑗))
114	113	breq1d 5134	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑐‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑗) ≤ 𝑥))
115	114, 113	ifbieq1d 4530	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥) = if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))
116	112, 113, 115	ifbieq12d 4534	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)) = if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))
117	116	cbvmptv 5230	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
119	111, 118	eqtrd 2771	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
120	119	cbvmptv 5230	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))) = (𝑐 ∈ (ℝ ↑_m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
121	120	mpteq2i 5222	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))))
122		eqid 2736	. . . . . . . 8 ⊢ ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌))
123		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
124		oveq1 7417	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍)))
125	124	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) = (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))))
126		breq2 5128	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑑‘𝑖) ≤ 𝑤 ↔ (𝑑‘𝑖) ≤ 𝑥))
127		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → (𝑑‘𝑖) = (𝑑‘𝑖))
128		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → 𝑤 = 𝑥)
129	126, 127, 128	ifbieq12d 4534	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑥 → if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤) = if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))
130	129	ifeq2d 4526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑥 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)) = if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))
131	130	mpteq2dv 5220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))
132	131	mpteq2dv 5220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑥 → (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))) = (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))
133	132	cbvmptv 5230	. . . . . . . . . . . . . . . . . 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 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤) = ((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧))
137	136	fveq1d 6883	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → (((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))
138	137	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))) = ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))))
139	138	mpteq2dv 5220	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))))
140		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑗 → (𝐶‘𝑙) = (𝐶‘𝑗))
141		2fveq3 6886	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑗 → (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))
142	140, 141	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑗 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))) = ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))
143	142	cbvmptv 5230	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))
144	143	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))
145	139, 144	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))
146	145	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))
147	146	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) = ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))))
148	125, 147	breq12d 5137	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → ((((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) ↔ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))))
149	148	cbvrabv 3431	. . . . . . . 8 ⊢ {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))}
150		eqid 2736	. . . . . . . 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 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑒 ∈ (ℝ ↑_m 𝑌)∀𝑓 ∈ (ℝ ↑_m 𝑌)∀𝑔 ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)∀ℎ ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗))))))
153		hoidmvlelem5.s	. . . . . . . . 9 ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
154	153	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
155	4, 85, 86, 88, 90, 5, 91, 92, 102, 103, 104, 106, 121, 122, 123, 149, 150, 152, 154	hoidmvlelem4 46594	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
156	75, 83, 84, 155	syl21anc 837	. . . . . 6 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
157	156	ralrimiva 3133	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ∀𝑟 ∈ ℝ⁺ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
158		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑟((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
159	42	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
160		0xr 11287	. . . . . . . 8 ⊢ 0 ∈ ℝ^*
161	160	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ∈ ℝ^*)
162		pnfxr 11294	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
163	162	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → +∞ ∈ ℝ^*)
164	44	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
165	37	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
166		ltpnf 13141	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞)
167	166	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞)
168	161, 163, 164, 165, 167	elicod 13417	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ (0[,)+∞))
169	158, 159, 168	xralrple2 45348	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ((𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ↔ ∀𝑟 ∈ ℝ⁺ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))))
170	157, 169	mpbird 257	. . . 4 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
171	57, 68, 74, 170	syl21anc 837	. . 3 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
172	56, 171	pm2.61dan 812	. 2 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
173	39, 172	pm2.61dan 812	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 {crab 3420 Vcvv 3464 ∖ cdif 3928 ∪ cun 3929 ⊆ wss 3931 ∅c0 4313 ifcif 4505 {csn 4606 ∪ ciun 4972 class class class wbr 5124 ↦ cmpt 5206 ↾ cres 5661 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 ↑_m cmap 8845 Xcixp 8916 Fincfn 8964 supcsup 9457 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 · cmul 11139 +∞cpnf 11271 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 − cmin 11471 ℕcn 12245 ℝ⁺crp 13013 [,)cico 13369 [,]cicc 13370 ∏cprod 15924 volcvol 25421 Σ^{^}csumge0 46358

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 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-inf2 9660 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

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 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-er 8724 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fi 9428 df-sup 9459 df-inf 9460 df-oi 9529 df-dju 9920 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-n0 12507 df-z 12594 df-uz 12858 df-q 12970 df-rp 13014 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-ioo 13371 df-ico 13373 df-icc 13374 df-fz 13530 df-fzo 13677 df-fl 13814 df-seq 14025 df-exp 14085 df-hash 14354 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-clim 15509 df-rlim 15510 df-sum 15708 df-prod 15925 df-rest 17441 df-topgen 17462 df-psmet 21312 df-xmet 21313 df-met 21314 df-bl 21315 df-mopn 21316 df-top 22837 df-topon 22854 df-bases 22889 df-cmp 23330 df-ovol 25422 df-vol 25423 df-sumge0 46359

This theorem is referenced by: hoidmvle 46596

W3C validator