Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑠𝜑 |
2 | | nfre1 2988 |
. . . . 5
⊢
Ⅎ𝑠∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠) |
3 | 1, 2 | nfan 1816 |
. . . 4
⊢
Ⅎ𝑠(𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) |
4 | | hoidmvlelem5.l |
. . . 4
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
5 | | hoidmvlelem5.w |
. . . . . 6
⊢ 𝑊 = (𝑌 ∪ {𝑍}) |
6 | | hoidmvlelem5.f |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ Fin) |
7 | | hoidmvlelem5.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
8 | | ssfi 8065 |
. . . . . . . 8
⊢ ((𝑋 ∈ Fin ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ Fin) |
9 | 6, 7, 8 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ Fin) |
10 | | snfi 7923 |
. . . . . . . 8
⊢ {𝑍} ∈ Fin |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → {𝑍} ∈ Fin) |
12 | | unfi 8112 |
. . . . . . 7
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) |
13 | 9, 11, 12 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) |
14 | 5, 13 | syl5eqel 2692 |
. . . . 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 476 |
. . . 4
⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) |
21 | 3, 4, 15, 17, 19, 20 | hoidmvval0 39477 |
. . 3
⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) = 0) |
22 | | nnex 10903 |
. . . . . 6
⊢ ℕ
∈ V |
23 | 22 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℕ ∈
V) |
24 | | icossicc 12131 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
25 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin) |
26 | | hoidmvlelem5.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ
↑𝑚 𝑊)) |
27 | 26 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑊)) |
28 | | elmapi 7765 |
. . . . . . . . 9
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑊) → (𝐶‘𝑗):𝑊⟶ℝ) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ) |
30 | | hoidmvlelem5.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ
↑𝑚 𝑊)) |
31 | 30 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑊)) |
32 | | elmapi 7765 |
. . . . . . . . 9
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑊) → (𝐷‘𝑗):𝑊⟶ℝ) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ) |
34 | 4, 25, 29, 33 | hoidmvcl 39472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,)+∞)) |
35 | 24, 34 | sseldi 3566 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) ∈ (0[,]+∞)) |
36 | | eqid 2610 |
. . . . . 6
⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) |
37 | 35, 36 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞)) |
38 | 23, 37 | sge0ge0 39277 |
. . . 4
⊢ (𝜑 → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
39 | 38 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
40 | 21, 39 | eqbrtrd 4605 |
. 2
⊢ ((𝜑 ∧ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
41 | | icossxr 12129 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ* |
42 | 4, 14, 16, 18 | hoidmvcl 39472 |
. . . . . . 7
⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ (0[,)+∞)) |
43 | 41, 42 | sseldi 3566 |
. . . . . 6
⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈
ℝ*) |
44 | 43 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ∈
ℝ*) |
45 | 23, 37 | sge0xrcl 39278 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈
ℝ*) |
46 | 45 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈
ℝ*) |
47 | | rge0ssre 12151 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ |
48 | 47, 42 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ∈ ℝ) |
49 | | ltpnf 11830 |
. . . . . . . 8
⊢ ((𝐴(𝐿‘𝑊)𝐵) ∈ ℝ → (𝐴(𝐿‘𝑊)𝐵) < +∞) |
50 | 48, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) < +∞) |
51 | 50 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) < +∞) |
52 | | id 22 |
. . . . . . . 8
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) |
53 | 52 | eqcomd 2616 |
. . . . . . 7
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞ → +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
54 | 53 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → +∞ =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
55 | 51, 54 | breqtrd 4609 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) <
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
56 | 44, 46, 55 | xrltled 38427 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
57 | 56 | adantlr 747 |
. . 3
⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
58 | | simpll 786 |
. . . 4
⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → 𝜑) |
59 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) |
60 | 16 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐴‘𝑠) ∈ ℝ) |
61 | 18 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → (𝐵‘𝑠) ∈ ℝ) |
62 | 60, 61 | ltnled 10063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑊) → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠))) |
63 | 62 | ralbidva 2968 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠))) |
64 | | ralnex 2975 |
. . . . . . . . 9
⊢
(∀𝑠 ∈
𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) |
65 | 64 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑠 ∈ 𝑊 ¬ (𝐵‘𝑠) ≤ (𝐴‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))) |
66 | 63, 65 | bitrd 267 |
. . . . . . 7
⊢ (𝜑 → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))) |
67 | 66 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠))) |
68 | 59, 67 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) |
69 | 68 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) |
70 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) |
71 | 22 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → ℕ ∈
V) |
72 | 37 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))):ℕ⟶(0[,]+∞)) |
73 | 71, 72 | sge0repnf 39279 |
. . . . . 6
⊢ ((𝜑 ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) →
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞)) |
74 | 70, 73 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) |
75 | 74 | adantlr 747 |
. . . 4
⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) |
76 | | simpll 786 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠))) |
77 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖)) |
78 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖)) |
79 | 77, 78 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)) = ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖))) |
80 | 79 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))) = (𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖))) |
81 | 80 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) =
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) |
82 | 81 | eleq1i 2679 |
. . . . . . . . 9
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ ↔
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) |
83 | 82 | biimpi 205 |
. . . . . . . 8
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ →
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) |
84 | 83 | ad2antlr 759 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) →
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) |
85 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
86 | 6 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑋 ∈ Fin) |
87 | 7 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑌 ⊆ 𝑋) |
88 | | hoidmvlelem5.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ≠ ∅) |
89 | 88 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑌 ≠ ∅) |
90 | | hoidmvlelem5.z |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
91 | 90 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
92 | 16 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝐴:𝑊⟶ℝ) |
93 | 18 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝐵:𝑊⟶ℝ) |
94 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑘 → (𝐴‘𝑠) = (𝐴‘𝑘)) |
95 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑘 → (𝐵‘𝑠) = (𝐵‘𝑘)) |
96 | 94, 95 | breq12d 4596 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑘 → ((𝐴‘𝑠) < (𝐵‘𝑠) ↔ (𝐴‘𝑘) < (𝐵‘𝑘))) |
97 | 96 | cbvralv 3147 |
. . . . . . . . . . . 12
⊢
(∀𝑠 ∈
𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ↔ ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘)) |
98 | 97 | biimpi 205 |
. . . . . . . . . . 11
⊢
(∀𝑠 ∈
𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘)) |
99 | 98 | adantr 480 |
. . . . . . . . . 10
⊢
((∀𝑠 ∈
𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → ∀𝑘 ∈ 𝑊 (𝐴‘𝑘) < (𝐵‘𝑘)) |
100 | | simpr 476 |
. . . . . . . . . 10
⊢
((∀𝑠 ∈
𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑊) |
101 | | rspa 2914 |
. . . . . . . . . 10
⊢
((∀𝑘 ∈
𝑊 (𝐴‘𝑘) < (𝐵‘𝑘) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
102 | 99, 100, 101 | syl2anc 691 |
. . . . . . . . 9
⊢
((∀𝑠 ∈
𝑊 (𝐴‘𝑠) < (𝐵‘𝑠) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
103 | 102 | ad5ant25 1298 |
. . . . . . . 8
⊢
(((((𝜑 ∧
∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑊) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
104 | 26 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝐶:ℕ⟶(ℝ
↑𝑚 𝑊)) |
105 | 30 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝐷:ℕ⟶(ℝ
↑𝑚 𝑊)) |
106 | 82 | biimpri 217 |
. . . . . . . . 9
⊢
((Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) |
107 | 106 | ad2antlr 759 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) |
108 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑐 → (𝑑‘𝑖) = (𝑐‘𝑖)) |
109 | 108 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 𝑐 → ((𝑑‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑖) ≤ 𝑥)) |
110 | 109, 108 | ifbieq1d 4059 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑐 → if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥) = if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)) |
111 | 108, 110 | ifeq12d 4056 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑐 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)) = if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) |
112 | 111 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)))) |
113 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (𝑖 ∈ 𝑌 ↔ 𝑗 ∈ 𝑌)) |
114 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (𝑐‘𝑖) = (𝑐‘𝑗)) |
115 | 114 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑗 → ((𝑐‘𝑖) ≤ 𝑥 ↔ (𝑐‘𝑗) ≤ 𝑥)) |
116 | 115, 114 | ifbieq1d 4059 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥) = if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)) |
117 | 113, 114,
116 | ifbieq12d 4063 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥)) = if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))) |
118 | 117 | cbvmptv 4678 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))) |
119 | 118 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑐‘𝑖), if((𝑐‘𝑖) ≤ 𝑥, (𝑐‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))) |
120 | 112, 119 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑐 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) = (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))) |
121 | 120 | cbvmptv 4678 |
. . . . . . . . 9
⊢ (𝑑 ∈ (ℝ
↑𝑚 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))) = (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))) |
122 | 121 | mpteq2i 4669 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ
↑𝑚 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) |
123 | | eqid 2610 |
. . . . . . . 8
⊢ ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) |
124 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
125 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → (𝑤 − (𝐴‘𝑍)) = (𝑧 − (𝐴‘𝑍))) |
126 | 125 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) = (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍)))) |
127 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑥 → ((𝑑‘𝑖) ≤ 𝑤 ↔ (𝑑‘𝑖) ≤ 𝑥)) |
128 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑥 → (𝑑‘𝑖) = (𝑑‘𝑖)) |
129 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = 𝑥 → 𝑤 = 𝑥) |
130 | 127, 128,
129 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑥 → if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤) = if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)) |
131 | 130 | ifeq2d 4055 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑥 → if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)) = if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))) |
132 | 131 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑥 → (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))) = (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))) |
133 | 132 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑥 → (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))) = (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))) |
134 | 133 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ
↑𝑚 𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))))) = (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥))))) |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → (𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤))))) = (𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))) |
136 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
137 | 135, 136 | fveq12d 6109 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → ((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤) = ((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)) |
138 | 137 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑧 → (((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))) |
139 | 138 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))) = ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) |
140 | 139 | mpteq2dv 4673 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))))) |
141 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑗 → (𝐶‘𝑙) = (𝐶‘𝑗)) |
142 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑗 → (𝐷‘𝑙) = (𝐷‘𝑗)) |
143 | 142 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 = 𝑗 → (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)) = (((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))) |
144 | 141, 143 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑗 → ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙))) = ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))) |
145 | 144 | cbvmptv 4678 |
. . . . . . . . . . . . . 14
⊢ (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))) |
146 | 145 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))) |
147 | 140, 146 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → (𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))) |
148 | 147 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 →
(Σ^‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))) |
149 | 148 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑧 → ((1 + 𝑟) ·
(Σ^‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) = ((1 + 𝑟) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))) |
150 | 126, 149 | breq12d 4596 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → ((((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙)))))) ↔ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗)))))))) |
151 | 150 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))} = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(((𝑥 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑥, (𝑑‘𝑖), 𝑥)))))‘𝑧)‘(𝐷‘𝑗))))))} |
152 | | eqid 2610 |
. . . . . . . 8
⊢
sup({𝑤 ∈
((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))}, ℝ, < ) = sup({𝑤 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) · (𝑤 − (𝐴‘𝑍))) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑙 ∈ ℕ ↦ ((𝐶‘𝑙)(𝐿‘𝑊)(((𝑤 ∈ ℝ ↦ (𝑑 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑖 ∈ 𝑊 ↦ if(𝑖 ∈ 𝑌, (𝑑‘𝑖), if((𝑑‘𝑖) ≤ 𝑤, (𝑑‘𝑖), 𝑤)))))‘𝑤)‘(𝐷‘𝑙))))))}, ℝ, < ) |
153 | | hoidmvlelem5.i |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑒 ∈ (ℝ ↑𝑚
𝑌)∀𝑓 ∈ (ℝ
↑𝑚 𝑌)∀𝑔 ∈ ((ℝ ↑𝑚
𝑌)
↑𝑚 ℕ)∀ℎ ∈ ((ℝ ↑𝑚
𝑌)
↑𝑚 ℕ)(X𝑘 ∈ 𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗)))))) |
154 | 153 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) →
∀𝑒 ∈ (ℝ
↑𝑚 𝑌)∀𝑓 ∈ (ℝ ↑𝑚
𝑌)∀𝑔 ∈ ((ℝ
↑𝑚 𝑌) ↑𝑚
ℕ)∀ℎ ∈
((ℝ ↑𝑚 𝑌) ↑𝑚 ℕ)(X𝑘 ∈
𝑌 ((𝑒‘𝑘)[,)(𝑓‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑌 (((𝑔‘𝑗)‘𝑘)[,)((ℎ‘𝑗)‘𝑘)) → (𝑒(𝐿‘𝑌)𝑓) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝑔‘𝑗)(𝐿‘𝑌)(ℎ‘𝑗)))))) |
155 | | hoidmvlelem5.s |
. . . . . . . . 9
⊢ (𝜑 → X𝑘 ∈
𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
156 | 155 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → X𝑘 ∈
𝑊 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑊 (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
157 | 4, 86, 87, 89, 91, 5, 92, 93, 103, 104, 105, 107, 122, 123, 124, 151, 152, 154, 156 | hoidmvlelem4 39488 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑖 ∈ ℕ ↦ ((𝐶‘𝑖)(𝐿‘𝑊)(𝐷‘𝑖)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))) |
158 | 76, 84, 85, 157 | syl21anc 1317 |
. . . . . 6
⊢ ((((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) ∧ 𝑟 ∈ ℝ+) → (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))) |
159 | 158 | ralrimiva 2949 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ∀𝑟 ∈ ℝ+
(𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))))) |
160 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑟((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) |
161 | 43 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ∈
ℝ*) |
162 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
163 | 162 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ∈
ℝ*) |
164 | | pnfxr 9971 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
165 | 164 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → +∞ ∈
ℝ*) |
166 | 45 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈
ℝ*) |
167 | 38 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → 0 ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
168 | | ltpnf 11830 |
. . . . . . . 8
⊢
((Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞) |
169 | 168 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) < +∞) |
170 | 163, 165,
166, 167, 169 | elicod 12095 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ (0[,)+∞)) |
171 | 160, 161,
170 | xralrple2 38511 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → ((𝐴(𝐿‘𝑊)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ↔ ∀𝑟 ∈ ℝ+ (𝐴(𝐿‘𝑊)𝐵) ≤ ((1 + 𝑟) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))))) |
172 | 159, 171 | mpbird 246 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑠 ∈ 𝑊 (𝐴‘𝑠) < (𝐵‘𝑠)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) → (𝐴(𝐿‘𝑊)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
173 | 58, 69, 75, 172 | syl21anc 1317 |
. . 3
⊢ (((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) ∧ ¬
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) = +∞) → (𝐴(𝐿‘𝑊)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
174 | 57, 173 | pm2.61dan 828 |
. 2
⊢ ((𝜑 ∧ ¬ ∃𝑠 ∈ 𝑊 (𝐵‘𝑠) ≤ (𝐴‘𝑠)) → (𝐴(𝐿‘𝑊)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |
175 | 40, 174 | pm2.61dan 828 |
1
⊢ (𝜑 → (𝐴(𝐿‘𝑊)𝐵) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗))))) |