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

Metamath Proof Explorer

Theorem dvfsumlem1

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 ⊢ ( 𝜑 → 𝑌 ≤ 𝑈 )
dvfsumlem1.6 ⊢ ( 𝜑 → 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
Assertion dvfsumlem1 ( 𝜑 → ( 𝐻 ‘ 𝑌 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )

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 22 15 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
25 24 flcld ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ∈ ℤ )
26 reflcl ⊢ ( 𝑋 ∈ ℝ → ( ⌊ ‘ 𝑋 ) ∈ ℝ )
27 24 26 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ∈ ℝ )
28 flle ⊢ ( 𝑋 ∈ ℝ → ( ⌊ ‘ 𝑋 ) ≤ 𝑋 )
29 24 28 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ≤ 𝑋 )
30 27 24 23 29 18 letrd ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ≤ 𝑌 )
31 flbi ⊢ ( ( 𝑌 ∈ ℝ ∧ ( ⌊ ‘ 𝑋 ) ∈ ℤ ) → ( ( ⌊ ‘ 𝑌 ) = ( ⌊ ‘ 𝑋 ) ↔ ( ( ⌊ ‘ 𝑋 ) ≤ 𝑌 ∧ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ) )
32 31 baibd ⊢ ( ( ( 𝑌 ∈ ℝ ∧ ( ⌊ ‘ 𝑋 ) ∈ ℤ ) ∧ ( ⌊ ‘ 𝑋 ) ≤ 𝑌 ) → ( ( ⌊ ‘ 𝑌 ) = ( ⌊ ‘ 𝑋 ) ↔ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
33 23 25 30 32 syl21anc ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑌 ) = ( ⌊ ‘ 𝑋 ) ↔ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
34 33 biimpar ⊢ ( ( 𝜑 ∧ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ⌊ ‘ 𝑌 ) = ( ⌊ ‘ 𝑋 ) )
35 34 oveq2d ⊢ ( ( 𝜑 ∧ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) = ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) )
36 35 oveq1d ⊢ ( ( 𝜑 ∧ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
37 34 oveq2d ⊢ ( ( 𝜑 ∧ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) = ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) )
38 37 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 )
39 38 oveq1d ⊢ ( ( 𝜑 ∧ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
40 36 39 oveq12d ⊢ ( ( 𝜑 ∧ 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) )
42 24 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑋 ∈ ℝ )
43 42 flcld ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ⌊ ‘ 𝑋 ) ∈ ℤ )
44 43 peano2zd ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℤ )
45 41 44 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑌 ∈ ℤ )
46 flid ⊢ ( 𝑌 ∈ ℤ → ( ⌊ ‘ 𝑌 ) = 𝑌 )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ⌊ ‘ 𝑌 ) = 𝑌 )
48 47 41 eqtrd ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ⌊ ‘ 𝑌 ) = ( ( ⌊ ‘ 𝑋 ) + 1 ) )
49 48 oveq2d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) = ( 𝑌 − ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
50 49 oveq1d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( 𝑌 − ( ( ⌊ ‘ 𝑋 ) + 1 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
51 23 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
52 27 recnd ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ∈ ℂ )
53 51 52 subcld ⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) ∈ ℂ )
54 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
55 22 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
56 55 7 8 10 dvmptrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
57 56 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℂ )
58 57 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℂ )
59 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐵
60 59 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ
61 csbeq1a ⊢ ( 𝑥 = 𝑌 → 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
62 61 eleq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
63 60 62 rspc ⊢ ( 𝑌 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℂ → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
64 16 58 63 sylc ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ )
65 53 54 64 subdird ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
66 51 52 54 subsub4d ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) = ( 𝑌 − ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
67 66 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) − 1 ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( 𝑌 − ( ( ⌊ ‘ 𝑋 ) + 1 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
68 64 mullidd ⊢ ( 𝜑 → ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
69 68 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
70 65 67 69 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑌 − ( ( ⌊ ‘ 𝑋 ) + 1 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( 𝑌 − ( ( ⌊ ‘ 𝑋 ) + 1 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
72 50 71 eqtrd ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
73 25 peano2zd ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℤ )
74 3 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
75 peano2rem ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
76 74 75 syl ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℝ )
77 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
78 74 77 4 lesubaddd ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) ≤ 𝐷 ↔ 𝑀 ≤ ( 𝐷 + 1 ) ) )
79 5 78 mpbird ⊢ ( 𝜑 → ( 𝑀 − 1 ) ≤ 𝐷 )
80 76 4 24 79 17 letrd ⊢ ( 𝜑 → ( 𝑀 − 1 ) ≤ 𝑋 )
81 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
82 3 81 syl ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℤ )
83 flge ⊢ ( ( 𝑋 ∈ ℝ ∧ ( 𝑀 − 1 ) ∈ ℤ ) → ( ( 𝑀 − 1 ) ≤ 𝑋 ↔ ( 𝑀 − 1 ) ≤ ( ⌊ ‘ 𝑋 ) ) )
84 24 82 83 syl2anc ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) ≤ 𝑋 ↔ ( 𝑀 − 1 ) ≤ ( ⌊ ‘ 𝑋 ) ) )
85 80 84 mpbid ⊢ ( 𝜑 → ( 𝑀 − 1 ) ≤ ( ⌊ ‘ 𝑋 ) )
86 74 77 27 lesubaddd ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) ≤ ( ⌊ ‘ 𝑋 ) ↔ 𝑀 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
87 85 86 mpbid ⊢ ( 𝜑 → 𝑀 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) )
88 eluz2 ⊢ ( ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
89 3 73 87 88 syl3anbrc ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
90 9 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
91 90 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℂ )
92 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
93 92 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑘 ∈ 𝑍 )
94 11 eleq1d ⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
95 94 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℂ ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℂ )
96 91 93 95 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ) → 𝐶 ∈ ℂ )
97 eqvisset ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ V )
98 eqeq2 ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → ( 𝑥 = 𝑘 ↔ 𝑥 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
99 98 biimpar ⊢ ( ( 𝑘 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ∧ 𝑥 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝑥 = 𝑘 )
100 99 11 syl ⊢ ( ( 𝑘 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ∧ 𝑥 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → 𝐵 = 𝐶 )
101 97 100 csbied ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 = 𝐶 )
102 101 eqcomd ⊢ ( 𝑘 = ( ( ⌊ ‘ 𝑋 ) + 1 ) → 𝐶 = ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 )
103 89 96 102 fsumm1 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ( ⌊ ‘ 𝑋 ) + 1 ) ) 𝐶 = ( Σ 𝑘 ∈ ( 𝑀 ... ( ( ( ⌊ ‘ 𝑋 ) + 1 ) − 1 ) ) 𝐶 + ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) )
104 ax-1cn ⊢ 1 ∈ ℂ
105 pncan ⊢ ( ( ( ⌊ ‘ 𝑋 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ⌊ ‘ 𝑋 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑋 ) )
106 52 104 105 sylancl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ 𝑋 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑋 ) )
107 106 oveq2d ⊢ ( 𝜑 → ( 𝑀 ... ( ( ( ⌊ ‘ 𝑋 ) + 1 ) − 1 ) ) = ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) )
108 107 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ( ( ⌊ ‘ 𝑋 ) + 1 ) − 1 ) ) 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 )
109 108 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ( ( ⌊ ‘ 𝑋 ) + 1 ) − 1 ) ) 𝐶 + ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) )
110 103 109 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ( ⌊ ‘ 𝑋 ) + 1 ) ) 𝐶 = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( ( ⌊ ‘ 𝑋 ) + 1 ) ) 𝐶 = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) )
112 48 oveq2d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) = ( 𝑀 ... ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
113 112 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ( ⌊ ‘ 𝑋 ) + 1 ) ) 𝐶 )
114 41 csbeq1d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 = ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 )
115 114 oveq2d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ ( ( ⌊ ‘ 𝑋 ) + 1 ) / 𝑥 ⦌ 𝐵 ) )
116 111 113 115 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
117 116 oveq1d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
118 fzfid ⊢ ( 𝜑 → ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ∈ Fin )
119 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
120 119 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) → 𝑘 ∈ 𝑍 )
121 91 120 95 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐶 ∈ ℂ )
122 118 121 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ∈ ℂ )
123 7 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℂ )
124 123 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℂ )
125 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐴
126 125 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℂ
127 csbeq1a ⊢ ( 𝑥 = 𝑌 → 𝐴 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
128 127 eleq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
129 126 128 rspc ⊢ ( 𝑌 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℂ → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
130 16 124 129 sylc ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℂ )
131 122 64 130 addsubd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
132 131 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
133 117 132 eqtrd ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
134 72 133 oveq12d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
135 53 64 mulcld ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
137 64 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ )
138 122 130 subcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
140 136 137 139 nppcan3d ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
141 134 140 eqtrd ⊢ ( ( 𝜑 ∧ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
142 peano2re ⊢ ( ( ⌊ ‘ 𝑋 ) ∈ ℝ → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ )
143 27 142 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ 𝑋 ) + 1 ) ∈ ℝ )
144 23 143 leloed ⊢ ( 𝜑 → ( 𝑌 ≤ ( ( ⌊ ‘ 𝑋 ) + 1 ) ↔ ( 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ∨ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) ) )
145 20 144 mpbid ⊢ ( 𝜑 → ( 𝑌 < ( ( ⌊ ‘ 𝑋 ) + 1 ) ∨ 𝑌 = ( ( ⌊ ‘ 𝑋 ) + 1 ) ) )
146 40 141 145 mpjaodan ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
147 ovex ⊢ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ V
148 nfcv ⊢ Ⅎ 𝑥 𝑌
149 nfcv ⊢ Ⅎ 𝑥 ( 𝑌 − ( ⌊ ‘ 𝑌 ) )
150 nfcv ⊢ Ⅎ 𝑥 ·
151 149 150 59 nfov ⊢ Ⅎ 𝑥 ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
152 nfcv ⊢ Ⅎ 𝑥 +
153 nfcv ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶
154 nfcv ⊢ Ⅎ 𝑥 −
155 153 154 125 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
156 151 152 155 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
157 id ⊢ ( 𝑥 = 𝑌 → 𝑥 = 𝑌 )
158 fveq2 ⊢ ( 𝑥 = 𝑌 → ( ⌊ ‘ 𝑥 ) = ( ⌊ ‘ 𝑌 ) )
159 157 158 oveq12d ⊢ ( 𝑥 = 𝑌 → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) = ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) )
160 159 61 oveq12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) = ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
161 158 oveq2d ⊢ ( 𝑥 = 𝑌 → ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) = ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) )
162 161 sumeq1d ⊢ ( 𝑥 = 𝑌 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 )
163 162 127 oveq12d ⊢ ( 𝑥 = 𝑌 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
164 160 163 oveq12d ⊢ ( 𝑥 = 𝑌 → ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
165 148 156 164 14 fvmptf ⊢ ( ( 𝑌 ∈ 𝑆 ∧ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ V ) → ( 𝐻 ‘ 𝑌 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
166 16 147 165 sylancl ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑌 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
167 135 130 122 subadd23d ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
168 146 166 167 3eqtr4d ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑌 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )