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 47608

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 1947	. . . . 5 ⊢ Ⅎ𝑠𝜑
2		nfre1 3288	. . . . 5 ⊢ Ⅎ𝑠∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)
3	1, 2	nfan 1932	. . . 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 9188	. . . . . . . 8 ⊢ ((𝑋 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ Fin)
9	6, 7, 8	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ Fin)
10		snfi 9071	. . . . . . . 8 ⊢ {𝑍} ∈ Fin
11	10	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑍} ∈ Fin)
12		unfi 9186	. . . . . . 7 ⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin)
13	9, 11, 12	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin)
14	5, 13	eqeltrid 2865	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ Fin)
15	14	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝑊 ∈ Fin)
16		hoidmvlelem5.a	. . . . 5 ⊢ (𝜑 → 𝐴:𝑊⟶ℝ)
17	16	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝐴:𝑊⟶ℝ)
18		hoidmvlelem5.b	. . . . 5 ⊢ (𝜑 → 𝐵:𝑊⟶ℝ)
19	18	adantr 486	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 𝐵:𝑊⟶ℝ)
20		simpr 490	. . . 4 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
21	3, 4, 15, 17, 19, 20	hoidmvval0 47596	. . 3 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) = 0)
22		nnex 12341	. . . . . 6 ⊢ ℕ ∈ V
23	22	a1i 11	. . . . 5 ⊢ (𝜑 → ℕ ∈ V)
24		icossicc 13567	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
25	14	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin)
26		hoidmvlelem5.c	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
27	26	ffvelcdmda 7084	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑_m 𝑊))
28		elmapi 8869	. . . . . . . . 9 ⊢ ((𝐶‘𝑗) ∈ (ℝ ↑_m 𝑊) → (𝐶‘𝑗):𝑊⟶ℝ)
29	27, 28	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ)
30		hoidmvlelem5.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
31	30	ffvelcdmda 7084	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑_m 𝑊))
32		elmapi 8869	. . . . . . . . 9 ⊢ ((𝐷‘𝑗) ∈ (ℝ ↑_m 𝑊) → (𝐷‘𝑗):𝑊⟶ℝ)
33	31, 32	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ)
34	4, 25, 29, 33	hoidmvcl 47591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,)+∞))
35	24, 34	sselid 3929	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,]+∞))
36	35	fmpttd 7115	. . . . 5 ⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
37	23, 36	sge0ge0 47393	. . . 4 ⊢ (𝜑 → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
38	37	adantr 486	. . 3 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
39	21, 38	eqbrtrd 5127	. 2 ⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
40		icossxr 13563	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ^*
41	4, 14, 16, 18	hoidmvcl 47591	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ (0[,)+∞))
42	40, 41	sselid 3929	. . . . . 6 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
43	42	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
44	23, 36	sge0xrcl 47394	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
45	44	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
46		rge0ssre 13587	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ
47	46, 41	sselid 3929	. . . . . . . 8 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ)
48		ltpnf 13249	. . . . . . . 8 ⊢ ((𝐴(𝐿‘𝑊)𝐵) ∈ ℝ → (𝐴(𝐿‘𝑊)𝐵) < +∞)
49	47, 48	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) < +∞)
50	49	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < +∞)
51		id 23	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞)
52	51	eqcomd 2767	. . . . . . 7 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
53	52	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → +∞ = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
54	50, 53	breqtrd 5131	. . . . 5 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
55	43, 45, 54	xrltled 13279	. . . 4 ⊢ ((𝜑 ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
56	55	adantlr 728	. . 3 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
57		simpll 779	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → 𝜑)
58		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
59	16	ffvelcdmda 7084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐴‘𝑠) ∈ ℝ)
60	18	ffvelcdmda 7084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐵‘𝑠) ∈ ℝ)
61	59, 60	ltnled 11457	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
62	61	ralbidva 3184	. . . . . . . 8 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
63		ralnex 3089	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
65	62, 64	bitrd 282	. . . . . . 7 ⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
66	65	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)))
67	58, 66	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠))
68	67	adantr 486	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠))
69		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞)
70	22	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ℕ ∈ V)
71	36	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞))
72	70, 71	sge0repnf 47395	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞))
73	69, 72	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
74	73	adantlr 728	. . . 4 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
75		simpll 779	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)))
76		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖))
77		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖))
78	76, 77	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) = ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))
79	78	cbvmptv 5209	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) = (𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))
80	79	fveq2i 6888	. . . . . . . . . 10 ⊢ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖))))
81	80	eleq1i 2852	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
82	81	biimpi 219	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ → (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
83	82	ad2antlr 740	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ)
84		simpr 490	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
85	6	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑋 ∈ Fin)
86	7	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑌 ⊆ 𝑋)
87		hoidmvlelem5.n	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ≠ ∅)
88	87	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑌 ≠ ∅)
89		hoidmvlelem5.z	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌))
90	89	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑍 ∈ (𝑋 ∖ 𝑌))
91	16	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐴:𝑊⟶ℝ)
92	18	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐵:𝑊⟶ℝ)
93		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑘 → (𝐴‘𝑠) = (𝐴‘𝑘))
94		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑘 → (𝐵‘𝑠) = (𝐵‘𝑘))
95	93, 94	breq12d 5116	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑘 → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ (𝐴‘𝑘) < (𝐵‘𝑘)))
96	95	cbvralvw 3241	. . . . . . . . . . 11 ⊢ (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
97	96	birani 509	. . . . . . . . . 10 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘))
98		simpr 490	. . . . . . . . . 10 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑊)
99		rspa 3252	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
100	97, 98, 99	syl2anc 596	. . . . . . . . 9 ⊢ ((∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
101	100	ad5ant25 774	. . . . . . . 8 ⊢ (((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘))
102	26	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐶:ℕ⟶(ℝ ↑_m 𝑊))
103	30	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝐷:ℕ⟶(ℝ ↑_m 𝑊))
104	81	biimpri 231	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
105	104	ad2antlr 740	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
106		fveq1 6884	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑐 → (𝑑‘𝑖) = (𝑐‘𝑖))
107	106	breq1d 5113	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑐 → ((𝑑‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑖) ≤ 𝑥))
108	107, 106	ifbieq1d 4507	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑐 → if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥) = if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))
109	106, 108	ifeq12d 4504	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑐 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)) = if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)))
110	109	mpteq2dv 5199	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))))
111		eleq1w 2844	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ 𝑌 ↔ 𝑗 ∈ 𝑌))
112		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑐‘𝑖) = (𝑐‘𝑗))
113	112	breq1d 5113	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑗 → ((𝑐‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑗) ≤ 𝑥))
114	113, 112	ifbieq1d 4507	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥) = if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))
115	111, 112, 114	ifbieq12d 4511	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)) = if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))
116	115	cbvmptv 5209	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))
117	116	a1i 11	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
118	110, 117	eqtrd 2796	. . . . . . . . . 10 ⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
119	118	cbvmptv 5209	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))) = (𝑐 ∈ (ℝ ↑_m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))
120	119	mpteq2i 5201	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))))
121		eqid 2761	. . . . . . . 8 ⊢ ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌))
122		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → 𝑟 ∈ ℝ⁺)
123		oveq1 7427	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍)))
124	123	oveq2d 7436	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) = (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))))
125		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑑‘𝑖) ≤ 𝑤 ↔ (𝑑‘𝑖) ≤ 𝑥))
126		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → (𝑑‘𝑖) = (𝑑‘𝑖))
127		id 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → 𝑤 = 𝑥)
128	125, 126, 127	ifbieq12d 4511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑥 → if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤) = if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))
129	128	ifeq2d 4503	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑥 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)) = if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))
130	129	mpteq2dv 5199	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑥 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))
131	130	mpteq2dv 5199	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑥 → (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))) = (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))
132	131	cbvmptv 5209	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))))) = (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))
133	132	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → (𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))))) = (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))))
134		id 23	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧)
135	133, 134	fveq12d 6892	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤) = ((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧))
136	135	fveq1d 6887	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑧 → (((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))
137	136	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑧 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))) = ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))))
138	137	mpteq2dv 5199	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))))
139		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑗 → (𝐶‘𝑙) = (𝐶‘𝑗))
140		2fveq3 6890	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑗 → (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))
141	139, 140	oveq12d 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑗 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))) = ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))
142	141	cbvmptv 5209	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))
143	142	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))
144	138, 143	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))
145	144	fveq2d 6889	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑧 → (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))) = (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))
146	145	oveq2d 7436	. . . . . . . . . 10 ⊢ (𝑤 = 𝑧 → ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) = ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))))
147	124, 146	breq12d 5116	. . . . . . . . 9 ⊢ (𝑤 = 𝑧 → ((((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) ↔ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))))
148	147	cbvrabv 3423	. . . . . . . 8 ⊢ {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))}
149		eqid 2761	. . . . . . . 8 ⊢ sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑_m 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))}, ℝ, < )
150		hoidmvlelem5.i	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑_m 𝑌)∀𝑓 ∈ (ℝ ↑_m 𝑌)∀𝑔 ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)∀ℎ ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗))))))
151	150	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → ∀𝑒 ∈ (ℝ ↑_m 𝑌)∀𝑓 ∈ (ℝ ↑_m 𝑌)∀𝑔 ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)∀ℎ ∈ ((ℝ ↑_m 𝑌) ↑_m ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗))))))
152		hoidmvlelem5.s	. . . . . . . . 9 ⊢ (𝜑 → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
153	152	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → X𝑘 ∈ 𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))
154	4, 85, 86, 88, 90, 5, 91, 92, 101, 102, 103, 105, 120, 121, 122, 148, 149, 151, 153	hoidmvlelem4 47607	. . . . . . 7 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
155	75, 83, 84, 154	syl21anc 851	. . . . . 6 ⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ⁺) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
156	155	ralrimiva 3155	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ∀𝑟 ∈ ℝ⁺ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))
157		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑟((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ)
158	42	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ^*)
159		0xr 11356	. . . . . . . 8 ⊢ 0 ∈ ℝ^*
160	159	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ∈ ℝ^*)
161		pnfxr 11363	. . . . . . . 8 ⊢ +∞ ∈ ℝ^*
162	161	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → +∞ ∈ ℝ^*)
163	44	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ^*)
164	37	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
165		ltpnf 13249	. . . . . . . 8 ⊢ ((Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞)
166	165	adantl 487	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞)
167	160, 162, 163, 164, 166	elicod 13526	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ (0[,)+∞))
168	157, 158, 167	xralrple2 46365	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ((𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ↔ ∀𝑟 ∈ ℝ⁺ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) · (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))))
169	156, 168	mpbird 260	. . . 4 ⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
170	57, 68, 74, 169	syl21anc 851	. . 3 ⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
171	56, 170	pm2.61dan 825	. 2 ⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))
172	39, 171	pm2.61dan 825	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤ (Σ^{^}‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ⊆ wss 3899 ∅c0 4279 ifcif 4482 {csn 4584 ∪ ciun 4951 class class class wbr 5103 ↦ cmpt 5186 ↾ cres 5653 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ∈ cmpo 7422 ↑_m cmap 8847 Xcixp 8925 Fincfn 8973 supcsup 9432 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 +∞cpnf 11340 ℝ^*cxr 11342 < clt 11343 ≤ cle 11344 − cmin 11541 ℕcn 12335 ℝ⁺crp 13120 [,)cico 13478 [,]cicc 13479 ∏cprod 16072 volcvol 25784 Σ^{^}csumge0 47371

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 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

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 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9504 df-dju 9982 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-z 12694 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-ioo 13480 df-ico 13482 df-icc 13483 df-fz 13640 df-fzo 13789 df-fl 13932 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-rlim 15656 df-sum 15854 df-prod 16073 df-rest 17593 df-topgen 17614 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-top 23212 df-topon 23229 df-bases 23264 df-cmp 23705 df-ovol 25785 df-vol 25786 df-sumge0 47372

This theorem is used by: hoidmvle 47609

W3C validator