This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvfsumlem2

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 dvfsumlem2 ( 𝜑 → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )

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 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
84 csbeq1 ⊢ ( 𝑧 = 𝑌 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
85 84 eleq1d ⊢ ( 𝑧 = 𝑌 → ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
86 nfcv ⊢ Ⅎ 𝑧 𝐵
87 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
88 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
89 86 87 88 cbvmpt ⊢ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = ( 𝑧 ∈ 𝑆 ↦ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
90 89 fmpt ⊢ ( ∀ 𝑧 ∈ 𝑆 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℝ )
91 37 90 sylibr ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ ℝ )
92 85 91 16 rspcdva ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ )
93 pnfxr ⊢ +∞ ∈ ℝ*
94 93 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
95 28 simprd ⊢ ( 𝜑 → 𝑇 < 𝑋 )
96 23 ltpnfd ⊢ ( 𝜑 → 𝑌 < +∞ )
97 iccssioo ⊢ ( ( ( 𝑇 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( 𝑇 < 𝑋 ∧ 𝑌 < +∞ ) ) → ( 𝑋 [,] 𝑌 ) ⊆ ( 𝑇 (,) +∞ ) )
98 25 94 95 96 97 syl22anc ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ( 𝑇 (,) +∞ ) )
99 98 21 sstrdi ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
100 ax-resscn ⊢ ℝ ⊆ ℂ
101 99 100 sstrdi ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℂ )
102 100 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
103 cncfmptc ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
104 92 101 102 103 syl3anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
105 cncfmptid ⊢ ( ( ( 𝑋 [,] 𝑌 ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝑦 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
106 99 100 105 sylancl ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝑦 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
107 remulcl ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ∈ ℝ )
108 simpl ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ )
109 108 recnd ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ )
110 simpr ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
111 110 recnd ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
112 109 111 jca ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
113 ovmpot ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) )
114 113 eqcomd ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
115 112 114 syl ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
116 115 eleq1d ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ∈ ℝ ↔ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℝ ) )
117 116 biimpd ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ∈ ℝ → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℝ ) )
118 107 117 mpd ⊢ ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℝ )
119 82 83 104 106 100 118 cncfmpt2ss ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
120 df-mpt ⊢ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) }
121 120 eleq1i ⊢ ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ↔ { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
122 121 biimpi ⊢ ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
123 119 122 syl ⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
124 idd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) )
125 124 a1dd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ) )
126 125 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) )
127 csbeq1 ⊢ ( 𝑚 = 𝑌 → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
128 127 eleq1d ⊢ ( 𝑚 = 𝑌 → ( ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
129 nfcv ⊢ Ⅎ 𝑚 𝐵
130 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑚 / 𝑥 ⦌ 𝐵
131 csbeq1a ⊢ ( 𝑥 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑥 ⦌ 𝐵 )
132 129 130 131 cbvmpt ⊢ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = ( 𝑚 ∈ 𝑆 ↦ ⦋ 𝑚 / 𝑥 ⦌ 𝐵 )
133 132 fmpt ⊢ ( ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℝ )
134 37 133 sylibr ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ )
135 128 134 16 rspcdva ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ )
136 135 recnd ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ )
137 136 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ )
138 elicc2 ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ) ) )
139 29 23 138 syl2anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ) ) )
140 139 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ) )
141 140 simp1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ∈ ℝ )
142 141 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ∈ ℂ )
143 137 142 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
144 143 113 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) )
145 144 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ↔ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
146 145 biimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) → 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
147 146 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) → 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) )
148 147 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) → 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
149 126 148 jcad ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) )
150 124 a1dd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ) )
151 150 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) )
152 csbeq1 ⊢ ( 𝑘 = 𝑌 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
153 152 eleq1d ⊢ ( 𝑘 = 𝑌 → ( ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
154 nfcv ⊢ Ⅎ 𝑘 𝐵
155 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑘 / 𝑥 ⦌ 𝐵
156 csbeq1a ⊢ ( 𝑥 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
157 154 155 156 cbvmpt ⊢ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑆 ↦ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
158 157 fmpt ⊢ ( ∀ 𝑘 ∈ 𝑆 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℝ )
159 37 158 sylibr ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑆 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ℝ )
160 153 159 16 rspcdva ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ )
161 160 recnd ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ )
162 161 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ )
163 162 142 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
164 163 114 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
165 164 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ↔ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) )
166 165 biimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) → 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) )
167 166 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) → 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ) )
168 167 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) → 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) )
169 151 168 jcad ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ) )
170 149 169 impbid ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ↔ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) )
171 170 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) } )
172 df-mpt ⊢ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) }
173 172 eqcomi ⊢ { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) )
174 173 eqeq2i ⊢ ( { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) } ↔ { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
175 174 biimpi ⊢ ( { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) } → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
176 171 175 syl ⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
177 176 eleq1d ⊢ ( 𝜑 → ( { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ↔ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) )
178 177 biimpd ⊢ ( 𝜑 → ( { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) )
179 123 178 mpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
180 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
181 180 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
182 ioossicc ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
183 182 99 sstrid ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ℝ )
184 183 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑦 ∈ ℝ )
185 184 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑦 ∈ ℂ )
186 1cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → 1 ∈ ℂ )
187 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
188 187 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
189 1cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ )
190 181 dvmptid ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) )
191 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
192 iooretop ⊢ ( 𝑋 (,) 𝑌 ) ∈ ( topGen ‘ ran (,) )
193 192 a1i ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ ( topGen ‘ ran (,) ) )
194 181 188 189 190 183 191 82 193 dvmptres ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ 1 ) )
195 181 185 186 194 78 dvmptcmul ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 1 ) ) )
196 78 mulridd ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 1 ) = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
197 196 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 1 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
198 195 197 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
199 98 1 sseqtrrdi ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ 𝑆 )
200 199 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ↾ ( 𝑋 [,] 𝑌 ) ) = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) )
201 7 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℂ )
202 201 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℂ )
203 10 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
204 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ 𝑉 )
205 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = 𝑆 )
206 204 205 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = 𝑆 )
207 203 206 eqtrd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = 𝑆 )
208 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℂ ∧ 𝑆 ⊆ ℝ ) ∧ dom ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℂ ) )
209 102 202 35 207 208 syl31anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℂ ) )
210 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℂ ) ) → ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℝ ) )
211 100 209 210 sylancr ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) ↔ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℝ ) )
212 48 211 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) )
213 52 212 eqeltrrid ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) )
214 rescncf ⊢ ( ( 𝑋 [,] 𝑌 ) ⊆ 𝑆 → ( ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( 𝑆 –cn→ ℝ ) → ( ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ↾ ( 𝑋 [,] 𝑌 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) )
215 199 213 214 sylc ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ↾ ( 𝑋 [,] 𝑌 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
216 200 215 eqeltrrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
217 54 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ )
218 217 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
219 43 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ )
220 52 oveq2i ⊢ ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( ℝ D ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) )
221 10 220 41 3eqtr3g ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ 𝑆 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
222 182 199 sstrid ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ 𝑆 )
223 181 218 219 221 222 191 82 193 dvmptres ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
224 182 sseli ⊢ ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) )
225 simpl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝜑 )
226 199 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ∈ 𝑆 )
227 16 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑌 ∈ 𝑆 )
228 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐷 ∈ ℝ )
229 29 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑋 ∈ ℝ )
230 17 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐷 ≤ 𝑋 )
231 140 simp2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑋 ≤ 𝑦 )
232 228 229 141 230 231 letrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐷 ≤ 𝑦 )
233 140 simp3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ≤ 𝑌 )
234 19 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑌 ≤ 𝑈 )
235 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → 𝑌 ∈ 𝑆 )
236 eleq1 ⊢ ( 𝑘 = 𝑌 → ( 𝑘 ∈ 𝑆 ↔ 𝑌 ∈ 𝑆 ) )
237 236 anbi2d ⊢ ( 𝑘 = 𝑌 → ( ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ↔ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) )
238 breq2 ⊢ ( 𝑘 = 𝑌 → ( 𝑦 ≤ 𝑘 ↔ 𝑦 ≤ 𝑌 ) )
239 breq1 ⊢ ( 𝑘 = 𝑌 → ( 𝑘 ≤ 𝑈 ↔ 𝑌 ≤ 𝑈 ) )
240 238 239 3anbi23d ⊢ ( 𝑘 = 𝑌 → ( ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ↔ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) )
241 237 240 3anbi23d ⊢ ( 𝑘 = 𝑌 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) ) )
242 vex ⊢ 𝑘 ∈ V
243 242 11 csbie ⊢ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐶
244 243 152 eqtr3id ⊢ ( 𝑘 = 𝑌 → 𝐶 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
245 244 breq1d ⊢ ( 𝑘 = 𝑌 → ( 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
246 241 245 imbi12d ⊢ ( 𝑘 = 𝑌 → ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
247 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) )
248 nfcv ⊢ Ⅎ 𝑥 𝐶
249 nfcv ⊢ Ⅎ 𝑥 ≤
250 248 249 39 nfbr ⊢ Ⅎ 𝑥 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
251 247 250 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
252 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆 ) )
253 252 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ↔ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) )
254 breq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑦 ) )
255 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ 𝑘 ↔ 𝑦 ≤ 𝑘 ) )
256 254 255 3anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ↔ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) )
257 253 256 3anbi23d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ) )
258 40 breq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
259 257 258 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) )
260 251 259 13 chvarfv ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
261 246 260 vtoclg ⊢ ( 𝑌 ∈ 𝑆 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
262 235 261 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
263 225 226 227 232 233 234 262 syl123anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
264 224 263 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
265 29 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
266 23 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
267 lbicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
268 265 266 18 267 syl3anc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
269 ubicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
270 265 266 18 269 syl3anc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
271 oveq2 ⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑋 ) )
272 oveq2 ⊢ ( 𝑦 = 𝑌 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑌 ) )
273 29 23 179 198 216 223 264 268 270 18 271 62 272 46 dvle ⊢ ( 𝜑 → ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑌 ) − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
274 81 273 eqbrtrd ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
275 77 55 64 274 lesubd ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) )
276 74 recnd ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
277 45 recnd ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
278 55 recnd ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℂ )
279 276 277 278 subsubd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
280 277 276 negsubdi2d ⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
281 31 recnd ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ∈ ℂ )
282 79 80 281 nnncan2d ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) = ( 𝑌 − 𝑋 ) )
283 282 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( 𝑌 − 𝑋 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
284 32 recnd ⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ∈ ℂ )
285 57 recnd ⊢ ( 𝜑 → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ∈ ℂ )
286 284 285 78 subdird ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
287 76 recnd ⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℂ )
288 287 78 mulcomd ⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) )
289 283 286 288 3eqtr3d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) )
290 289 negeqd ⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = - ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) )
291 280 290 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = - ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) )
292 291 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( - ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
293 77 recnd ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ∈ ℂ )
294 293 278 negsubdid ⊢ ( 𝜑 → - ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( - ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
295 292 294 eqtr4d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = - ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
296 293 278 negsubdi2d ⊢ ( 𝜑 → - ( ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) )
297 279 295 296 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) )
298 275 297 breqtrrd ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
299 64 74 56 298 lesubd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
300 flle ⊢ ( 𝑋 ∈ ℝ → ( ⌊ ‘ 𝑋 ) ≤ 𝑋 )
301 29 300 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ≤ 𝑋 )
302 29 31 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ↔ ( ⌊ ‘ 𝑋 ) ≤ 𝑋 ) )
303 301 302 mpbird ⊢ ( 𝜑 → 0 ≤ ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) )
304 58 breq2d ⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
305 263 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
306 304 305 268 rspcdva ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
307 44 60 57 303 306 lemul2ad ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
308 74 61 64 307 lesub1dd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
309 56 75 65 299 308 letrd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
310 56 65 73 309 leadd1dd ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ≤ ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )
311 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dvfsumlem1 ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑌 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )
312 29 leidd ⊢ ( 𝜑 → 𝑋 ≤ 𝑋 )
313 265 266 12 18 19 xrletrd ⊢ ( 𝜑 → 𝑋 ≤ 𝑈 )
314 fllep1 ⊢ ( 𝑋 ∈ ℝ → 𝑋 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
315 29 314 syl ⊢ ( 𝜑 → 𝑋 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
316 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 312 313 315 dvfsumlem1 ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )
317 310 311 316 3brtr4d ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) )
318 65 60 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
319 56 44 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
320 peano2rem ⊢ ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ∈ ℝ → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ )
321 57 320 syl ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ )
322 321 60 remulcld ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
323 322 64 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℝ )
324 peano2rem ⊢ ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ∈ ℝ → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ )
325 32 324 syl ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ )
326 325 60 remulcld ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
327 326 55 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ )
328 325 44 remulcld ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
329 328 55 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ )
330 322 recnd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
331 326 recnd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
332 330 331 subcld ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ∈ ℂ )
333 332 278 addcomd ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 + ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) )
334 330 331 278 subsubd ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
335 278 331 330 subsub2d ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 + ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) )
336 333 334 335 3eqtr4d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) )
337 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
338 284 285 337 nnncan2d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) = ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ) )
339 338 282 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) = ( 𝑌 − 𝑋 ) )
340 339 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( 𝑌 − 𝑋 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
341 325 recnd ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℂ )
342 321 recnd ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℂ )
343 60 recnd ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ )
344 341 342 343 subdird ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) − ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
345 287 343 mulcomd ⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) )
346 340 344 345 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) )
347 346 oveq2d ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) )
348 336 347 eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) )
349 60 76 remulcld ⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ∈ ℝ )
350 cncfmptc ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
351 60 101 102 350 syl3anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
352 remulcl ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ∈ ℝ )
353 simpl ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ )
354 353 recnd ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ )
355 simpr ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
356 355 recnd ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
357 354 356 jca ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
358 ovmpot ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) )
359 358 eqcomd ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
360 357 359 syl ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
361 360 eleq1d ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ∈ ℝ ↔ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℝ ) )
362 361 biimpd ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ∈ ℝ → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℝ ) )
363 352 362 mpd ⊢ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℝ )
364 82 83 351 106 100 363 cncfmpt2ss ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
365 df-mpt ⊢ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) }
366 365 eleq1i ⊢ ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ↔ { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
367 366 biimpi ⊢ ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
368 364 367 syl ⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
369 124 a1dd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ) )
370 369 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) )
371 343 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ )
372 371 142 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
373 372 358 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) )
374 373 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ↔ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
375 374 biimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) → 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
376 375 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) → 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) )
377 376 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) → 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
378 370 377 jcad ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) )
379 124 a1dd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) ) )
380 379 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) → 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) )
381 372 359 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
382 381 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ↔ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) )
383 382 biimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) → 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) )
384 383 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) → ( 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) → 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ) )
385 384 impd ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) → 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) )
386 380 385 jcad ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ) )
387 378 386 impbid ⊢ ( 𝜑 → ( ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ↔ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) )
388 387 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) } )
389 df-mpt ⊢ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) }
390 389 eqcomi ⊢ { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) )
391 390 eqeq2i ⊢ ( { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) } ↔ { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
392 391 biimpi ⊢ ( { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) } → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
393 388 392 syl ⊢ ( 𝜑 → { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) )
394 393 eleq1d ⊢ ( 𝜑 → ( { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ↔ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) )
395 394 biimpd ⊢ ( 𝜑 → ( { ⟨ 𝑦 , 𝑤 ⟩ ∣ ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ∧ 𝑤 = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) ) )
396 368 395 mpd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℝ ) )
397 181 185 186 194 343 dvmptcmul ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 1 ) ) )
398 343 mulridd ⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 1 ) = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
399 398 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 1 ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
400 397 399 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
401 15 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑋 ∈ 𝑆 )
402 141 rexrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ∈ ℝ* )
403 266 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑌 ∈ ℝ* )
404 12 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑈 ∈ ℝ* )
405 402 403 404 233 234 xrletrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝑦 ≤ 𝑈 )
406 vex ⊢ 𝑦 ∈ V
407 eleq1 ⊢ ( 𝑘 = 𝑦 → ( 𝑘 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆 ) )
408 407 anbi2d ⊢ ( 𝑘 = 𝑦 → ( ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ↔ ( 𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) )
409 breq2 ⊢ ( 𝑘 = 𝑦 → ( 𝑋 ≤ 𝑘 ↔ 𝑋 ≤ 𝑦 ) )
410 breq1 ⊢ ( 𝑘 = 𝑦 → ( 𝑘 ≤ 𝑈 ↔ 𝑦 ≤ 𝑈 ) )
411 409 410 3anbi23d ⊢ ( 𝑘 = 𝑦 → ( ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ↔ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈 ) ) )
412 408 411 3anbi23d ⊢ ( 𝑘 = 𝑦 → ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈 ) ) ) )
413 csbeq1 ⊢ ( 𝑘 = 𝑦 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
414 243 413 eqtr3id ⊢ ( 𝑘 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
415 414 breq1d ⊢ ( 𝑘 = 𝑦 → ( 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
416 412 415 imbi12d ⊢ ( 𝑘 = 𝑦 → ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
417 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝑋 ∈ 𝑆 )
418 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) )
419 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐵
420 248 249 419 nfbr ⊢ Ⅎ 𝑥 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵
421 418 420 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
422 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆 ) )
423 422 anbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ↔ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) )
424 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋 ) )
425 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑘 ↔ 𝑋 ≤ 𝑘 ) )
426 424 425 3anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ↔ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) )
427 423 426 3anbi23d ⊢ ( 𝑥 = 𝑋 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) ) )
428 csbeq1a ⊢ ( 𝑥 = 𝑋 → 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
429 428 breq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
430 427 429 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
431 421 430 13 vtoclg1f ⊢ ( 𝑋 ∈ 𝑆 → ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
432 417 431 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
433 406 416 432 vtocl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
434 225 401 226 230 231 405 433 syl123anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,] 𝑌 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
435 224 434 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 (,) 𝑌 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
436 oveq2 ⊢ ( 𝑦 = 𝑋 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑋 ) )
437 oveq2 ⊢ ( 𝑦 = 𝑌 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑦 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑌 ) )
438 29 23 216 223 396 400 435 268 270 18 62 436 46 437 dvle ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑌 ) − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) )
439 343 79 80 subdid ⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) = ( ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑌 ) − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · 𝑋 ) ) )
440 438 439 breqtrrd ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) )
441 55 64 349 440 subled ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 · ( 𝑌 − 𝑋 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
442 348 441 eqbrtrd ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
443 322 327 64 442 subled ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
444 325 renegcld ⊢ ( 𝜑 → - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ∈ ℝ )
445 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
446 23 31 445 lesubadd2d ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 ↔ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
447 20 446 mpbird ⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 )
448 32 445 suble0d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ≤ 0 ↔ ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 ) )
449 447 448 mpbird ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ≤ 0 )
450 325 le0neg1d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ≤ 0 ↔ 0 ≤ - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) ) )
451 449 450 mpbid ⊢ ( 𝜑 → 0 ≤ - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) )
452 44 60 444 451 306 lemul2ad ⊢ ( 𝜑 → ( - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ ( - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
453 341 78 mulneg1d ⊢ ( 𝜑 → ( - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
454 341 343 mulneg1d ⊢ ( 𝜑 → ( - ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
455 452 453 454 3brtr3d ⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
456 326 328 lenegd ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ↔ - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ - ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
457 455 456 mpbird ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
458 326 328 55 457 lesub1dd ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
459 323 327 329 443 458 letrd ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
460 285 337 343 subdird ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
461 343 mullidd ⊢ ( 𝜑 → ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
462 461 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
463 460 462 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
464 463 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
465 284 337 78 subdird ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
466 78 mullidd ⊢ ( 𝜑 → ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
467 466 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
468 465 467 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
469 468 oveq1d ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
470 459 464 469 3brtr3d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
471 61 recnd ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
472 64 recnd ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℂ )
473 471 472 343 sub32d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
474 277 278 78 sub32d ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
475 470 473 474 3brtr4d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
476 318 319 73 475 leadd1dd ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) ≤ ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )
477 65 recnd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
478 73 recnd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ∈ ℂ )
479 477 478 343 addsubd ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )
480 56 recnd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
481 480 478 78 addsubd ⊢ ( 𝜑 → ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )
482 476 479 481 3brtr4d ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
483 316 oveq1d ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
484 311 oveq1d ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
485 482 483 484 3brtr4d ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
486 317 485 jca ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )