MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvfsumlem2 Structured version   Visualization version   GIF version

Theorem dvfsumlem2 25883
Description: Lemma for dvfsumrlim 25888. (Contributed by Mario Carneiro, 17-May-2016.) Avoid ax-mulf 11186. (Revised by GG, 16-Mar-2025.)
Hypotheses
Ref Expression
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
Ref Expression
dvfsumlem2 (𝜑 → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
Distinct variable groups:   𝐵,𝑘   𝑥,𝐶   𝑥,𝑘,𝐷   𝜑,𝑘,𝑥   𝑆,𝑘,𝑥   𝑘,𝑀,𝑥   𝑥,𝑇   𝑘,𝑌,𝑥   𝑥,𝑍   𝑈,𝑘,𝑥   𝑘,𝑋,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥)   𝐶(𝑘)   𝑇(𝑘)   𝐻(𝑥,𝑘)   𝑉(𝑥,𝑘)   𝑍(𝑘)

Proof of Theorem dvfsumlem2
Dummy variables 𝑦 𝑧 𝑚 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . . . . . . 9 𝑆 = (𝑇(,)+∞)
2 ioossre 13382 . . . . . . . . 9 (𝑇(,)+∞) ⊆ ℝ
31, 2eqsstri 4008 . . . . . . . 8 𝑆 ⊆ ℝ
4 dvfsumlem1.2 . . . . . . . 8 (𝜑𝑌𝑆)
53, 4sselid 3972 . . . . . . 7 (𝜑𝑌 ∈ ℝ)
6 dvfsumlem1.1 . . . . . . . . . . 11 (𝜑𝑋𝑆)
76, 1eleqtrdi 2835 . . . . . . . . . 10 (𝜑𝑋 ∈ (𝑇(,)+∞))
8 dvfsum.t . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ)
98rexrd 11261 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ*)
10 elioopnf 13417 . . . . . . . . . . 11 (𝑇 ∈ ℝ* → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
119, 10syl 17 . . . . . . . . . 10 (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
127, 11mpbid 231 . . . . . . . . 9 (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))
1312simpld 494 . . . . . . . 8 (𝜑𝑋 ∈ ℝ)
14 reflcl 13758 . . . . . . . 8 (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
1513, 14syl 17 . . . . . . 7 (𝜑 → (⌊‘𝑋) ∈ ℝ)
165, 15resubcld 11639 . . . . . 6 (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℝ)
17 csbeq1 3888 . . . . . . . 8 (𝑦 = 𝑌𝑦 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
1817eleq1d 2810 . . . . . . 7 (𝑦 = 𝑌 → (𝑦 / 𝑥𝐵 ∈ ℝ ↔ 𝑌 / 𝑥𝐵 ∈ ℝ))
193a1i 11 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℝ)
20 dvfsum.a . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
21 dvfsum.b1 . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝐵𝑉)
22 dvfsum.b3 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
2319, 20, 21, 22dvmptrecl 25880 . . . . . . . . 9 ((𝜑𝑥𝑆) → 𝐵 ∈ ℝ)
2423fmpttd 7106 . . . . . . . 8 (𝜑 → (𝑥𝑆𝐵):𝑆⟶ℝ)
25 nfcv 2895 . . . . . . . . . 10 𝑦𝐵
26 nfcsb1v 3910 . . . . . . . . . 10 𝑥𝑦 / 𝑥𝐵
27 csbeq1a 3899 . . . . . . . . . 10 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
2825, 26, 27cbvmpt 5249 . . . . . . . . 9 (𝑥𝑆𝐵) = (𝑦𝑆𝑦 / 𝑥𝐵)
2928fmpt 7101 . . . . . . . 8 (∀𝑦𝑆 𝑦 / 𝑥𝐵 ∈ ℝ ↔ (𝑥𝑆𝐵):𝑆⟶ℝ)
3024, 29sylibr 233 . . . . . . 7 (𝜑 → ∀𝑦𝑆 𝑦 / 𝑥𝐵 ∈ ℝ)
3118, 30, 4rspcdva 3605 . . . . . 6 (𝜑𝑌 / 𝑥𝐵 ∈ ℝ)
3216, 31remulcld 11241 . . . . 5 (𝜑 → ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℝ)
33 csbeq1 3888 . . . . . . 7 (𝑦 = 𝑌𝑦 / 𝑥𝐴 = 𝑌 / 𝑥𝐴)
3433eleq1d 2810 . . . . . 6 (𝑦 = 𝑌 → (𝑦 / 𝑥𝐴 ∈ ℝ ↔ 𝑌 / 𝑥𝐴 ∈ ℝ))
3520fmpttd 7106 . . . . . . 7 (𝜑 → (𝑥𝑆𝐴):𝑆⟶ℝ)
36 nfcv 2895 . . . . . . . . 9 𝑦𝐴
37 nfcsb1v 3910 . . . . . . . . 9 𝑥𝑦 / 𝑥𝐴
38 csbeq1a 3899 . . . . . . . . 9 (𝑥 = 𝑦𝐴 = 𝑦 / 𝑥𝐴)
3936, 37, 38cbvmpt 5249 . . . . . . . 8 (𝑥𝑆𝐴) = (𝑦𝑆𝑦 / 𝑥𝐴)
4039fmpt 7101 . . . . . . 7 (∀𝑦𝑆 𝑦 / 𝑥𝐴 ∈ ℝ ↔ (𝑥𝑆𝐴):𝑆⟶ℝ)
4135, 40sylibr 233 . . . . . 6 (𝜑 → ∀𝑦𝑆 𝑦 / 𝑥𝐴 ∈ ℝ)
4234, 41, 4rspcdva 3605 . . . . 5 (𝜑𝑌 / 𝑥𝐴 ∈ ℝ)
4332, 42resubcld 11639 . . . 4 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
4413, 15resubcld 11639 . . . . . 6 (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ)
45 csbeq1 3888 . . . . . . . 8 (𝑦 = 𝑋𝑦 / 𝑥𝐵 = 𝑋 / 𝑥𝐵)
4645eleq1d 2810 . . . . . . 7 (𝑦 = 𝑋 → (𝑦 / 𝑥𝐵 ∈ ℝ ↔ 𝑋 / 𝑥𝐵 ∈ ℝ))
4746, 30, 6rspcdva 3605 . . . . . 6 (𝜑𝑋 / 𝑥𝐵 ∈ ℝ)
4844, 47remulcld 11241 . . . . 5 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ∈ ℝ)
49 csbeq1 3888 . . . . . . 7 (𝑦 = 𝑋𝑦 / 𝑥𝐴 = 𝑋 / 𝑥𝐴)
5049eleq1d 2810 . . . . . 6 (𝑦 = 𝑋 → (𝑦 / 𝑥𝐴 ∈ ℝ ↔ 𝑋 / 𝑥𝐴 ∈ ℝ))
5150, 41, 6rspcdva 3605 . . . . 5 (𝜑𝑋 / 𝑥𝐴 ∈ ℝ)
5248, 51resubcld 11639 . . . 4 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
53 fzfid 13935 . . . . 5 (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin)
54 dvfsum.b2 . . . . . . 7 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
5554ralrimiva 3138 . . . . . 6 (𝜑 → ∀𝑥𝑍 𝐵 ∈ ℝ)
56 elfzuz 13494 . . . . . . 7 (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ𝑀))
57 dvfsum.z . . . . . . 7 𝑍 = (ℤ𝑀)
5856, 57eleqtrrdi 2836 . . . . . 6 (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘𝑍)
59 dvfsum.c . . . . . . . 8 (𝑥 = 𝑘𝐵 = 𝐶)
6059eleq1d 2810 . . . . . . 7 (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
6160rspccva 3603 . . . . . 6 ((∀𝑥𝑍 𝐵 ∈ ℝ ∧ 𝑘𝑍) → 𝐶 ∈ ℝ)
6255, 58, 61syl2an 595 . . . . 5 ((𝜑𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ)
6353, 62fsumrecl 15677 . . . 4 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ)
6444, 31remulcld 11241 . . . . . 6 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℝ)
6564, 51resubcld 11639 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
665, 13resubcld 11639 . . . . . . . . 9 (𝜑 → (𝑌𝑋) ∈ ℝ)
6731, 66remulcld 11241 . . . . . . . 8 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℝ)
6831recnd 11239 . . . . . . . . . 10 (𝜑𝑌 / 𝑥𝐵 ∈ ℂ)
695recnd 11239 . . . . . . . . . 10 (𝜑𝑌 ∈ ℂ)
7013recnd 11239 . . . . . . . . . 10 (𝜑𝑋 ∈ ℂ)
7168, 69, 70subdid 11667 . . . . . . . . 9 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) = ((𝑌 / 𝑥𝐵 · 𝑌) − (𝑌 / 𝑥𝐵 · 𝑋)))
72 eqid 2724 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
7372mpomulcn 24707 . . . . . . . . . . . . 13 (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
74 csbeq1 3888 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑌𝑧 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
7574eleq1d 2810 . . . . . . . . . . . . . . 15 (𝑧 = 𝑌 → (𝑧 / 𝑥𝐵 ∈ ℝ ↔ 𝑌 / 𝑥𝐵 ∈ ℝ))
76 nfcv 2895 . . . . . . . . . . . . . . . . . 18 𝑧𝐵
77 nfcsb1v 3910 . . . . . . . . . . . . . . . . . 18 𝑥𝑧 / 𝑥𝐵
78 csbeq1a 3899 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
7976, 77, 78cbvmpt 5249 . . . . . . . . . . . . . . . . 17 (𝑥𝑆𝐵) = (𝑧𝑆𝑧 / 𝑥𝐵)
8079fmpt 7101 . . . . . . . . . . . . . . . 16 (∀𝑧𝑆 𝑧 / 𝑥𝐵 ∈ ℝ ↔ (𝑥𝑆𝐵):𝑆⟶ℝ)
8124, 80sylibr 233 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑧𝑆 𝑧 / 𝑥𝐵 ∈ ℝ)
8275, 81, 4rspcdva 3605 . . . . . . . . . . . . . 14 (𝜑𝑌 / 𝑥𝐵 ∈ ℝ)
83 pnfxr 11265 . . . . . . . . . . . . . . . . . 18 +∞ ∈ ℝ*
8483a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → +∞ ∈ ℝ*)
8512simprd 495 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 < 𝑋)
865ltpnfd 13098 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 < +∞)
87 iccssioo 13390 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋𝑌 < +∞)) → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞))
889, 84, 85, 86, 87syl22anc 836 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞))
8988, 2sstrdi 3986 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
90 ax-resscn 11163 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
9189, 90sstrdi 3986 . . . . . . . . . . . . . 14 (𝜑 → (𝑋[,]𝑌) ⊆ ℂ)
9290a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ⊆ ℂ)
93 cncfmptc 24754 . . . . . . . . . . . . . 14 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑌 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
9482, 91, 92, 93syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑌 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
95 cncfmptid 24755 . . . . . . . . . . . . . 14 (((𝑋[,]𝑌) ⊆ ℝ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ))
9689, 90, 95sylancl 585 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ))
97 remulcl 11191 . . . . . . . . . . . . . 14 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑌 / 𝑥𝐵 · 𝑦) ∈ ℝ)
98 simpl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑌 / 𝑥𝐵 ∈ ℝ)
9998recnd 11239 . . . . . . . . . . . . . . . . . 18 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑌 / 𝑥𝐵 ∈ ℂ)
100 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
101100recnd 11239 . . . . . . . . . . . . . . . . . 18 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
10299, 101jca 511 . . . . . . . . . . . . . . . . 17 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑌 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ))
103 ovmpot 7561 . . . . . . . . . . . . . . . . . 18 ((𝑌 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (𝑌 / 𝑥𝐵 · 𝑦))
104103eqcomd 2730 . . . . . . . . . . . . . . . . 17 ((𝑌 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
105102, 104syl 17 . . . . . . . . . . . . . . . 16 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
106105eleq1d 2810 . . . . . . . . . . . . . . 15 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑌 / 𝑥𝐵 · 𝑦) ∈ ℝ ↔ (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ))
107106biimpd 228 . . . . . . . . . . . . . 14 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑌 / 𝑥𝐵 · 𝑦) ∈ ℝ → (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ))
10897, 107mpd 15 . . . . . . . . . . . . 13 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ)
10972, 73, 94, 96, 90, 108cncfmpt2ss 24758 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
110 df-mpt 5222 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))}
111110eleq1i 2816 . . . . . . . . . . . . 13 ((𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ) ↔ {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ))
112111biimpi 215 . . . . . . . . . . . 12 ((𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ) → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ))
113109, 112syl 17 . . . . . . . . . . 11 (𝜑 → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ))
114 idd 24 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → 𝑦 ∈ (𝑋[,]𝑌)))
115114a1dd 50 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑦 ∈ (𝑋[,]𝑌))))
116115impd 410 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → 𝑦 ∈ (𝑋[,]𝑌)))
117 csbeq1 3888 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 = 𝑌𝑚 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
118117eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑌 → (𝑚 / 𝑥𝐵 ∈ ℝ ↔ 𝑌 / 𝑥𝐵 ∈ ℝ))
119 nfcv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑚𝐵
120 nfcsb1v 3910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑥𝑚 / 𝑥𝐵
121 csbeq1a 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑚𝐵 = 𝑚 / 𝑥𝐵)
122119, 120, 121cbvmpt 5249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝑆𝐵) = (𝑚𝑆𝑚 / 𝑥𝐵)
123122fmpt 7101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑚𝑆 𝑚 / 𝑥𝐵 ∈ ℝ ↔ (𝑥𝑆𝐵):𝑆⟶ℝ)
12424, 123sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑚𝑆 𝑚 / 𝑥𝐵 ∈ ℝ)
125118, 124, 4rspcdva 3605 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑌 / 𝑥𝐵 ∈ ℝ)
126125recnd 11239 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑌 / 𝑥𝐵 ∈ ℂ)
127126adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 / 𝑥𝐵 ∈ ℂ)
128 elicc2 13386 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌)))
12913, 5, 128syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌)))
130129biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌))
131130simp1d 1139 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ)
132131recnd 11239 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℂ)
133127, 132jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑌 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ))
134133, 103syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (𝑌 / 𝑥𝐵 · 𝑦))
135134eqeq2d 2735 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ↔ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦)))
136135biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦)))
137136ex 412 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦))))
138137impd 410 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦)))
139116, 138jcad 512 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦))))
140114a1dd 50 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (𝑌 / 𝑥𝐵 · 𝑦) → 𝑦 ∈ (𝑋[,]𝑌))))
141140impd 410 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦)) → 𝑦 ∈ (𝑋[,]𝑌)))
142 csbeq1 3888 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = 𝑌𝑘 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
143142eleq1d 2810 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 = 𝑌 → (𝑘 / 𝑥𝐵 ∈ ℝ ↔ 𝑌 / 𝑥𝐵 ∈ ℝ))
144 nfcv 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑘𝐵
145 nfcsb1v 3910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑥𝑘 / 𝑥𝐵
146 csbeq1a 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑘𝐵 = 𝑘 / 𝑥𝐵)
147144, 145, 146cbvmpt 5249 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥𝑆𝐵) = (𝑘𝑆𝑘 / 𝑥𝐵)
148147fmpt 7101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (∀𝑘𝑆 𝑘 / 𝑥𝐵 ∈ ℝ ↔ (𝑥𝑆𝐵):𝑆⟶ℝ)
14924, 148sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∀𝑘𝑆 𝑘 / 𝑥𝐵 ∈ ℝ)
150143, 149, 4rspcdva 3605 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑌 / 𝑥𝐵 ∈ ℝ)
151150recnd 11239 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑌 / 𝑥𝐵 ∈ ℂ)
152151adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 / 𝑥𝐵 ∈ ℂ)
153152, 132jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑌 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ))
154153, 104syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
155154eqeq2d 2735 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (𝑌 / 𝑥𝐵 · 𝑦) ↔ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))
156155biimpd 228 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (𝑌 / 𝑥𝐵 · 𝑦) → 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))
157156ex 412 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (𝑌 / 𝑥𝐵 · 𝑦) → 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))))
158157impd 410 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦)) → 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))
159141, 158jcad 512 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦)) → (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))))
160139, 159impbid 211 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦))))
161160opabbidv 5204 . . . . . . . . . . . . . 14 (𝜑 → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦))})
162 df-mpt 5222 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)) = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦))}
163162eqcomi 2733 . . . . . . . . . . . . . . . 16 {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦))
164163eqeq2i 2737 . . . . . . . . . . . . . . 15 ({⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦))} ↔ {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)))
165164biimpi 215 . . . . . . . . . . . . . 14 ({⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵 · 𝑦))} → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)))
166161, 165syl 17 . . . . . . . . . . . . 13 (𝜑 → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)))
167166eleq1d 2810 . . . . . . . . . . . 12 (𝜑 → ({⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ) ↔ (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)))
168167biimpd 228 . . . . . . . . . . 11 (𝜑 → ({⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑌 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)))
169113, 168mpd 15 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
170 reelprrecn 11198 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, ℂ}
171170a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ {ℝ, ℂ})
172 ioossicc 13407 . . . . . . . . . . . . . . 15 (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
173172, 89sstrid 3985 . . . . . . . . . . . . . 14 (𝜑 → (𝑋(,)𝑌) ⊆ ℝ)
174173sselda 3974 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
175174recnd 11239 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
176 1cnd 11206 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 1 ∈ ℂ)
177 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
178177recnd 11239 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
179 1cnd 11206 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 1 ∈ ℂ)
180171dvmptid 25811 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
18172tgioo2 24641 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
182 iooretop 24604 . . . . . . . . . . . . . 14 (𝑋(,)𝑌) ∈ (topGen‘ran (,))
183182a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑋(,)𝑌) ∈ (topGen‘ran (,)))
184171, 178, 179, 180, 173, 181, 72, 183dvmptres 25817 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 1))
185171, 175, 176, 184, 68dvmptcmul 25818 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 1)))
18668mulridd 11228 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐵 · 1) = 𝑌 / 𝑥𝐵)
187186mpteq2dv 5240 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑌 / 𝑥𝐵))
188185, 187eqtrd 2764 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑌 / 𝑥𝐵))
18988, 1sseqtrrdi 4025 . . . . . . . . . . . 12 (𝜑 → (𝑋[,]𝑌) ⊆ 𝑆)
190189resmptd 6030 . . . . . . . . . . 11 (𝜑 → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) = (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦 / 𝑥𝐴))
19120recnd 11239 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝐴 ∈ ℂ)
192191fmpttd 7106 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝑆𝐴):𝑆⟶ℂ)
19322dmeqd 5895 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (ℝ D (𝑥𝑆𝐴)) = dom (𝑥𝑆𝐵))
19421ralrimiva 3138 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑥𝑆 𝐵𝑉)
195 dmmptg 6231 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝑆 𝐵𝑉 → dom (𝑥𝑆𝐵) = 𝑆)
196194, 195syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑥𝑆𝐵) = 𝑆)
197193, 196eqtrd 2764 . . . . . . . . . . . . . . . 16 (𝜑 → dom (ℝ D (𝑥𝑆𝐴)) = 𝑆)
198 dvcn 25773 . . . . . . . . . . . . . . . 16 (((ℝ ⊆ ℂ ∧ (𝑥𝑆𝐴):𝑆⟶ℂ ∧ 𝑆 ⊆ ℝ) ∧ dom (ℝ D (𝑥𝑆𝐴)) = 𝑆) → (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ))
19992, 192, 19, 197, 198syl31anc 1370 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ))
200 cncfcdm 24740 . . . . . . . . . . . . . . 15 ((ℝ ⊆ ℂ ∧ (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ)) → ((𝑥𝑆𝐴) ∈ (𝑆cn→ℝ) ↔ (𝑥𝑆𝐴):𝑆⟶ℝ))
20190, 199, 200sylancr 586 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥𝑆𝐴) ∈ (𝑆cn→ℝ) ↔ (𝑥𝑆𝐴):𝑆⟶ℝ))
20235, 201mpbird 257 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑆𝐴) ∈ (𝑆cn→ℝ))
20339, 202eqeltrrid 2830 . . . . . . . . . . . 12 (𝜑 → (𝑦𝑆𝑦 / 𝑥𝐴) ∈ (𝑆cn→ℝ))
204 rescncf 24739 . . . . . . . . . . . 12 ((𝑋[,]𝑌) ⊆ 𝑆 → ((𝑦𝑆𝑦 / 𝑥𝐴) ∈ (𝑆cn→ℝ) → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ)))
205189, 203, 204sylc 65 . . . . . . . . . . 11 (𝜑 → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
206190, 205eqeltrrd 2826 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦 / 𝑥𝐴) ∈ ((𝑋[,]𝑌)–cn→ℝ))
20741r19.21bi 3240 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐴 ∈ ℝ)
208207recnd 11239 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐴 ∈ ℂ)
20930r19.21bi 3240 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐵 ∈ ℝ)
21039oveq2i 7412 . . . . . . . . . . . 12 (ℝ D (𝑥𝑆𝐴)) = (ℝ D (𝑦𝑆𝑦 / 𝑥𝐴))
21122, 210, 283eqtr3g 2787 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦𝑆𝑦 / 𝑥𝐴)) = (𝑦𝑆𝑦 / 𝑥𝐵))
212172, 189sstrid 3985 . . . . . . . . . . 11 (𝜑 → (𝑋(,)𝑌) ⊆ 𝑆)
213171, 208, 209, 211, 212, 181, 72, 183dvmptres 25817 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦 / 𝑥𝐴)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦 / 𝑥𝐵))
214172sseli 3970 . . . . . . . . . . 11 (𝑦 ∈ (𝑋(,)𝑌) → 𝑦 ∈ (𝑋[,]𝑌))
215 simpl 482 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝜑)
216189sselda 3974 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑆)
2174adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌𝑆)
218 dvfsum.d . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℝ)
219218adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ∈ ℝ)
22013adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ ℝ)
221 dvfsumlem1.3 . . . . . . . . . . . . . 14 (𝜑𝐷𝑋)
222221adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷𝑋)
223130simp2d 1140 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋𝑦)
224219, 220, 131, 222, 223letrd 11368 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷𝑦)
225130simp3d 1141 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑌)
226 dvfsumlem1.5 . . . . . . . . . . . . 13 (𝜑𝑌𝑈)
227226adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌𝑈)
228 simp2r 1197 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌𝑆)
229 eleq1 2813 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑘𝑆𝑌𝑆))
230229anbi2d 628 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌 → ((𝑦𝑆𝑘𝑆) ↔ (𝑦𝑆𝑌𝑆)))
231 breq2 5142 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑦𝑘𝑦𝑌))
232 breq1 5141 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑘𝑈𝑌𝑈))
233231, 2323anbi23d 1435 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌 → ((𝐷𝑦𝑦𝑘𝑘𝑈) ↔ (𝐷𝑦𝑦𝑌𝑌𝑈)))
234230, 2333anbi23d 1435 . . . . . . . . . . . . . . 15 (𝑘 = 𝑌 → ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈))))
235 vex 3470 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ V
236235, 59csbie 3921 . . . . . . . . . . . . . . . . 17 𝑘 / 𝑥𝐵 = 𝐶
237236, 142eqtr3id 2778 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌𝐶 = 𝑌 / 𝑥𝐵)
238237breq1d 5148 . . . . . . . . . . . . . . 15 (𝑘 = 𝑌 → (𝐶𝑦 / 𝑥𝐵𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵))
239234, 238imbi12d 344 . . . . . . . . . . . . . 14 (𝑘 = 𝑌 → (((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵) ↔ ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)))
240 nfv 1909 . . . . . . . . . . . . . . . 16 𝑥(𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈))
241 nfcv 2895 . . . . . . . . . . . . . . . . 17 𝑥𝐶
242 nfcv 2895 . . . . . . . . . . . . . . . . 17 𝑥
243241, 242, 26nfbr 5185 . . . . . . . . . . . . . . . 16 𝑥 𝐶𝑦 / 𝑥𝐵
244240, 243nfim 1891 . . . . . . . . . . . . . . 15 𝑥((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)
245 eleq1 2813 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑆𝑦𝑆))
246245anbi1d 629 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑥𝑆𝑘𝑆) ↔ (𝑦𝑆𝑘𝑆)))
247 breq2 5142 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐷𝑥𝐷𝑦))
248 breq1 5141 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑘𝑦𝑘))
249247, 2483anbi12d 1433 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐷𝑥𝑥𝑘𝑘𝑈) ↔ (𝐷𝑦𝑦𝑘𝑘𝑈)))
250246, 2493anbi23d 1435 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈))))
25127breq2d 5150 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝐶𝐵𝐶𝑦 / 𝑥𝐵))
252250, 251imbi12d 344 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵) ↔ ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)))
253 dvfsum.l . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵)
254244, 252, 253chvarfv 2225 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)
255239, 254vtoclg 3535 . . . . . . . . . . . . 13 (𝑌𝑆 → ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵))
256228, 255mpcom 38 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
257215, 216, 217, 224, 225, 227, 256syl123anc 1384 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
258214, 257sylan2 592 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
25913rexrd 11261 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℝ*)
2605rexrd 11261 . . . . . . . . . . 11 (𝜑𝑌 ∈ ℝ*)
261 dvfsumlem1.4 . . . . . . . . . . 11 (𝜑𝑋𝑌)
262 lbicc2 13438 . . . . . . . . . . 11 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*𝑋𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
263259, 260, 261, 262syl3anc 1368 . . . . . . . . . 10 (𝜑𝑋 ∈ (𝑋[,]𝑌))
264 ubicc2 13439 . . . . . . . . . . 11 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*𝑋𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
265259, 260, 261, 264syl3anc 1368 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑋[,]𝑌))
266 oveq2 7409 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵 · 𝑋))
267 oveq2 7409 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵 · 𝑌))
26813, 5, 169, 188, 206, 213, 258, 263, 265, 261, 266, 49, 267, 33dvle 25862 . . . . . . . . 9 (𝜑 → ((𝑌 / 𝑥𝐵 · 𝑌) − (𝑌 / 𝑥𝐵 · 𝑋)) ≤ (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴))
26971, 268eqbrtrd 5160 . . . . . . . 8 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ≤ (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴))
27067, 42, 51, 269lesubd 11815 . . . . . . 7 (𝜑𝑋 / 𝑥𝐴 ≤ (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
27164recnd 11239 . . . . . . . . 9 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℂ)
27232recnd 11239 . . . . . . . . 9 (𝜑 → ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℂ)
27342recnd 11239 . . . . . . . . 9 (𝜑𝑌 / 𝑥𝐴 ∈ ℂ)
274271, 272, 273subsubd 11596 . . . . . . . 8 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴))
275272, 271negsubdi2d 11584 . . . . . . . . . . 11 (𝜑 → -(((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)))
27615recnd 11239 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘𝑋) ∈ ℂ)
27769, 70, 276nnncan2d 11603 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) = (𝑌𝑋))
278277oveq1d 7416 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · 𝑌 / 𝑥𝐵) = ((𝑌𝑋) · 𝑌 / 𝑥𝐵))
27916recnd 11239 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℂ)
28044recnd 11239 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ)
281279, 280, 68subdird 11668 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)))
28266recnd 11239 . . . . . . . . . . . . . 14 (𝜑 → (𝑌𝑋) ∈ ℂ)
283282, 68mulcomd 11232 . . . . . . . . . . . . 13 (𝜑 → ((𝑌𝑋) · 𝑌 / 𝑥𝐵) = (𝑌 / 𝑥𝐵 · (𝑌𝑋)))
284278, 281, 2833eqtr3d 2772 . . . . . . . . . . . 12 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = (𝑌 / 𝑥𝐵 · (𝑌𝑋)))
285284negeqd 11451 . . . . . . . . . . 11 (𝜑 → -(((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = -(𝑌 / 𝑥𝐵 · (𝑌𝑋)))
286275, 285eqtr3d 2766 . . . . . . . . . 10 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = -(𝑌 / 𝑥𝐵 · (𝑌𝑋)))
287286oveq1d 7416 . . . . . . . . 9 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = (-(𝑌 / 𝑥𝐵 · (𝑌𝑋)) + 𝑌 / 𝑥𝐴))
28867recnd 11239 . . . . . . . . . 10 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℂ)
289288, 273negsubdid 11583 . . . . . . . . 9 (𝜑 → -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴) = (-(𝑌 / 𝑥𝐵 · (𝑌𝑋)) + 𝑌 / 𝑥𝐴))
290287, 289eqtr4d 2767 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴))
291288, 273negsubdi2d 11584 . . . . . . . 8 (𝜑 → -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴) = (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
292274, 290, 2913eqtrd 2768 . . . . . . 7 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
293270, 292breqtrrd 5166 . . . . . 6 (𝜑𝑋 / 𝑥𝐴 ≤ (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)))
29451, 64, 43, 293lesubd 11815 . . . . 5 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
295 flle 13761 . . . . . . . . 9 (𝑋 ∈ ℝ → (⌊‘𝑋) ≤ 𝑋)
29613, 295syl 17 . . . . . . . 8 (𝜑 → (⌊‘𝑋) ≤ 𝑋)
29713, 15subge0d 11801 . . . . . . . 8 (𝜑 → (0 ≤ (𝑋 − (⌊‘𝑋)) ↔ (⌊‘𝑋) ≤ 𝑋))
298296, 297mpbird 257 . . . . . . 7 (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋)))
29945breq2d 5150 . . . . . . . 8 (𝑦 = 𝑋 → (𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵𝑌 / 𝑥𝐵𝑋 / 𝑥𝐵))
300257ralrimiva 3138 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
301299, 300, 263rspcdva 3605 . . . . . . 7 (𝜑𝑌 / 𝑥𝐵𝑋 / 𝑥𝐵)
30231, 47, 44, 298, 301lemul2ad 12151 . . . . . 6 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ≤ ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵))
30364, 48, 51, 302lesub1dd 11827 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
30443, 65, 52, 294, 303letrd 11368 . . . 4 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
30543, 52, 63, 304leadd1dd 11825 . . 3 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
306 dvfsum.m . . . 4 (𝜑𝑀 ∈ ℤ)
307 dvfsum.md . . . 4 (𝜑𝑀 ≤ (𝐷 + 1))
308 dvfsum.u . . . 4 (𝜑𝑈 ∈ ℝ*)
309 dvfsum.h . . . 4 𝐻 = (𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴)))
310 dvfsumlem1.6 . . . 4 (𝜑𝑌 ≤ ((⌊‘𝑋) + 1))
3111, 57, 306, 218, 307, 8, 20, 21, 54, 22, 59, 308, 253, 309, 6, 4, 221, 261, 226, 310dvfsumlem1 25882 . . 3 (𝜑 → (𝐻𝑌) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
31213leidd 11777 . . . 4 (𝜑𝑋𝑋)
313259, 260, 308, 261, 226xrletrd 13138 . . . 4 (𝜑𝑋𝑈)
314 fllep1 13763 . . . . 5 (𝑋 ∈ ℝ → 𝑋 ≤ ((⌊‘𝑋) + 1))
31513, 314syl 17 . . . 4 (𝜑𝑋 ≤ ((⌊‘𝑋) + 1))
3161, 57, 306, 218, 307, 8, 20, 21, 54, 22, 59, 308, 253, 309, 6, 6, 221, 312, 313, 315dvfsumlem1 25882 . . 3 (𝜑 → (𝐻𝑋) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
317305, 311, 3163brtr4d 5170 . 2 (𝜑 → (𝐻𝑌) ≤ (𝐻𝑋))
31852, 47resubcld 11639 . . . . 5 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) ∈ ℝ)
31943, 31resubcld 11639 . . . . 5 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) ∈ ℝ)
320 peano2rem 11524 . . . . . . . . . . 11 ((𝑋 − (⌊‘𝑋)) ∈ ℝ → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℝ)
32144, 320syl 17 . . . . . . . . . 10 (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℝ)
322321, 47remulcld 11241 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℝ)
323322, 51resubcld 11639 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
324 peano2rem 11524 . . . . . . . . . . 11 ((𝑌 − (⌊‘𝑋)) ∈ ℝ → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
32516, 324syl 17 . . . . . . . . . 10 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
326325, 47remulcld 11241 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℝ)
327326, 42resubcld 11639 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
328325, 31remulcld 11241 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ∈ ℝ)
329328, 42resubcld 11639 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
330322recnd 11239 . . . . . . . . . . . . . 14 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℂ)
331326recnd 11239 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℂ)
332330, 331subcld 11568 . . . . . . . . . . . . 13 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) ∈ ℂ)
333332, 273addcomd 11413 . . . . . . . . . . . 12 (𝜑 → (((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = (𝑌 / 𝑥𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
334330, 331, 273subsubd 11596 . . . . . . . . . . . 12 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴))
335273, 331, 330subsub2d 11597 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))) = (𝑌 / 𝑥𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
336333, 334, 3353eqtr4d 2774 . . . . . . . . . . 11 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
337 1cnd 11206 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℂ)
338279, 280, 337nnncan2d 11603 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))))
339338, 277eqtrd 2764 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = (𝑌𝑋))
340339oveq1d 7416 . . . . . . . . . . . . 13 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · 𝑋 / 𝑥𝐵) = ((𝑌𝑋) · 𝑋 / 𝑥𝐵))
341325recnd 11239 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℂ)
342321recnd 11239 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℂ)
34347recnd 11239 . . . . . . . . . . . . . 14 (𝜑𝑋 / 𝑥𝐵 ∈ ℂ)
344341, 342, 343subdird 11668 . . . . . . . . . . . . 13 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · 𝑋 / 𝑥𝐵) = ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)))
345282, 343mulcomd 11232 . . . . . . . . . . . . 13 (𝜑 → ((𝑌𝑋) · 𝑋 / 𝑥𝐵) = (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
346340, 344, 3453eqtr3d 2772 . . . . . . . . . . . 12 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) = (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
347346oveq2d 7417 . . . . . . . . . . 11 (𝜑 → (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))) = (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))))
348336, 347eqtrd 2764 . . . . . . . . . 10 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))))
34947, 66remulcld 11241 . . . . . . . . . . 11 (𝜑 → (𝑋 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℝ)
350 cncfmptc 24754 . . . . . . . . . . . . . . . . 17 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑋 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
35147, 91, 92, 350syl3anc 1368 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑋 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
352 remulcl 11191 . . . . . . . . . . . . . . . . 17 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 / 𝑥𝐵 · 𝑦) ∈ ℝ)
353 simpl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑋 / 𝑥𝐵 ∈ ℝ)
354353recnd 11239 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑋 / 𝑥𝐵 ∈ ℂ)
355 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
356355recnd 11239 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
357354, 356jca 511 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ))
358 ovmpot 7561 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (𝑋 / 𝑥𝐵 · 𝑦))
359358eqcomd 2730 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
360357, 359syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
361360eleq1d 2810 . . . . . . . . . . . . . . . . . 18 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑋 / 𝑥𝐵 · 𝑦) ∈ ℝ ↔ (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ))
362361biimpd 228 . . . . . . . . . . . . . . . . 17 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑋 / 𝑥𝐵 · 𝑦) ∈ ℝ → (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ))
363352, 362mpd 15 . . . . . . . . . . . . . . . 16 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ)
36472, 73, 351, 96, 90, 363cncfmpt2ss 24758 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
365 df-mpt 5222 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))}
366365eleq1i 2816 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ) ↔ {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ))
367366biimpi 215 . . . . . . . . . . . . . . 15 ((𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ) → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ))
368364, 367syl 17 . . . . . . . . . . . . . 14 (𝜑 → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ))
369114a1dd 50 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑦 ∈ (𝑋[,]𝑌))))
370369impd 410 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → 𝑦 ∈ (𝑋[,]𝑌)))
371343adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 / 𝑥𝐵 ∈ ℂ)
372371, 132jca 511 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑋 / 𝑥𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ))
373372, 358syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (𝑋 / 𝑥𝐵 · 𝑦))
374373eqeq2d 2735 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ↔ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦)))
375374biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦)))
376375ex 412 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦))))
377376impd 410 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦)))
378370, 377jcad 512 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦))))
379114a1dd 50 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (𝑋 / 𝑥𝐵 · 𝑦) → 𝑦 ∈ (𝑋[,]𝑌))))
380379impd 410 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦)) → 𝑦 ∈ (𝑋[,]𝑌)))
381372, 359syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
382381eqeq2d 2735 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (𝑋 / 𝑥𝐵 · 𝑦) ↔ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))
383382biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (𝑋 / 𝑥𝐵 · 𝑦) → 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))
384383ex 412 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (𝑋 / 𝑥𝐵 · 𝑦) → 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))))
385384impd 410 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦)) → 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))
386380, 385jcad 512 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦)) → (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))))
387378, 386impbid 211 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦))))
388387opabbidv 5204 . . . . . . . . . . . . . . . . 17 (𝜑 → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦))})
389 df-mpt 5222 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)) = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦))}
390389eqcomi 2733 . . . . . . . . . . . . . . . . . . 19 {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦))
391390eqeq2i 2737 . . . . . . . . . . . . . . . . . 18 ({⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦))} ↔ {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)))
392391biimpi 215 . . . . . . . . . . . . . . . . 17 ({⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵 · 𝑦))} → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)))
393388, 392syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)))
394393eleq1d 2810 . . . . . . . . . . . . . . 15 (𝜑 → ({⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ) ↔ (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)))
395394biimpd 228 . . . . . . . . . . . . . 14 (𝜑 → ({⟨𝑦, 𝑤⟩ ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (𝑋 / 𝑥𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)))
396368, 395mpd 15 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
397171, 175, 176, 184, 343dvmptcmul 25818 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 1)))
398343mulridd 11228 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋 / 𝑥𝐵 · 1) = 𝑋 / 𝑥𝐵)
399398mpteq2dv 5240 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑋 / 𝑥𝐵))
400397, 399eqtrd 2764 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑋 / 𝑥𝐵))
4016adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋𝑆)
402131rexrd 11261 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ*)
403260adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈ ℝ*)
404308adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑈 ∈ ℝ*)
405402, 403, 404, 225, 227xrletrd 13138 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑈)
406 vex 3470 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
407 eleq1 2813 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑘𝑆𝑦𝑆))
408407anbi2d 628 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → ((𝑋𝑆𝑘𝑆) ↔ (𝑋𝑆𝑦𝑆)))
409 breq2 5142 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑋𝑘𝑋𝑦))
410 breq1 5141 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑘𝑈𝑦𝑈))
411409, 4103anbi23d 1435 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → ((𝐷𝑋𝑋𝑘𝑘𝑈) ↔ (𝐷𝑋𝑋𝑦𝑦𝑈)))
412408, 4113anbi23d 1435 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈))))
413 csbeq1 3888 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦𝑘 / 𝑥𝐵 = 𝑦 / 𝑥𝐵)
414236, 413eqtr3id 2778 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦𝐶 = 𝑦 / 𝑥𝐵)
415414breq1d 5148 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → (𝐶𝑋 / 𝑥𝐵𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵))
416412, 415imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → (((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵) ↔ ((𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)))
417 simp2l 1196 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝑋𝑆)
418 nfv 1909 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈))
419 nfcsb1v 3910 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑋 / 𝑥𝐵
420241, 242, 419nfbr 5185 . . . . . . . . . . . . . . . . . . 19 𝑥 𝐶𝑋 / 𝑥𝐵
421418, 420nfim 1891 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)
422 eleq1 2813 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝑥𝑆𝑋𝑆))
423422anbi1d 629 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝑥𝑆𝑘𝑆) ↔ (𝑋𝑆𝑘𝑆)))
424 breq2 5142 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝐷𝑥𝐷𝑋))
425 breq1 5141 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝑥𝑘𝑋𝑘))
426424, 4253anbi12d 1433 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝐷𝑥𝑥𝑘𝑘𝑈) ↔ (𝐷𝑋𝑋𝑘𝑘𝑈)))
427423, 4263anbi23d 1435 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈))))
428 csbeq1a 3899 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋𝐵 = 𝑋 / 𝑥𝐵)
429428breq2d 5150 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (𝐶𝐵𝐶𝑋 / 𝑥𝐵))
430427, 429imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵) ↔ ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)))
431421, 430, 253vtoclg1f 3551 . . . . . . . . . . . . . . . . 17 (𝑋𝑆 → ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵))
432417, 431mpcom 38 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)
433406, 416, 432vtocl 3538 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
434215, 401, 216, 222, 223, 405, 433syl123anc 1384 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
435214, 434sylan2 592 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
436 oveq2 7409 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵 · 𝑋))
437 oveq2 7409 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵 · 𝑌))
43813, 5, 206, 213, 396, 400, 435, 263, 265, 261, 49, 436, 33, 437dvle 25862 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴) ≤ ((𝑋 / 𝑥𝐵 · 𝑌) − (𝑋 / 𝑥𝐵 · 𝑋)))
439343, 69, 70subdid 11667 . . . . . . . . . . . 12 (𝜑 → (𝑋 / 𝑥𝐵 · (𝑌𝑋)) = ((𝑋 / 𝑥𝐵 · 𝑌) − (𝑋 / 𝑥𝐵 · 𝑋)))
440438, 439breqtrrd 5166 . . . . . . . . . . 11 (𝜑 → (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴) ≤ (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
44142, 51, 349, 440subled 11814 . . . . . . . . . 10 (𝜑 → (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))) ≤ 𝑋 / 𝑥𝐴)
442348, 441eqbrtrd 5160 . . . . . . . . 9 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) ≤ 𝑋 / 𝑥𝐴)
443322, 327, 51, 442subled 11814 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
444325renegcld 11638 . . . . . . . . . . . 12 (𝜑 → -((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
445 1red 11212 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
4465, 15, 445lesubadd2d 11810 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (⌊‘𝑋)) ≤ 1 ↔ 𝑌 ≤ ((⌊‘𝑋) + 1)))
447310, 446mpbird 257 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 − (⌊‘𝑋)) ≤ 1)
44816, 445suble0d 11802 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ (𝑌 − (⌊‘𝑋)) ≤ 1))
449447, 448mpbird 257 . . . . . . . . . . . . 13 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ≤ 0)
450325le0neg1d 11782 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1)))
451449, 450mpbid 231 . . . . . . . . . . . 12 (𝜑 → 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1))
45231, 47, 444, 451, 301lemul2ad 12151 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
453341, 68mulneg1d 11664 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵))
454341, 343mulneg1d 11664 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
455452, 453, 4543brtr3d 5169 . . . . . . . . . 10 (𝜑 → -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
456326, 328lenegd 11790 . . . . . . . . . 10 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ↔ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)))
457455, 456mpbird 257 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵))
458326, 328, 42, 457lesub1dd 11827 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
459323, 327, 329, 443, 458letrd 11368 . . . . . . 7 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
460280, 337, 343subdird 11668 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − (1 · 𝑋 / 𝑥𝐵)))
461343mullidd 11229 . . . . . . . . . 10 (𝜑 → (1 · 𝑋 / 𝑥𝐵) = 𝑋 / 𝑥𝐵)
462461oveq2d 7417 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − (1 · 𝑋 / 𝑥𝐵)) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵))
463460, 462eqtrd 2764 . . . . . . . 8 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵))
464463oveq1d 7416 . . . . . . 7 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
465279, 337, 68subdird 11668 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (1 · 𝑌 / 𝑥𝐵)))
46668mullidd 11229 . . . . . . . . . 10 (𝜑 → (1 · 𝑌 / 𝑥𝐵) = 𝑌 / 𝑥𝐵)
467466oveq2d 7417 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (1 · 𝑌 / 𝑥𝐵)) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵))
468465, 467eqtrd 2764 . . . . . . . 8 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵))
469468oveq1d 7416 . . . . . . 7 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
470459, 464, 4693brtr3d 5169 . . . . . 6 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
47148recnd 11239 . . . . . . 7 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ∈ ℂ)
47251recnd 11239 . . . . . . 7 (𝜑𝑋 / 𝑥𝐴 ∈ ℂ)
473471, 472, 343sub32d 11600 . . . . . 6 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
474272, 273, 68sub32d 11600 . . . . . 6 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
475470, 473, 4743brtr4d 5170 . . . . 5 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) ≤ ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵))
476318, 319, 63, 475leadd1dd 11825 . . . 4 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
47752recnd 11239 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℂ)
47863recnd 11239 . . . . 5 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ)
479477, 478, 343addsubd 11589 . . . 4 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵) = (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
48043recnd 11239 . . . . 5 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℂ)
481480, 478, 68addsubd 11589 . . . 4 (𝜑 → (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵) = (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
482476, 479, 4813brtr4d 5170 . . 3 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵) ≤ (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵))
483316oveq1d 7416 . . 3 (𝜑 → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) = (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵))
484311oveq1d 7416 . . 3 (𝜑 → ((𝐻𝑌) − 𝑌 / 𝑥𝐵) = (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵))
485482, 483, 4843brtr4d 5170 . 2 (𝜑 → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵))
486317, 485jca 511 1 (𝜑 → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wral 3053  csb 3885  wss 3940  {cpr 4622   class class class wbr 5138  {copab 5200  cmpt 5221  dom cdm 5666  ran crn 5667  cres 5668  wf 6529  cfv 6533  (class class class)co 7401  cmpo 7403  cc 11104  cr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111  +∞cpnf 11242  *cxr 11244   < clt 11245  cle 11246  cmin 11441  -cneg 11442  cz 12555  cuz 12819  (,)cioo 13321  [,]cicc 13324  ...cfz 13481  cfl 13752  Σcsu 15629  TopOpenctopn 17366  topGenctg 17382  fldccnfld 21228  cnccncf 24718   D cdv 25714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-sum 15630  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-fbas 21225  df-fg 21226  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-nei 22924  df-lp 22962  df-perf 22963  df-cn 23053  df-cnp 23054  df-haus 23141  df-cmp 23213  df-tx 23388  df-hmeo 23581  df-fil 23672  df-fm 23764  df-flim 23765  df-flf 23766  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718
This theorem is referenced by:  dvfsumlem3  25885
  Copyright terms: Public domain W3C validator