Metamath Proof Explorer

Theorem dvfsumlem2OLD

Description: Obsolete version of dvfsumlem2 as of 17-Apr-2025. (Contributed by Mario Carneiro, 17-May-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dvfsum.s ⊢ 𝑆 = ( 𝑇 (,) +∞ )
dvfsum.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
dvfsum.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
dvfsum.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
dvfsum.md ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
dvfsum.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
dvfsum.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
dvfsum.b1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
dvfsum.b2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
dvfsum.b3 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
dvfsum.c ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
dvfsum.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
dvfsum.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 )
dvfsum.h ⊢ 𝐻 = ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) )
dvfsumlem1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dvfsumlem1.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
dvfsumlem1.3 ⊢ ( 𝜑 → 𝐷 ≤ 𝑋 )
dvfsumlem1.4 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
dvfsumlem1.5 ⊢ ( 𝜑 → 𝑌 ≤ 𝑈 )
dvfsumlem1.6 ⊢ ( 𝜑 → 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
Assertion dvfsumlem2OLD ( 𝜑 → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )

Proof

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 sselid ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
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 mulridd ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 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 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –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 eqtr3id ⊢ ( 𝑘 = 𝑌 → 𝐶 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
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 mulridd ⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 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 eqtr3id ⊢ ( 𝑘 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
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 mullidd ⊢ ( 𝜑 → ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
344 343 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
345 342 344 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
346 345 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
347 209 262 78 subdird ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
348 78 mullidd ⊢ ( 𝜑 → ( 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 ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )