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

Metamath Proof Explorer

Theorem dvfsumlem3

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016)

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

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 ioossre ⊢ ( 𝑇 (,) +∞ ) ⊆ ℝ
21 1 20 eqsstri ⊢ 𝑆 ⊆ ℝ
22 21 16 sselid ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
23 21 15 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
24 reflcl ⊢ ( 𝑋 ∈ ℝ → ( ⌊ ‘ 𝑋 ) ∈ ℝ )
25 peano2re ⊢ ( ( ⌊ ‘ 𝑋 ) ∈ ℝ → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ )
26 23 24 25 3syl ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ )
27 3 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑀 ∈ ℤ )
28 4 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝐷 ∈ ℝ )
29 5 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑀 ≤ ( 𝐷 + 1 ) )
30 6 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑇 ∈ ℝ )
31 7 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
32 8 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
33 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
34 10 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
35 12 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑈 ∈ ℝ* )
36 13 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 )
37 15 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑋 ∈ 𝑆 )
38 16 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑌 ∈ 𝑆 )
39 17 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝐷 ≤ 𝑋 )
40 18 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑋 ≤ 𝑌 )
41 19 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑌 ≤ 𝑈 )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
43 1 2 27 28 29 30 31 32 33 34 11 35 36 14 37 38 39 40 41 42 dvfsumlem2 ⊢ ( ( 𝜑 ∧ 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
44 21 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
45 44 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ℝ )
46 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
48 45 47 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) ∈ ℝ )
49 44 7 8 10 dvmptrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
50 48 49 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) ∈ ℝ )
51 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
52 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ )
54 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
55 54 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ 𝑍 )
56 11 eleq1d ⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
57 56 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℝ )
58 53 55 57 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐶 ∈ ℝ )
59 51 58 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 ∈ ℝ )
60 59 7 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ∈ ℝ )
61 50 60 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ∈ ℝ )
62 61 14 fmptd ⊢ ( 𝜑 → 𝐻 : 𝑆 ⟶ ℝ )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝐻 : 𝑆 ⟶ ℝ )
64 16 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑌 ∈ 𝑆 )
65 63 64 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ 𝑌 ) ∈ ℝ )
66 22 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑌 ∈ ℝ )
67 reflcl ⊢ ( 𝑌 ∈ ℝ → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
68 66 67 syl ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
69 6 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑇 ∈ ℝ )
70 23 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑋 ∈ ℝ )
71 70 24 25 3syl ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ )
72 15 1 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 (,) +∞ ) )
73 6 rexrd ⊢ ( 𝜑 → 𝑇 ∈ ℝ* )
74 elioopnf ⊢ ( 𝑇 ∈ ℝ* → ( 𝑋 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) ) )
75 73 74 syl ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) ) )
76 72 75 mpbid ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) )
77 76 simprd ⊢ ( 𝜑 → 𝑇 < 𝑋 )
78 fllep1 ⊢ ( 𝑋 ∈ ℝ → 𝑋 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
79 23 78 syl ⊢ ( 𝜑 → 𝑋 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
80 6 23 26 77 79 ltletrd ⊢ ( 𝜑 → 𝑇 < ( ( ⌊ ‘ 𝑋 ) + 1 ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑇 < ( ( ⌊ ‘ 𝑋 ) + 1 ) )
82 simpr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 )
83 70 flcld ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑋 ) ∈ ℤ )
84 83 peano2zd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℤ )
85 flge ⊢ ( ( 𝑌 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℤ ) → ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ↔ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ ( ⌊ ‘ 𝑌 ) ) )
86 66 84 85 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ↔ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ ( ⌊ ‘ 𝑌 ) ) )
87 82 86 mpbid ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ ( ⌊ ‘ 𝑌 ) )
88 69 71 68 81 87 ltletrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑇 < ( ⌊ ‘ 𝑌 ) )
89 73 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑇 ∈ ℝ* )
90 elioopnf ⊢ ( 𝑇 ∈ ℝ* → ( ( ⌊ ‘ 𝑌 ) ∈ ( 𝑇 (,) +∞ ) ↔ ( ( ⌊ ‘ 𝑌 ) ∈ ℝ ∧ 𝑇 < ( ⌊ ‘ 𝑌 ) ) ) )
91 89 90 syl ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑌 ) ∈ ( 𝑇 (,) +∞ ) ↔ ( ( ⌊ ‘ 𝑌 ) ∈ ℝ ∧ 𝑇 < ( ⌊ ‘ 𝑌 ) ) ) )
92 68 88 91 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ ( 𝑇 (,) +∞ ) )
93 92 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ 𝑆 )
94 63 93 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) ∈ ℝ )
95 15 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑋 ∈ 𝑆 )
96 63 95 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ 𝑋 ) ∈ ℝ )
97 3 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑀 ∈ ℤ )
98 4 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝐷 ∈ ℝ )
99 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑀 ≤ ( 𝐷 + 1 ) )
100 7 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
101 8 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
102 9 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
103 10 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
104 12 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑈 ∈ ℝ* )
105 13 3adant1r ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 )
106 17 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝐷 ≤ 𝑋 )
107 70 78 syl ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑋 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
108 98 70 71 106 107 letrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝐷 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
109 98 71 68 108 87 letrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝐷 ≤ ( ⌊ ‘ 𝑌 ) )
110 flle ⊢ ( 𝑌 ∈ ℝ → ( ⌊ ‘ 𝑌 ) ≤ 𝑌 )
111 66 110 syl ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ≤ 𝑌 )
112 19 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑌 ≤ 𝑈 )
113 fllep1 ⊢ ( 𝑌 ∈ ℝ → 𝑌 ≤ ( ( ⌊ ‘ 𝑌 ) + 1 ) )
114 66 113 syl ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑌 ≤ ( ( ⌊ ‘ 𝑌 ) + 1 ) )
115 flidm ⊢ ( 𝑌 ∈ ℝ → ( ⌊ ‘ ( ⌊ ‘ 𝑌 ) ) = ( ⌊ ‘ 𝑌 ) )
116 66 115 syl ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ ( ⌊ ‘ 𝑌 ) ) = ( ⌊ ‘ 𝑌 ) )
117 116 oveq1d ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ ( ⌊ ‘ 𝑌 ) ) + 1 ) = ( ( ⌊ ‘ 𝑌 ) + 1 ) )
118 114 117 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑌 ≤ ( ( ⌊ ‘ ( ⌊ ‘ 𝑌 ) ) + 1 ) )
119 1 2 97 98 99 69 100 101 102 103 11 104 105 14 93 64 109 111 112 118 dvfsumlem2 ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) ∧ ( ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) − ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
120 119 simpld ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) )
121 elioopnf ⊢ ( 𝑇 ∈ ℝ* → ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ( 𝑇 (,) +∞ ) ↔ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ ∧ 𝑇 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ) )
122 73 121 syl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ( 𝑇 (,) +∞ ) ↔ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ ∧ 𝑇 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ) )
123 26 80 122 mpbir2and ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ( 𝑇 (,) +∞ ) )
124 123 1 eleqtrrdi ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ 𝑆 )
125 124 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ 𝑆 )
126 63 125 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ∈ ℝ )
127 66 flcld ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ ℤ )
128 eluz2 ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ↔ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℤ ∧ ( ⌊ ‘ 𝑌 ) ∈ ℤ ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ ( ⌊ ‘ 𝑌 ) ) )
129 84 127 87 128 syl3anbrc ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
130 63 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝐻 : 𝑆 ⟶ ℝ )
131 elfzelz ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → 𝑚 ∈ ℤ )
132 131 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑚 ∈ ℤ )
133 132 zred ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑚 ∈ ℝ )
134 69 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑇 ∈ ℝ )
135 71 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ )
136 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑇 < ( ( ⌊ ‘ 𝑋 ) + 1 ) )
137 elfzle1 ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑚 )
138 137 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑚 )
139 134 135 133 136 138 ltletrd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑇 < 𝑚 )
140 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑇 ∈ ℝ* )
141 elioopnf ⊢ ( 𝑇 ∈ ℝ* → ( 𝑚 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑇 < 𝑚 ) ) )
142 140 141 syl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → ( 𝑚 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑇 < 𝑚 ) ) )
143 133 139 142 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑚 ∈ ( 𝑇 (,) +∞ ) )
144 143 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → 𝑚 ∈ 𝑆 )
145 130 144 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → ( 𝐻 ‘ 𝑚 ) ∈ ℝ )
146 97 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑀 ∈ ℤ )
147 98 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝐷 ∈ ℝ )
148 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑀 ≤ ( 𝐷 + 1 ) )
149 69 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑇 ∈ ℝ )
150 100 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
151 101 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
152 102 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
153 103 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
154 104 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑈 ∈ ℝ* )
155 105 3adant1r ⊢ ( ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 )
156 elfzelz ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) → 𝑚 ∈ ℤ )
157 156 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑚 ∈ ℤ )
158 157 zred ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑚 ∈ ℝ )
159 71 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ )
160 80 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑇 < ( ( ⌊ ‘ 𝑋 ) + 1 ) )
161 elfzle1 ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑚 )
162 161 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑚 )
163 149 159 158 160 162 ltletrd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑇 < 𝑚 )
164 149 rexrd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑇 ∈ ℝ* )
165 164 141 syl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑚 ∈ ℝ ∧ 𝑇 < 𝑚 ) ) )
166 158 163 165 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑚 ∈ ( 𝑇 (,) +∞ ) )
167 166 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑚 ∈ 𝑆 )
168 peano2re ⊢ ( 𝑚 ∈ ℝ → ( 𝑚 + 1 ) ∈ ℝ )
169 158 168 syl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 + 1 ) ∈ ℝ )
170 158 lep1d ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑚 ≤ ( 𝑚 + 1 ) )
171 149 158 169 163 170 ltletrd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑇 < ( 𝑚 + 1 ) )
172 elioopnf ⊢ ( 𝑇 ∈ ℝ* → ( ( 𝑚 + 1 ) ∈ ( 𝑇 (,) +∞ ) ↔ ( ( 𝑚 + 1 ) ∈ ℝ ∧ 𝑇 < ( 𝑚 + 1 ) ) ) )
173 164 172 syl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ( 𝑚 + 1 ) ∈ ( 𝑇 (,) +∞ ) ↔ ( ( 𝑚 + 1 ) ∈ ℝ ∧ 𝑇 < ( 𝑚 + 1 ) ) ) )
174 169 171 173 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 + 1 ) ∈ ( 𝑇 (,) +∞ ) )
175 174 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 + 1 ) ∈ 𝑆 )
176 108 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝐷 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
177 147 159 158 176 162 letrd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝐷 ≤ 𝑚 )
178 169 rexrd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 + 1 ) ∈ ℝ* )
179 68 rexrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ∈ ℝ* )
180 179 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ⌊ ‘ 𝑌 ) ∈ ℝ* )
181 elfzle2 ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) → 𝑚 ≤ ( ( ⌊ ‘ 𝑌 ) − 1 ) )
182 181 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑚 ≤ ( ( ⌊ ‘ 𝑌 ) − 1 ) )
183 1red ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 1 ∈ ℝ )
184 66 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑌 ∈ ℝ )
185 184 67 syl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
186 leaddsub ⊢ ( ( 𝑚 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ⌊ ‘ 𝑌 ) ∈ ℝ ) → ( ( 𝑚 + 1 ) ≤ ( ⌊ ‘ 𝑌 ) ↔ 𝑚 ≤ ( ( ⌊ ‘ 𝑌 ) − 1 ) ) )
187 158 183 185 186 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ( 𝑚 + 1 ) ≤ ( ⌊ ‘ 𝑌 ) ↔ 𝑚 ≤ ( ( ⌊ ‘ 𝑌 ) − 1 ) ) )
188 182 187 mpbird ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 + 1 ) ≤ ( ⌊ ‘ 𝑌 ) )
189 66 rexrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → 𝑌 ∈ ℝ* )
190 179 189 104 111 112 xrletrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ⌊ ‘ 𝑌 ) ≤ 𝑈 )
191 190 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ⌊ ‘ 𝑌 ) ≤ 𝑈 )
192 178 180 154 188 191 xrletrd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 + 1 ) ≤ 𝑈 )
193 flid ⊢ ( 𝑚 ∈ ℤ → ( ⌊ ‘ 𝑚 ) = 𝑚 )
194 157 193 syl ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ⌊ ‘ 𝑚 ) = 𝑚 )
195 194 eqcomd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → 𝑚 = ( ⌊ ‘ 𝑚 ) )
196 195 oveq1d ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 + 1 ) = ( ( ⌊ ‘ 𝑚 ) + 1 ) )
197 169 196 eqled ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝑚 + 1 ) ≤ ( ( ⌊ ‘ 𝑚 ) + 1 ) )
198 1 2 146 147 148 149 150 151 152 153 11 154 155 14 167 175 177 170 192 197 dvfsumlem2 ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ( 𝐻 ‘ ( 𝑚 + 1 ) ) ≤ ( 𝐻 ‘ 𝑚 ) ∧ ( ( 𝐻 ‘ 𝑚 ) − ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ ( 𝑚 + 1 ) ) − ⦋ ( 𝑚 + 1 ) / 𝑥 ⦌ 𝐵 ) ) )
199 198 simpld ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( 𝐻 ‘ ( 𝑚 + 1 ) ) ≤ ( 𝐻 ‘ 𝑚 ) )
200 129 145 199 monoord2 ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) ≤ ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
201 71 rexrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ* )
202 201 179 104 87 190 xrletrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑈 )
203 71 leidd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
204 1 2 97 98 99 69 100 101 102 103 11 104 105 14 95 125 106 107 202 203 dvfsumlem2 ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) − ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) ) )
205 204 simpld ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ≤ ( 𝐻 ‘ 𝑋 ) )
206 94 126 96 200 205 letrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) ≤ ( 𝐻 ‘ 𝑋 ) )
207 65 94 96 120 206 letrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) )
208 csbeq1 ⊢ ( 𝑚 = 𝑋 → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
209 208 eleq1d ⊢ ( 𝑚 = 𝑋 → ( ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
210 49 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ )
211 210 adantr ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ )
212 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑚 / 𝑥 ⦌ 𝐵
213 212 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ
214 csbeq1a ⊢ ( 𝑥 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑥 ⦌ 𝐵 )
215 214 eleq1d ⊢ ( 𝑥 = 𝑚 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
216 213 215 rspc ⊢ ( 𝑚 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
217 211 216 mpan9 ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ 𝑆 ) → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ )
218 217 ralrimiva ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ )
219 209 218 95 rspcdva ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ )
220 96 219 resubcld ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
221 csbeq1 ⊢ ( 𝑚 = ( ⌊ ‘ 𝑌 ) → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 = ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 )
222 221 eleq1d ⊢ ( 𝑚 = ( ⌊ ‘ 𝑌 ) → ( ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
223 222 218 93 rspcdva ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ∈ ℝ )
224 94 223 resubcld ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) − ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
225 csbeq1 ⊢ ( 𝑚 = 𝑌 → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
226 225 eleq1d ⊢ ( 𝑚 = 𝑌 → ( ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
227 226 218 64 rspcdva ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ )
228 65 227 resubcld ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
229 csbeq1 ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 = ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 )
230 229 eleq1d ⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → ( ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
231 230 218 125 rspcdva ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ∈ ℝ )
232 126 231 resubcld ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) − ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
233 204 simprd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) − ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) )
234 fveq2 ⊢ ( 𝑦 = 𝑚 → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑚 ) )
235 csbeq1 ⊢ ( 𝑦 = 𝑚 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑚 / 𝑥 ⦌ 𝐵 )
236 234 235 oveq12d ⊢ ( 𝑦 = 𝑚 → ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( ( 𝐻 ‘ 𝑚 ) − ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ) )
237 eqid ⊢ ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) = ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
238 ovex ⊢ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∈ V
239 236 237 238 fvmpt3i ⊢ ( 𝑚 ∈ V → ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝐻 ‘ 𝑚 ) − ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ) )
240 239 elv ⊢ ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝐻 ‘ 𝑚 ) − ⦋ 𝑚 / 𝑥 ⦌ 𝐵 )
241 144 217 syldan ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ )
242 145 241 resubcld ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → ( ( 𝐻 ‘ 𝑚 ) − ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
243 240 242 eqeltrid ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ⌊ ‘ 𝑌 ) ) ) → ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ 𝑚 ) ∈ ℝ )
244 198 simprd ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ( 𝐻 ‘ 𝑚 ) − ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ ( 𝑚 + 1 ) ) − ⦋ ( 𝑚 + 1 ) / 𝑥 ⦌ 𝐵 ) )
245 ovex ⊢ ( 𝑚 + 1 ) ∈ V
246 fveq2 ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ ( 𝑚 + 1 ) ) )
247 csbeq1 ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ ( 𝑚 + 1 ) / 𝑥 ⦌ 𝐵 )
248 246 247 oveq12d ⊢ ( 𝑦 = ( 𝑚 + 1 ) → ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( ( 𝐻 ‘ ( 𝑚 + 1 ) ) − ⦋ ( 𝑚 + 1 ) / 𝑥 ⦌ 𝐵 ) )
249 248 237 238 fvmpt3i ⊢ ( ( 𝑚 + 1 ) ∈ V → ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝐻 ‘ ( 𝑚 + 1 ) ) − ⦋ ( 𝑚 + 1 ) / 𝑥 ⦌ 𝐵 ) )
250 245 249 ax-mp ⊢ ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( 𝑚 + 1 ) ) = ( ( 𝐻 ‘ ( 𝑚 + 1 ) ) − ⦋ ( 𝑚 + 1 ) / 𝑥 ⦌ 𝐵 )
251 244 240 250 3brtr4g ⊢ ( ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ... ( ( ⌊ ‘ 𝑌 ) − 1 ) ) ) → ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ 𝑚 ) ≤ ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( 𝑚 + 1 ) ) )
252 129 243 251 monoord ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ≤ ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( ⌊ ‘ 𝑌 ) ) )
253 ovex ⊢ ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ V
254 fveq2 ⊢ ( 𝑦 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
255 csbeq1 ⊢ ( 𝑦 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 )
256 254 255 oveq12d ⊢ ( 𝑦 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) − ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) )
257 256 237 238 fvmpt3i ⊢ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ V → ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) = ( ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) − ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) )
258 253 257 ax-mp ⊢ ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) = ( ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) − ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 )
259 fvex ⊢ ( ⌊ ‘ 𝑌 ) ∈ V
260 fveq2 ⊢ ( 𝑦 = ( ⌊ ‘ 𝑌 ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) )
261 csbeq1 ⊢ ( 𝑦 = ( ⌊ ‘ 𝑌 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 )
262 260 261 oveq12d ⊢ ( 𝑦 = ( ⌊ ‘ 𝑌 ) → ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) − ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ) )
263 262 237 238 fvmpt3i ⊢ ( ( ⌊ ‘ 𝑌 ) ∈ V → ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( ⌊ ‘ 𝑌 ) ) = ( ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) − ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ) )
264 259 263 ax-mp ⊢ ( ( 𝑦 ∈ V ↦ ( ( 𝐻 ‘ 𝑦 ) − ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ) ‘ ( ⌊ ‘ 𝑌 ) ) = ( ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) − ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 )
265 252 258 264 3brtr3g ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) − ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) − ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ) )
266 220 232 224 233 265 letrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) − ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ) )
267 119 simprd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ ( ⌊ ‘ 𝑌 ) ) − ⦋ ( ⌊ ‘ 𝑌 ) / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
268 220 224 228 266 267 letrd ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
269 207 268 jca ⊢ ( ( 𝜑 ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ≤ 𝑌 ) → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
270 22 26 43 269 lecasei ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑌 ) ≤ ( 𝐻 ‘ 𝑋 ) ∧ ( ( 𝐻 ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( 𝐻 ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )