Step |
Hyp |
Ref |
Expression |
1 |
|
dvfsum.s |
⊢ 𝑆 = ( 𝑇 (,) +∞ ) |
2 |
|
dvfsum.z |
⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 ) |
3 |
|
dvfsum.m |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
4 |
|
dvfsum.d |
⊢ ( 𝜑 → 𝐷 ∈ ℝ ) |
5 |
|
dvfsum.md |
⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) ) |
6 |
|
dvfsum.t |
⊢ ( 𝜑 → 𝑇 ∈ ℝ ) |
7 |
|
dvfsum.a |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ ) |
8 |
|
dvfsum.b1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 ) |
9 |
|
dvfsum.b2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ ) |
10 |
|
dvfsum.b3 |
⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ) |
11 |
|
dvfsum.c |
⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 ) |
12 |
|
dvfsum.u |
⊢ ( 𝜑 → 𝑈 ∈ ℝ* ) |
13 |
|
dvfsum.l |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 ) |
14 |
|
dvfsum.h |
⊢ 𝐻 = ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) |
15 |
|
dvfsumlem1.1 |
⊢ ( 𝜑 → 𝑋 ∈ 𝑆 ) |
16 |
|
dvfsumlem1.2 |
⊢ ( 𝜑 → 𝑌 ∈ 𝑆 ) |
17 |
|
dvfsumlem1.3 |
⊢ ( 𝜑 → 𝐷 ≤ 𝑋 ) |
18 |
|
dvfsumlem1.4 |
⊢ ( 𝜑 → 𝑋 ≤ 𝑌 ) |
19 |
|
dvfsumlem1.5 |
⊢ ( 𝜑 → 𝑌 ≤ 𝑈 ) |
20 |
|
dvfsumlem1.6 |
⊢ ( 𝜑 → 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) |
21 |
|
ioossre |
⊢ ( 𝑇 (,) +∞ ) ⊆ ℝ |
22 |
1 21
|
eqsstri |
⊢ 𝑆 ⊆ ℝ |
23 |
22 16
|
sseldi |
⊢ ( 𝜑 → 𝑌 ∈ ℝ ) |
24 |
15 1
|
eleqtrdi |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 (,) +∞ ) ) |
25 |
6
|
rexrd |
⊢ ( 𝜑 → 𝑇 ∈ ℝ* ) |
26 |
|
elioopnf |
⊢ ( 𝑇 ∈ ℝ* → ( 𝑋 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) ) ) |
27 |
25 26
|
syl |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) ) ) |
28 |
24 27
|
mpbid |
⊢ ( 𝜑 → ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) ) |
29 |
28
|
simpld |
⊢ ( 𝜑 → 𝑋 ∈ ℝ ) |
30 |
|
reflcl |
⊢ ( 𝑋 ∈ ℝ → ( ⌊ ‘ 𝑋 ) ∈ ℝ ) |
31 |
29 30
|
syl |
⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ∈ ℝ ) |
32 |
23 31
|
resubcld |
⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ∈ ℝ ) |
33 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑌 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) |
34 |
33
|
eleq1d |
⊢ ( 𝑦 = 𝑌 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ) ) |
35 |
22
|
a1i |
⊢ ( 𝜑 → 𝑆 ⊆ ℝ ) |
36 |
35 7 8 10
|
dvmptrecl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ ) |
37 |
36
|
fmpttd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℝ ) |
38 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐵 |
39 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 |
40 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
41 |
38 39 40
|
cbvmpt |
⊢ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
42 |
41
|
fmpt |
⊢ ( ∀ 𝑦 ∈ 𝑆 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℝ ) |
43 |
37 42
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ) |
44 |
34 43 16
|
rspcdva |
⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ) |
45 |
32 44
|
remulcld |
⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ ) |
46 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑌 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) |
47 |
46
|
eleq1d |
⊢ ( 𝑦 = 𝑌 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ ) ) |
48 |
7
|
fmpttd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℝ ) |
49 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐴 |
50 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 |
51 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) |
52 |
49 50 51
|
cbvmpt |
⊢ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) = ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) |
53 |
52
|
fmpt |
⊢ ( ∀ 𝑦 ∈ 𝑆 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℝ ) |
54 |
48 53
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ) |
55 |
47 54 16
|
rspcdva |
⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ ) |
56 |
45 55
|
resubcld |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) |
57 |
29 31
|
resubcld |
⊢ ( 𝜑 → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ∈ ℝ ) |
58 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑋 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
59 |
58
|
eleq1d |
⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) ) |
60 |
59 43 15
|
rspcdva |
⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) |
61 |
57 60
|
remulcld |
⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ ) |
62 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑋 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) |
63 |
62
|
eleq1d |
⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ ) ) |
64 |
63 54 15
|
rspcdva |
⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ ) |
65 |
61 64
|
resubcld |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) |
66 |
|
fzfid |
⊢ ( 𝜑 → ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ∈ Fin ) |
67 |
9
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ ) |
68 |
|
elfzuz |
⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
69 |
68 2
|
eleqtrrdi |
⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) → 𝑘 ∈ 𝑍 ) |
70 |
11
|
eleq1d |
⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ ) ) |
71 |
70
|
rspccva |
⊢ ( ( ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℝ ) |
72 |
67 69 71
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐶 ∈ ℝ ) |
73 |
66 72
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ∈ ℝ ) |
74 |
57 44
|
remulcld |
⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ ) |
75 |
74 64
|
resubcld |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) |
76 |
23 29
|
resubcld |
⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℝ ) |
77 |
44 76
|
remulcld |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ∈ ℝ ) |
78 |
44
|
recnd |
⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ ) |
79 |
23
|
recnd |
⊢ ( 𝜑 → 𝑌 ∈ ℂ ) |
80 |
29
|
recnd |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
81 |
78 79 80
|
subdid |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) = ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑌 ) − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) ) |
82 |
|
eqid |
⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld ) |
83 |
82
|
mulcn |
⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) |
84 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
85 |
84
|
a1i |
⊢ ( 𝜑 → +∞ ∈ ℝ* ) |
86 |
28
|
simprd |
⊢ ( 𝜑 → 𝑇 < 𝑋 ) |
87 |
23
|
ltpnfd |
⊢ ( 𝜑 → 𝑌 < +∞ ) |
88 |
|
iccssioo |
⊢ ( ( ( 𝑇 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝑇 < 𝑋 ∧ 𝑌 < +∞ ) ) → ( 𝑋 [,] 𝑌 ) ⊆ ( 𝑇 (,) +∞ ) ) |
89 |
25 85 86 87 88
|
syl22anc |
⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ( 𝑇 (,) +∞ ) ) |
90 |
89 21
|
sstrdi |
⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ ) |
91 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
92 |
90 91
|
sstrdi |
⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℂ ) |
93 |
91
|
a1i |
⊢ ( 𝜑 → ℝ ⊆ ℂ ) |
94 |
|
cncfmptc |
⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
95 |
44 92 93 94
|
syl3anc |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
96 |
|
cncfmptid |
⊢ ( ( ( 𝑋 [,] 𝑌 ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝑦 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
97 |
90 91 96
|
sylancl |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝑦 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
98 |
|
remulcl |
⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ∈ ℝ ) |
99 |
82 83 95 97 91 98
|
cncfmpt2ss |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
100 |
|
reelprrecn |
⊢ ℝ ∈ { ℝ , ℂ } |
101 |
100
|
a1i |
⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } ) |
102 |
|
ioossicc |
⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) |
103 |
102 90
|
sstrid |
⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ℝ ) |
104 |
103
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑦 ∈ ℝ ) |
105 |
104
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑦 ∈ ℂ ) |
106 |
|
1cnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → 1 ∈ ℂ ) |
107 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ ) |
108 |
107
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ ) |
109 |
|
1cnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ ) |
110 |
101
|
dvmptid |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) ) |
111 |
82
|
tgioo2 |
⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) |
112 |
|
iooretop |
⊢ ( 𝑋 (,) 𝑌 ) ∈ ( topGen ‘ ran (,) ) |
113 |
112
|
a1i |
⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ ( topGen ‘ ran (,) ) ) |
114 |
101 108 109 110 103 111 82 113
|
dvmptres |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ 1 ) ) |
115 |
101 105 106 114 78
|
dvmptcmul |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 1 ) ) ) |
116 |
78
|
mulid1d |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 1 ) = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) |
117 |
116
|
mpteq2dv |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 1 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
118 |
115 117
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
119 |
89 1
|
sseqtrrdi |
⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ 𝑆 ) |
120 |
119
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ↾ ( 𝑋 [,] 𝑌 ) ) = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) |
121 |
7
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℂ ) |
122 |
121
|
fmpttd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℂ ) |
123 |
10
|
dmeqd |
⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ) |
124 |
8
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ 𝑉 ) |
125 |
|
dmmptg |
⊢ ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = 𝑆 ) |
126 |
124 125
|
syl |
⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = 𝑆 ) |
127 |
123 126
|
eqtrd |
⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = 𝑆 ) |
128 |
|
dvcn |
⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℂ ∧ 𝑆 ⊆ ℝ ) ∧ dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℂ ) ) |
129 |
93 122 35 127 128
|
syl31anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℂ ) ) |
130 |
|
cncffvrn |
⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℂ ) ) → ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℝ ) ) |
131 |
91 129 130
|
sylancr |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℝ ) ) |
132 |
48 131
|
mpbird |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) ) |
133 |
52 132
|
eqeltrrid |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) ) |
134 |
|
rescncf |
⊢ ( ( 𝑋 [,] 𝑌 ) ⊆ 𝑆 → ( ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) → ( ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ↾ ( 𝑋 [,] 𝑌 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) ) |
135 |
119 133 134
|
sylc |
⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ↾ ( 𝑋 [,] 𝑌 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
136 |
120 135
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
137 |
54
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ) |
138 |
137
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ) |
139 |
43
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ) |
140 |
52
|
oveq2i |
⊢ ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( ℝ D ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) |
141 |
10 140 41
|
3eqtr3g |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) |
142 |
102 119
|
sstrid |
⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ 𝑆 ) |
143 |
101 138 139 141 142 111 82 113
|
dvmptres |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) |
144 |
102
|
sseli |
⊢ ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) |
145 |
|
simpl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝜑 ) |
146 |
119
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ∈ 𝑆 ) |
147 |
16
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑌 ∈ 𝑆 ) |
148 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐷 ∈ ℝ ) |
149 |
29
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑋 ∈ ℝ ) |
150 |
|
elicc2 |
⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ) ) ) |
151 |
29 23 150
|
syl2anc |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ) ) ) |
152 |
151
|
biimpa |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ) ) |
153 |
152
|
simp1d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ∈ ℝ ) |
154 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐷 ≤ 𝑋 ) |
155 |
152
|
simp2d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑋 ≤ 𝑦 ) |
156 |
148 149 153 154 155
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐷 ≤ 𝑦 ) |
157 |
152
|
simp3d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ≤ 𝑌 ) |
158 |
19
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑌 ≤ 𝑈 ) |
159 |
|
simp2r |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → 𝑌 ∈ 𝑆 ) |
160 |
|
eleq1 |
⊢ ( 𝑘 = 𝑌 → ( 𝑘 ∈ 𝑆 ↔ 𝑌 ∈ 𝑆 ) ) |
161 |
160
|
anbi2d |
⊢ ( 𝑘 = 𝑌 → ( ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ↔ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) ) |
162 |
|
breq2 |
⊢ ( 𝑘 = 𝑌 → ( 𝑦 ≤ 𝑘 ↔ 𝑦 ≤ 𝑌 ) ) |
163 |
|
breq1 |
⊢ ( 𝑘 = 𝑌 → ( 𝑘 ≤ 𝑈 ↔ 𝑌 ≤ 𝑈 ) ) |
164 |
162 163
|
3anbi23d |
⊢ ( 𝑘 = 𝑌 → ( ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ↔ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) ) |
165 |
161 164
|
3anbi23d |
⊢ ( 𝑘 = 𝑌 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) ) ) |
166 |
|
vex |
⊢ 𝑘 ∈ V |
167 |
166 11
|
csbie |
⊢ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐶 |
168 |
|
csbeq1 |
⊢ ( 𝑘 = 𝑌 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) |
169 |
167 168
|
syl5eqr |
⊢ ( 𝑘 = 𝑌 → 𝐶 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) |
170 |
169
|
breq1d |
⊢ ( 𝑘 = 𝑌 → ( 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) |
171 |
165 170
|
imbi12d |
⊢ ( 𝑘 = 𝑌 → ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ) |
172 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) |
173 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐶 |
174 |
|
nfcv |
⊢ Ⅎ 𝑥 ≤ |
175 |
173 174 39
|
nfbr |
⊢ Ⅎ 𝑥 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 |
176 |
172 175
|
nfim |
⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
177 |
|
eleq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆 ) ) |
178 |
177
|
anbi1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ↔ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ) |
179 |
|
breq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑦 ) ) |
180 |
|
breq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ 𝑘 ↔ 𝑦 ≤ 𝑘 ) ) |
181 |
179 180
|
3anbi12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ↔ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ) |
182 |
178 181
|
3anbi23d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ) ) |
183 |
40
|
breq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) |
184 |
182 183
|
imbi12d |
⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ) |
185 |
176 184 13
|
chvarfv |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
186 |
171 185
|
vtoclg |
⊢ ( 𝑌 ∈ 𝑆 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) |
187 |
159 186
|
mpcom |
⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
188 |
145 146 147 156 157 158 187
|
syl123anc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
189 |
144 188
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
190 |
29
|
rexrd |
⊢ ( 𝜑 → 𝑋 ∈ ℝ* ) |
191 |
23
|
rexrd |
⊢ ( 𝜑 → 𝑌 ∈ ℝ* ) |
192 |
|
lbicc2 |
⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) ) |
193 |
190 191 18 192
|
syl3anc |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) ) |
194 |
|
ubicc2 |
⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) ) |
195 |
190 191 18 194
|
syl3anc |
⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) ) |
196 |
|
oveq2 |
⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) |
197 |
|
oveq2 |
⊢ ( 𝑦 = 𝑌 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑌 ) ) |
198 |
29 23 99 118 136 143 189 193 195 18 196 62 197 46
|
dvle |
⊢ ( 𝜑 → ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑌 ) − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) |
199 |
81 198
|
eqbrtrd |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) |
200 |
77 55 64 199
|
lesubd |
⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) ) |
201 |
74
|
recnd |
⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℂ ) |
202 |
45
|
recnd |
⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℂ ) |
203 |
55
|
recnd |
⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℂ ) |
204 |
201 202 203
|
subsubd |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
205 |
202 201
|
negsubdi2d |
⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ) |
206 |
31
|
recnd |
⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ∈ ℂ ) |
207 |
79 80 206
|
nnncan2d |
⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) = ( 𝑌 − 𝑋 ) ) |
208 |
207
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( 𝑌 − 𝑋 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
209 |
32
|
recnd |
⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ∈ ℂ ) |
210 |
57
|
recnd |
⊢ ( 𝜑 → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ∈ ℂ ) |
211 |
209 210 78
|
subdird |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ) |
212 |
76
|
recnd |
⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℂ ) |
213 |
212 78
|
mulcomd |
⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) |
214 |
208 211 213
|
3eqtr3d |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) |
215 |
214
|
negeqd |
⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = - ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) |
216 |
205 215
|
eqtr3d |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = - ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) |
217 |
216
|
oveq1d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( - ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
218 |
77
|
recnd |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ∈ ℂ ) |
219 |
218 203
|
negsubdid |
⊢ ( 𝜑 → - ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( - ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
220 |
217 219
|
eqtr4d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = - ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
221 |
218 203
|
negsubdi2d |
⊢ ( 𝜑 → - ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) ) |
222 |
204 220 221
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) ) |
223 |
200 222
|
breqtrrd |
⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) |
224 |
64 74 56 223
|
lesubd |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) |
225 |
|
flle |
⊢ ( 𝑋 ∈ ℝ → ( ⌊ ‘ 𝑋 ) ≤ 𝑋 ) |
226 |
29 225
|
syl |
⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ≤ 𝑋 ) |
227 |
29 31
|
subge0d |
⊢ ( 𝜑 → ( 0 ≤ ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ↔ ( ⌊ ‘ 𝑋 ) ≤ 𝑋 ) ) |
228 |
226 227
|
mpbird |
⊢ ( 𝜑 → 0 ≤ ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) |
229 |
58
|
breq2d |
⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
230 |
188
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
231 |
229 230 193
|
rspcdva |
⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
232 |
44 60 57 228 231
|
lemul2ad |
⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
233 |
74 61 64 232
|
lesub1dd |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) |
234 |
56 75 65 224 233
|
letrd |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) |
235 |
56 65 73 234
|
leadd1dd |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ≤ ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ) |
236 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
|
dvfsumlem1 |
⊢ ( 𝜑 → ( 𝐻 ‘ 𝑌 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ) |
237 |
29
|
leidd |
⊢ ( 𝜑 → 𝑋 ≤ 𝑋 ) |
238 |
190 191 12 18 19
|
xrletrd |
⊢ ( 𝜑 → 𝑋 ≤ 𝑈 ) |
239 |
|
fllep1 |
⊢ ( 𝑋 ∈ ℝ → 𝑋 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) |
240 |
29 239
|
syl |
⊢ ( 𝜑 → 𝑋 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) |
241 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 237 238 240
|
dvfsumlem1 |
⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ) |
242 |
235 236 241
|
3brtr4d |
⊢ ( 𝜑 → ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ) |
243 |
65 60
|
resubcld |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ ) |
244 |
56 44
|
resubcld |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ ) |
245 |
|
peano2rem |
⊢ ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ∈ ℝ → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ ) |
246 |
57 245
|
syl |
⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ ) |
247 |
246 60
|
remulcld |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ ) |
248 |
247 64
|
resubcld |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) |
249 |
|
peano2rem |
⊢ ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ∈ ℝ → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ ) |
250 |
32 249
|
syl |
⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ ) |
251 |
250 60
|
remulcld |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ ) |
252 |
251 55
|
resubcld |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) |
253 |
250 44
|
remulcld |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ ) |
254 |
253 55
|
resubcld |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) |
255 |
247
|
recnd |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℂ ) |
256 |
251
|
recnd |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℂ ) |
257 |
255 256
|
subcld |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ∈ ℂ ) |
258 |
257 203
|
addcomd |
⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 + ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) ) |
259 |
255 256 203
|
subsubd |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
260 |
203 256 255
|
subsub2d |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 + ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) ) |
261 |
258 259 260
|
3eqtr4d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) ) |
262 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
263 |
209 210 262
|
nnncan2d |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) = ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) ) |
264 |
263 207
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) = ( 𝑌 − 𝑋 ) ) |
265 |
264
|
oveq1d |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( 𝑌 − 𝑋 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
266 |
250
|
recnd |
⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℂ ) |
267 |
246
|
recnd |
⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℂ ) |
268 |
60
|
recnd |
⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ ) |
269 |
266 267 268
|
subdird |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) |
270 |
212 268
|
mulcomd |
⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) |
271 |
265 269 270
|
3eqtr3d |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) |
272 |
271
|
oveq2d |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) ) |
273 |
261 272
|
eqtrd |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) ) |
274 |
60 76
|
remulcld |
⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ∈ ℝ ) |
275 |
|
cncfmptc |
⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
276 |
60 92 93 275
|
syl3anc |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
277 |
|
remulcl |
⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ∈ ℝ ) |
278 |
82 83 276 97 91 277
|
cncfmpt2ss |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) |
279 |
101 105 106 114 268
|
dvmptcmul |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 1 ) ) ) |
280 |
268
|
mulid1d |
⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 1 ) = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
281 |
280
|
mpteq2dv |
⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 1 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
282 |
279 281
|
eqtrd |
⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
283 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑋 ∈ 𝑆 ) |
284 |
153
|
rexrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ∈ ℝ* ) |
285 |
191
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑌 ∈ ℝ* ) |
286 |
12
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑈 ∈ ℝ* ) |
287 |
284 285 286 157 158
|
xrletrd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ≤ 𝑈 ) |
288 |
|
vex |
⊢ 𝑦 ∈ V |
289 |
|
eleq1 |
⊢ ( 𝑘 = 𝑦 → ( 𝑘 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆 ) ) |
290 |
289
|
anbi2d |
⊢ ( 𝑘 = 𝑦 → ( ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ↔ ( 𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ) |
291 |
|
breq2 |
⊢ ( 𝑘 = 𝑦 → ( 𝑋 ≤ 𝑘 ↔ 𝑋 ≤ 𝑦 ) ) |
292 |
|
breq1 |
⊢ ( 𝑘 = 𝑦 → ( 𝑘 ≤ 𝑈 ↔ 𝑦 ≤ 𝑈 ) ) |
293 |
291 292
|
3anbi23d |
⊢ ( 𝑘 = 𝑦 → ( ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ↔ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈 ) ) ) |
294 |
290 293
|
3anbi23d |
⊢ ( 𝑘 = 𝑦 → ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈 ) ) ) ) |
295 |
|
csbeq1 |
⊢ ( 𝑘 = 𝑦 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
296 |
167 295
|
syl5eqr |
⊢ ( 𝑘 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) |
297 |
296
|
breq1d |
⊢ ( 𝑘 = 𝑦 → ( 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
298 |
294 297
|
imbi12d |
⊢ ( 𝑘 = 𝑦 → ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) |
299 |
|
simp2l |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝑋 ∈ 𝑆 ) |
300 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) |
301 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐵 |
302 |
173 174 301
|
nfbr |
⊢ Ⅎ 𝑥 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 |
303 |
300 302
|
nfim |
⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
304 |
|
eleq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆 ) ) |
305 |
304
|
anbi1d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ↔ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) ) |
306 |
|
breq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋 ) ) |
307 |
|
breq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑘 ↔ 𝑋 ≤ 𝑘 ) ) |
308 |
306 307
|
3anbi12d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ↔ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ) |
309 |
305 308
|
3anbi23d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ) ) |
310 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑋 → 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
311 |
310
|
breq2d |
⊢ ( 𝑥 = 𝑋 → ( 𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
312 |
309 311
|
imbi12d |
⊢ ( 𝑥 = 𝑋 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) |
313 |
303 312 13
|
vtoclg1f |
⊢ ( 𝑋 ∈ 𝑆 → ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
314 |
299 313
|
mpcom |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
315 |
288 298 314
|
vtocl |
⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
316 |
145 283 146 154 155 287 315
|
syl123anc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
317 |
144 316
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
318 |
|
oveq2 |
⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) |
319 |
|
oveq2 |
⊢ ( 𝑦 = 𝑌 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑌 ) ) |
320 |
29 23 136 143 278 282 317 193 195 18 62 318 46 319
|
dvle |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑌 ) − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) ) |
321 |
268 79 80
|
subdid |
⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) = ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑌 ) − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) ) |
322 |
320 321
|
breqtrrd |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) |
323 |
55 64 274 322
|
subled |
⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) |
324 |
273 323
|
eqbrtrd |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) |
325 |
247 252 64 324
|
subled |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
326 |
250
|
renegcld |
⊢ ( 𝜑 → - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ ) |
327 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
328 |
23 31 327
|
lesubadd2d |
⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 ↔ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ) |
329 |
20 328
|
mpbird |
⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 ) |
330 |
32 327
|
suble0d |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ≤ 0 ↔ ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 ) ) |
331 |
329 330
|
mpbird |
⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ≤ 0 ) |
332 |
250
|
le0neg1d |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ≤ 0 ↔ 0 ≤ - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) ) |
333 |
331 332
|
mpbid |
⊢ ( 𝜑 → 0 ≤ - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) |
334 |
44 60 326 333 231
|
lemul2ad |
⊢ ( 𝜑 → ( - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ ( - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
335 |
266 78
|
mulneg1d |
⊢ ( 𝜑 → ( - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
336 |
266 268
|
mulneg1d |
⊢ ( 𝜑 → ( - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
337 |
334 335 336
|
3brtr3d |
⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
338 |
251 253
|
lenegd |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ↔ - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) |
339 |
337 338
|
mpbird |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
340 |
251 253 55 339
|
lesub1dd |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
341 |
248 252 254 325 340
|
letrd |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
342 |
210 262 268
|
subdird |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) |
343 |
268
|
mulid2d |
⊢ ( 𝜑 → ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) |
344 |
343
|
oveq2d |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
345 |
342 344
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
346 |
345
|
oveq1d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) |
347 |
209 262 78
|
subdird |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ) |
348 |
78
|
mulid2d |
⊢ ( 𝜑 → ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) |
349 |
348
|
oveq2d |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
350 |
347 349
|
eqtrd |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
351 |
350
|
oveq1d |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
352 |
341 346 351
|
3brtr3d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
353 |
61
|
recnd |
⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℂ ) |
354 |
64
|
recnd |
⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℂ ) |
355 |
353 354 268
|
sub32d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) |
356 |
202 203 78
|
sub32d |
⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) |
357 |
352 355 356
|
3brtr4d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
358 |
243 244 73 357
|
leadd1dd |
⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ≤ ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ) |
359 |
65
|
recnd |
⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℂ ) |
360 |
73
|
recnd |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ∈ ℂ ) |
361 |
359 360 268
|
addsubd |
⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ) |
362 |
56
|
recnd |
⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℂ ) |
363 |
362 360 78
|
addsubd |
⊢ ( 𝜑 → ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ) |
364 |
358 361 363
|
3brtr4d |
⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
365 |
241
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) |
366 |
236
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
367 |
364 365 366
|
3brtr4d |
⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) |
368 |
242 367
|
jca |
⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ) |