Step | Hyp | Ref
| Expression |
1 | | hoidmvlelem2.a |
. . . . . . 7
⊢ (𝜑 → 𝐴:𝑊⟶ℝ) |
2 | | hoidmvlelem2.z |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
3 | | snidg 4592 |
. . . . . . . . . 10
⊢ (𝑍 ∈ (𝑋 ∖ 𝑌) → 𝑍 ∈ {𝑍}) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ {𝑍}) |
5 | | elun2 4107 |
. . . . . . . . 9
⊢ (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ∈ (𝑌 ∪ {𝑍})) |
7 | | hoidmvlelem2.w |
. . . . . . . 8
⊢ 𝑊 = (𝑌 ∪ {𝑍}) |
8 | 6, 7 | eleqtrrdi 2850 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑊) |
9 | 1, 8 | ffvelrnd 6944 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℝ) |
10 | | hoidmvlelem2.b |
. . . . . . 7
⊢ (𝜑 → 𝐵:𝑊⟶ℝ) |
11 | 10, 8 | ffvelrnd 6944 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝑍) ∈ ℝ) |
12 | | hoidmvlelem2.v |
. . . . . . . 8
⊢ 𝑉 = ({(𝐵‘𝑍)} ∪ 𝑂) |
13 | 11 | snssd 4739 |
. . . . . . . . 9
⊢ (𝜑 → {(𝐵‘𝑍)} ⊆ ℝ) |
14 | | hoidmvlelem2.O |
. . . . . . . . . 10
⊢ 𝑂 = ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) |
15 | | nfv 1918 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝜑 |
16 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) = (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) |
17 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝜑) |
18 | | fz1ssnn 13216 |
. . . . . . . . . . . . . 14
⊢
(1...𝑀) ⊆
ℕ |
19 | | elrabi 3611 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑖 ∈ (1...𝑀)) |
20 | 18, 19 | sselid 3915 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑖 ∈ ℕ) |
21 | 20 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑖 ∈ ℕ) |
22 | | eleq1w 2821 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝑗 ∈ ℕ ↔ 𝑖 ∈ ℕ)) |
23 | 22 | anbi2d 628 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝜑 ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ 𝑖 ∈ ℕ))) |
24 | | fveq2 6756 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (𝐷‘𝑗) = (𝐷‘𝑖)) |
25 | 24 | fveq1d 6758 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍)) |
26 | 25 | eleq1d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → (((𝐷‘𝑗)‘𝑍) ∈ ℝ ↔ ((𝐷‘𝑖)‘𝑍) ∈ ℝ)) |
27 | 23, 26 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ))) |
28 | | hoidmvlelem2.d |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷:ℕ⟶(ℝ ↑m
𝑊)) |
29 | 28 | ffvelrnda 6943 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗) ∈ (ℝ ↑m 𝑊)) |
30 | | elmapi 8595 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷‘𝑗) ∈ (ℝ ↑m 𝑊) → (𝐷‘𝑗):𝑊⟶ℝ) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐷‘𝑗):𝑊⟶ℝ) |
32 | 8 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ 𝑊) |
33 | 31, 32 | ffvelrnd 6944 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
34 | 27, 33 | chvarvv 2003 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ) |
35 | 17, 21, 34 | syl2anc 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐷‘𝑖)‘𝑍) ∈ ℝ) |
36 | 15, 16, 35 | rnmptssd 42624 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ⊆ ℝ) |
37 | 14, 36 | eqsstrid 3965 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 ⊆ ℝ) |
38 | 13, 37 | unssd 4116 |
. . . . . . . 8
⊢ (𝜑 → ({(𝐵‘𝑍)} ∪ 𝑂) ⊆ ℝ) |
39 | 12, 38 | eqsstrid 3965 |
. . . . . . 7
⊢ (𝜑 → 𝑉 ⊆ ℝ) |
40 | | hoidmvlelem2.q |
. . . . . . . 8
⊢ 𝑄 = inf(𝑉, ℝ, < ) |
41 | | ltso 10986 |
. . . . . . . . . 10
⊢ < Or
ℝ |
42 | 41 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → < Or
ℝ) |
43 | | snfi 8788 |
. . . . . . . . . . . 12
⊢ {(𝐵‘𝑍)} ∈ Fin |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → {(𝐵‘𝑍)} ∈ Fin) |
45 | | fzfi 13620 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑀) ∈
Fin |
46 | | rabfi 8973 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∈ Fin
→ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin |
48 | 47 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin) |
49 | 16 | rnmptfi 42596 |
. . . . . . . . . . . . 13
⊢ ({𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∈ Fin → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ∈ Fin) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ∈ Fin) |
51 | 14, 50 | eqeltrid 2843 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑂 ∈ Fin) |
52 | | unfi 8917 |
. . . . . . . . . . 11
⊢ (({(𝐵‘𝑍)} ∈ Fin ∧ 𝑂 ∈ Fin) → ({(𝐵‘𝑍)} ∪ 𝑂) ∈ Fin) |
53 | 44, 51, 52 | syl2anc 583 |
. . . . . . . . . 10
⊢ (𝜑 → ({(𝐵‘𝑍)} ∪ 𝑂) ∈ Fin) |
54 | 12, 53 | eqeltrid 2843 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ Fin) |
55 | | fvex 6769 |
. . . . . . . . . . . . . 14
⊢ (𝐵‘𝑍) ∈ V |
56 | 55 | snid 4594 |
. . . . . . . . . . . . 13
⊢ (𝐵‘𝑍) ∈ {(𝐵‘𝑍)} |
57 | | elun1 4106 |
. . . . . . . . . . . . 13
⊢ ((𝐵‘𝑍) ∈ {(𝐵‘𝑍)} → (𝐵‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐵‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂) |
59 | 12 | eqcomi 2747 |
. . . . . . . . . . . 12
⊢ ({(𝐵‘𝑍)} ∪ 𝑂) = 𝑉 |
60 | 58, 59 | eleqtri 2837 |
. . . . . . . . . . 11
⊢ (𝐵‘𝑍) ∈ 𝑉 |
61 | 60 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵‘𝑍) ∈ 𝑉) |
62 | | ne0i 4265 |
. . . . . . . . . 10
⊢ ((𝐵‘𝑍) ∈ 𝑉 → 𝑉 ≠ ∅) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ≠ ∅) |
64 | | fiinfcl 9190 |
. . . . . . . . 9
⊢ (( <
Or ℝ ∧ (𝑉 ∈
Fin ∧ 𝑉 ≠ ∅
∧ 𝑉 ⊆ ℝ))
→ inf(𝑉, ℝ, <
) ∈ 𝑉) |
65 | 42, 54, 63, 39, 64 | syl13anc 1370 |
. . . . . . . 8
⊢ (𝜑 → inf(𝑉, ℝ, < ) ∈ 𝑉) |
66 | 40, 65 | eqeltrid 2843 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
67 | 39, 66 | sseldd 3918 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ ℝ) |
68 | | hoidmvlelem2.u |
. . . . . . . . . . . 12
⊢ 𝑈 = {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} |
69 | | ssrab2 4009 |
. . . . . . . . . . . 12
⊢ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍)) |
70 | 68, 69 | eqsstri 3951 |
. . . . . . . . . . 11
⊢ 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍)) |
71 | 70 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ⊆ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
72 | 9, 11 | iccssred 13095 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘𝑍)[,](𝐵‘𝑍)) ⊆ ℝ) |
73 | 71, 72 | sstrd 3927 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ ℝ) |
74 | | hoidmvlelem2.su |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑈) |
75 | 73, 74 | sseldd 3918 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℝ) |
76 | 9 | rexrd 10956 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘𝑍) ∈
ℝ*) |
77 | 11 | rexrd 10956 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵‘𝑍) ∈
ℝ*) |
78 | 70, 74 | sselid 3915 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
79 | | iccgelb 13064 |
. . . . . . . . 9
⊢ (((𝐴‘𝑍) ∈ ℝ* ∧ (𝐵‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) → (𝐴‘𝑍) ≤ 𝑆) |
80 | 76, 77, 78, 79 | syl3anc 1369 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘𝑍) ≤ 𝑆) |
81 | | hoidmvlelem2.sb |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 < (𝐵‘𝑍)) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < (𝐵‘𝑍)) |
83 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐵‘𝑍) → 𝑥 = (𝐵‘𝑍)) |
84 | 83 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐵‘𝑍) → (𝐵‘𝑍) = 𝑥) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → (𝐵‘𝑍) = 𝑥) |
86 | 82, 85 | breqtrd 5096 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥) |
87 | 86 | adantlr 711 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥) |
88 | | simpll 763 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝜑) |
89 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑉) |
90 | 89, 12 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
91 | 90 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
92 | | elsni 4575 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {(𝐵‘𝑍)} → 𝑥 = (𝐵‘𝑍)) |
93 | 92 | con3i 154 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 = (𝐵‘𝑍) → ¬ 𝑥 ∈ {(𝐵‘𝑍)}) |
94 | 93 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → ¬ 𝑥 ∈ {(𝐵‘𝑍)}) |
95 | | elunnel1 4080 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ({(𝐵‘𝑍)} ∪ 𝑂) ∧ ¬ 𝑥 ∈ {(𝐵‘𝑍)}) → 𝑥 ∈ 𝑂) |
96 | 91, 94, 95 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑉 ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ 𝑂) |
97 | 96 | adantll 710 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑥 ∈ 𝑂) |
98 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑂 → 𝑥 ∈ 𝑂) |
99 | 98, 14 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑂 → 𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍))) |
100 | | vex 3426 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
101 | 16 | elrnmpt 5854 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ↔ ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍))) |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍)) ↔ ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍)) |
103 | 99, 102 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑂 → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍)) |
104 | 103 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍)) |
105 | | fveq2 6756 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = 𝑖 → (𝐶‘𝑗) = (𝐶‘𝑖)) |
106 | 105 | fveq1d 6758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑖 → ((𝐶‘𝑗)‘𝑍) = ((𝐶‘𝑖)‘𝑍)) |
107 | 106 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍) ∈ ℝ ↔ ((𝐶‘𝑖)‘𝑍) ∈ ℝ)) |
108 | 23, 107 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑖 → (((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) ↔ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ ℝ))) |
109 | | hoidmvlelem2.c |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐶:ℕ⟶(ℝ ↑m
𝑊)) |
110 | 109 | ffvelrnda 6943 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗) ∈ (ℝ ↑m 𝑊)) |
111 | | elmapi 8595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐶‘𝑗) ∈ (ℝ ↑m 𝑊) → (𝐶‘𝑗):𝑊⟶ℝ) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐶‘𝑗):𝑊⟶ℝ) |
113 | 112, 32 | ffvelrnd 6944 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
114 | 108, 113 | chvarvv 2003 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈ ℝ) |
115 | 114 | rexrd 10956 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐶‘𝑖)‘𝑍) ∈
ℝ*) |
116 | 17, 21, 115 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐶‘𝑖)‘𝑍) ∈
ℝ*) |
117 | 34 | rexrd 10956 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝐷‘𝑖)‘𝑍) ∈
ℝ*) |
118 | 17, 21, 117 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → ((𝐷‘𝑖)‘𝑍) ∈
ℝ*) |
119 | 106, 25 | oveq12d 7273 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑖 → (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) = (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
120 | 119 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 𝑖 → (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) ↔ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
121 | 120 | elrab 3617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↔ (𝑖 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
122 | 121 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑖 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍)))) |
123 | 122 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
124 | 123 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) |
125 | | icoltub 42936 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐶‘𝑖)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑖)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑖)‘𝑍)[,)((𝐷‘𝑖)‘𝑍))) → 𝑆 < ((𝐷‘𝑖)‘𝑍)) |
126 | 116, 118,
124, 125 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) → 𝑆 < ((𝐷‘𝑖)‘𝑍)) |
127 | 126 | 3adant3 1130 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → 𝑆 < ((𝐷‘𝑖)‘𝑍)) |
128 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑥 = ((𝐷‘𝑖)‘𝑍)) |
129 | 128 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ((𝐷‘𝑖)‘𝑍) → ((𝐷‘𝑖)‘𝑍) = 𝑥) |
130 | 129 | 3ad2ant3 1133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → ((𝐷‘𝑖)‘𝑍) = 𝑥) |
131 | 127, 130 | breqtrd 5096 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ 𝑥 = ((𝐷‘𝑖)‘𝑍)) → 𝑆 < 𝑥) |
132 | 131 | 3exp 1117 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥))) |
133 | 132 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} → (𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥))) |
134 | 133 | rexlimdv 3211 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → (∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}𝑥 = ((𝐷‘𝑖)‘𝑍) → 𝑆 < 𝑥)) |
135 | 104, 134 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝑆 < 𝑥) |
136 | 88, 97, 135 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ ¬ 𝑥 = (𝐵‘𝑍)) → 𝑆 < 𝑥) |
137 | 87, 136 | pm2.61dan 809 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑆 < 𝑥) |
138 | 137 | ralrimiva 3107 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑉 𝑆 < 𝑥) |
139 | | breq2 5074 |
. . . . . . . . . . 11
⊢ (𝑥 = inf(𝑉, ℝ, < ) → (𝑆 < 𝑥 ↔ 𝑆 < inf(𝑉, ℝ, < ))) |
140 | 139 | rspcva 3550 |
. . . . . . . . . 10
⊢
((inf(𝑉, ℝ,
< ) ∈ 𝑉 ∧
∀𝑥 ∈ 𝑉 𝑆 < 𝑥) → 𝑆 < inf(𝑉, ℝ, < )) |
141 | 65, 138, 140 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 < inf(𝑉, ℝ, < )) |
142 | 40 | eqcomi 2747 |
. . . . . . . . . 10
⊢ inf(𝑉, ℝ, < ) = 𝑄 |
143 | 142 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → inf(𝑉, ℝ, < ) = 𝑄) |
144 | 141, 143 | breqtrd 5096 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 < 𝑄) |
145 | 9, 75, 67, 80, 144 | lelttrd 11063 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘𝑍) < 𝑄) |
146 | 9, 67, 145 | ltled 11053 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝑍) ≤ 𝑄) |
147 | | fiminre 11852 |
. . . . . . . . 9
⊢ ((𝑉 ⊆ ℝ ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) →
∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦) |
148 | 39, 54, 63, 147 | syl3anc 1369 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦) |
149 | | lbinfle 11860 |
. . . . . . . 8
⊢ ((𝑉 ⊆ ℝ ∧
∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦 ∧ (𝐵‘𝑍) ∈ 𝑉) → inf(𝑉, ℝ, < ) ≤ (𝐵‘𝑍)) |
150 | 39, 148, 61, 149 | syl3anc 1369 |
. . . . . . 7
⊢ (𝜑 → inf(𝑉, ℝ, < ) ≤ (𝐵‘𝑍)) |
151 | 40, 150 | eqbrtrid 5105 |
. . . . . 6
⊢ (𝜑 → 𝑄 ≤ (𝐵‘𝑍)) |
152 | 9, 11, 67, 146, 151 | eliccd 42932 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍))) |
153 | 67 | recnd 10934 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℂ) |
154 | 75 | recnd 10934 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℂ) |
155 | 9 | recnd 10934 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘𝑍) ∈ ℂ) |
156 | 153, 154,
155 | npncand 11286 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍))) = (𝑄 − (𝐴‘𝑍))) |
157 | 156 | eqcomd 2744 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 − (𝐴‘𝑍)) = ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍)))) |
158 | 157 | oveq2d 7271 |
. . . . . . 7
⊢ (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) = (𝐺 · ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍))))) |
159 | | rge0ssre 13117 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
160 | | hoidmvlelem2.g |
. . . . . . . . . . 11
⊢ 𝐺 = ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) |
161 | | hoidmvlelem2.l |
. . . . . . . . . . . 12
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) |
162 | | hoidmvlelem2.x |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ Fin) |
163 | | hoidmvlelem2.y |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
164 | 162, 163 | ssfid 8971 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ Fin) |
165 | | ssun1 4102 |
. . . . . . . . . . . . . . 15
⊢ 𝑌 ⊆ (𝑌 ∪ {𝑍}) |
166 | 165, 7 | sseqtrri 3954 |
. . . . . . . . . . . . . 14
⊢ 𝑌 ⊆ 𝑊 |
167 | 166 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ⊆ 𝑊) |
168 | 1, 167 | fssresd 6625 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ↾ 𝑌):𝑌⟶ℝ) |
169 | 10, 167 | fssresd 6625 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ↾ 𝑌):𝑌⟶ℝ) |
170 | 161, 164,
168, 169 | hoidmvcl 44010 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 ↾ 𝑌)(𝐿‘𝑌)(𝐵 ↾ 𝑌)) ∈ (0[,)+∞)) |
171 | 160, 170 | eqeltrid 2843 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (0[,)+∞)) |
172 | 159, 171 | sselid 3915 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ ℝ) |
173 | 172 | recnd 10934 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ℂ) |
174 | 153, 154 | subcld 11262 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 − 𝑆) ∈ ℂ) |
175 | 154, 155 | subcld 11262 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 − (𝐴‘𝑍)) ∈ ℂ) |
176 | 173, 174,
175 | adddid 10930 |
. . . . . . 7
⊢ (𝜑 → (𝐺 · ((𝑄 − 𝑆) + (𝑆 − (𝐴‘𝑍)))) = ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍))))) |
177 | 173, 174 | mulcld 10926 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · (𝑄 − 𝑆)) ∈ ℂ) |
178 | 173, 175 | mulcld 10926 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℂ) |
179 | 177, 178 | addcomd 11107 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) = ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆)))) |
180 | 158, 176,
179 | 3eqtrd 2782 |
. . . . . 6
⊢ (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) = ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆)))) |
181 | 67, 75 | jca 511 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄 ∈ ℝ ∧ 𝑆 ∈ ℝ)) |
182 | | resubcl 11215 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑄 − 𝑆) ∈ ℝ) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 − 𝑆) ∈ ℝ) |
184 | 172, 183 | jca 511 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∈ ℝ ∧ (𝑄 − 𝑆) ∈ ℝ)) |
185 | | remulcl 10887 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ ℝ ∧ (𝑄 − 𝑆) ∈ ℝ) → (𝐺 · (𝑄 − 𝑆)) ∈ ℝ) |
186 | 184, 185 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 · (𝑄 − 𝑆)) ∈ ℝ) |
187 | 75, 9 | jca 511 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∈ ℝ ∧ (𝐴‘𝑍) ∈ ℝ)) |
188 | | resubcl 11215 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℝ ∧ (𝐴‘𝑍) ∈ ℝ) → (𝑆 − (𝐴‘𝑍)) ∈ ℝ) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 − (𝐴‘𝑍)) ∈ ℝ) |
190 | 172, 189 | jca 511 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 ∈ ℝ ∧ (𝑆 − (𝐴‘𝑍)) ∈ ℝ)) |
191 | | remulcl 10887 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ ℝ ∧ (𝑆 − (𝐴‘𝑍)) ∈ ℝ) → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ) |
192 | 190, 191 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ) |
193 | 186, 192 | jca 511 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺 · (𝑄 − 𝑆)) ∈ ℝ ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ)) |
194 | | readdcl 10885 |
. . . . . . . . 9
⊢ (((𝐺 · (𝑄 − 𝑆)) ∈ ℝ ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ∈ ℝ) → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) ∈ ℝ) |
195 | 193, 194 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺 · (𝑄 − 𝑆)) + (𝐺 · (𝑆 − (𝐴‘𝑍)))) ∈ ℝ) |
196 | 179, 195 | eqeltrrd 2840 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ∈ ℝ) |
197 | | 1red 10907 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
198 | | hoidmvlelem2.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
199 | 198 | rpred 12701 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℝ) |
200 | 197, 199 | readdcld 10935 |
. . . . . . . . 9
⊢ (𝜑 → (1 + 𝐸) ∈ ℝ) |
201 | 2 | eldifbd 3896 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑍 ∈ 𝑌) |
202 | 8, 201 | eldifd 3894 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ (𝑊 ∖ 𝑌)) |
203 | | hoidmvlelem2.r |
. . . . . . . . . 10
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)(𝐷‘𝑗)))) ∈ ℝ) |
204 | | hoidmvlelem2.h |
. . . . . . . . . 10
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) |
205 | 161, 164,
202, 7, 109, 28, 203, 204, 75 | sge0hsphoire 44017 |
. . . . . . . . 9
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |
206 | 200, 205 | remulcld 10936 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ) |
207 | | fzfid 13621 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
208 | 183 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − 𝑆) ∈ ℝ) |
209 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝜑) |
210 | | elfznn 13214 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
211 | 210 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
212 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ) |
213 | | ovexd 7290 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ V) |
214 | | hoidmvlelem2.p |
. . . . . . . . . . . . . . . . 17
⊢ 𝑃 = (𝑗 ∈ ℕ ↦ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
215 | 214 | fvmpt2 6868 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ℕ ∧ ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ V) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
216 | 212, 213,
215 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
217 | 216 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
218 | 164 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ∈ Fin) |
219 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑌 ⊆ 𝑊) |
220 | 112, 219 | fssresd 6625 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ) |
221 | 220 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ) |
222 | | iftrue 4462 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌)) |
223 | 222 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌)) |
224 | 223 | feq1d 6569 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ ((𝐶‘𝑗) ↾ 𝑌):𝑌⟶ℝ)) |
225 | 221, 224 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
226 | | 0red 10909 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑌) → 0 ∈ ℝ) |
227 | | hoidmvlelem2.f |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐹 = (𝑦 ∈ 𝑌 ↦ 0) |
228 | 226, 227 | fmptd 6970 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝑌⟶ℝ) |
229 | 228 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝐹:𝑌⟶ℝ) |
230 | | iffalse 4465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = 𝐹) |
231 | 230 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = 𝐹) |
232 | 231 | feq1d 6569 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ 𝐹:𝑌⟶ℝ)) |
233 | 229, 232 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
234 | 225, 233 | pm2.61dan 809 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
235 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
236 | | fvex 6769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐶‘𝑗) ∈ V |
237 | 236 | resex 5928 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶‘𝑗) ↾ 𝑌) ∈ V |
238 | 237 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐶‘𝑗) ↾ 𝑌) ∈ V) |
239 | 162, 163 | ssexd 5243 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑌 ∈ V) |
240 | | mptexg 7079 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑌 ∈ V → (𝑦 ∈ 𝑌 ↦ 0) ∈ V) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 0) ∈ V) |
242 | 227, 241 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹 ∈ V) |
243 | 238, 242 | ifcld 4502 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V) |
244 | 243 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V) |
245 | | hoidmvlelem2.j |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
246 | 245 | fvmpt2 6868 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
247 | 235, 244,
246 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
248 | 247 | feq1d 6569 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐽‘𝑗):𝑌⟶ℝ ↔ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)) |
249 | 234, 248 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐽‘𝑗):𝑌⟶ℝ) |
250 | 31, 219 | fssresd 6625 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ) |
251 | 250 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ) |
252 | | iftrue 4462 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌)) |
253 | 252 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌)) |
254 | 253 | feq1d 6569 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ ((𝐷‘𝑗) ↾ 𝑌):𝑌⟶ℝ)) |
255 | 251, 254 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
256 | | iffalse 4465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = 𝐹) |
257 | 256 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = 𝐹) |
258 | 257 | feq1d 6569 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ ↔ 𝐹:𝑌⟶ℝ)) |
259 | 229, 258 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
260 | 255, 259 | pm2.61dan 809 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ) |
261 | | fvex 6769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷‘𝑗) ∈ V |
262 | 261 | resex 5928 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷‘𝑗) ↾ 𝑌) ∈ V |
263 | 262 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐷‘𝑗) ↾ 𝑌) ∈ V) |
264 | 263, 242 | ifcld 4502 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V) |
265 | 264 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V) |
266 | | hoidmvlelem2.k |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐾 = (𝑗 ∈ ℕ ↦ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
267 | 266 | fvmpt2 6868 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ ∧ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) ∈ V) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
268 | 235, 265,
267 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
269 | 268 | feq1d 6569 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐾‘𝑗):𝑌⟶ℝ ↔ if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹):𝑌⟶ℝ)) |
270 | 260, 269 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐾‘𝑗):𝑌⟶ℝ) |
271 | 161, 218,
249, 270 | hoidmvcl 44010 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) ∈ (0[,)+∞)) |
272 | 217, 271 | eqeltrd 2839 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ (0[,)+∞)) |
273 | 159, 272 | sselid 3915 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ ℝ) |
274 | 209, 211,
273 | syl2anc 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃‘𝑗) ∈ ℝ) |
275 | 208, 274 | remulcld 10936 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ) |
276 | 207, 275 | fsumrecl 15374 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ) |
277 | 200, 276 | remulcld 10936 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
278 | 206, 277 | readdcld 10935 |
. . . . . . 7
⊢ (𝜑 → (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) ∈ ℝ) |
279 | 161, 164,
202, 7, 109, 28, 203, 204, 67 | sge0hsphoire 44017 |
. . . . . . . 8
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) |
280 | 200, 279 | remulcld 10936 |
. . . . . . 7
⊢ (𝜑 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) ∈ ℝ) |
281 | 74, 68 | eleqtrdi 2849 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}) |
282 | | oveq1 7262 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 → (𝑧 − (𝐴‘𝑍)) = (𝑆 − (𝐴‘𝑍))) |
283 | 282 | oveq2d 7271 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · (𝑆 − (𝐴‘𝑍)))) |
284 | | fveq2 6756 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑆 → (𝐻‘𝑧) = (𝐻‘𝑆)) |
285 | 284 | fveq1d 6758 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑆 → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘𝑆)‘(𝐷‘𝑗))) |
286 | 285 | oveq2d 7271 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑆 → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
287 | 286 | mpteq2dv 5172 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑆 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) |
288 | 287 | fveq2d 6760 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑆 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) |
289 | 288 | oveq2d 7271 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑆 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
290 | 283, 289 | breq12d 5083 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑆 → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
291 | 290 | elrab 3617 |
. . . . . . . . . 10
⊢ (𝑆 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ (𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
292 | 281, 291 | sylib 217 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
293 | 292 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · (𝑆 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
294 | 207, 274 | fsumrecl 15374 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) ∈ ℝ) |
295 | 200, 294 | remulcld 10936 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) ∈ ℝ) |
296 | | 0red 10909 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) |
297 | 75, 67 | posdifd 11492 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 < 𝑄 ↔ 0 < (𝑄 − 𝑆))) |
298 | 144, 297 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝑄 − 𝑆)) |
299 | 296, 183,
298 | ltled 11053 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝑄 − 𝑆)) |
300 | | hoidmvlelem2.le |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗))) |
301 | 172, 295,
183, 299, 300 | lemul1ad 11844 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 · (𝑄 − 𝑆)) ≤ (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆))) |
302 | 200 | recnd 10934 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 + 𝐸) ∈ ℂ) |
303 | 294 | recnd 10934 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) ∈ ℂ) |
304 | 302, 303,
174 | mulassd 10929 |
. . . . . . . . . 10
⊢ (𝜑 → (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆)) = ((1 + 𝐸) · (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆)))) |
305 | 274 | recnd 10934 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑃‘𝑗) ∈ ℂ) |
306 | 207, 174,
305 | fsummulc1 15425 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑃‘𝑗) · (𝑄 − 𝑆))) |
307 | 174 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − 𝑆) ∈ ℂ) |
308 | 305, 307 | mulcomd 10927 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑃‘𝑗) · (𝑄 − 𝑆)) = ((𝑄 − 𝑆) · (𝑃‘𝑗))) |
309 | 308 | sumeq2dv 15343 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) |
310 | 306, 309 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆)) = Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) |
311 | 310 | oveq2d 7271 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + 𝐸) · (Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗) · (𝑄 − 𝑆))) = ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
312 | 304, 311 | eqtrd 2778 |
. . . . . . . . 9
⊢ (𝜑 → (((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)(𝑃‘𝑗)) · (𝑄 − 𝑆)) = ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
313 | 301, 312 | breqtrd 5096 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 · (𝑄 − 𝑆)) ≤ ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
314 | 192, 186,
206, 277, 293, 313 | leadd12dd 42745 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ≤ (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
315 | | hoidmvlelem2.m |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℕ) |
316 | | nnsplit 42787 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ℕ =
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
317 | 315, 316 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℕ = ((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
318 | | uncom 4083 |
. . . . . . . . . . . . . . . . 17
⊢
((1...𝑀) ∪
(ℤ≥‘(𝑀 + 1))) =
((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) |
319 | 318 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((1...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) =
((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀))) |
320 | 317, 319 | eqtr2d 2779 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) = ℕ) |
321 | 320 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ =
((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀))) |
322 | 321 | mpteq1d 5165 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) = (𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) |
323 | 322 | fveq2d 6760 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) |
324 | | nfv 1918 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝜑 |
325 | | fvexd 6771 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ∈ V) |
326 | | ovexd 7290 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝑀) ∈ V) |
327 | | incom 4131 |
. . . . . . . . . . . . . . 15
⊢
((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ((1...𝑀) ∩ (ℤ≥‘(𝑀 + 1))) |
328 | | nnuzdisj 42784 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∩
(ℤ≥‘(𝑀 + 1))) = ∅ |
329 | 327, 328 | eqtri 2766 |
. . . . . . . . . . . . . 14
⊢
((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ∅ |
330 | 329 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((ℤ≥‘(𝑀 + 1)) ∩ (1...𝑀)) = ∅) |
331 | | icossicc 13097 |
. . . . . . . . . . . . . 14
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
332 | | ssid 3939 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ (0[,)+∞) |
333 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑) |
334 | 315 | peano2nnd 11920 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 + 1) ∈ ℕ) |
335 | | uznnssnn 12564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 + 1) ∈ ℕ →
(ℤ≥‘(𝑀 + 1)) ⊆ ℕ) |
336 | 334, 335 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ ℕ) |
337 | 336 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) →
(ℤ≥‘(𝑀 + 1)) ⊆ ℕ) |
338 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈
(ℤ≥‘(𝑀 + 1))) |
339 | 337, 338 | sseldd 3918 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈
ℕ) |
340 | | snfi 8788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑍} ∈ Fin |
341 | 340 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → {𝑍} ∈ Fin) |
342 | | unfi 8917 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑌 ∪ {𝑍}) ∈ Fin) |
343 | 164, 341,
342 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑌 ∪ {𝑍}) ∈ Fin) |
344 | 7, 343 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑊 ∈ Fin) |
345 | 344 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑊 ∈ Fin) |
346 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑙 → (𝑗 ∈ 𝑌 ↔ 𝑙 ∈ 𝑌)) |
347 | | fveq2 6756 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑙 → (𝑐‘𝑗) = (𝑐‘𝑙)) |
348 | 347 | breq1d 5080 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = 𝑙 → ((𝑐‘𝑗) ≤ 𝑥 ↔ (𝑐‘𝑙) ≤ 𝑥)) |
349 | 348, 347 | ifbieq1d 4480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 = 𝑙 → if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥) = if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥)) |
350 | 346, 347,
349 | ifbieq12d 4484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑙 → if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)) = if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))) |
351 | 350 | cbvmptv 5183 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))) = (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))) |
352 | 351 | mpteq2i 5175 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ (ℝ
↑m 𝑊)
↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥)))) = (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥)))) |
353 | 352 | mpteq2i 5175 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ
↑m 𝑊)
↦ (𝑗 ∈ 𝑊 ↦ if(𝑗 ∈ 𝑌, (𝑐‘𝑗), if((𝑐‘𝑗) ≤ 𝑥, (𝑐‘𝑗), 𝑥))))) = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))))) |
354 | 204, 353 | eqtri 2766 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑊) ↦ (𝑙 ∈ 𝑊 ↦ if(𝑙 ∈ 𝑌, (𝑐‘𝑙), if((𝑐‘𝑙) ≤ 𝑥, (𝑐‘𝑙), 𝑥))))) |
355 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℝ) |
356 | 354, 355,
345, 31 | hsphoif 44004 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑆)‘(𝐷‘𝑗)):𝑊⟶ℝ) |
357 | 161, 345,
112, 356 | hoidmvcl 44010 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
358 | 333, 339,
357 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
359 | 332, 358 | sselid 3915 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
360 | 331, 359 | sselid 3915 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
361 | 209, 211,
357 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
362 | 331, 361 | sselid 3915 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
363 | 324, 325,
326, 330, 360, 362 | sge0splitmpt 43839 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
364 | | nnex 11909 |
. . . . . . . . . . . . . . 15
⊢ ℕ
∈ V |
365 | 364 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ ∈
V) |
366 | 331, 357 | sselid 3915 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
367 | 324, 365,
366, 205, 336 | sge0ssrempt 43833 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |
368 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...𝑀) ⊆ ℕ) |
369 | 324, 365,
366, 205, 368 | sge0ssrempt 43833 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) |
370 | | rexadd 12895 |
. . . . . . . . . . . . 13
⊢
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ ∧
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℝ) →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
371 | 367, 369,
370 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
372 | 323, 363,
371 | 3eqtrd 2782 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) |
373 | 372 | oveq2d 7271 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))))) |
374 | 373 | oveq1d 7270 |
. . . . . . . . 9
⊢ (𝜑 → (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = (((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
375 | 372, 205 | eqeltrrd 2840 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℝ) |
376 | 375 | recnd 10934 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) ∈ ℂ) |
377 | 276 | recnd 10934 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ) |
378 | 302, 376,
377 | adddid 10930 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + 𝐸) ·
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = (((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
379 | 378 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → (((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) ·
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
380 | 367 | recnd 10934 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℂ) |
381 | 369 | recnd 10934 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ∈ ℂ) |
382 | 380, 381,
377 | addassd 10928 |
. . . . . . . . . . 11
⊢ (𝜑 →
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
383 | 207, 361 | sge0fsummpt 43818 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) = Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
384 | 383 | oveq1d 7270 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
385 | | ax-resscn 10859 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℂ |
386 | 159, 385 | sstri 3926 |
. . . . . . . . . . . . . . . . 17
⊢
(0[,)+∞) ⊆ ℂ |
387 | 386, 357 | sselid 3915 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℂ) |
388 | 209, 211,
387 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℂ) |
389 | 183 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑄 − 𝑆) ∈ ℝ) |
390 | 389, 273 | remulcld 10936 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℝ) |
391 | 390 | recnd 10934 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ) |
392 | 211, 391 | syldan 590 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) ∈ ℂ) |
393 | 207, 388,
392 | fsumadd 15380 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
394 | 393 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
395 | 384, 394 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) = Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
396 | 395 | oveq2d 7271 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
((Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
397 | 382, 396 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (𝜑 →
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))) |
398 | 397 | oveq2d 7271 |
. . . . . . . . 9
⊢ (𝜑 → ((1 + 𝐸) ·
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))))) |
399 | 374, 379,
398 | 3eqtrd 2782 |
. . . . . . . 8
⊢ (𝜑 → (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) = ((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))))) |
400 | 159, 357 | sselid 3915 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ∈ ℝ) |
401 | 400, 390 | readdcld 10935 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
402 | 209, 211,
401 | syl2anc 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
403 | 207, 402 | fsumrecl 15374 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
404 | 367, 403 | readdcld 10935 |
. . . . . . . . 9
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ∈ ℝ) |
405 | | 0le1 11428 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
406 | 405 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 1) |
407 | 198 | rpge0d 12705 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝐸) |
408 | 197, 199,
406, 407 | addge0d 11481 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (1 + 𝐸)) |
409 | 67 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑄 ∈ ℝ) |
410 | 354, 409,
345, 31 | hsphoif 44004 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐻‘𝑄)‘(𝐷‘𝑗)):𝑊⟶ℝ) |
411 | 161, 345,
112, 410 | hoidmvcl 44010 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
412 | 331, 411 | sselid 3915 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
413 | 324, 365,
412, 279, 336 | sge0ssrempt 43833 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) |
414 | 159, 411 | sselid 3915 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ) |
415 | 209, 211,
414 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ) |
416 | 207, 415 | fsumrecl 15374 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ ℝ) |
417 | 333, 339,
412 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
418 | 202 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑊 ∖ 𝑌)) |
419 | 75, 67, 144 | ltled 11053 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ≤ 𝑄) |
420 | 419 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ≤ 𝑄) |
421 | 161, 345,
418, 7, 355, 409, 420, 354, 112, 31 | hsphoidmvle2 44013 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
422 | 333, 339,
421 | syl2anc 583 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
423 | 324, 325,
360, 417, 422 | sge0lempt 43838 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) ≤
(Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
424 | 209 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → 𝜑) |
425 | 211 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → 𝑗 ∈ ℕ) |
426 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → (𝑃‘𝑗) = 0) |
427 | | oveq2 7263 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃‘𝑗) = 0 → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = ((𝑄 − 𝑆) · 0)) |
428 | 427 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = ((𝑄 − 𝑆) · 0)) |
429 | 174 | mul01d 11104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑄 − 𝑆) · 0) = 0) |
430 | 429 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · 0) = 0) |
431 | 428, 430 | eqtrd 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝑄 − 𝑆) · (𝑃‘𝑗)) = 0) |
432 | 431 | oveq2d 7271 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0)) |
433 | 387 | addid1d 11105 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
434 | 433 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + 0) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
435 | 432, 434 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))) |
436 | 421 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
437 | 435, 436 | eqbrtrd 5092 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
438 | 424, 425,
426, 437 | syl21anc 834 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
439 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (𝜑 ∧ 𝑗 ∈ (1...𝑀))) |
440 | | neqne 2950 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝑃‘𝑗) = 0 → (𝑃‘𝑗) ≠ 0) |
441 | 440 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (𝑃‘𝑗) ≠ 0) |
442 | 402 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ∈ ℝ) |
443 | 209 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝜑) |
444 | 211 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ ℕ) |
445 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (𝑃‘𝑗) ≠ 0) |
446 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑍 ∈ (𝑋 ∖ 𝑌)) |
447 | 201 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ¬ 𝑍 ∈ 𝑌) |
448 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
∏𝑘 ∈
𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) |
449 | 161, 218,
446, 447, 7, 112, 356, 448 | hoiprodp1 44016 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))))) |
450 | 449 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))))) |
451 | 217 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
452 | 218 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑌 ∈ Fin) |
453 | 217 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
454 | | fveq2 6756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑌 = ∅ → (𝐿‘𝑌) = (𝐿‘∅)) |
455 | 454 | oveqd 7272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑌 = ∅ → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗))) |
456 | 455 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗))) |
457 | 249 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐽‘𝑗):𝑌⟶ℝ) |
458 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑌 = ∅ → 𝑌 = ∅) |
459 | 458 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑌 = ∅ → ∅ =
𝑌) |
460 | 459 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ∅ = 𝑌) |
461 | 460 | feq2d 6570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗):∅⟶ℝ ↔ (𝐽‘𝑗):𝑌⟶ℝ)) |
462 | 457, 461 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐽‘𝑗):∅⟶ℝ) |
463 | 270 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐾‘𝑗):𝑌⟶ℝ) |
464 | 460 | feq2d 6570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐾‘𝑗):∅⟶ℝ ↔ (𝐾‘𝑗):𝑌⟶ℝ)) |
465 | 463, 464 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝐾‘𝑗):∅⟶ℝ) |
466 | 161, 462,
465 | hoidmv0val 44011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → ((𝐽‘𝑗)(𝐿‘∅)(𝐾‘𝑗)) = 0) |
467 | 453, 456,
466 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = 0) |
468 | 467 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑌 = ∅) → (𝑃‘𝑗) = 0) |
469 | | neneq 2948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃‘𝑗) ≠ 0 → ¬ (𝑃‘𝑗) = 0) |
470 | 469 | ad2antlr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑌 = ∅) → ¬ (𝑃‘𝑗) = 0) |
471 | 468, 470 | pm2.65da 813 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ¬ 𝑌 = ∅) |
472 | 471 | neqned 2949 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑌 ≠ ∅) |
473 | 249 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗):𝑌⟶ℝ) |
474 | 270 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗):𝑌⟶ℝ) |
475 | 161, 452,
472, 473, 474 | hoidmvn0val 44012 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘)))) |
476 | 247 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
477 | 217 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
478 | 247 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐽‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹)) |
479 | 478, 231 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐽‘𝑗) = 𝐹) |
480 | 268 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
481 | 480, 257 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐾‘𝑗) = 𝐹) |
482 | 479, 481 | oveq12d 7273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = (𝐹(𝐿‘𝑌)𝐹)) |
483 | 161, 164,
228 | hoidmvval0b 44018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝐹(𝐿‘𝑌)𝐹) = 0) |
484 | 483 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝐹(𝐿‘𝑌)𝐹) = 0) |
485 | 477, 482,
484 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = 0) |
486 | 485 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → (𝑃‘𝑗) = 0) |
487 | 469 | ad2antlr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ¬ (𝑃‘𝑗) = 0) |
488 | 486, 487 | condan 814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
489 | 488 | iftrued 4464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐶‘𝑗) ↾ 𝑌), 𝐹) = ((𝐶‘𝑗) ↾ 𝑌)) |
490 | 476, 489 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐽‘𝑗) = ((𝐶‘𝑗) ↾ 𝑌)) |
491 | 490 | fveq1d 6758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)‘𝑘) = (((𝐶‘𝑗) ↾ 𝑌)‘𝑘)) |
492 | 491 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐽‘𝑗)‘𝑘) = (((𝐶‘𝑗) ↾ 𝑌)‘𝑘)) |
493 | | fvres 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ 𝑌 → (((𝐶‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐶‘𝑗)‘𝑘)) |
494 | 493 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐶‘𝑗)‘𝑘)) |
495 | 492, 494 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐽‘𝑗)‘𝑘) = ((𝐶‘𝑗)‘𝑘)) |
496 | 268 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗) = if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹)) |
497 | 488, 252 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)), ((𝐷‘𝑗) ↾ 𝑌), 𝐹) = ((𝐷‘𝑗) ↾ 𝑌)) |
498 | 496, 497 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝐾‘𝑗) = ((𝐷‘𝑗) ↾ 𝑌)) |
499 | 498 | fveq1d 6758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐾‘𝑗)‘𝑘) = (((𝐷‘𝑗) ↾ 𝑌)‘𝑘)) |
500 | 499 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐾‘𝑗)‘𝑘) = (((𝐷‘𝑗) ↾ 𝑌)‘𝑘)) |
501 | | fvres 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ 𝑌 → (((𝐷‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
502 | 501 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐷‘𝑗) ↾ 𝑌)‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
503 | 500, 502 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → ((𝐾‘𝑗)‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
504 | 495, 503 | oveq12d 7273 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
505 | 504 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
506 | 505 | prodeq2dv 15561 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐽‘𝑗)‘𝑘)[,)((𝐾‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
507 | 475, 506 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗)) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
508 | 355 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑆 ∈ ℝ) |
509 | 345 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑊 ∈ Fin) |
510 | 31 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (𝐷‘𝑗):𝑊⟶ℝ) |
511 | | elun1 4106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ (𝑌 ∪ {𝑍})) |
512 | 511, 7 | eleqtrrdi 2850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈ 𝑌 → 𝑘 ∈ 𝑊) |
513 | 512 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑘 ∈ 𝑊) |
514 | 354, 508,
509, 510, 513 | hsphoival 44007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆))) |
515 | | iftrue 4462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ 𝑌 → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆)) = ((𝐷‘𝑗)‘𝑘)) |
516 | 515 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑆, ((𝐷‘𝑗)‘𝑘), 𝑆)) = ((𝐷‘𝑗)‘𝑘)) |
517 | 514, 516 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
518 | 517 | oveq2d 7271 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
519 | 518 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
520 | 519 | prodeq2dv 15561 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
521 | 520 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘)))) |
522 | 521 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘)))) |
523 | 451, 507,
522 | 3eqtrrd 2783 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗)) |
524 | 354, 355,
345, 31, 32 | hsphoival 44007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))) |
525 | 201 | iffalsed 4467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) |
526 | 525 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) |
527 | 524, 526 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) |
528 | 527 | oveq2d 7271 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))) |
529 | 528 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆))) |
530 | 113 | rexrd 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈
ℝ*) |
531 | 530 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ∈
ℝ*) |
532 | 33 | rexrd 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐷‘𝑗)‘𝑍) ∈
ℝ*) |
533 | 532 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈
ℝ*) |
534 | | icoltub 42936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → 𝑆 < ((𝐷‘𝑗)‘𝑍)) |
535 | 531, 533,
488, 534 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 < ((𝐷‘𝑗)‘𝑍)) |
536 | 355 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ ℝ) |
537 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
538 | 536, 537 | ltnled 11052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (𝑆 < ((𝐷‘𝑗)‘𝑍) ↔ ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑆)) |
539 | 535, 538 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑆) |
540 | 539 | iffalsed 4467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆) = 𝑆) |
541 | 540 | oveq2d 7271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)if(((𝐷‘𝑗)‘𝑍) ≤ 𝑆, ((𝐷‘𝑗)‘𝑍), 𝑆)) = (((𝐶‘𝑗)‘𝑍)[,)𝑆)) |
542 | 529, 541 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)𝑆)) |
543 | 542 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆))) |
544 | | volico 43414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ 𝑆 ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0)) |
545 | 113, 536,
544 | syl2an 595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0)) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0)) |
546 | 545 | anabss5 664 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑆)) = if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0)) |
547 | | iftrue 4462 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐶‘𝑗)‘𝑍) < 𝑆 → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
548 | 547 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
549 | | iffalse 4465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
((𝐶‘𝑗)‘𝑍) < 𝑆 → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = 0) |
550 | 549 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = 0) |
551 | | simpll 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (𝜑 ∧ 𝑗 ∈ ℕ)) |
552 | | icogelb 13059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ* ∧ ((𝐷‘𝑗)‘𝑍) ∈ ℝ* ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆) |
553 | 531, 533,
488, 552 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆) |
554 | 553 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆) |
555 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) |
556 | 554, 555 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (((𝐶‘𝑗)‘𝑍) ≤ 𝑆 ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆)) |
557 | 551, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
558 | 551, 355 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → 𝑆 ∈ ℝ) |
559 | 557, 558 | eqleltd 11049 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → (((𝐶‘𝑗)‘𝑍) = 𝑆 ↔ (((𝐶‘𝑗)‘𝑍) ≤ 𝑆 ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆))) |
560 | 556, 559 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → ((𝐶‘𝑗)‘𝑍) = 𝑆) |
561 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐶‘𝑗)‘𝑍) = 𝑆 → ((𝐶‘𝑗)‘𝑍) = 𝑆) |
562 | 561 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐶‘𝑗)‘𝑍) = 𝑆 → 𝑆 = ((𝐶‘𝑗)‘𝑍)) |
563 | 562 | oveq1d 7270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐶‘𝑗)‘𝑍) = 𝑆 → (𝑆 − ((𝐶‘𝑗)‘𝑍)) = (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍))) |
564 | 563 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) = (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍))) |
565 | 385, 113 | sselid 3915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)‘𝑍) ∈ ℂ) |
566 | 565 | subidd 11250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍)) = 0) |
567 | 566 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → (((𝐶‘𝑗)‘𝑍) − ((𝐶‘𝑗)‘𝑍)) = 0) |
568 | 564, 567 | eqtr2d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ ((𝐶‘𝑗)‘𝑍) = 𝑆) → 0 = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
569 | 551, 560,
568 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → 0 = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
570 | 550, 569 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐶‘𝑗)‘𝑍) < 𝑆) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
571 | 548, 570 | pm2.61dan 809 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐶‘𝑗)‘𝑍) < 𝑆, (𝑆 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
572 | 543, 546,
571 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍))) = (𝑆 − ((𝐶‘𝑗)‘𝑍))) |
573 | 523, 572 | oveq12d 7273 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑆)‘(𝐷‘𝑗))‘𝑍)))) = ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍)))) |
574 | 386, 272 | sselid 3915 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑃‘𝑗) ∈ ℂ) |
575 | 355, 113 | resubcld 11333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) ∈ ℝ) |
576 | 575 | recnd 10934 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑆 − ((𝐶‘𝑗)‘𝑍)) ∈ ℂ) |
577 | 574, 576 | mulcomd 10927 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
578 | 577 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝑃‘𝑗) · (𝑆 − ((𝐶‘𝑗)‘𝑍))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
579 | 450, 573,
578 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) = ((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
580 | 579 | oveq1d 7270 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
581 | 174 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝑄 − 𝑆) ∈ ℂ) |
582 | 576, 581,
574 | adddird 10931 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) |
583 | 582 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗))) |
584 | 583 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗)) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗))) |
585 | 576, 581 | addcomd 11107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) = ((𝑄 − 𝑆) + (𝑆 − ((𝐶‘𝑗)‘𝑍)))) |
586 | 153 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑄 ∈ ℂ) |
587 | 154 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → 𝑆 ∈ ℂ) |
588 | 586, 587,
565 | npncand 11286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑄 − 𝑆) + (𝑆 − ((𝐶‘𝑗)‘𝑍))) = (𝑄 − ((𝐶‘𝑗)‘𝑍))) |
589 | 585, 588 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) = (𝑄 − ((𝐶‘𝑗)‘𝑍))) |
590 | 589 | oveq1d 7270 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
591 | 590 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝑆 − ((𝐶‘𝑗)‘𝑍)) + (𝑄 − 𝑆)) · (𝑃‘𝑗)) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
592 | 580, 584,
591 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
593 | 443, 444,
445, 592 | syl21anc 834 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
594 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∏𝑘 ∈
𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) |
595 | 161, 218,
32, 447, 7, 112, 410, 594 | hoiprodp1 44016 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))))) |
596 | 209, 211,
595 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))))) |
597 | 596 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))))) |
598 | 507 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) = ((𝐽‘𝑗)(𝐿‘𝑌)(𝐾‘𝑗))) |
599 | 409 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → 𝑄 ∈ ℝ) |
600 | 354, 599,
509, 510, 513 | hsphoival 44007 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘) = if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄))) |
601 | | iftrue 4462 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ 𝑌 → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄)) = ((𝐷‘𝑗)‘𝑘)) |
602 | 601 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → if(𝑘 ∈ 𝑌, ((𝐷‘𝑗)‘𝑘), if(((𝐷‘𝑗)‘𝑘) ≤ 𝑄, ((𝐷‘𝑗)‘𝑘), 𝑄)) = ((𝐷‘𝑗)‘𝑘)) |
603 | 600, 602 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘) = ((𝐷‘𝑗)‘𝑘)) |
604 | 603 | oveq2d 7271 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘)) = (((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘))) |
605 | 604 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑌) → (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
606 | 605 | prodeq2dv 15561 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
607 | 606 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)((𝐷‘𝑗)‘𝑘)))) |
608 | 598, 607,
451 | 3eqtr4d 2788 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗)) |
609 | 443, 444,
445, 608 | syl21anc 834 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) = (𝑃‘𝑗)) |
610 | 354, 409,
345, 31, 32 | hsphoival 44007 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄))) |
611 | 211, 610 | syldan 590 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄))) |
612 | 611 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄))) |
613 | 201 | iffalsed 4467 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) |
614 | 613 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(𝑍 ∈ 𝑌, ((𝐷‘𝑗)‘𝑍), if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) = if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄)) |
615 | 211, 33 | syldan 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
616 | 615 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
617 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) = 𝑄) |
618 | 616, 617 | eqled 11008 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ≤ 𝑄) |
619 | 618 | iftrued 4464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = ((𝐷‘𝑗)‘𝑍)) |
620 | 619, 617 | eqtrd 2778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄) |
621 | 620 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄) |
622 | 67 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑄 ∈ ℝ) |
623 | 622 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ∈ ℝ) |
624 | 623 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ∈ ℝ) |
625 | 615 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
626 | 625 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ∈ ℝ) |
627 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 = inf(𝑉, ℝ, < )) |
628 | 443, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑉 ⊆ ℝ) |
629 | 148 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦) |
630 | | simplr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ (1...𝑀)) |
631 | 210, 488 | sylanl2 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))) |
632 | 630, 631 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (𝑗 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
633 | | rabid 3304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↔ (𝑗 ∈ (1...𝑀) ∧ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍)))) |
634 | 632, 633 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))}) |
635 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍)) |
636 | | fveq2 6756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑖 = 𝑗 → (𝐷‘𝑖) = (𝐷‘𝑗)) |
637 | 636 | fveq1d 6758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑖 = 𝑗 → ((𝐷‘𝑖)‘𝑍) = ((𝐷‘𝑗)‘𝑍)) |
638 | 637 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑖 = 𝑗 → (((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍) ↔ ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍))) |
639 | 638 | rspcev 3552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑗 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ∧ ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑗)‘𝑍)) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍)) |
640 | 634, 635,
639 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ∃𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ((𝐷‘𝑗)‘𝑍) = ((𝐷‘𝑖)‘𝑍)) |
641 | | fvexd 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ V) |
642 | 16, 640, 641 | elrnmptd 5859 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ran (𝑖 ∈ {𝑗 ∈ (1...𝑀) ∣ 𝑆 ∈ (((𝐶‘𝑗)‘𝑍)[,)((𝐷‘𝑗)‘𝑍))} ↦ ((𝐷‘𝑖)‘𝑍))) |
643 | 642, 14 | eleqtrrdi 2850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ 𝑂) |
644 | | elun2 4107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐷‘𝑗)‘𝑍) ∈ 𝑂 → ((𝐷‘𝑗)‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
645 | 643, 644 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ ({(𝐵‘𝑍)} ∪ 𝑂)) |
646 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ({(𝐵‘𝑍)} ∪ 𝑂) = 𝑉) |
647 | 645, 646 | eleqtrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐷‘𝑗)‘𝑍) ∈ 𝑉) |
648 | | lbinfle 11860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑉 ⊆ ℝ ∧
∃𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 𝑥 ≤ 𝑦 ∧ ((𝐷‘𝑗)‘𝑍) ∈ 𝑉) → inf(𝑉, ℝ, < ) ≤ ((𝐷‘𝑗)‘𝑍)) |
649 | 628, 629,
647, 648 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → inf(𝑉, ℝ, < ) ≤ ((𝐷‘𝑗)‘𝑍)) |
650 | 627, 649 | eqbrtrd 5092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 ≤ ((𝐷‘𝑗)‘𝑍)) |
651 | 650 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 ≤ ((𝐷‘𝑗)‘𝑍)) |
652 | | neqne 2950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
((𝐷‘𝑗)‘𝑍) = 𝑄 → ((𝐷‘𝑗)‘𝑍) ≠ 𝑄) |
653 | 652 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ((𝐷‘𝑗)‘𝑍) ≠ 𝑄) |
654 | 624, 626,
651, 653 | leneltd 11059 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → 𝑄 < ((𝐷‘𝑗)‘𝑍)) |
655 | 624, 626 | ltnled 11052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → (𝑄 < ((𝐷‘𝑗)‘𝑍) ↔ ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑄)) |
656 | 654, 655 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → ¬ ((𝐷‘𝑗)‘𝑍) ≤ 𝑄) |
657 | 656 | iffalsed 4467 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) ∧ ¬ ((𝐷‘𝑗)‘𝑍) = 𝑄) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄) |
658 | 621, 657 | pm2.61dan 809 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐷‘𝑗)‘𝑍) ≤ 𝑄, ((𝐷‘𝑗)‘𝑍), 𝑄) = 𝑄) |
659 | 612, 614,
658 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍) = 𝑄) |
660 | 659 | oveq2d 7271 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)) = (((𝐶‘𝑗)‘𝑍)[,)𝑄)) |
661 | 660 | fveq2d 6760 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))) = (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄))) |
662 | 209, 211,
113 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
663 | 662 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ∈ ℝ) |
664 | 443, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑄 ∈ ℝ) |
665 | | volico 43414 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐶‘𝑗)‘𝑍) ∈ ℝ ∧ 𝑄 ∈ ℝ) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄)) = if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0)) |
666 | 663, 664,
665 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)𝑄)) = if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0)) |
667 | 443, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 ∈ ℝ) |
668 | 443, 444,
445, 553 | syl21anc 834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) ≤ 𝑆) |
669 | 443, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → 𝑆 < 𝑄) |
670 | 663, 667,
664, 668, 669 | lelttrd 11063 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)‘𝑍) < 𝑄) |
671 | 670 | iftrued 4464 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → if(((𝐶‘𝑗)‘𝑍) < 𝑄, (𝑄 − ((𝐶‘𝑗)‘𝑍)), 0) = (𝑄 − ((𝐶‘𝑗)‘𝑍))) |
672 | 661, 666,
671 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍))) = (𝑄 − ((𝐶‘𝑗)‘𝑍))) |
673 | 609, 672 | oveq12d 7273 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (∏𝑘 ∈ 𝑌 (vol‘(((𝐶‘𝑗)‘𝑘)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑘))) · (vol‘(((𝐶‘𝑗)‘𝑍)[,)(((𝐻‘𝑄)‘(𝐷‘𝑗))‘𝑍)))) = ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍)))) |
674 | 209, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝑄 ∈ ℂ) |
675 | 385, 662 | sselid 3915 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)‘𝑍) ∈ ℂ) |
676 | 674, 675 | subcld 11262 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝑄 − ((𝐶‘𝑗)‘𝑍)) ∈ ℂ) |
677 | 305, 676 | mulcomd 10927 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
678 | 677 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝑃‘𝑗) · (𝑄 − ((𝐶‘𝑗)‘𝑍))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
679 | 597, 673,
678 | 3eqtrd 2782 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) = ((𝑄 − ((𝐶‘𝑗)‘𝑍)) · (𝑃‘𝑗))) |
680 | 593, 679 | eqtr4d 2781 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
681 | 442, 680 | eqled 11008 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ (𝑃‘𝑗) ≠ 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
682 | 439, 441,
681 | syl2anc 583 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ ¬ (𝑃‘𝑗) = 0) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
683 | 438, 682 | pm2.61dan 809 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
684 | 207, 402,
415, 683 | fsumle 15439 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))) ≤ Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
685 | 367, 403,
413, 416, 423, 684 | leadd12dd 42745 |
. . . . . . . . . 10
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) |
686 | 321 | mpteq1d 5165 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) = (𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) |
687 | 686 | fveq2d 6760 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
688 | 211, 412 | syldan 590 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,]+∞)) |
689 | 324, 325,
326, 330, 417, 688 | sge0splitmpt 43839 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ((ℤ≥‘(𝑀 + 1)) ∪ (1...𝑀)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
690 | 687, 689 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
691 | 209, 211,
411 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))) ∈ (0[,)+∞)) |
692 | 207, 691 | sge0fsummpt 43818 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) = Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
693 | 692, 416 | eqeltrd 2839 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) |
694 | | rexadd 12895 |
. . . . . . . . . . . 12
⊢
(((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ ∧
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) ∈ ℝ) →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
695 | 413, 693,
694 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +𝑒
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
696 | 692 | oveq2d 7271 |
. . . . . . . . . . 11
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) +
(Σ^‘(𝑗 ∈ (1...𝑀) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) =
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) |
697 | 690, 695,
696 | 3eqtrrd 2783 |
. . . . . . . . . 10
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
698 | 685, 697 | breqtrd 5096 |
. . . . . . . . 9
⊢ (𝜑 →
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
699 | 404, 279,
200, 408, 698 | lemul2ad 11845 |
. . . . . . . 8
⊢ (𝜑 → ((1 + 𝐸) ·
((Σ^‘(𝑗 ∈ (ℤ≥‘(𝑀 + 1)) ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))))) + Σ𝑗 ∈ (1...𝑀)(((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗))) + ((𝑄 − 𝑆) · (𝑃‘𝑗))))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
700 | 399, 699 | eqbrtrd 5092 |
. . . . . . 7
⊢ (𝜑 → (((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑆)‘(𝐷‘𝑗)))))) + ((1 + 𝐸) · Σ𝑗 ∈ (1...𝑀)((𝑄 − 𝑆) · (𝑃‘𝑗)))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
701 | 196, 278,
280, 314, 700 | letrd 11062 |
. . . . . 6
⊢ (𝜑 → ((𝐺 · (𝑆 − (𝐴‘𝑍))) + (𝐺 · (𝑄 − 𝑆))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
702 | 180, 701 | eqbrtrd 5092 |
. . . . 5
⊢ (𝜑 → (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
703 | 152, 702 | jca 511 |
. . . 4
⊢ (𝜑 → (𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))) |
704 | | oveq1 7262 |
. . . . . . 7
⊢ (𝑧 = 𝑄 → (𝑧 − (𝐴‘𝑍)) = (𝑄 − (𝐴‘𝑍))) |
705 | 704 | oveq2d 7271 |
. . . . . 6
⊢ (𝑧 = 𝑄 → (𝐺 · (𝑧 − (𝐴‘𝑍))) = (𝐺 · (𝑄 − (𝐴‘𝑍)))) |
706 | | fveq2 6756 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑄 → (𝐻‘𝑧) = (𝐻‘𝑄)) |
707 | 706 | fveq1d 6758 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑄 → ((𝐻‘𝑧)‘(𝐷‘𝑗)) = ((𝐻‘𝑄)‘(𝐷‘𝑗))) |
708 | 707 | oveq2d 7271 |
. . . . . . . . 9
⊢ (𝑧 = 𝑄 → ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))) = ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))) |
709 | 708 | mpteq2dv 5172 |
. . . . . . . 8
⊢ (𝑧 = 𝑄 → (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))) = (𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))) |
710 | 709 | fveq2d 6760 |
. . . . . . 7
⊢ (𝑧 = 𝑄 →
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))) |
711 | 710 | oveq2d 7271 |
. . . . . 6
⊢ (𝑧 = 𝑄 → ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) = ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗))))))) |
712 | 705, 711 | breq12d 5083 |
. . . . 5
⊢ (𝑧 = 𝑄 → ((𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗)))))) ↔ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))) |
713 | 712 | elrab 3617 |
. . . 4
⊢ (𝑄 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))} ↔ (𝑄 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∧ (𝐺 · (𝑄 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑄)‘(𝐷‘𝑗)))))))) |
714 | 703, 713 | sylibr 233 |
. . 3
⊢ (𝜑 → 𝑄 ∈ {𝑧 ∈ ((𝐴‘𝑍)[,](𝐵‘𝑍)) ∣ (𝐺 · (𝑧 − (𝐴‘𝑍))) ≤ ((1 + 𝐸) ·
(Σ^‘(𝑗 ∈ ℕ ↦ ((𝐶‘𝑗)(𝐿‘𝑊)((𝐻‘𝑧)‘(𝐷‘𝑗))))))}) |
715 | 714, 68 | eleqtrrdi 2850 |
. 2
⊢ (𝜑 → 𝑄 ∈ 𝑈) |
716 | | breq2 5074 |
. . 3
⊢ (𝑢 = 𝑄 → (𝑆 < 𝑢 ↔ 𝑆 < 𝑄)) |
717 | 716 | rspcev 3552 |
. 2
⊢ ((𝑄 ∈ 𝑈 ∧ 𝑆 < 𝑄) → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |
718 | 715, 144,
717 | syl2anc 583 |
1
⊢ (𝜑 → ∃𝑢 ∈ 𝑈 𝑆 < 𝑢) |