Step | Hyp | Ref
| Expression |
1 | | hoidmvlelem2.a |
. . . . . . 7
⊢ (𝜑 → 𝐴:𝑊⟶ℝ) |
2 | | hoidmvlelem2.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
3 | | snidg 4153 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝑋 ∖ 𝑌) → 𝑍 ∈ {𝑍}) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ {𝑍}) |
5 | | elun2 3743 |
. . . . . . . . 9
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
7 | | hoidmvlelem2.w |
. . . . . . . 8
⊢ 𝑊 = (𝑌 ∪ {𝑍}) |
8 | 6, 7 | syl6eleqr 2699 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑊) |
9 | 1, 8 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
10 | | hoidmvlelem2.b |
. . . . . . 7
⊢ (𝜑 → 𝐵:𝑊⟶ℝ) |
11 | 10, 8 | ffvelrnd 6268 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
12 | | hoidmvlelem2.v |
. . . . . . . 8
⊢ 𝑉 = ({(𝐵‘𝑍)} ∪ 𝑂) |
13 | 11 | snssd 4281 |
. . . . . . . . 9
⊢ (𝜑 → {(𝐵‘𝑍)} ⊆ ℝ) |
14 | | hoidmvlelem2.O |
. . . . . . . . . 10
⊢ 𝑂 = ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) |
15 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝜑 |
16 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) = (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) |
17 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝜑) |
18 | | fz1ssnn 12243 |
. . . . . . . . . . . . . 14
⊢
(1...𝑀) ⊆
ℕ |
19 | | elrabi 3328 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑖 ∈ (1...𝑀)) |
20 | 18, 19 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑖 ∈ ℕ) |
21 | 20 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑖 ∈ ℕ) |
22 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝑗 ∈ ℕ ↔ 𝑖 ∈ ℕ)) |
23 | 22 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑖 ∈ ℕ))) |
24 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖)) |
25 | 24 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍)) |
26 | 25 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → (((𝐷‘𝑗)‘𝑍) ∈ ℝ ↔ ((𝐷‘𝑖)‘𝑍) ∈ ℝ)) |
27 | 23, 26 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ))) |
28 | | hoidmvlelem2.d |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ
↑𝑚 𝑊)) |
29 | 28 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑊)) |
30 | | elmapi 7765 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑𝑚
𝑊) → (𝐷‘𝑗):𝑊⟶ℝ) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ) |
32 | 8 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑊) |
33 | 31, 32 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
34 | 27, 33 | chvarv 2251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ) |
35 | 17, 21, 34 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ) |
36 | 15, 16, 35 | rnmptssd 38380 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ⊆ ℝ) |
37 | 14, 36 | syl5eqss 3612 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 ⊆ ℝ) |
38 | 13, 37 | unssd 3751 |
. . . . . . . 8
⊢ (𝜑 → ({(𝐵‘𝑍)} ∪ 𝑂) ⊆ ℝ) |
39 | 12, 38 | syl5eqss 3612 |
. . . . . . 7
⊢ (𝜑 → 𝑉 ⊆ ℝ) |
40 | | hoidmvlelem2.q |
. . . . . . . 8
⊢ 𝑄 = inf(𝑉, ℝ, < ) |
41 | | ltso 9997 |
. . . . . . . . . 10
⊢ < Or
ℝ |
42 | 41 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → < Or
ℝ) |
43 | | snfi 7923 |
. . . . . . . . . . . 12
⊢ {(𝐵‘𝑍)} ∈ Fin |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → {(𝐵‘𝑍)} ∈ Fin) |
45 | | fzfi 12633 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑀) ∈
Fin |
46 | | rabfi 8070 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∈ Fin
→ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin |
48 | 47 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin) |
49 | 16 | rnmptfi 38346 |
. . . . . . . . . . . . 13
⊢ ({𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ∈ Fin) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ∈ Fin) |
51 | 14, 50 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑂 ∈ Fin) |
52 | | unfi 8112 |
. . . . . . . . . . 11
⊢ (({(𝐵‘𝑍)} ∈ Fin ∧ 𝑂 ∈ Fin) → ({(𝐵‘𝑍)} ∪ 𝑂) ∈ Fin) |
53 | 44, 51, 52 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ({(𝐵‘𝑍)} ∪ 𝑂) ∈ Fin) |
54 | 12, 53 | syl5eqel 2692 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ Fin) |
55 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝐵‘𝑍) ∈ V |
56 | 55 | snid 4155 |
. . . . . . . . . . . . 13
⊢ (𝐵‘𝑍) ∈ {(𝐵‘𝑍)} |
57 | | elun1 3742 |
. . . . . . . . . . . . 13
⊢ ((𝐵‘𝑍) ∈ {(𝐵‘𝑍)} → (𝐵‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐵‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂) |
59 | 12 | eqcomi 2619 |
. . . . . . . . . . . 12
⊢ ({(𝐵‘𝑍)} ∪ 𝑂) = 𝑉 |
60 | 58, 59 | eleqtri 2686 |
. . . . . . . . . . 11
⊢ (𝐵‘𝑍) ∈ 𝑉 |
61 | 60 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵‘𝑍) ∈ 𝑉) |
62 | | ne0i 3880 |
. . . . . . . . . 10
⊢ ((𝐵‘𝑍) ∈ 𝑉 → 𝑉 ≠ ∅) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ≠ ∅) |
64 | | fiinfcl 8290 |
. . . . . . . . 9
⊢ (( <
Or ℝ ∧ (𝑉 ∈
Fin ∧ 𝑉 ≠ ∅
∧ 𝑉 ⊆ ℝ))
→ inf(𝑉, ℝ, <
) ∈ 𝑉) |
65 | 42, 54, 63, 39, 64 | syl13anc 1320 |
. . . . . . . 8
⊢ (𝜑 → inf(𝑉, ℝ, < ) ∈ 𝑉) |
66 | 40, 65 | syl5eqel 2692 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
67 | 39, 66 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ ℝ) |
68 | | hoidmvlelem2.u |
. . . . . . . . . . . 12
⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} |
69 | | ssrab2 3650 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍)) |
70 | 68, 69 | eqsstri 3598 |
. . . . . . . . . . 11
⊢ 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍)) |
71 | 70 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
72 | 9, 11 | iccssred 38574 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘𝑍)[,](𝐵‘𝑍)) ⊆ ℝ) |
73 | 71, 72 | sstrd 3578 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ ℝ) |
74 | | hoidmvlelem2.su |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑈) |
75 | 73, 74 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
76 | 9 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘𝑍) ∈
ℝ*) |
77 | 11 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵‘𝑍) ∈
ℝ*) |
78 | 70, 74 | sseldi 3566 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
79 | | iccgelb 12101 |
. . . . . . . . 9
⊢ (((𝐴‘𝑍) ∈ ℝ* ∧ (𝐵‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) → (𝐴‘𝑍) ≤ 𝑆) |
80 | 76, 77, 78, 79 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘𝑍) ≤ 𝑆) |
81 | | hoidmvlelem2.sb |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 < (𝐵‘𝑍)) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < (𝐵‘𝑍)) |
83 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐵‘𝑍) → 𝑥 = (𝐵‘𝑍)) |
84 | 83 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐵‘𝑍) → (𝐵‘𝑍) = 𝑥) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → (𝐵‘𝑍) = 𝑥) |
86 | 82, 85 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥) |
87 | 86 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥) |
88 | | simpll 786 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝜑) |
89 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑉) |
90 | 89, 12 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
91 | 90 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
92 | | elsni 4142 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {(𝐵‘𝑍)} → 𝑥 = (𝐵‘𝑍)) |
93 | 92 | con3i 149 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 = (𝐵‘𝑍) → ¬ 𝑥 ∈ {(𝐵‘𝑍)}) |
94 | 93 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → ¬ 𝑥 ∈ {(𝐵‘𝑍)}) |
95 | | elunnel1 3716 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂) ∧ ¬ 𝑥 ∈ {(𝐵‘𝑍)}) → 𝑥 ∈ 𝑂) |
96 | 91, 94, 95 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ 𝑂) |
97 | 96 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ 𝑂) |
98 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑂 → 𝑥 ∈ 𝑂) |
99 | 98, 14 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑂 → 𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍))) |
100 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
101 | 16 | elrnmpt 5293 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ↔ ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍))) |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ↔ ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍)) |
103 | 99, 102 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑂 → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍)) |
104 | 103 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍)) |
105 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖)) |
106 | 105 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍)) |
107 | 106 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍) ∈ ℝ ↔ ((𝐶‘𝑖)‘𝑍) ∈ ℝ)) |
108 | 23, 107 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ ℝ))) |
109 | | hoidmvlelem2.c |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ
↑𝑚 𝑊)) |
110 | 109 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑊)) |
111 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑𝑚
𝑊) → (𝐶‘𝑗):𝑊⟶ℝ) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ) |
113 | 112, 32 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
114 | 108, 113 | chvarv 2251 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ ℝ) |
115 | 114 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈
ℝ*) |
116 | 17, 21, 115 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐶‘𝑖)‘𝑍) ∈
ℝ*) |
117 | 34 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈
ℝ*) |
118 | 17, 21, 117 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐷‘𝑖)‘𝑍) ∈
ℝ*) |
119 | 106, 25 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
120 | 119 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 𝑖 → (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
121 | 120 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↔ (𝑖 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
122 | 121 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑖 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
123 | 122 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
124 | 123 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
125 | | icoltub 38579 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐶‘𝑖)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑖)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) → 𝑆 < ((𝐷‘𝑖)‘𝑍)) |
126 | 116, 118,
124, 125 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑆 < ((𝐷‘𝑖)‘𝑍)) |
127 | 126 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → 𝑆 < ((𝐷‘𝑖)‘𝑍)) |
128 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑥 = ((𝐷‘𝑖)‘𝑍)) |
129 | 128 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ((𝐷‘𝑖)‘𝑍) → ((𝐷‘𝑖)‘𝑍) = 𝑥) |
130 | 129 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → ((𝐷‘𝑖)‘𝑍) = 𝑥) |
131 | 127, 130 | breqtrd 4609 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → 𝑆 < 𝑥) |
132 | 131 | 3exp 1256 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥))) |
133 | 132 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥))) |
134 | 133 | rexlimdv 3012 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥)) |
135 | 104, 134 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝑆 < 𝑥) |
136 | 88, 97, 135 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥) |
137 | 87, 136 | pm2.61dan 828 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑆 < 𝑥) |
138 | 137 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑉 𝑆 < 𝑥) |
139 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑥 = inf(𝑉, ℝ, < ) → (𝑆 < 𝑥 ↔ 𝑆 < inf(𝑉, ℝ, < ))) |
140 | 139 | rspcva 3280 |
. . . . . . . . . 10
⊢
((inf(𝑉, ℝ,
< ) ∈ 𝑉 ∧
∀𝑥 ∈ 𝑉 𝑆 < 𝑥) → 𝑆 < inf(𝑉, ℝ, < )) |
141 | 65, 138, 140 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 < inf(𝑉, ℝ, < )) |
142 | 40 | eqcomi 2619 |
. . . . . . . . . 10
⊢ inf(𝑉, ℝ, < ) = 𝑄 |
143 | 142 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → inf(𝑉, ℝ, < ) = 𝑄) |
144 | 141, 143 | breqtrd 4609 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 < 𝑄) |
145 | 9, 75, 67, 80, 144 | lelttrd 10074 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘𝑍) < 𝑄) |
146 | 9, 67, 145 | ltled 10064 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ≤ 𝑄) |
147 | | fiminre 10851 |
. . . . . . . . 9
⊢ ((𝑉 ⊆ ℝ ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦) |
148 | 39, 54, 63, 147 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦) |
149 | | lbinfle 10857 |
. . . . . . . 8
⊢ ((𝑉 ⊆ ℝ ∧
∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦 ∧ (𝐵‘𝑍) ∈ 𝑉) → inf(𝑉, ℝ, < ) ≤ (𝐵‘𝑍)) |
150 | 39, 148, 61, 149 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → inf(𝑉, ℝ, < ) ≤ (𝐵‘𝑍)) |
151 | 40, 150 | syl5eqbr 4618 |
. . . . . 6
⊢ (𝜑 → 𝑄 ≤ (𝐵‘𝑍)) |
152 | 9, 11, 67, 146, 151 | eliccd 38573 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
153 | 67 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℂ) |
154 | 75 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℂ) |
155 | 9 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℂ) |
156 | 153, 154,
155 | npncand 10295 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍))) = (𝑄 − (𝐴‘𝑍))) |
157 | 156 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 − (𝐴‘𝑍)) = ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍)))) |
158 | 157 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) = (𝐺 · ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍))))) |
159 | | rge0ssre 12151 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
160 | | hoidmvlelem2.g |
. . . . . . . . . . 11
⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) |
161 | | hoidmvlelem2.l |
. . . . . . . . . . . 12
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑𝑚
𝑥), 𝑏 ∈ (ℝ ↑𝑚
𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
162 | | hoidmvlelem2.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ Fin) |
163 | | hoidmvlelem2.y |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
164 | 162, 163 | ssfid 8068 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ Fin) |
165 | | ssun1 3738 |
. . . . . . . . . . . . . . 15
⊢ 𝑌 ⊆ (𝑌 ∪ {𝑍}) |
166 | 165, 7 | sseqtr4i 3601 |
. . . . . . . . . . . . . 14
⊢ 𝑌 ⊆ 𝑊 |
167 | 166 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ⊆ 𝑊) |
168 | 1, 167 | fssresd 5984 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ↾ 𝑌):𝑌⟶ℝ) |
169 | 10, 167 | fssresd 5984 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ↾ 𝑌):𝑌⟶ℝ) |
170 | 161, 164,
168, 169 | hoidmvcl 39472 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) ∈ (0[,)+∞)) |
171 | 160, 170 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (0[,)+∞)) |
172 | 159, 171 | sseldi 3566 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ ℝ) |
173 | 172 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ℂ) |
174 | 153, 154 | subcld 10271 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 − 𝑆) ∈ ℂ) |
175 | 154, 155 | subcld 10271 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 − (𝐴‘𝑍)) ∈ ℂ) |
176 | 173, 174,
175 | adddid 9943 |
. . . . . . 7
⊢ (𝜑 → (𝐺 · ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍)))) = ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍))))) |
177 | 173, 174 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · (𝑄 − 𝑆)) ∈ ℂ) |
178 | 173, 175 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℂ) |
179 | 177, 178 | addcomd 10117 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) = ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆)))) |
180 | 158, 176,
179 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) = ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆)))) |
181 | 67, 75 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 ∈ ℝ ∧ 𝑆 ∈ ℝ)) |
182 | | resubcl 10224 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑄 − 𝑆) ∈ ℝ) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 − 𝑆) ∈ ℝ) |
184 | 172, 183 | jca 553 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∈ ℝ ∧ (𝑄 − 𝑆) ∈ ℝ)) |
185 | | remulcl 9900 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ ℝ ∧ (𝑄 − 𝑆) ∈ ℝ) → (𝐺 · (𝑄 − 𝑆)) ∈ ℝ) |
186 | 184, 185 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 · (𝑄 − 𝑆)) ∈ ℝ) |
187 | 75, 9 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∈ ℝ ∧ (𝐴‘𝑍) ∈ ℝ)) |
188 | | resubcl 10224 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℝ ∧ (𝐴‘𝑍) ∈ ℝ) → (𝑆 − (𝐴‘𝑍)) ∈ ℝ) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 − (𝐴‘𝑍)) ∈ ℝ) |
190 | 172, 189 | jca 553 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∈ ℝ ∧ (𝑆 − (𝐴‘𝑍)) ∈ ℝ)) |
191 | | remulcl 9900 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ ℝ ∧ (𝑆 − (𝐴‘𝑍)) ∈ ℝ) → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ) |
192 | 190, 191 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ) |
193 | 186, 192 | jca 553 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺 · (𝑄 − 𝑆)) ∈ ℝ ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ)) |
194 | | readdcl 9898 |
. . . . . . . . 9
⊢ (((𝐺 · (𝑄 − 𝑆)) ∈ ℝ ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ) → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) ∈ ℝ) |
195 | 193, 194 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) ∈ ℝ) |
196 | 179, 195 | eqeltrrd 2689 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ∈ ℝ) |
197 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
198 | | hoidmvlelem2.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
199 | 198 | rpred 11748 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℝ) |
200 | 197, 199 | readdcld 9948 |
. . . . . . . . 9
⊢ (𝜑 → (1 + 𝐸) ∈ ℝ) |
201 | 2 | eldifbd 3553 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) |
202 | 8, 201 | eldifd 3551 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑊 ∖ 𝑌)) |
203 | | hoidmvlelem2.r |
. . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) |
204 | | hoidmvlelem2.h |
. . . . . . . . . 10
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) |
205 | 161, 164,
202, 7, 109, 28, 203, 204, 75 | sge0hsphoire 39479 |
. . . . . . . . 9
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |
206 | 200, 205 | remulcld 9949 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ) |
207 | | fzfid 12634 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
208 | 183 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − 𝑆) ∈ ℝ) |
209 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝜑) |
210 | | elfznn 12241 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
211 | 210 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
212 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
213 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ V |
214 | 213 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ V) |
215 | | hoidmvlelem2.p |
. . . . . . . . . . . . . . . . 17
⊢ 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
216 | 215 | fvmpt2 6200 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ℕ ∧ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ V) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
217 | 212, 214,
216 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
218 | 217 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
219 | 164 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ∈ Fin) |
220 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ⊆ 𝑊) |
221 | 112, 220 | fssresd 5984 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ) |
222 | 221 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ) |
223 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌)) |
224 | 223 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌)) |
225 | 224 | feq1d 5943 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ)) |
226 | 222, 225 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
227 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 0 ∈ ℝ) |
228 | | hoidmvlelem2.f |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐹 = (𝑦 ∈ 𝑌 ↦ 0) |
229 | 227, 228 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝑌⟶ℝ) |
230 | 229 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝐹:𝑌⟶ℝ) |
231 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = 𝐹) |
232 | 231 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = 𝐹) |
233 | 232 | feq1d 5943 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ 𝐹:𝑌⟶ℝ)) |
234 | 230, 233 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
235 | 226, 234 | pm2.61dan 828 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
236 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
237 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐶‘𝑗) ∈ V |
238 | 237 | resex 5363 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶‘𝑗) ↾ 𝑌) ∈ V |
239 | 238 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐶‘𝑗) ↾ 𝑌) ∈ V) |
240 | 162, 163 | ssexd 4733 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑌 ∈ V) |
241 | | mptexg 6389 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑌 ∈ V → (𝑦 ∈ 𝑌 ↦ 0) ∈ V) |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 0) ∈ V) |
243 | 228, 242 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹 ∈ V) |
244 | 239, 243 | ifcld 4081 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V) |
245 | 244 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V) |
246 | | hoidmvlelem2.j |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
247 | 246 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
248 | 236, 245,
247 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
249 | 248 | feq1d 5943 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐽‘𝑗):𝑌⟶ℝ ↔ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)) |
250 | 235, 249 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐽‘𝑗):𝑌⟶ℝ) |
251 | 31, 220 | fssresd 5984 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ) |
252 | 251 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ) |
253 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌)) |
254 | 253 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌)) |
255 | 254 | feq1d 5943 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ)) |
256 | 252, 255 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
257 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = 𝐹) |
258 | 257 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = 𝐹) |
259 | 258 | feq1d 5943 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ 𝐹:𝑌⟶ℝ)) |
260 | 230, 259 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
261 | 256, 260 | pm2.61dan 828 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
262 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷‘𝑗) ∈ V |
263 | 262 | resex 5363 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷‘𝑗) ↾ 𝑌) ∈ V |
264 | 263 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐷‘𝑗) ↾ 𝑌) ∈ V) |
265 | 264, 243 | ifcld 4081 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V) |
266 | 265 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V) |
267 | | hoidmvlelem2.k |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
268 | 267 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
269 | 236, 266,
268 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
270 | 269 | feq1d 5943 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐾‘𝑗):𝑌⟶ℝ ↔ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)) |
271 | 261, 270 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗):𝑌⟶ℝ) |
272 | 161, 219,
250, 271 | hoidmvcl 39472 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ (0[,)+∞)) |
273 | 218, 272 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ (0[,)+∞)) |
274 | 159, 273 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ ℝ) |
275 | 209, 211,
274 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃‘𝑗) ∈ ℝ) |
276 | 208, 275 | remulcld 9949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ) |
277 | 207, 276 | fsumrecl 14312 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ) |
278 | 200, 277 | remulcld 9949 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
279 | 206, 278 | readdcld 9948 |
. . . . . . 7
⊢ (𝜑 → (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) ∈ ℝ) |
280 | 161, 164,
202, 7, 109, 28, 203, 204, 67 | sge0hsphoire 39479 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) |
281 | 200, 280 | remulcld 9949 |
. . . . . . 7
⊢ (𝜑 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) ∈ ℝ) |
282 | 74, 68 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}) |
283 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (𝑧 − (𝐴‘𝑍)) = (𝑆 − (𝐴‘𝑍))) |
284 | 283 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · (𝑆 − (𝐴‘𝑍)))) |
285 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑆 → (𝐻‘𝑧) = (𝐻‘𝑆)) |
286 | 285 | fveq1d 6105 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑆 → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘𝑆)‘(𝐷‘𝑗))) |
287 | 286 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
288 | 287 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) |
289 | 288 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) |
290 | 289 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
291 | 284, 290 | breq12d 4596 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
292 | 291 | elrab 3331 |
. . . . . . . . . 10
⊢ (𝑆 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ (𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
293 | 282, 292 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
294 | 293 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
295 | 207, 275 | fsumrecl 14312 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) ∈ ℝ) |
296 | 200, 295 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) ∈ ℝ) |
297 | | 0red 9920 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) |
298 | 75, 67 | posdifd 10493 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 < 𝑄 ↔ 0 < (𝑄 − 𝑆))) |
299 | 144, 298 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝑄 − 𝑆)) |
300 | 297, 183,
299 | ltled 10064 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝑄 − 𝑆)) |
301 | | hoidmvlelem2.le |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗))) |
302 | 172, 296,
183, 300, 301 | lemul1ad 10842 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 · (𝑄 − 𝑆)) ≤ (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆))) |
303 | 200 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 + 𝐸) ∈ ℂ) |
304 | 295 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) ∈ ℂ) |
305 | 303, 304,
174 | mulassd 9942 |
. . . . . . . . . 10
⊢ (𝜑 → (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆)) = ((1 + 𝐸) · (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆)))) |
306 | 275 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃‘𝑗) ∈ ℂ) |
307 | 207, 174,
306 | fsummulc1 14359 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑃‘𝑗) · (𝑄 − 𝑆))) |
308 | 174 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − 𝑆) ∈ ℂ) |
309 | 306, 308 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑃‘𝑗) · (𝑄 − 𝑆)) = ((𝑄 − 𝑆) · (𝑃‘𝑗))) |
310 | 309 | sumeq2dv 14281 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) |
311 | 307, 310 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) |
312 | 311 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + 𝐸) · (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆))) = ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
313 | 305, 312 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆)) = ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
314 | 302, 313 | breqtrd 4609 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · (𝑄 − 𝑆)) ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
315 | 192, 186,
206, 278, 294, 314 | leadd12dd 38473 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ≤ (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
316 | | hoidmvlelem2.m |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℕ) |
317 | | nnsplit 38515 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ℕ =
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
318 | 316, 317 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℕ = ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
319 | | uncom 3719 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))) =
((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) |
320 | 319 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) =
((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀))) |
321 | 318, 320 | eqtr2d 2645 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) = ℕ) |
322 | 321 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ =
((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀))) |
323 | 322 | mpteq1d 4666 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) = (𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) |
324 | 323 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) |
325 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝜑 |
326 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘(𝑀 + 1)) ∈ V |
327 | 326 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ∈ V) |
328 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(1...𝑀) ∈
V |
329 | 328 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ∈ V) |
330 | | incom 3767 |
. . . . . . . . . . . . . . 15
⊢
((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ((1...𝑀) ∩ (ℤ≥‘(𝑀 + 1))) |
331 | | nnuzdisj 38512 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∩
(ℤ≥‘(𝑀 + 1))) = ∅ |
332 | 330, 331 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢
((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ∅ |
333 | 332 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ∅) |
334 | | icossicc 12131 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
335 | | ssid 3587 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ (0[,)+∞) |
336 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑) |
337 | 316 | peano2nnd 10914 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
338 | | uznnssnn 11611 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 + 1) ∈ ℕ →
(ℤ≥‘(𝑀 + 1)) ⊆ ℕ) |
339 | 337, 338 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ ℕ) |
340 | 339 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) →
(ℤ≥‘(𝑀 + 1)) ⊆ ℕ) |
341 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈
(ℤ≥‘(𝑀 + 1))) |
342 | 340, 341 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈
ℕ) |
343 | | snfi 7923 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑍} ∈ Fin |
344 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → {𝑍} ∈ Fin) |
345 | | unfi 8112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) |
346 | 164, 344,
345 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) |
347 | 7, 346 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑊 ∈ Fin) |
348 | 347 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin) |
349 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑙 → (𝑗 ∈ 𝑌 ↔ 𝑙 ∈ 𝑌)) |
350 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑙 → (𝑐‘𝑗) = (𝑐‘𝑙)) |
351 | 350 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 𝑙 → ((𝑐‘𝑗) ≤ 𝑥 ↔ (𝑐‘𝑙) ≤ 𝑥)) |
352 | 351, 350 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑙 → if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥) = if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥)) |
353 | 349, 350,
352 | ifbieq12d 4063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑙 → if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)) = if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))) |
354 | 353 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))) = (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))) |
355 | 354 | mpteq2i 4669 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ (ℝ
↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥)))) |
356 | 355 | mpteq2i 4669 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ
↑𝑚 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))))) |
357 | 204, 356 | eqtri 2632 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚
𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))))) |
358 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ) |
359 | 357, 358,
348, 31 | hsphoif 39466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑆)‘(𝐷‘𝑗)):𝑊⟶ℝ) |
360 | 161, 348,
112, 359 | hoidmvcl 39472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
361 | 336, 342,
360 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
362 | 335, 361 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
363 | 334, 362 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
364 | 209, 211,
360 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
365 | 334, 364 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
366 | 325, 327,
329, 333, 363, 365 | sge0splitmpt 39304 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
367 | | nnex 10903 |
. . . . . . . . . . . . . . 15
⊢ ℕ
∈ V |
368 | 367 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ ∈
V) |
369 | 334, 360 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
370 | 325, 368,
369, 205, 339 | sge0ssrempt 39298 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |
371 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...𝑀) ⊆ ℕ) |
372 | 325, 368,
369, 205, 371 | sge0ssrempt 39298 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |
373 | | rexadd 11937 |
. . . . . . . . . . . . 13
⊢
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ ∧
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
374 | 370, 372,
373 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
375 | 324, 366,
374 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
376 | 375 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
377 | 376 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = (((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
378 | 375, 205 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ) |
379 | 378 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℂ) |
380 | 277 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ) |
381 | 303, 379,
380 | adddid 9943 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + 𝐸) ·
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = (((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
382 | 381 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝜑 → (((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) ·
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
383 | 370 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℂ) |
384 | 372 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℂ) |
385 | 383, 384,
380 | addassd 9941 |
. . . . . . . . . . 11
⊢ (𝜑 →
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
386 | 207, 364 | sge0fsummpt 39283 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) = Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
387 | 386 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
388 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℂ |
389 | 159, 388 | sstri 3577 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,)+∞) ⊆ ℂ |
390 | 389, 360 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℂ) |
391 | 209, 211,
390 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℂ) |
392 | 183 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑄 − 𝑆) ∈ ℝ) |
393 | 392, 274 | remulcld 9949 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ) |
394 | 393 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ) |
395 | 211, 394 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ) |
396 | 207, 391,
395 | fsumadd 14317 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
397 | 396 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
398 | 387, 397 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
399 | 398 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
400 | 385, 399 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 →
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
401 | 400 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → ((1 + 𝐸) ·
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))))) |
402 | 377, 382,
401 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 → (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))))) |
403 | 159, 360 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℝ) |
404 | 403, 393 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
405 | 209, 211,
404 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
406 | 207, 405 | fsumrecl 14312 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
407 | 370, 406 | readdcld 9948 |
. . . . . . . . 9
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ∈ ℝ) |
408 | | 0le1 10430 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
409 | 408 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 1) |
410 | 198 | rpge0d 11752 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝐸) |
411 | 197, 199,
409, 410 | addge0d 10482 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (1 + 𝐸)) |
412 | 67 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑄 ∈ ℝ) |
413 | 357, 412,
348, 31 | hsphoif 39466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑄)‘(𝐷‘𝑗)):𝑊⟶ℝ) |
414 | 161, 348,
112, 413 | hoidmvcl 39472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
415 | 334, 414 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
416 | 325, 368,
415, 280, 339 | sge0ssrempt 39298 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) |
417 | 159, 414 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ) |
418 | 209, 211,
417 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ) |
419 | 207, 418 | fsumrecl 14312 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ) |
420 | 336, 342,
415 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
421 | 202 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊 ∖ 𝑌)) |
422 | 75, 67, 144 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ≤ 𝑄) |
423 | 422 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ≤ 𝑄) |
424 | 161, 348,
421, 7, 358, 412, 423, 357, 112, 31 | hsphoidmvle2 39475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
425 | 336, 342,
424 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
426 | 325, 327,
363, 420, 425 | sge0lempt 39303 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ≤
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
427 | 209 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → 𝜑) |
428 | 211 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → 𝑗 ∈ ℕ) |
429 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → (𝑃‘𝑗) = 0) |
430 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘𝑗) = 0 → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = ((𝑄 − 𝑆) · 0)) |
431 | 430 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = ((𝑄 − 𝑆) · 0)) |
432 | 174 | mul01d 10114 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑄 − 𝑆) · 0) = 0) |
433 | 432 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · 0) = 0) |
434 | 431, 433 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = 0) |
435 | 434 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0)) |
436 | 390 | addid1d 10115 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
437 | 436 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
438 | 435, 437 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
439 | 424 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
440 | 438, 439 | eqbrtrd 4605 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
441 | 427, 428,
429, 440 | syl21anc 1317 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
442 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (𝜑 ∧ 𝑗 ∈ (1...𝑀))) |
443 | | neqne 2790 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝑃‘𝑗) = 0 → (𝑃‘𝑗) ≠ 0) |
444 | 443 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (𝑃‘𝑗) ≠ 0) |
445 | 405 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
446 | 209 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝜑) |
447 | 211 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ ℕ) |
448 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (𝑃‘𝑗) ≠ 0) |
449 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
450 | 201 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ¬ 𝑍 ∈ 𝑌) |
451 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
∏𝑘 ∈
𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) |
452 | 161, 219,
449, 450, 7, 112, 359, 451 | hoiprodp1 39478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))))) |
453 | 452 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))))) |
454 | 218 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
455 | 219 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑌 ∈ Fin) |
456 | 218 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
457 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑌 = ∅ → (𝐿‘𝑌) = (𝐿‘∅)) |
458 | 457 | oveqd 6566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑌 = ∅ → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗))) |
459 | 458 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗))) |
460 | 250 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐽‘𝑗):𝑌⟶ℝ) |
461 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑌 = ∅ → 𝑌 = ∅) |
462 | 461 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑌 = ∅ → ∅ =
𝑌) |
463 | 462 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ∅ = 𝑌) |
464 | 463 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗):∅⟶ℝ ↔ (𝐽‘𝑗):𝑌⟶ℝ)) |
465 | 460, 464 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐽‘𝑗):∅⟶ℝ) |
466 | 271 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐾‘𝑗):𝑌⟶ℝ) |
467 | 463 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐾‘𝑗):∅⟶ℝ ↔ (𝐾‘𝑗):𝑌⟶ℝ)) |
468 | 466, 467 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐾‘𝑗):∅⟶ℝ) |
469 | 161, 465,
468 | hoidmv0val 39473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗)) = 0) |
470 | 456, 459,
469 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = 0) |
471 | 470 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = 0) |
472 | | neneq 2788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃‘𝑗) ≠ 0 → ¬ (𝑃‘𝑗) = 0) |
473 | 472 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑌 = ∅) → ¬ (𝑃‘𝑗) = 0) |
474 | 471, 473 | pm2.65da 598 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ¬ 𝑌 = ∅) |
475 | 474 | neqned 2789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑌 ≠ ∅) |
476 | 250 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗):𝑌⟶ℝ) |
477 | 271 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗):𝑌⟶ℝ) |
478 | 161, 455,
475, 476, 477 | hoidmvn0val 39474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘)))) |
479 | 248 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
480 | 218 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
481 | 248 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
482 | 481, 232 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐽‘𝑗) = 𝐹) |
483 | 269 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
484 | 483, 258 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐾‘𝑗) = 𝐹) |
485 | 482, 484 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = (𝐹(𝐿‘𝑌)𝐹)) |
486 | 161, 164,
229 | hoidmvval0b 39480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝐹(𝐿‘𝑌)𝐹) = 0) |
487 | 486 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐹(𝐿‘𝑌)𝐹) = 0) |
488 | 480, 485,
487 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = 0) |
489 | 488 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = 0) |
490 | 472 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ¬ (𝑃‘𝑗) = 0) |
491 | 489, 490 | condan 831 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
492 | 491 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌)) |
493 | 479, 492 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗) = ((𝐶‘𝑗) ↾ 𝑌)) |
494 | 493 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)‘𝑘) = (((𝐶‘𝑗) ↾ 𝑌)‘𝑘)) |
495 | 494 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐽‘𝑗)‘𝑘) = (((𝐶‘𝑗) ↾ 𝑌)‘𝑘)) |
496 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ 𝑌 → (((𝐶‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐶‘𝑗)‘𝑘)) |
497 | 496 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐶‘𝑗)‘𝑘)) |
498 | 495, 497 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐽‘𝑗)‘𝑘) = ((𝐶‘𝑗)‘𝑘)) |
499 | 269 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
500 | 491, 253 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌)) |
501 | 499, 500 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗) = ((𝐷‘𝑗) ↾ 𝑌)) |
502 | 501 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐾‘𝑗)‘𝑘) = (((𝐷‘𝑗) ↾ 𝑌)‘𝑘)) |
503 | 502 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐾‘𝑗)‘𝑘) = (((𝐷‘𝑗) ↾ 𝑌)‘𝑘)) |
504 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ 𝑌 → (((𝐷‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
505 | 504 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐷‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
506 | 503, 505 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐾‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
507 | 498, 506 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
508 | 507 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
509 | 508 | prodeq2dv 14492 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
510 | 478, 509 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
511 | 358 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑆 ∈ ℝ) |
512 | 348 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑊 ∈ Fin) |
513 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (𝐷‘𝑗):𝑊⟶ℝ) |
514 | | elun1 3742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ (𝑌 ∪ {𝑍})) |
515 | 514, 7 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑊) |
516 | 515 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑘 ∈ 𝑊) |
517 | 357, 511,
512, 513, 516 | hsphoival 39469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆))) |
518 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ 𝑌 → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆)) = ((𝐷‘𝑗)‘𝑘)) |
519 | 518 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆)) = ((𝐷‘𝑗)‘𝑘)) |
520 | 517, 519 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
521 | 520 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
522 | 521 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
523 | 522 | prodeq2dv 14492 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
524 | 523 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘)))) |
525 | 524 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘)))) |
526 | 454, 510,
525 | 3eqtrrd 2649 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗)) |
527 | 357, 358,
348, 31, 32 | hsphoival 39469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))) |
528 | 201 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) |
529 | 528 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) |
530 | 527, 529 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) |
531 | 530 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))) |
532 | 531 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))) |
533 | 113 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈
ℝ*) |
534 | 533 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ∈
ℝ*) |
535 | 33 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈
ℝ*) |
536 | 535 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈
ℝ*) |
537 | | icoltub 38579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝑆 < ((𝐷‘𝑗)‘𝑍)) |
538 | 534, 536,
491, 537 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 < ((𝐷‘𝑗)‘𝑍)) |
539 | 358 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ ℝ) |
540 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
541 | 539, 540 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝑆 < ((𝐷‘𝑗)‘𝑍) ↔ ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑆)) |
542 | 538, 541 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑆) |
543 | 542 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆) = 𝑆) |
544 | 543 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = (((𝐶‘𝑗)‘𝑍)[,)𝑆)) |
545 | 532, 544 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)𝑆)) |
546 | 545 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆))) |
547 | | volico 38876 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0)) |
548 | 113, 539,
547 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0)) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0)) |
549 | 548 | anabss5 853 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0)) |
550 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐶‘𝑗)‘𝑍) < 𝑆 → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
551 | 550 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
552 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
((𝐶‘𝑗)‘𝑍) < 𝑆 → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = 0) |
553 | 552 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = 0) |
554 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (𝜑 ∧ 𝑗 ∈ ℕ)) |
555 | | icogelb 12096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆) |
556 | 534, 536,
491, 555 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆) |
557 | 556 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆) |
558 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) |
559 | 557, 558 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (((𝐶‘𝑗)‘𝑍) ≤ 𝑆 ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆)) |
560 | 554, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
561 | 554, 358 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → 𝑆 ∈ ℝ) |
562 | 560, 561 | eqleltd 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (((𝐶‘𝑗)‘𝑍) = 𝑆 ↔ (((𝐶‘𝑗)‘𝑍) ≤ 𝑆 ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆))) |
563 | 559, 562 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) = 𝑆) |
564 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐶‘𝑗)‘𝑍) = 𝑆 → ((𝐶‘𝑗)‘𝑍) = 𝑆) |
565 | 564 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐶‘𝑗)‘𝑍) = 𝑆 → 𝑆 = ((𝐶‘𝑗)‘𝑍)) |
566 | 565 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐶‘𝑗)‘𝑍) = 𝑆 → (𝑆 − ((𝐶‘𝑗)‘𝑍)) = (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍))) |
567 | 566 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) = (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍))) |
568 | 388, 113 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℂ) |
569 | 568 | subidd 10259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍)) = 0) |
570 | 569 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍)) = 0) |
571 | 567, 570 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → 0 = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
572 | 554, 563,
571 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → 0 = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
573 | 553, 572 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
574 | 551, 573 | pm2.61dan 828 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
575 | 546, 549,
574 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
576 | 526, 575 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)))) = ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍)))) |
577 | 389, 273 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ ℂ) |
578 | 358, 113 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) ∈ ℝ) |
579 | 578 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) ∈ ℂ) |
580 | 577, 579 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
581 | 580 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
582 | 453, 576,
581 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
583 | 582 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
584 | 174 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑄 − 𝑆) ∈ ℂ) |
585 | 579, 584,
577 | adddird 9944 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
586 | 585 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗))) |
587 | 586 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗))) |
588 | 579, 584 | addcomd 10117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) = ((𝑄 − 𝑆) + (𝑆 − ((𝐶‘𝑗)‘𝑍)))) |
589 | 153 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑄 ∈ ℂ) |
590 | 154 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℂ) |
591 | 589, 590,
568 | npncand 10295 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) + (𝑆 − ((𝐶‘𝑗)‘𝑍))) = (𝑄 − ((𝐶‘𝑗)‘𝑍))) |
592 | 588, 591 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) = (𝑄 − ((𝐶‘𝑗)‘𝑍))) |
593 | 592 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
594 | 593 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
595 | 583, 587,
594 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
596 | 446, 447,
448, 595 | syl21anc 1317 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
597 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∏𝑘 ∈
𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) |
598 | 161, 219,
32, 450, 7, 112, 413, 597 | hoiprodp1 39478 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))))) |
599 | 209, 211,
598 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))))) |
600 | 599 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))))) |
601 | 510 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
602 | 412 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑄 ∈ ℝ) |
603 | 357, 602,
512, 513, 516 | hsphoival 39469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄))) |
604 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ 𝑌 → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄)) = ((𝐷‘𝑗)‘𝑘)) |
605 | 604 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄)) = ((𝐷‘𝑗)‘𝑘)) |
606 | 603, 605 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
607 | 606 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
608 | 607 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
609 | 608 | prodeq2dv 14492 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
610 | 609 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
611 | 601, 610,
454 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗)) |
612 | 446, 447,
448, 611 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗)) |
613 | 357, 412,
348, 31, 32 | hsphoival 39469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄))) |
614 | 211, 613 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄))) |
615 | 614 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄))) |
616 | 201 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) |
617 | 616 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) |
618 | 211, 33 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
619 | 618 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
620 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) = 𝑄) |
621 | 619, 620 | eqled 10019 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ≤ 𝑄) |
622 | 621 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = ((𝐷‘𝑗)‘𝑍)) |
623 | 622, 620 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄) |
624 | 623 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄) |
625 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑄 ∈ ℝ) |
626 | 625 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ∈ ℝ) |
627 | 626 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ∈ ℝ) |
628 | 618 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
629 | 628 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
630 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 = inf(𝑉, ℝ, < )) |
631 | 446, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑉 ⊆ ℝ) |
632 | 148 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦) |
633 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ (1...𝑀)) |
634 | 210, 491 | sylanl2 681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
635 | 633, 634 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (𝑗 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
636 | | rabid 3095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↔ (𝑗 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
637 | 635, 636 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) |
638 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍)) |
639 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑖 = 𝑗 → (𝐷‘𝑖) = (𝐷‘𝑗)) |
640 | 639 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑖 = 𝑗 → ((𝐷‘𝑖)‘𝑍) = ((𝐷‘𝑗)‘𝑍)) |
641 | 640 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑖 = 𝑗 → (((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍) ↔ ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍))) |
642 | 641 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍)) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍)) |
643 | 637, 638,
642 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍)) |
644 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐷‘𝑗)‘𝑍) ∈ V |
645 | 644 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ V) |
646 | 16, 643, 645 | elrnmptd 38361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍))) |
647 | 646, 14 | syl6eleqr 2699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ 𝑂) |
648 | | elun2 3743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐷‘𝑗)‘𝑍) ∈ 𝑂 → ((𝐷‘𝑗)‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
649 | 647, 648 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
650 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ({(𝐵‘𝑍)} ∪ 𝑂) = 𝑉) |
651 | 649, 650 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ 𝑉) |
652 | | lbinfle 10857 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑉 ⊆ ℝ ∧
∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦 ∧ ((𝐷‘𝑗)‘𝑍) ∈ 𝑉) → inf(𝑉, ℝ, < ) ≤ ((𝐷‘𝑗)‘𝑍)) |
653 | 631, 632,
651, 652 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → inf(𝑉, ℝ, < ) ≤ ((𝐷‘𝑗)‘𝑍)) |
654 | 630, 653 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 ≤ ((𝐷‘𝑗)‘𝑍)) |
655 | 654 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ≤ ((𝐷‘𝑗)‘𝑍)) |
656 | | neqne 2790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
((𝐷‘𝑗)‘𝑍) = 𝑄 → ((𝐷‘𝑗)‘𝑍) ≠ 𝑄) |
657 | 656 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ≠ 𝑄) |
658 | 627, 629,
655, 657 | leneltd 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 < ((𝐷‘𝑗)‘𝑍)) |
659 | 627, 629 | ltnled 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → (𝑄 < ((𝐷‘𝑗)‘𝑍) ↔ ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑄)) |
660 | 658, 659 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑄) |
661 | 660 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄) |
662 | 624, 661 | pm2.61dan 828 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄) |
663 | 615, 617,
662 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = 𝑄) |
664 | 663 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)𝑄)) |
665 | 664 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄))) |
666 | 209, 211,
113 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
667 | 666 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
668 | 446, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 ∈ ℝ) |
669 | | volico 38876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄)) = if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0)) |
670 | 667, 668,
669 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄)) = if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0)) |
671 | 446, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ ℝ) |
672 | 446, 447,
448, 556 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆) |
673 | 446, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 < 𝑄) |
674 | 667, 671,
668, 672, 673 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) < 𝑄) |
675 | 674 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑄 − ((𝐶‘𝑗)‘𝑍))) |
676 | 665, 670,
675 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))) = (𝑄 − ((𝐶‘𝑗)‘𝑍))) |
677 | 612, 676 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)))) = ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍)))) |
678 | 209, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑄 ∈ ℂ) |
679 | 388, 666 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)‘𝑍) ∈ ℂ) |
680 | 678, 679 | subcld 10271 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − ((𝐶‘𝑗)‘𝑍)) ∈ ℂ) |
681 | 306, 680 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
682 | 681 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
683 | 600, 677,
682 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
684 | 596, 683 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
685 | 445, 684 | eqled 10019 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
686 | 442, 444,
685 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
687 | 441, 686 | pm2.61dan 828 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
688 | 207, 405,
418, 687 | fsumle 14372 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
689 | 370, 406,
416, 419, 426, 688 | leadd12dd 38473 |
. . . . . . . . . 10
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) |
690 | 322 | mpteq1d 4666 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) = (𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) |
691 | 690 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
692 | 211, 415 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
693 | 325, 327,
329, 333, 420, 692 | sge0splitmpt 39304 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
694 | 691, 693 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
695 | 209, 211,
414 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
696 | 207, 695 | sge0fsummpt 39283 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) = Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
697 | 696, 419 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) |
698 | | rexadd 11937 |
. . . . . . . . . . . 12
⊢
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ ∧
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
699 | 416, 697,
698 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
700 | 696 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) |
701 | 694, 699,
700 | 3eqtrrd 2649 |
. . . . . . . . . 10
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
702 | 689, 701 | breqtrd 4609 |
. . . . . . . . 9
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
703 | 407, 280,
200, 411, 702 | lemul2ad 10843 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
704 | 402, 703 | eqbrtrd 4605 |
. . . . . . 7
⊢ (𝜑 → (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
705 | 196, 279,
281, 315, 704 | letrd 10073 |
. . . . . 6
⊢ (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
706 | 180, 705 | eqbrtrd 4605 |
. . . . 5
⊢ (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
707 | 152, 706 | jca 553 |
. . . 4
⊢ (𝜑 → (𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))) |
708 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑧 = 𝑄 → (𝑧 − (𝐴‘𝑍)) = (𝑄 − (𝐴‘𝑍))) |
709 | 708 | oveq2d 6565 |
. . . . . 6
⊢ (𝑧 = 𝑄 → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · (𝑄 − (𝐴‘𝑍)))) |
710 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑄 → (𝐻‘𝑧) = (𝐻‘𝑄)) |
711 | 710 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑄 → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘𝑄)‘(𝐷‘𝑗))) |
712 | 711 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑧 = 𝑄 → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
713 | 712 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑧 = 𝑄 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) |
714 | 713 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑧 = 𝑄 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
715 | 714 | oveq2d 6565 |
. . . . . 6
⊢ (𝑧 = 𝑄 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
716 | 709, 715 | breq12d 4596 |
. . . . 5
⊢ (𝑧 = 𝑄 → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))) |
717 | 716 | elrab 3331 |
. . . 4
⊢ (𝑄 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ (𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))) |
718 | 707, 717 | sylibr 223 |
. . 3
⊢ (𝜑 → 𝑄 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}) |
719 | 718, 68 | syl6eleqr 2699 |
. 2
⊢ (𝜑 → 𝑄 ∈ 𝑈) |
720 | | breq2 4587 |
. . 3
⊢ (𝑢 = 𝑄 → (𝑆 < 𝑢 ↔ 𝑆 < 𝑄)) |
721 | 720 | rspcev 3282 |
. 2
⊢ ((𝑄 ∈ 𝑈 ∧ 𝑆 < 𝑄) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
722 | 719, 144,
721 | syl2anc 691 |
1
⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |