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 82 tgioo2 ( 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 ( 𝜑 → ( ( 𝐻𝑌 ) ≤ ( 𝐻𝑋 ) ∧ ( ( 𝐻𝑋 ) − 𝑋 / 𝑥 𝐵 ) ≤ ( ( 𝐻𝑌 ) − 𝑌 / 𝑥 𝐵 ) ) )