Step |
Hyp |
Ref |
Expression |
1 |
|
hoidmvlelem4.l |
⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) |
2 |
|
hoidmvlelem4.x |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
3 |
|
hoidmvlelem4.y |
⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 ) |
4 |
|
hoidmvlelem4.n |
⊢ ( 𝜑 → 𝑌 ≠ ∅ ) |
5 |
|
hoidmvlelem4.z |
⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) ) |
6 |
|
hoidmvlelem4.w |
⊢ 𝑊 = ( 𝑌 ∪ { 𝑍 } ) |
7 |
|
hoidmvlelem4.a |
⊢ ( 𝜑 → 𝐴 : 𝑊 ⟶ ℝ ) |
8 |
|
hoidmvlelem4.b |
⊢ ( 𝜑 → 𝐵 : 𝑊 ⟶ ℝ ) |
9 |
|
hoidmvlelem4.k |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) |
10 |
|
hoidmvlelem4.c |
⊢ ( 𝜑 → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) ) |
11 |
|
hoidmvlelem4.d |
⊢ ( 𝜑 → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) ) |
12 |
|
hoidmvlelem4.r |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) |
13 |
|
hoidmvlelem4.h |
⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) ) |
14 |
|
hoidmvlelem4.14 |
⊢ 𝐺 = ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) |
15 |
|
hoidmvlelem4.e |
⊢ ( 𝜑 → 𝐸 ∈ ℝ+ ) |
16 |
|
hoidmvlelem4.u |
⊢ 𝑈 = { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } |
17 |
|
hoidmvlelem4.s |
⊢ 𝑆 = sup ( 𝑈 , ℝ , < ) |
18 |
|
hoidmvlelem4.i |
⊢ ( 𝜑 → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) ) |
19 |
|
hoidmvlelem4.i2 |
⊢ ( 𝜑 → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
20 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
21 |
5
|
eldifad |
⊢ ( 𝜑 → 𝑍 ∈ 𝑋 ) |
22 |
|
snssi |
⊢ ( 𝑍 ∈ 𝑋 → { 𝑍 } ⊆ 𝑋 ) |
23 |
21 22
|
syl |
⊢ ( 𝜑 → { 𝑍 } ⊆ 𝑋 ) |
24 |
3 23
|
unssd |
⊢ ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) ⊆ 𝑋 ) |
25 |
6 24
|
eqsstrid |
⊢ ( 𝜑 → 𝑊 ⊆ 𝑋 ) |
26 |
|
ssfi |
⊢ ( ( 𝑋 ∈ Fin ∧ 𝑊 ⊆ 𝑋 ) → 𝑊 ∈ Fin ) |
27 |
2 25 26
|
syl2anc |
⊢ ( 𝜑 → 𝑊 ∈ Fin ) |
28 |
1 27 7 8
|
hoidmvcl |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ( 0 [,) +∞ ) ) |
29 |
20 28
|
sselid |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ∈ ℝ ) |
30 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
31 |
15
|
rpred |
⊢ ( 𝜑 → 𝐸 ∈ ℝ ) |
32 |
30 31
|
readdcld |
⊢ ( 𝜑 → ( 1 + 𝐸 ) ∈ ℝ ) |
33 |
|
nfv |
⊢ Ⅎ 𝑗 𝜑 |
34 |
|
nnex |
⊢ ℕ ∈ V |
35 |
34
|
a1i |
⊢ ( 𝜑 → ℕ ∈ V ) |
36 |
|
icossicc |
⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) |
37 |
27
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑊 ∈ Fin ) |
38 |
10
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) ) |
39 |
|
elmapi |
⊢ ( ( 𝐶 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ ) |
40 |
38 39
|
syl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐶 ‘ 𝑗 ) : 𝑊 ⟶ ℝ ) |
41 |
|
eleq1 |
⊢ ( 𝑗 = ℎ → ( 𝑗 ∈ 𝑌 ↔ ℎ ∈ 𝑌 ) ) |
42 |
|
fveq2 |
⊢ ( 𝑗 = ℎ → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ ℎ ) ) |
43 |
42
|
breq1d |
⊢ ( 𝑗 = ℎ → ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝑐 ‘ ℎ ) ≤ 𝑥 ) ) |
44 |
43 42
|
ifbieq1d |
⊢ ( 𝑗 = ℎ → if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) = if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) |
45 |
41 42 44
|
ifbieq12d |
⊢ ( 𝑗 = ℎ → if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) = if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) |
46 |
45
|
cbvmptv |
⊢ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) = ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) |
47 |
46
|
mpteq2i |
⊢ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) |
48 |
47
|
mpteq2i |
⊢ ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗 ∈ 𝑊 ↦ if ( 𝑗 ∈ 𝑌 , ( 𝑐 ‘ 𝑗 ) , if ( ( 𝑐 ‘ 𝑗 ) ≤ 𝑥 , ( 𝑐 ‘ 𝑗 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) ) |
49 |
13 48
|
eqtri |
⊢ 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( ℎ ∈ 𝑊 ↦ if ( ℎ ∈ 𝑌 , ( 𝑐 ‘ ℎ ) , if ( ( 𝑐 ‘ ℎ ) ≤ 𝑥 , ( 𝑐 ‘ ℎ ) , 𝑥 ) ) ) ) ) |
50 |
|
snidg |
⊢ ( 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) → 𝑍 ∈ { 𝑍 } ) |
51 |
5 50
|
syl |
⊢ ( 𝜑 → 𝑍 ∈ { 𝑍 } ) |
52 |
|
elun2 |
⊢ ( 𝑍 ∈ { 𝑍 } → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) ) |
53 |
51 52
|
syl |
⊢ ( 𝜑 → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) ) |
54 |
6
|
a1i |
⊢ ( 𝜑 → 𝑊 = ( 𝑌 ∪ { 𝑍 } ) ) |
55 |
54
|
eqcomd |
⊢ ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) = 𝑊 ) |
56 |
53 55
|
eleqtrd |
⊢ ( 𝜑 → 𝑍 ∈ 𝑊 ) |
57 |
8 56
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) |
58 |
57
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) |
59 |
11
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) ) |
60 |
|
elmapi |
⊢ ( ( 𝐷 ‘ 𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ ) |
61 |
59 60
|
syl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐷 ‘ 𝑗 ) : 𝑊 ⟶ ℝ ) |
62 |
49 58 37 61
|
hsphoif |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) : 𝑊 ⟶ ℝ ) |
63 |
1 37 40 62
|
hoidmvcl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,) +∞ ) ) |
64 |
36 63
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ( 0 [,] +∞ ) ) |
65 |
33 35 64
|
sge0clmpt |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ) |
66 |
33 35 64
|
sge0xrclmpt |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ* ) |
67 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
68 |
67
|
a1i |
⊢ ( 𝜑 → +∞ ∈ ℝ* ) |
69 |
12
|
rexrd |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ* ) |
70 |
1 37 40 61
|
hoidmvcl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,) +∞ ) ) |
71 |
36 70
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ∈ ( 0 [,] +∞ ) ) |
72 |
5
|
eldifbd |
⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝑌 ) |
73 |
56 72
|
eldifd |
⊢ ( 𝜑 → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) ) |
74 |
73
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑍 ∈ ( 𝑊 ∖ 𝑌 ) ) |
75 |
1 37 74 6 58 49 40 61
|
hsphoidmvle |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ≤ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) |
76 |
33 35 64 71 75
|
sge0lempt |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) |
77 |
12
|
ltpnfd |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) < +∞ ) |
78 |
66 69 68 76 77
|
xrlelttrd |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) < +∞ ) |
79 |
66 68 78
|
xrltned |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ ) |
80 |
|
ge0xrre |
⊢ ( ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ≠ +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ ) |
81 |
65 79 80
|
syl2anc |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ ) |
82 |
32 81
|
remulcld |
⊢ ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℝ ) |
83 |
32 12
|
remulcld |
⊢ ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℝ ) |
84 |
56
|
ancli |
⊢ ( 𝜑 → ( 𝜑 ∧ 𝑍 ∈ 𝑊 ) ) |
85 |
|
eleq1 |
⊢ ( 𝑘 = 𝑍 → ( 𝑘 ∈ 𝑊 ↔ 𝑍 ∈ 𝑊 ) ) |
86 |
85
|
anbi2d |
⊢ ( 𝑘 = 𝑍 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ↔ ( 𝜑 ∧ 𝑍 ∈ 𝑊 ) ) ) |
87 |
|
fveq2 |
⊢ ( 𝑘 = 𝑍 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑍 ) ) |
88 |
|
fveq2 |
⊢ ( 𝑘 = 𝑍 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑍 ) ) |
89 |
87 88
|
breq12d |
⊢ ( 𝑘 = 𝑍 → ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ↔ ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ) |
90 |
86 89
|
imbi12d |
⊢ ( 𝑘 = 𝑍 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ) ) |
91 |
90 9
|
vtoclg |
⊢ ( 𝑍 ∈ 𝑊 → ( ( 𝜑 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) ) |
92 |
56 84 91
|
sylc |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) < ( 𝐵 ‘ 𝑍 ) ) |
93 |
1 2 3 5 6 7 8 10 11 12 13 14 15 16 17 92
|
hoidmvlelem1 |
⊢ ( 𝜑 → 𝑆 ∈ 𝑈 ) |
94 |
57
|
rexrd |
⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ) |
95 |
|
iccssxr |
⊢ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ⊆ ℝ* |
96 |
|
ssrab2 |
⊢ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) |
97 |
16 96
|
eqsstri |
⊢ 𝑈 ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) |
98 |
97 93
|
sselid |
⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) |
99 |
95 98
|
sselid |
⊢ ( 𝜑 → 𝑆 ∈ ℝ* ) |
100 |
|
simpl |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → 𝜑 ) |
101 |
|
simpr |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) |
102 |
7 56
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ ) |
103 |
102 57
|
iccssred |
⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ⊆ ℝ ) |
104 |
103 98
|
sseldd |
⊢ ( 𝜑 → 𝑆 ∈ ℝ ) |
105 |
104
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → 𝑆 ∈ ℝ ) |
106 |
100 57
|
syl |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ ) |
107 |
105 106
|
ltnled |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ( 𝑆 < ( 𝐵 ‘ 𝑍 ) ↔ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) ) |
108 |
101 107
|
mpbird |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → 𝑆 < ( 𝐵 ‘ 𝑍 ) ) |
109 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑋 ∈ Fin ) |
110 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑌 ⊆ 𝑋 ) |
111 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑍 ∈ ( 𝑋 ∖ 𝑌 ) ) |
112 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐴 : 𝑊 ⟶ ℝ ) |
113 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐵 : 𝑊 ⟶ ℝ ) |
114 |
9
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) |
115 |
|
eqid |
⊢ ( 𝑦 ∈ 𝑌 ↦ 0 ) = ( 𝑦 ∈ 𝑌 ↦ 0 ) |
116 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) ) |
117 |
|
fveq2 |
⊢ ( 𝑖 = 𝑗 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑗 ) ) |
118 |
117
|
fveq1d |
⊢ ( 𝑖 = 𝑗 → ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) = ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) ) |
119 |
|
fveq2 |
⊢ ( 𝑖 = 𝑗 → ( 𝐷 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑗 ) ) |
120 |
119
|
fveq1d |
⊢ ( 𝑖 = 𝑗 → ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) = ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) |
121 |
118 120
|
oveq12d |
⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) = ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) |
122 |
121
|
eleq2d |
⊢ ( 𝑖 = 𝑗 → ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) ) ) |
123 |
117
|
reseq1d |
⊢ ( 𝑖 = 𝑗 → ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) = ( ( 𝐶 ‘ 𝑗 ) ↾ 𝑌 ) ) |
124 |
122 123
|
ifbieq1d |
⊢ ( 𝑖 = 𝑗 → if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑗 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) |
125 |
124
|
cbvmptv |
⊢ ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑗 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) |
126 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) ) |
127 |
119
|
reseq1d |
⊢ ( 𝑖 = 𝑗 → ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) = ( ( 𝐷 ‘ 𝑗 ) ↾ 𝑌 ) ) |
128 |
122 127
|
ifbieq1d |
⊢ ( 𝑖 = 𝑗 → if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑗 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) |
129 |
128
|
cbvmptv |
⊢ ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑗 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) |
130 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ∈ ℝ ) |
131 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝐸 ∈ ℝ+ ) |
132 |
93
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑆 ∈ 𝑈 ) |
133 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → 𝑆 < ( 𝐵 ‘ 𝑍 ) ) |
134 |
|
biid |
⊢ ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) ) |
135 |
|
eqidd |
⊢ ( 𝑤 = 𝑦 → 0 = 0 ) |
136 |
135
|
cbvmptv |
⊢ ( 𝑤 ∈ 𝑌 ↦ 0 ) = ( 𝑦 ∈ 𝑌 ↦ 0 ) |
137 |
134 136
|
ifbieq2i |
⊢ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) |
138 |
137
|
mpteq2i |
⊢ ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) |
139 |
138
|
a1i |
⊢ ( 𝑙 = 𝑗 → ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ) |
140 |
|
id |
⊢ ( 𝑙 = 𝑗 → 𝑙 = 𝑗 ) |
141 |
139 140
|
fveq12d |
⊢ ( 𝑙 = 𝑗 → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) = ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ) |
142 |
134 136
|
ifbieq2i |
⊢ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) |
143 |
142
|
mpteq2i |
⊢ ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) |
144 |
143
|
a1i |
⊢ ( 𝑙 = 𝑗 → ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ) |
145 |
144 140
|
fveq12d |
⊢ ( 𝑙 = 𝑗 → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) = ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ) |
146 |
141 145
|
oveq12d |
⊢ ( 𝑙 = 𝑗 → ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) ( 𝐿 ‘ 𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) ) = ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ) ) |
147 |
146
|
cbvmptv |
⊢ ( 𝑙 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) ( 𝐿 ‘ 𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑤 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑙 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶 ‘ 𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷 ‘ 𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷 ‘ 𝑖 ) ↾ 𝑌 ) , ( 𝑦 ∈ 𝑌 ↦ 0 ) ) ) ‘ 𝑗 ) ) ) |
148 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ℎ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘 ∈ 𝑌 ( ( 𝑒 ‘ 𝑘 ) [,) ( 𝑓 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑌 ( ( ( 𝑔 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( ℎ ‘ 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿 ‘ 𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑗 ) ( 𝐿 ‘ 𝑌 ) ( ℎ ‘ 𝑗 ) ) ) ) ) ) |
149 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → X 𝑘 ∈ 𝑊 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑊 ( ( ( 𝐶 ‘ 𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷 ‘ 𝑗 ) ‘ 𝑘 ) ) ) |
150 |
|
eqid |
⊢ ( 𝑥 ∈ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) ↦ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) ) = ( 𝑥 ∈ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) ↦ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) ) |
151 |
|
fveq2 |
⊢ ( 𝑦 = 𝑘 → ( 𝐴 ‘ 𝑦 ) = ( 𝐴 ‘ 𝑘 ) ) |
152 |
|
fveq2 |
⊢ ( 𝑦 = 𝑘 → ( 𝐵 ‘ 𝑦 ) = ( 𝐵 ‘ 𝑘 ) ) |
153 |
151 152
|
oveq12d |
⊢ ( 𝑦 = 𝑘 → ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) |
154 |
153
|
cbvixpv |
⊢ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) = X 𝑘 ∈ 𝑌 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) |
155 |
|
eleq1 |
⊢ ( 𝑦 = 𝑘 → ( 𝑦 ∈ 𝑌 ↔ 𝑘 ∈ 𝑌 ) ) |
156 |
|
fveq2 |
⊢ ( 𝑦 = 𝑘 → ( 𝑥 ‘ 𝑦 ) = ( 𝑥 ‘ 𝑘 ) ) |
157 |
155 156
|
ifbieq1d |
⊢ ( 𝑦 = 𝑘 → if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) = if ( 𝑘 ∈ 𝑌 , ( 𝑥 ‘ 𝑘 ) , 𝑆 ) ) |
158 |
157
|
cbvmptv |
⊢ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) = ( 𝑘 ∈ 𝑊 ↦ if ( 𝑘 ∈ 𝑌 , ( 𝑥 ‘ 𝑘 ) , 𝑆 ) ) |
159 |
154 158
|
mpteq12i |
⊢ ( 𝑥 ∈ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) ↦ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) ) = ( 𝑥 ∈ X 𝑘 ∈ 𝑌 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ↦ ( 𝑘 ∈ 𝑊 ↦ if ( 𝑘 ∈ 𝑌 , ( 𝑥 ‘ 𝑘 ) , 𝑆 ) ) ) |
160 |
150 159
|
eqtri |
⊢ ( 𝑥 ∈ X 𝑦 ∈ 𝑌 ( ( 𝐴 ‘ 𝑦 ) [,) ( 𝐵 ‘ 𝑦 ) ) ↦ ( 𝑦 ∈ 𝑊 ↦ if ( 𝑦 ∈ 𝑌 , ( 𝑥 ‘ 𝑦 ) , 𝑆 ) ) ) = ( 𝑥 ∈ X 𝑘 ∈ 𝑌 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ↦ ( 𝑘 ∈ 𝑊 ↦ if ( 𝑘 ∈ 𝑌 , ( 𝑥 ‘ 𝑘 ) , 𝑆 ) ) ) |
161 |
1 109 110 111 6 112 113 114 115 116 125 126 129 130 13 14 131 16 132 133 147 148 149 160
|
hoidmvlelem3 |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 ) |
162 |
100 108 161
|
syl2anc |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 ) |
163 |
97
|
a1i |
⊢ ( 𝜑 → 𝑈 ⊆ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) |
164 |
163 103
|
sstrd |
⊢ ( 𝜑 → 𝑈 ⊆ ℝ ) |
165 |
164
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ⊆ ℝ ) |
166 |
|
ne0i |
⊢ ( 𝑢 ∈ 𝑈 → 𝑈 ≠ ∅ ) |
167 |
166
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑈 ≠ ∅ ) |
168 |
102
|
rexrd |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ) |
169 |
168
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ) |
170 |
94
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ) |
171 |
163
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) |
172 |
|
iccleub |
⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ∧ 𝑢 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) → 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) ) |
173 |
169 170 171 172
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) ) |
174 |
173
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) ) |
175 |
|
brralrspcev |
⊢ ( ( ( 𝐵 ‘ 𝑍 ) ∈ ℝ ∧ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ ( 𝐵 ‘ 𝑍 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑦 ) |
176 |
57 174 175
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑦 ) |
177 |
176
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑦 ) |
178 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ 𝑈 ) |
179 |
|
suprub |
⊢ ( ( ( 𝑈 ⊆ ℝ ∧ 𝑈 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑦 ) ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) ) |
180 |
165 167 177 178 179
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ sup ( 𝑈 , ℝ , < ) ) |
181 |
180 17
|
breqtrrdi |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ≤ 𝑆 ) |
182 |
181
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑆 ) |
183 |
165 178
|
sseldd |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑢 ∈ ℝ ) |
184 |
104
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → 𝑆 ∈ ℝ ) |
185 |
183 184
|
lenltd |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑈 ) → ( 𝑢 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑢 ) ) |
186 |
185
|
ralbidva |
⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝑈 𝑢 ≤ 𝑆 ↔ ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 ) ) |
187 |
182 186
|
mpbid |
⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 ) |
188 |
|
ralnex |
⊢ ( ∀ 𝑢 ∈ 𝑈 ¬ 𝑆 < 𝑢 ↔ ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 ) |
189 |
187 188
|
sylib |
⊢ ( 𝜑 → ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 ) |
190 |
189
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐵 ‘ 𝑍 ) ) → ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 ) |
191 |
100 108 190
|
syl2anc |
⊢ ( ( 𝜑 ∧ ¬ ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) → ¬ ∃ 𝑢 ∈ 𝑈 𝑆 < 𝑢 ) |
192 |
162 191
|
condan |
⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ≤ 𝑆 ) |
193 |
|
iccleub |
⊢ ( ( ( 𝐴 ‘ 𝑍 ) ∈ ℝ* ∧ ( 𝐵 ‘ 𝑍 ) ∈ ℝ* ∧ 𝑆 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ) → 𝑆 ≤ ( 𝐵 ‘ 𝑍 ) ) |
194 |
168 94 98 193
|
syl3anc |
⊢ ( 𝜑 → 𝑆 ≤ ( 𝐵 ‘ 𝑍 ) ) |
195 |
94 99 192 194
|
xrletrid |
⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) = 𝑆 ) |
196 |
16
|
eqcomi |
⊢ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } = 𝑈 |
197 |
196
|
a1i |
⊢ ( 𝜑 → { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } = 𝑈 ) |
198 |
195 197
|
eleq12d |
⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ 𝑆 ∈ 𝑈 ) ) |
199 |
93 198
|
mpbird |
⊢ ( 𝜑 → ( 𝐵 ‘ 𝑍 ) ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ) |
200 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) = ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) |
201 |
200
|
oveq2d |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) = ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) |
202 |
|
fveq2 |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ) |
203 |
202
|
fveq1d |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) = ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) |
204 |
203
|
oveq2d |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) |
205 |
204
|
mpteq2dv |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) |
206 |
205
|
fveq2d |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) |
207 |
206
|
oveq2d |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) |
208 |
201 207
|
breq12d |
⊢ ( 𝑧 = ( 𝐵 ‘ 𝑍 ) → ( ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ) |
209 |
208
|
elrab |
⊢ ( ( 𝐵 ‘ 𝑍 ) ∈ { 𝑧 ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ 𝑧 ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) } ↔ ( ( 𝐵 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ) |
210 |
199 209
|
sylib |
⊢ ( 𝜑 → ( ( 𝐵 ‘ 𝑍 ) ∈ ( ( 𝐴 ‘ 𝑍 ) [,] ( 𝐵 ‘ 𝑍 ) ) ∧ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ) |
211 |
210
|
simprd |
⊢ ( 𝜑 → ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) |
212 |
2 3
|
ssfid |
⊢ ( 𝜑 → 𝑌 ∈ Fin ) |
213 |
|
eqid |
⊢ ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) |
214 |
1 212 5 72 6 7 8 213
|
hoiprodp1 |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) = ( ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ) ) |
215 |
|
eqidd |
⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ) |
216 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐴 : 𝑊 ⟶ ℝ ) |
217 |
|
ssun1 |
⊢ 𝑌 ⊆ ( 𝑌 ∪ { 𝑍 } ) |
218 |
6
|
eqcomi |
⊢ ( 𝑌 ∪ { 𝑍 } ) = 𝑊 |
219 |
217 218
|
sseqtri |
⊢ 𝑌 ⊆ 𝑊 |
220 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝑘 ∈ 𝑌 ) |
221 |
219 220
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝑘 ∈ 𝑊 ) |
222 |
216 221
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ ) |
223 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 : 𝑊 ⟶ ℝ ) |
224 |
223 221
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) |
225 |
221 9
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) ) |
226 |
222 224 225
|
volicon0 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ) |
227 |
226
|
prodeq2dv |
⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ) |
228 |
14
|
a1i |
⊢ ( 𝜑 → 𝐺 = ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) ) |
229 |
219
|
a1i |
⊢ ( 𝜑 → 𝑌 ⊆ 𝑊 ) |
230 |
7 229
|
fssresd |
⊢ ( 𝜑 → ( 𝐴 ↾ 𝑌 ) : 𝑌 ⟶ ℝ ) |
231 |
8 229
|
fssresd |
⊢ ( 𝜑 → ( 𝐵 ↾ 𝑌 ) : 𝑌 ⟶ ℝ ) |
232 |
1 212 4 230 231
|
hoidmvn0val |
⊢ ( 𝜑 → ( ( 𝐴 ↾ 𝑌 ) ( 𝐿 ‘ 𝑌 ) ( 𝐵 ↾ 𝑌 ) ) = ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) ) |
233 |
|
fvres |
⊢ ( 𝑘 ∈ 𝑌 → ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) ) |
234 |
|
fvres |
⊢ ( 𝑘 ∈ 𝑌 → ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) ) |
235 |
233 234
|
oveq12d |
⊢ ( 𝑘 ∈ 𝑌 → ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) |
236 |
235
|
fveq2d |
⊢ ( 𝑘 ∈ 𝑌 → ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) |
237 |
236
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) ) |
238 |
|
volico |
⊢ ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) ) |
239 |
222 224 238
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) ) |
240 |
239 226
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → if ( ( 𝐴 ‘ 𝑘 ) < ( 𝐵 ‘ 𝑘 ) , ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) , 0 ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ) |
241 |
237 239 240
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) = ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ) |
242 |
241
|
prodeq2dv |
⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( ( 𝐴 ↾ 𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵 ↾ 𝑌 ) ‘ 𝑘 ) ) ) = ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ) |
243 |
228 232 242
|
3eqtrd |
⊢ ( 𝜑 → 𝐺 = ∏ 𝑘 ∈ 𝑌 ( ( 𝐵 ‘ 𝑘 ) − ( 𝐴 ‘ 𝑘 ) ) ) |
244 |
215 227 243
|
3eqtr4d |
⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) = 𝐺 ) |
245 |
102 57 92
|
volicon0 |
⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) = ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) |
246 |
244 245
|
oveq12d |
⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝑌 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) · ( vol ‘ ( ( 𝐴 ‘ 𝑍 ) [,) ( 𝐵 ‘ 𝑍 ) ) ) ) = ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) |
247 |
214 246
|
eqtrd |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) = ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ) |
248 |
247
|
breq1d |
⊢ ( 𝜑 → ( ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( ( 𝐵 ‘ 𝑍 ) − ( 𝐴 ‘ 𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ) |
249 |
211 248
|
mpbird |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) |
250 |
|
0le1 |
⊢ 0 ≤ 1 |
251 |
250
|
a1i |
⊢ ( 𝜑 → 0 ≤ 1 ) |
252 |
15
|
rpge0d |
⊢ ( 𝜑 → 0 ≤ 𝐸 ) |
253 |
30 31 251 252
|
addge0d |
⊢ ( 𝜑 → 0 ≤ ( 1 + 𝐸 ) ) |
254 |
81 12 32 253 76
|
lemul2ad |
⊢ ( 𝜑 → ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( ( 𝐻 ‘ ( 𝐵 ‘ 𝑍 ) ) ‘ ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) |
255 |
29 82 83 249 254
|
letrd |
⊢ ( 𝜑 → ( 𝐴 ( 𝐿 ‘ 𝑊 ) 𝐵 ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶 ‘ 𝑗 ) ( 𝐿 ‘ 𝑊 ) ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) |