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