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 42888

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 1915	. . . . 5 ⊢ Ⅎ𝑠𝜑
2		nfre1 3308	. . . . 5 ⊢ Ⅎ𝑠∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)
3	1, 2	nfan 1900	. . . 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 8740	. . . . . . . 8 ⊢ ((𝑋 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ Fin)
9	6, 7, 8	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Fin)
10		snfi 8596	. . . . . . . 8 ⊢ {𝑍} ∈ Fin
11	10	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑍} ∈ Fin)
12		unfi 8787	. . . . . . 7 ⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
13	9, 11, 12	syl2anc 586	. . . . . 6 ⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
14	5, 13	eqeltrid 2919	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Fin)
15	14	adantr 483	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝑊 ∈ Fin)
16		hoidmvlelem5.a	. . . . 5 ⊢ (𝜑 → 𝐴:𝑊⟶ℝ)
17	16	adantr 483	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝐴:𝑊⟶ℝ)
18		hoidmvlelem5.b	. . . . 5 ⊢ (𝜑 → 𝐵:𝑊⟶ℝ)
19	18	adantr 483	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝐵:𝑊⟶ℝ)
20		simpr 487	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
21	3, 4, 15, 17, 19, 20	hoidmvval0 42876	. . 3 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) = 0)
22		nnex 11646	. . . . . 6 ⊢ ℕ ∈ V
23	22	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ ∈ V)
24		icossicc 12827	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
25	14	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
26		hoidmvlelem5.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
27	26	ffvelrnda 6853	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_m 𝑊))
28		elmapi 8430	. . . . . . . . 9 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_m 𝑊) → (𝐶‘𝑗):𝑊⟶ℝ)
29	27, 28	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ)
30		hoidmvlelem5.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
31	30	ffvelrnda 6853	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_m 𝑊))
32		elmapi 8430	. . . . . . . . 9 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_m 𝑊) → (𝐷‘𝑗):𝑊⟶ℝ)
33	31, 32	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ)
34	4, 25, 29, 33	hoidmvcl 42871	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,)+∞))
35	24, 34	sseldi 3967	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,]+∞))
36	35	fmpttd 6881	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
37	23, 36	sge0ge0 42673	. . . 4 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
38	37	adantr 483	. . 3 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
39	21, 38	eqbrtrd 5090	. 2 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
40		icossxr 12824	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ^*
41	4, 14, 16, 18	hoidmvcl 42871	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ (0[,)+∞))
42	40, 41	sseldi 3967	. . . . . 6 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
43	42	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
44	23, 36	sge0xrcl 42674	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
45	44	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
46		rge0ssre 12847	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ
47	46, 41	sseldi 3967	. . . . . . . 8 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ)
48		ltpnf 12518	. . . . . . . 8 ⊢ ((𝐴(𝐿‘𝑊)𝐵) ∈ ℝ → (𝐴(𝐿‘𝑊)𝐵) < +∞)
49	47, 48	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) < +∞)
50	49	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < +∞)
51		id 22	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞)
52	51	eqcomd 2829	. . . . . . 7 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
53	52	adantl 484	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
54	50, 53	breqtrd 5094	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
55	43, 45, 54	xrltled 12546	. . . 4 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
56	55	adantlr 713	. . 3 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
57		simpll 765	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → 𝜑)
58		simpr 487	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
59	16	ffvelrnda 6853	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐴‘𝑠) ∈ ℝ)
60	18	ffvelrnda 6853	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐵‘𝑠) ∈ ℝ)
61	59, 60	ltnled 10789	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
62	61	ralbidva 3198	. . . . . . . 8 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
63		ralnex 3238	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
65	62, 64	bitrd 281	. . . . . . 7 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
66	65	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
67	58, 66	mpbird 259	. . . . 5 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠))
68	67	adantr 483	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠))
69		simpr 487	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞)
70	22	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ℕ ∈ V)
71	36	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
72	70, 71	sge0repnf 42675	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞))
73	69, 72	mpbird 259	. . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
74	73	adantlr 713	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
75		simpll 765	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)))
76		fveq2 6672	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
77		fveq2 6672	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
78	76, 77	oveq12d 7176	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) = ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))
79	78	cbvmptv 5171	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) = (𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))
80	79	fveq2i 6675	. . . . . . . . . 10 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖))))
81	80	eleq1i 2905	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
82	81	biimpi 218	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ → (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
83	82	ad2antlr 725	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
84		simpr 487	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
85	6	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑋 ∈ Fin)
86	7	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑌 ⊆ 𝑋)
87		hoidmvlelem5.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ≠ ∅)
88	87	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑌 ≠ ∅)
89		hoidmvlelem5.z	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌))
90	89	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑍 ∈ (𝑋 ∖ 𝑌))
91	16	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐴:𝑊⟶ℝ)
92	18	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐵:𝑊⟶ℝ)
93		fveq2 6672	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑘 → (𝐴‘𝑠) = (𝐴‘𝑘))
94		fveq2 6672	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑘 → (𝐵‘𝑠) = (𝐵‘𝑘))
95	93, 94	breq12d 5081	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑘 → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ (𝐴‘𝑘) < (𝐵‘𝑘)))
96	95	cbvralvw 3451	. . . . . . . . . . . 12 ⊢ (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
97	96	biimpi 218	. . . . . . . . . . 11 ⊢ (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
98	97	adantr 483	. . . . . . . . . 10 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
99		simpr 487	. . . . . . . . . 10 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑊)
100		rspa 3208	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
101	98, 99, 100	syl2anc 586	. . . . . . . . 9 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
102	101	ad5ant25 760	. . . . . . . 8 ⊢ (((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
103	26	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
104	30	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
105	81	biimpri 230	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
106	105	ad2antlr 725	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
107		fveq1 6671	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑐 → (𝑑‘𝑖) = (𝑐‘𝑖))
108	107	breq1d 5078	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑐 → ((𝑑‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑖) ≤ 𝑥))
109	108, 107	ifbieq1d 4492	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑐 → if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥) = if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))
110	107, 109	ifeq12d 4489	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑐 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)) = if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)))
111	110	mpteq2dv 5164	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))))
112		eleq1w 2897	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ 𝑌 ↔ 𝑗 ∈ 𝑌))
113		fveq2 6672	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑐‘𝑖) = (𝑐‘𝑗))
114	113	breq1d 5078	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑐‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑗) ≤ 𝑥))
115	114, 113	ifbieq1d 4492	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥) = if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))
116	112, 113, 115	ifbieq12d 4496	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)) = if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))
117	116	cbvmptv 5171	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
119	111, 118	eqtrd 2858	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
120	119	cbvmptv 5171	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))) = (𝑐 ∈ (ℝ ↑_m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
121	120	mpteq2i 5160	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))))
122		eqid 2823	. . . . . . . 8 ⊢ ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌))
123		simpr 487	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
124		oveq1 7165	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍)))
125	124	oveq2d 7174	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) = (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))))
126		breq2 5072	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑑‘𝑖) ≤ 𝑤 ↔ (𝑑‘𝑖) ≤ 𝑥))
127		eqidd 2824	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → (𝑑‘𝑖) = (𝑑‘𝑖))
128		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → 𝑤 = 𝑥)
129	126, 127, 128	ifbieq12d 4496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑥 → if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤) = if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))
130	129	ifeq2d 4488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑥 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)) = if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))
131	130	mpteq2dv 5164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))
132	131	mpteq2dv 5164	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑥 → (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))) = (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))
133	132	cbvmptv 5171	. . . . . . . . . . . . . . . . . 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 6679	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤) = ((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧))
137	136	fveq1d 6674	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → (((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))
138	137	oveq2d 7174	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))) = ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))))
139	138	mpteq2dv 5164	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))))
140		fveq2 6672	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑗 → (𝐶‘𝑙) = (𝐶‘𝑗))
141		2fveq3 6677	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑗 → (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))
142	140, 141	oveq12d 7176	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑗 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))) = ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))
143	142	cbvmptv 5171	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))
144	143	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))
145	139, 144	eqtrd 2858	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))
146	145	fveq2d 6676	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))
147	146	oveq2d 7174	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) = ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))))
148	125, 147	breq12d 5081	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → ((((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) ↔ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))))
149	148	cbvrabv 3493	. . . . . . . 8 ⊢ {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))}
150		eqid 2823	. . . . . . . 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 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑒 ∈ (ℝ ↑_m 𝑌)∀𝑓 ∈ (ℝ ↑_m 𝑌)∀𝑔 ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)∀ℎ ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗))))))
153		hoidmvlelem5.s	. . . . . . . . 9 ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
154	153	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
155	4, 85, 86, 88, 90, 5, 91, 92, 102, 103, 104, 106, 121, 122, 123, 149, 150, 152, 154	hoidmvlelem4 42887	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
156	75, 83, 84, 155	syl21anc 835	. . . . . 6 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
157	156	ralrimiva 3184	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ∀𝑟 ∈ ℝ⁺ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
158		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑟((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
159	42	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
160		0xr 10690	. . . . . . . 8 ⊢ 0 ∈ ℝ^*
161	160	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ∈ ℝ^*)
162		pnfxr 10697	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
163	162	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → +∞ ∈ ℝ^*)
164	44	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
165	37	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
166		ltpnf 12518	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞)
167	166	adantl 484	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞)
168	161, 163, 164, 165, 167	elicod 12790	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ (0[,)+∞))
169	158, 159, 168	xralrple2 41629	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ((𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ↔ ∀𝑟 ∈ ℝ⁺ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))))
170	157, 169	mpbird 259	. . . 4 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
171	57, 68, 74, 170	syl21anc 835	. . 3 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
172	56, 171	pm2.61dan 811	. 2 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
173	39, 172	pm2.61dan 811	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 {crab 3144 Vcvv 3496 ∖ cdif 3935 ∪ cun 3936 ⊆ wss 3938 ∅c0 4293 ifcif 4469 {csn 4569 ∪ ciun 4921 class class class wbr 5068 ↦ cmpt 5148 ↾ cres 5559 ⟶wf 6353 ‘cfv 6357 (class class class)co 7158 ∈ cmpo 7160 ↑_m cmap 8408 Xcixp 8463 Fincfn 8511 supcsup 8906 ℝcr 10538 0cc0 10539 1c1 10540 + caddc 10542 · cmul 10544 +∞cpnf 10674 ℝ^*cxr 10676 < clt 10677 ≤ cle 10678 − cmin 10872 ℕcn 11640 ℝ⁺crp 12392 [,)cico 12743 [,]cicc 12744 ∏cprod 15261 volcvol 24066 Σ^{^}csumge0 42651

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-inf2 9106 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-se 5517 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-isom 6366 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-of 7411 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-map 8410 df-pm 8411 df-ixp 8464 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-fi 8877 df-sup 8908 df-inf 8909 df-oi 8976 df-dju 9332 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-n0 11901 df-z 11985 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-ico 12747 df-icc 12748 df-fz 12896 df-fzo 13037 df-fl 13165 df-seq 13373 df-exp 13433 df-hash 13694 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-clim 14847 df-rlim 14848 df-sum 15045 df-prod 15262 df-rest 16698 df-topgen 16719 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-mopn 20543 df-top 21504 df-topon 21521 df-bases 21556 df-cmp 21997 df-ovol 24067 df-vol 24068 df-sumge0 42652

This theorem is referenced by: hoidmvle 42889

W3C validator