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

Theorem dvfsumlem2OLD 25961
Description: Obsolete version of dvfsumlem2 25960 as of 17-Apr-2025. (Contributed by Mario Carneiro, 17-May-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
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
dvfsumlem2OLD (𝜑 → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
Distinct variable groups:   𝐵,𝑘   𝑥,𝐶   𝑥,𝑘,𝐷   𝜑,𝑘,𝑥   𝑆,𝑘,𝑥   𝑘,𝑀,𝑥   𝑥,𝑇   𝑘,𝑌,𝑥   𝑥,𝑍   𝑈,𝑘,𝑥   𝑘,𝑋,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥)   𝐶(𝑘)   𝑇(𝑘)   𝐻(𝑥,𝑘)   𝑉(𝑥,𝑘)   𝑍(𝑘)

Proof of Theorem dvfsumlem2OLD
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . . . . . . 9 𝑆 = (𝑇(,)+∞)
2 ioossre 13417 . . . . . . . . 9 (𝑇(,)+∞) ⊆ ℝ
31, 2eqsstri 4014 . . . . . . . 8 𝑆 ⊆ ℝ
4 dvfsumlem1.2 . . . . . . . 8 (𝜑𝑌𝑆)
53, 4sselid 3978 . . . . . . 7 (𝜑𝑌 ∈ ℝ)
6 dvfsumlem1.1 . . . . . . . . . . 11 (𝜑𝑋𝑆)
76, 1eleqtrdi 2839 . . . . . . . . . 10 (𝜑𝑋 ∈ (𝑇(,)+∞))
8 dvfsum.t . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℝ)
98rexrd 11294 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ*)
10 elioopnf 13452 . . . . . . . . . . 11 (𝑇 ∈ ℝ* → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
119, 10syl 17 . . . . . . . . . 10 (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
127, 11mpbid 231 . . . . . . . . 9 (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))
1312simpld 494 . . . . . . . 8 (𝜑𝑋 ∈ ℝ)
14 reflcl 13793 . . . . . . . 8 (𝑋 ∈ ℝ → (⌊‘𝑋) ∈ ℝ)
1513, 14syl 17 . . . . . . 7 (𝜑 → (⌊‘𝑋) ∈ ℝ)
165, 15resubcld 11672 . . . . . 6 (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℝ)
17 csbeq1 3895 . . . . . . . 8 (𝑦 = 𝑌𝑦 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
1817eleq1d 2814 . . . . . . 7 (𝑦 = 𝑌 → (𝑦 / 𝑥𝐵 ∈ ℝ ↔ 𝑌 / 𝑥𝐵 ∈ ℝ))
193a1i 11 . . . . . . . . . 10 (𝜑𝑆 ⊆ ℝ)
20 dvfsum.a . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
21 dvfsum.b1 . . . . . . . . . 10 ((𝜑𝑥𝑆) → 𝐵𝑉)
22 dvfsum.b3 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
2319, 20, 21, 22dvmptrecl 25957 . . . . . . . . 9 ((𝜑𝑥𝑆) → 𝐵 ∈ ℝ)
2423fmpttd 7125 . . . . . . . 8 (𝜑 → (𝑥𝑆𝐵):𝑆⟶ℝ)
25 nfcv 2899 . . . . . . . . . 10 𝑦𝐵
26 nfcsb1v 3917 . . . . . . . . . 10 𝑥𝑦 / 𝑥𝐵
27 csbeq1a 3906 . . . . . . . . . 10 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
2825, 26, 27cbvmpt 5259 . . . . . . . . 9 (𝑥𝑆𝐵) = (𝑦𝑆𝑦 / 𝑥𝐵)
2928fmpt 7120 . . . . . . . 8 (∀𝑦𝑆 𝑦 / 𝑥𝐵 ∈ ℝ ↔ (𝑥𝑆𝐵):𝑆⟶ℝ)
3024, 29sylibr 233 . . . . . . 7 (𝜑 → ∀𝑦𝑆 𝑦 / 𝑥𝐵 ∈ ℝ)
3118, 30, 4rspcdva 3610 . . . . . 6 (𝜑𝑌 / 𝑥𝐵 ∈ ℝ)
3216, 31remulcld 11274 . . . . 5 (𝜑 → ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℝ)
33 csbeq1 3895 . . . . . . 7 (𝑦 = 𝑌𝑦 / 𝑥𝐴 = 𝑌 / 𝑥𝐴)
3433eleq1d 2814 . . . . . 6 (𝑦 = 𝑌 → (𝑦 / 𝑥𝐴 ∈ ℝ ↔ 𝑌 / 𝑥𝐴 ∈ ℝ))
3520fmpttd 7125 . . . . . . 7 (𝜑 → (𝑥𝑆𝐴):𝑆⟶ℝ)
36 nfcv 2899 . . . . . . . . 9 𝑦𝐴
37 nfcsb1v 3917 . . . . . . . . 9 𝑥𝑦 / 𝑥𝐴
38 csbeq1a 3906 . . . . . . . . 9 (𝑥 = 𝑦𝐴 = 𝑦 / 𝑥𝐴)
3936, 37, 38cbvmpt 5259 . . . . . . . 8 (𝑥𝑆𝐴) = (𝑦𝑆𝑦 / 𝑥𝐴)
4039fmpt 7120 . . . . . . 7 (∀𝑦𝑆 𝑦 / 𝑥𝐴 ∈ ℝ ↔ (𝑥𝑆𝐴):𝑆⟶ℝ)
4135, 40sylibr 233 . . . . . 6 (𝜑 → ∀𝑦𝑆 𝑦 / 𝑥𝐴 ∈ ℝ)
4234, 41, 4rspcdva 3610 . . . . 5 (𝜑𝑌 / 𝑥𝐴 ∈ ℝ)
4332, 42resubcld 11672 . . . 4 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
4413, 15resubcld 11672 . . . . . 6 (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ)
45 csbeq1 3895 . . . . . . . 8 (𝑦 = 𝑋𝑦 / 𝑥𝐵 = 𝑋 / 𝑥𝐵)
4645eleq1d 2814 . . . . . . 7 (𝑦 = 𝑋 → (𝑦 / 𝑥𝐵 ∈ ℝ ↔ 𝑋 / 𝑥𝐵 ∈ ℝ))
4746, 30, 6rspcdva 3610 . . . . . 6 (𝜑𝑋 / 𝑥𝐵 ∈ ℝ)
4844, 47remulcld 11274 . . . . 5 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ∈ ℝ)
49 csbeq1 3895 . . . . . . 7 (𝑦 = 𝑋𝑦 / 𝑥𝐴 = 𝑋 / 𝑥𝐴)
5049eleq1d 2814 . . . . . 6 (𝑦 = 𝑋 → (𝑦 / 𝑥𝐴 ∈ ℝ ↔ 𝑋 / 𝑥𝐴 ∈ ℝ))
5150, 41, 6rspcdva 3610 . . . . 5 (𝜑𝑋 / 𝑥𝐴 ∈ ℝ)
5248, 51resubcld 11672 . . . 4 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
53 fzfid 13970 . . . . 5 (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin)
54 dvfsum.b2 . . . . . . 7 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
5554ralrimiva 3143 . . . . . 6 (𝜑 → ∀𝑥𝑍 𝐵 ∈ ℝ)
56 elfzuz 13529 . . . . . . 7 (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ𝑀))
57 dvfsum.z . . . . . . 7 𝑍 = (ℤ𝑀)
5856, 57eleqtrrdi 2840 . . . . . 6 (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘𝑍)
59 dvfsum.c . . . . . . . 8 (𝑥 = 𝑘𝐵 = 𝐶)
6059eleq1d 2814 . . . . . . 7 (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ))
6160rspccva 3608 . . . . . 6 ((∀𝑥𝑍 𝐵 ∈ ℝ ∧ 𝑘𝑍) → 𝐶 ∈ ℝ)
6255, 58, 61syl2an 595 . . . . 5 ((𝜑𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ)
6353, 62fsumrecl 15712 . . . 4 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ)
6444, 31remulcld 11274 . . . . . 6 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℝ)
6564, 51resubcld 11672 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
665, 13resubcld 11672 . . . . . . . . 9 (𝜑 → (𝑌𝑋) ∈ ℝ)
6731, 66remulcld 11274 . . . . . . . 8 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℝ)
6831recnd 11272 . . . . . . . . . 10 (𝜑𝑌 / 𝑥𝐵 ∈ ℂ)
695recnd 11272 . . . . . . . . . 10 (𝜑𝑌 ∈ ℂ)
7013recnd 11272 . . . . . . . . . 10 (𝜑𝑋 ∈ ℂ)
7168, 69, 70subdid 11700 . . . . . . . . 9 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) = ((𝑌 / 𝑥𝐵 · 𝑌) − (𝑌 / 𝑥𝐵 · 𝑋)))
72 eqid 2728 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
7372mulcn 24782 . . . . . . . . . . 11 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
74 pnfxr 11298 . . . . . . . . . . . . . . . 16 +∞ ∈ ℝ*
7574a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → +∞ ∈ ℝ*)
7612simprd 495 . . . . . . . . . . . . . . 15 (𝜑𝑇 < 𝑋)
775ltpnfd 13133 . . . . . . . . . . . . . . 15 (𝜑𝑌 < +∞)
78 iccssioo 13425 . . . . . . . . . . . . . . 15 (((𝑇 ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋𝑌 < +∞)) → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞))
799, 75, 76, 77, 78syl22anc 838 . . . . . . . . . . . . . 14 (𝜑 → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞))
8079, 2sstrdi 3992 . . . . . . . . . . . . 13 (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
81 ax-resscn 11195 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
8280, 81sstrdi 3992 . . . . . . . . . . . 12 (𝜑 → (𝑋[,]𝑌) ⊆ ℂ)
8381a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ⊆ ℂ)
84 cncfmptc 24831 . . . . . . . . . . . 12 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑌 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
8531, 82, 83, 84syl3anc 1369 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑌 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
86 cncfmptid 24832 . . . . . . . . . . . 12 (((𝑋[,]𝑌) ⊆ ℝ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ))
8780, 81, 86sylancl 585 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ))
88 remulcl 11223 . . . . . . . . . . 11 ((𝑌 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑌 / 𝑥𝐵 · 𝑦) ∈ ℝ)
8972, 73, 85, 87, 81, 88cncfmpt2ss 24835 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
90 reelprrecn 11230 . . . . . . . . . . . . 13 ℝ ∈ {ℝ, ℂ}
9190a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ {ℝ, ℂ})
92 ioossicc 13442 . . . . . . . . . . . . . . 15 (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
9392, 80sstrid 3991 . . . . . . . . . . . . . 14 (𝜑 → (𝑋(,)𝑌) ⊆ ℝ)
9493sselda 3980 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ)
9594recnd 11272 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ)
96 1cnd 11239 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 1 ∈ ℂ)
97 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
9897recnd 11272 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
99 1cnd 11239 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → 1 ∈ ℂ)
10091dvmptid 25888 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
10172tgioo2 24718 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
102 iooretop 24681 . . . . . . . . . . . . . 14 (𝑋(,)𝑌) ∈ (topGen‘ran (,))
103102a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑋(,)𝑌) ∈ (topGen‘ran (,)))
10491, 98, 99, 100, 93, 101, 72, 103dvmptres 25894 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 1))
10591, 95, 96, 104, 68dvmptcmul 25895 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 1)))
10668mulridd 11261 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐵 · 1) = 𝑌 / 𝑥𝐵)
107106mpteq2dv 5250 . . . . . . . . . . 11 (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑌 / 𝑥𝐵))
108105, 107eqtrd 2768 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑌 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑌 / 𝑥𝐵))
10979, 1sseqtrrdi 4031 . . . . . . . . . . . 12 (𝜑 → (𝑋[,]𝑌) ⊆ 𝑆)
110109resmptd 6044 . . . . . . . . . . 11 (𝜑 → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) = (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦 / 𝑥𝐴))
11120recnd 11272 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝑆) → 𝐴 ∈ ℂ)
112111fmpttd 7125 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝑆𝐴):𝑆⟶ℂ)
11322dmeqd 5908 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (ℝ D (𝑥𝑆𝐴)) = dom (𝑥𝑆𝐵))
11421ralrimiva 3143 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑥𝑆 𝐵𝑉)
115 dmmptg 6246 . . . . . . . . . . . . . . . . . 18 (∀𝑥𝑆 𝐵𝑉 → dom (𝑥𝑆𝐵) = 𝑆)
116114, 115syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑥𝑆𝐵) = 𝑆)
117113, 116eqtrd 2768 . . . . . . . . . . . . . . . 16 (𝜑 → dom (ℝ D (𝑥𝑆𝐴)) = 𝑆)
118 dvcn 25850 . . . . . . . . . . . . . . . 16 (((ℝ ⊆ ℂ ∧ (𝑥𝑆𝐴):𝑆⟶ℂ ∧ 𝑆 ⊆ ℝ) ∧ dom (ℝ D (𝑥𝑆𝐴)) = 𝑆) → (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ))
11983, 112, 19, 117, 118syl31anc 1371 . . . . . . . . . . . . . . 15 (𝜑 → (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ))
120 cncfcdm 24817 . . . . . . . . . . . . . . 15 ((ℝ ⊆ ℂ ∧ (𝑥𝑆𝐴) ∈ (𝑆cn→ℂ)) → ((𝑥𝑆𝐴) ∈ (𝑆cn→ℝ) ↔ (𝑥𝑆𝐴):𝑆⟶ℝ))
12181, 119, 120sylancr 586 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥𝑆𝐴) ∈ (𝑆cn→ℝ) ↔ (𝑥𝑆𝐴):𝑆⟶ℝ))
12235, 121mpbird 257 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑆𝐴) ∈ (𝑆cn→ℝ))
12339, 122eqeltrrid 2834 . . . . . . . . . . . 12 (𝜑 → (𝑦𝑆𝑦 / 𝑥𝐴) ∈ (𝑆cn→ℝ))
124 rescncf 24816 . . . . . . . . . . . 12 ((𝑋[,]𝑌) ⊆ 𝑆 → ((𝑦𝑆𝑦 / 𝑥𝐴) ∈ (𝑆cn→ℝ) → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ)))
125109, 123, 124sylc 65 . . . . . . . . . . 11 (𝜑 → ((𝑦𝑆𝑦 / 𝑥𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
126110, 125eqeltrrd 2830 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦 / 𝑥𝐴) ∈ ((𝑋[,]𝑌)–cn→ℝ))
12741r19.21bi 3245 . . . . . . . . . . . 12 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐴 ∈ ℝ)
128127recnd 11272 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐴 ∈ ℂ)
12930r19.21bi 3245 . . . . . . . . . . 11 ((𝜑𝑦𝑆) → 𝑦 / 𝑥𝐵 ∈ ℝ)
13039oveq2i 7431 . . . . . . . . . . . 12 (ℝ D (𝑥𝑆𝐴)) = (ℝ D (𝑦𝑆𝑦 / 𝑥𝐴))
13122, 130, 283eqtr3g 2791 . . . . . . . . . . 11 (𝜑 → (ℝ D (𝑦𝑆𝑦 / 𝑥𝐴)) = (𝑦𝑆𝑦 / 𝑥𝐵))
13292, 109sstrid 3991 . . . . . . . . . . 11 (𝜑 → (𝑋(,)𝑌) ⊆ 𝑆)
13391, 128, 129, 131, 132, 101, 72, 103dvmptres 25894 . . . . . . . . . 10 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦 / 𝑥𝐴)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦 / 𝑥𝐵))
13492sseli 3976 . . . . . . . . . . 11 (𝑦 ∈ (𝑋(,)𝑌) → 𝑦 ∈ (𝑋[,]𝑌))
135 simpl 482 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝜑)
136109sselda 3980 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑆)
1374adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌𝑆)
138 dvfsum.d . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℝ)
139138adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ∈ ℝ)
14013adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ ℝ)
141 elicc2 13421 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌)))
14213, 5, 141syl2anc 583 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌)))
143142biimpa 476 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → (𝑦 ∈ ℝ ∧ 𝑋𝑦𝑦𝑌))
144143simp1d 1140 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ)
145 dvfsumlem1.3 . . . . . . . . . . . . . 14 (𝜑𝐷𝑋)
146145adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷𝑋)
147143simp2d 1141 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋𝑦)
148139, 140, 144, 146, 147letrd 11401 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝐷𝑦)
149143simp3d 1142 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑌)
150 dvfsumlem1.5 . . . . . . . . . . . . 13 (𝜑𝑌𝑈)
151150adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌𝑈)
152 simp2r 1198 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌𝑆)
153 eleq1 2817 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑘𝑆𝑌𝑆))
154153anbi2d 629 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌 → ((𝑦𝑆𝑘𝑆) ↔ (𝑦𝑆𝑌𝑆)))
155 breq2 5152 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑦𝑘𝑦𝑌))
156 breq1 5151 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌 → (𝑘𝑈𝑌𝑈))
157155, 1563anbi23d 1436 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌 → ((𝐷𝑦𝑦𝑘𝑘𝑈) ↔ (𝐷𝑦𝑦𝑌𝑌𝑈)))
158154, 1573anbi23d 1436 . . . . . . . . . . . . . . 15 (𝑘 = 𝑌 → ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈))))
159 vex 3475 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ V
160159, 59csbie 3928 . . . . . . . . . . . . . . . . 17 𝑘 / 𝑥𝐵 = 𝐶
161 csbeq1 3895 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑌𝑘 / 𝑥𝐵 = 𝑌 / 𝑥𝐵)
162160, 161eqtr3id 2782 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑌𝐶 = 𝑌 / 𝑥𝐵)
163162breq1d 5158 . . . . . . . . . . . . . . 15 (𝑘 = 𝑌 → (𝐶𝑦 / 𝑥𝐵𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵))
164158, 163imbi12d 344 . . . . . . . . . . . . . 14 (𝑘 = 𝑌 → (((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵) ↔ ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)))
165 nfv 1910 . . . . . . . . . . . . . . . 16 𝑥(𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈))
166 nfcv 2899 . . . . . . . . . . . . . . . . 17 𝑥𝐶
167 nfcv 2899 . . . . . . . . . . . . . . . . 17 𝑥
168166, 167, 26nfbr 5195 . . . . . . . . . . . . . . . 16 𝑥 𝐶𝑦 / 𝑥𝐵
169165, 168nfim 1892 . . . . . . . . . . . . . . 15 𝑥((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)
170 eleq1 2817 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑆𝑦𝑆))
171170anbi1d 630 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝑥𝑆𝑘𝑆) ↔ (𝑦𝑆𝑘𝑆)))
172 breq2 5152 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐷𝑥𝐷𝑦))
173 breq1 5151 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑥𝑘𝑦𝑘))
174172, 1733anbi12d 1434 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐷𝑥𝑥𝑘𝑘𝑈) ↔ (𝐷𝑦𝑦𝑘𝑘𝑈)))
175171, 1743anbi23d 1436 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈))))
17627breq2d 5160 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (𝐶𝐵𝐶𝑦 / 𝑥𝐵))
177175, 176imbi12d 344 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵) ↔ ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)))
178 dvfsum.l . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵)
179169, 177, 178chvarfv 2229 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦𝑆𝑘𝑆) ∧ (𝐷𝑦𝑦𝑘𝑘𝑈)) → 𝐶𝑦 / 𝑥𝐵)
180164, 179vtoclg 3540 . . . . . . . . . . . . 13 (𝑌𝑆 → ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵))
181152, 180mpcom 38 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦𝑆𝑌𝑆) ∧ (𝐷𝑦𝑦𝑌𝑌𝑈)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
182135, 136, 137, 148, 149, 151, 181syl123anc 1385 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
183134, 182sylan2 592 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
18413rexrd 11294 . . . . . . . . . . 11 (𝜑𝑋 ∈ ℝ*)
1855rexrd 11294 . . . . . . . . . . 11 (𝜑𝑌 ∈ ℝ*)
186 dvfsumlem1.4 . . . . . . . . . . 11 (𝜑𝑋𝑌)
187 lbicc2 13473 . . . . . . . . . . 11 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*𝑋𝑌) → 𝑋 ∈ (𝑋[,]𝑌))
188184, 185, 186, 187syl3anc 1369 . . . . . . . . . 10 (𝜑𝑋 ∈ (𝑋[,]𝑌))
189 ubicc2 13474 . . . . . . . . . . 11 ((𝑋 ∈ ℝ*𝑌 ∈ ℝ*𝑋𝑌) → 𝑌 ∈ (𝑋[,]𝑌))
190184, 185, 186, 189syl3anc 1369 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑋[,]𝑌))
191 oveq2 7428 . . . . . . . . . 10 (𝑦 = 𝑋 → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵 · 𝑋))
192 oveq2 7428 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑌 / 𝑥𝐵 · 𝑦) = (𝑌 / 𝑥𝐵 · 𝑌))
19313, 5, 89, 108, 126, 133, 183, 188, 190, 186, 191, 49, 192, 33dvle 25939 . . . . . . . . 9 (𝜑 → ((𝑌 / 𝑥𝐵 · 𝑌) − (𝑌 / 𝑥𝐵 · 𝑋)) ≤ (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴))
19471, 193eqbrtrd 5170 . . . . . . . 8 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ≤ (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴))
19567, 42, 51, 194lesubd 11848 . . . . . . 7 (𝜑𝑋 / 𝑥𝐴 ≤ (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
19664recnd 11272 . . . . . . . . 9 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℂ)
19732recnd 11272 . . . . . . . . 9 (𝜑 → ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ∈ ℂ)
19842recnd 11272 . . . . . . . . 9 (𝜑𝑌 / 𝑥𝐴 ∈ ℂ)
199196, 197, 198subsubd 11629 . . . . . . . 8 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴))
200197, 196negsubdi2d 11617 . . . . . . . . . . 11 (𝜑 → -(((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)))
20115recnd 11272 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘𝑋) ∈ ℂ)
20269, 70, 201nnncan2d 11636 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) = (𝑌𝑋))
203202oveq1d 7435 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · 𝑌 / 𝑥𝐵) = ((𝑌𝑋) · 𝑌 / 𝑥𝐵))
20416recnd 11272 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℂ)
20544recnd 11272 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ)
206204, 205, 68subdird 11701 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)))
20766recnd 11272 . . . . . . . . . . . . . 14 (𝜑 → (𝑌𝑋) ∈ ℂ)
208207, 68mulcomd 11265 . . . . . . . . . . . . 13 (𝜑 → ((𝑌𝑋) · 𝑌 / 𝑥𝐵) = (𝑌 / 𝑥𝐵 · (𝑌𝑋)))
209203, 206, 2083eqtr3d 2776 . . . . . . . . . . . 12 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = (𝑌 / 𝑥𝐵 · (𝑌𝑋)))
210209negeqd 11484 . . . . . . . . . . 11 (𝜑 → -(((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = -(𝑌 / 𝑥𝐵 · (𝑌𝑋)))
211200, 210eqtr3d 2770 . . . . . . . . . 10 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) = -(𝑌 / 𝑥𝐵 · (𝑌𝑋)))
212211oveq1d 7435 . . . . . . . . 9 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = (-(𝑌 / 𝑥𝐵 · (𝑌𝑋)) + 𝑌 / 𝑥𝐴))
21367recnd 11272 . . . . . . . . . 10 (𝜑 → (𝑌 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℂ)
214213, 198negsubdid 11616 . . . . . . . . 9 (𝜑 → -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴) = (-(𝑌 / 𝑥𝐵 · (𝑌𝑋)) + 𝑌 / 𝑥𝐴))
215212, 214eqtr4d 2771 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − ((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴))
216213, 198negsubdi2d 11617 . . . . . . . 8 (𝜑 → -((𝑌 / 𝑥𝐵 · (𝑌𝑋)) − 𝑌 / 𝑥𝐴) = (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
217199, 215, 2163eqtrd 2772 . . . . . . 7 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − (𝑌 / 𝑥𝐵 · (𝑌𝑋))))
218195, 217breqtrrd 5176 . . . . . 6 (𝜑𝑋 / 𝑥𝐴 ≤ (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)))
21951, 64, 43, 218lesubd 11848 . . . . 5 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
220 flle 13796 . . . . . . . . 9 (𝑋 ∈ ℝ → (⌊‘𝑋) ≤ 𝑋)
22113, 220syl 17 . . . . . . . 8 (𝜑 → (⌊‘𝑋) ≤ 𝑋)
22213, 15subge0d 11834 . . . . . . . 8 (𝜑 → (0 ≤ (𝑋 − (⌊‘𝑋)) ↔ (⌊‘𝑋) ≤ 𝑋))
223221, 222mpbird 257 . . . . . . 7 (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋)))
22445breq2d 5160 . . . . . . . 8 (𝑦 = 𝑋 → (𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵𝑌 / 𝑥𝐵𝑋 / 𝑥𝐵))
225182ralrimiva 3143 . . . . . . . 8 (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)𝑌 / 𝑥𝐵𝑦 / 𝑥𝐵)
226224, 225, 188rspcdva 3610 . . . . . . 7 (𝜑𝑌 / 𝑥𝐵𝑋 / 𝑥𝐵)
22731, 47, 44, 223, 226lemul2ad 12184 . . . . . 6 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) ≤ ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵))
22864, 48, 51, 227lesub1dd 11860 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
22943, 65, 52, 219, 228letrd 11401 . . . 4 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
23043, 52, 63, 229leadd1dd 11858 . . 3 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
231 dvfsum.m . . . 4 (𝜑𝑀 ∈ ℤ)
232 dvfsum.md . . . 4 (𝜑𝑀 ≤ (𝐷 + 1))
233 dvfsum.u . . . 4 (𝜑𝑈 ∈ ℝ*)
234 dvfsum.h . . . 4 𝐻 = (𝑥𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴)))
235 dvfsumlem1.6 . . . 4 (𝜑𝑌 ≤ ((⌊‘𝑋) + 1))
2361, 57, 231, 138, 232, 8, 20, 21, 54, 22, 59, 233, 178, 234, 6, 4, 145, 186, 150, 235dvfsumlem1 25959 . . 3 (𝜑 → (𝐻𝑌) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
23713leidd 11810 . . . 4 (𝜑𝑋𝑋)
238184, 185, 233, 186, 150xrletrd 13173 . . . 4 (𝜑𝑋𝑈)
239 fllep1 13798 . . . . 5 (𝑋 ∈ ℝ → 𝑋 ≤ ((⌊‘𝑋) + 1))
24013, 239syl 17 . . . 4 (𝜑𝑋 ≤ ((⌊‘𝑋) + 1))
2411, 57, 231, 138, 232, 8, 20, 21, 54, 22, 59, 233, 178, 234, 6, 6, 145, 237, 238, 240dvfsumlem1 25959 . . 3 (𝜑 → (𝐻𝑋) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
242230, 236, 2413brtr4d 5180 . 2 (𝜑 → (𝐻𝑌) ≤ (𝐻𝑋))
24352, 47resubcld 11672 . . . . 5 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) ∈ ℝ)
24443, 31resubcld 11672 . . . . 5 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) ∈ ℝ)
245 peano2rem 11557 . . . . . . . . . . 11 ((𝑋 − (⌊‘𝑋)) ∈ ℝ → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℝ)
24644, 245syl 17 . . . . . . . . . 10 (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℝ)
247246, 47remulcld 11274 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℝ)
248247, 51resubcld 11672 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℝ)
249 peano2rem 11557 . . . . . . . . . . 11 ((𝑌 − (⌊‘𝑋)) ∈ ℝ → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
25016, 249syl 17 . . . . . . . . . 10 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
251250, 47remulcld 11274 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℝ)
252251, 42resubcld 11672 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
253250, 31remulcld 11274 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ∈ ℝ)
254253, 42resubcld 11672 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℝ)
255247recnd 11272 . . . . . . . . . . . . . 14 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℂ)
256251recnd 11272 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ∈ ℂ)
257255, 256subcld 11601 . . . . . . . . . . . . 13 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) ∈ ℂ)
258257, 198addcomd 11446 . . . . . . . . . . . 12 (𝜑 → (((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴) = (𝑌 / 𝑥𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
259255, 256, 198subsubd 11629 . . . . . . . . . . . 12 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) + 𝑌 / 𝑥𝐴))
260198, 256, 255subsub2d 11630 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))) = (𝑌 / 𝑥𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
261258, 259, 2603eqtr4d 2778 . . . . . . . . . . 11 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))))
262 1cnd 11239 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℂ)
263204, 205, 262nnncan2d 11636 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))))
264263, 202eqtrd 2768 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = (𝑌𝑋))
265264oveq1d 7435 . . . . . . . . . . . . 13 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · 𝑋 / 𝑥𝐵) = ((𝑌𝑋) · 𝑋 / 𝑥𝐵))
266250recnd 11272 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈ ℂ)
267246recnd 11272 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈ ℂ)
26847recnd 11272 . . . . . . . . . . . . . 14 (𝜑𝑋 / 𝑥𝐵 ∈ ℂ)
269266, 267, 268subdird 11701 . . . . . . . . . . . . 13 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · 𝑋 / 𝑥𝐵) = ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)))
270207, 268mulcomd 11265 . . . . . . . . . . . . 13 (𝜑 → ((𝑌𝑋) · 𝑋 / 𝑥𝐵) = (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
271265, 269, 2703eqtr3d 2776 . . . . . . . . . . . 12 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)) = (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
272271oveq2d 7436 . . . . . . . . . . 11 (𝜑 → (𝑌 / 𝑥𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))) = (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))))
273261, 272eqtrd 2768 . . . . . . . . . 10 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) = (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))))
27447, 66remulcld 11274 . . . . . . . . . . 11 (𝜑 → (𝑋 / 𝑥𝐵 · (𝑌𝑋)) ∈ ℝ)
275 cncfmptc 24831 . . . . . . . . . . . . . . 15 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑋 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
27647, 82, 83, 275syl3anc 1369 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑋 / 𝑥𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ))
277 remulcl 11223 . . . . . . . . . . . . . 14 ((𝑋 / 𝑥𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 / 𝑥𝐵 · 𝑦) ∈ ℝ)
27872, 73, 276, 87, 81, 277cncfmpt2ss 24835 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))
27991, 95, 96, 104, 268dvmptcmul 25895 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 1)))
280268mulridd 11261 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋 / 𝑥𝐵 · 1) = 𝑋 / 𝑥𝐵)
281280mpteq2dv 5250 . . . . . . . . . . . . . 14 (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑋 / 𝑥𝐵))
282279, 281eqtrd 2768 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (𝑋 / 𝑥𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑋 / 𝑥𝐵))
2836adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑋𝑆)
284144rexrd 11294 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ*)
285185adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈ ℝ*)
286233adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑈 ∈ ℝ*)
287284, 285, 286, 149, 151xrletrd 13173 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦𝑈)
288 vex 3475 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
289 eleq1 2817 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑘𝑆𝑦𝑆))
290289anbi2d 629 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → ((𝑋𝑆𝑘𝑆) ↔ (𝑋𝑆𝑦𝑆)))
291 breq2 5152 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑋𝑘𝑋𝑦))
292 breq1 5151 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑘𝑈𝑦𝑈))
293291, 2923anbi23d 1436 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → ((𝐷𝑋𝑋𝑘𝑘𝑈) ↔ (𝐷𝑋𝑋𝑦𝑦𝑈)))
294290, 2933anbi23d 1436 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈))))
295 csbeq1 3895 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦𝑘 / 𝑥𝐵 = 𝑦 / 𝑥𝐵)
296160, 295eqtr3id 2782 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦𝐶 = 𝑦 / 𝑥𝐵)
297296breq1d 5158 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → (𝐶𝑋 / 𝑥𝐵𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵))
298294, 297imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → (((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵) ↔ ((𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)))
299 simp2l 1197 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝑋𝑆)
300 nfv 1910 . . . . . . . . . . . . . . . . . . 19 𝑥(𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈))
301 nfcsb1v 3917 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑋 / 𝑥𝐵
302166, 167, 301nfbr 5195 . . . . . . . . . . . . . . . . . . 19 𝑥 𝐶𝑋 / 𝑥𝐵
303300, 302nfim 1892 . . . . . . . . . . . . . . . . . 18 𝑥((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)
304 eleq1 2817 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝑥𝑆𝑋𝑆))
305304anbi1d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝑥𝑆𝑘𝑆) ↔ (𝑋𝑆𝑘𝑆)))
306 breq2 5152 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝐷𝑥𝐷𝑋))
307 breq1 5151 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑋 → (𝑥𝑘𝑋𝑘))
308306, 3073anbi12d 1434 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋 → ((𝐷𝑥𝑥𝑘𝑘𝑈) ↔ (𝐷𝑋𝑋𝑘𝑘𝑈)))
309305, 3083anbi23d 1436 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) ↔ (𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈))))
310 csbeq1a 3906 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑋𝐵 = 𝑋 / 𝑥𝐵)
311310breq2d 5160 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑋 → (𝐶𝐵𝐶𝑋 / 𝑥𝐵))
312309, 311imbi12d 344 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘𝑈)) → 𝐶𝐵) ↔ ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)))
313303, 312, 178vtoclg1f 3556 . . . . . . . . . . . . . . . . 17 (𝑋𝑆 → ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵))
314299, 313mpcom 38 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑋𝑆𝑘𝑆) ∧ (𝐷𝑋𝑋𝑘𝑘𝑈)) → 𝐶𝑋 / 𝑥𝐵)
315288, 298, 314vtocl 3543 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑋𝑆𝑦𝑆) ∧ (𝐷𝑋𝑋𝑦𝑦𝑈)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
316135, 283, 136, 146, 147, 287, 315syl123anc 1385 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
317134, 316sylan2 592 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 / 𝑥𝐵𝑋 / 𝑥𝐵)
318 oveq2 7428 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵 · 𝑋))
319 oveq2 7428 . . . . . . . . . . . . 13 (𝑦 = 𝑌 → (𝑋 / 𝑥𝐵 · 𝑦) = (𝑋 / 𝑥𝐵 · 𝑌))
32013, 5, 126, 133, 278, 282, 317, 188, 190, 186, 49, 318, 33, 319dvle 25939 . . . . . . . . . . . 12 (𝜑 → (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴) ≤ ((𝑋 / 𝑥𝐵 · 𝑌) − (𝑋 / 𝑥𝐵 · 𝑋)))
321268, 69, 70subdid 11700 . . . . . . . . . . . 12 (𝜑 → (𝑋 / 𝑥𝐵 · (𝑌𝑋)) = ((𝑋 / 𝑥𝐵 · 𝑌) − (𝑋 / 𝑥𝐵 · 𝑋)))
322320, 321breqtrrd 5176 . . . . . . . . . . 11 (𝜑 → (𝑌 / 𝑥𝐴𝑋 / 𝑥𝐴) ≤ (𝑋 / 𝑥𝐵 · (𝑌𝑋)))
32342, 51, 274, 322subled 11847 . . . . . . . . . 10 (𝜑 → (𝑌 / 𝑥𝐴 − (𝑋 / 𝑥𝐵 · (𝑌𝑋))) ≤ 𝑋 / 𝑥𝐴)
324273, 323eqbrtrd 5170 . . . . . . . . 9 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴)) ≤ 𝑋 / 𝑥𝐴)
325247, 252, 51, 324subled 11847 . . . . . . . 8 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
326250renegcld 11671 . . . . . . . . . . . 12 (𝜑 → -((𝑌 − (⌊‘𝑋)) − 1) ∈ ℝ)
327 1red 11245 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
3285, 15, 327lesubadd2d 11843 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (⌊‘𝑋)) ≤ 1 ↔ 𝑌 ≤ ((⌊‘𝑋) + 1)))
329235, 328mpbird 257 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 − (⌊‘𝑋)) ≤ 1)
33016, 327suble0d 11835 . . . . . . . . . . . . . 14 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ (𝑌 − (⌊‘𝑋)) ≤ 1))
331329, 330mpbird 257 . . . . . . . . . . . . 13 (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ≤ 0)
332250le0neg1d 11815 . . . . . . . . . . . . 13 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1)))
333331, 332mpbid 231 . . . . . . . . . . . 12 (𝜑 → 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1))
33431, 47, 326, 333, 226lemul2ad 12184 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
335266, 68mulneg1d 11697 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵))
336266, 268mulneg1d 11697 . . . . . . . . . . 11 (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
337334, 335, 3363brtr3d 5179 . . . . . . . . . 10 (𝜑 → -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵))
338251, 253lenegd 11823 . . . . . . . . . 10 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ↔ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵)))
339337, 338mpbird 257 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵))
340251, 253, 42, 339lesub1dd 11860 . . . . . . . 8 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
341248, 252, 254, 325, 340letrd 11401 . . . . . . 7 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
342205, 262, 268subdird 11701 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − (1 · 𝑋 / 𝑥𝐵)))
343268mullidd 11262 . . . . . . . . . 10 (𝜑 → (1 · 𝑋 / 𝑥𝐵) = 𝑋 / 𝑥𝐵)
344343oveq2d 7436 . . . . . . . . 9 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − (1 · 𝑋 / 𝑥𝐵)) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵))
345342, 344eqtrd 2768 . . . . . . . 8 (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) = (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵))
346345oveq1d 7435 . . . . . . 7 (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
347204, 262, 68subdird 11701 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (1 · 𝑌 / 𝑥𝐵)))
34868mullidd 11262 . . . . . . . . . 10 (𝜑 → (1 · 𝑌 / 𝑥𝐵) = 𝑌 / 𝑥𝐵)
349348oveq2d 7436 . . . . . . . . 9 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − (1 · 𝑌 / 𝑥𝐵)) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵))
350347, 349eqtrd 2768 . . . . . . . 8 (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) = (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵))
351350oveq1d 7435 . . . . . . 7 (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
352341, 346, 3513brtr3d 5179 . . . . . 6 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
35348recnd 11272 . . . . . . 7 (𝜑 → ((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) ∈ ℂ)
35451recnd 11272 . . . . . . 7 (𝜑𝑋 / 𝑥𝐴 ∈ ℂ)
355353, 354, 268sub32d 11633 . . . . . 6 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) = ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴))
356197, 198, 68sub32d 11633 . . . . . 6 (𝜑 → ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) = ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴))
357352, 355, 3563brtr4d 5180 . . . . 5 (𝜑 → ((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) ≤ ((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵))
358243, 244, 63, 357leadd1dd 11858 . . . 4 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
35952recnd 11272 . . . . 5 (𝜑 → (((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) ∈ ℂ)
36063recnd 11272 . . . . 5 (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ)
361359, 360, 268addsubd 11622 . . . 4 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵) = (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) − 𝑋 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
36243recnd 11272 . . . . 5 (𝜑 → (((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) ∈ ℂ)
363362, 360, 68addsubd 11622 . . . 4 (𝜑 → (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵) = (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) − 𝑌 / 𝑥𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶))
364358, 361, 3633brtr4d 5180 . . 3 (𝜑 → (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵) ≤ (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵))
365241oveq1d 7435 . . 3 (𝜑 → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) = (((((𝑋 − (⌊‘𝑋)) · 𝑋 / 𝑥𝐵) − 𝑋 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑋 / 𝑥𝐵))
366236oveq1d 7435 . . 3 (𝜑 → ((𝐻𝑌) − 𝑌 / 𝑥𝐵) = (((((𝑌 − (⌊‘𝑋)) · 𝑌 / 𝑥𝐵) − 𝑌 / 𝑥𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − 𝑌 / 𝑥𝐵))
367364, 365, 3663brtr4d 5180 . 2 (𝜑 → ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵))
368242, 367jca 511 1 (𝜑 → ((𝐻𝑌) ≤ (𝐻𝑋) ∧ ((𝐻𝑋) − 𝑋 / 𝑥𝐵) ≤ ((𝐻𝑌) − 𝑌 / 𝑥𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wral 3058  csb 3892  wss 3947  {cpr 4631   class class class wbr 5148  cmpt 5231  dom cdm 5678  ran crn 5679  cres 5680  wf 6544  cfv 6548  (class class class)co 7420  cc 11136  cr 11137  0cc0 11138  1c1 11139   + caddc 11141   · cmul 11143  +∞cpnf 11275  *cxr 11277   < clt 11278  cle 11279  cmin 11474  -cneg 11475  cz 12588  cuz 12852  (,)cioo 13356  [,]cicc 13359  ...cfz 13516  cfl 13787  Σcsu 15664  TopOpenctopn 17402  topGenctg 17418  fldccnfld 21278  cnccncf 24795   D cdv 25791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-inf2 9664  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216  ax-addf 11217  ax-mulf 11218
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-isom 6557  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7685  df-om 7871  df-1st 7993  df-2nd 7994  df-supp 8166  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-1o 8486  df-2o 8487  df-er 8724  df-map 8846  df-pm 8847  df-ixp 8916  df-en 8964  df-dom 8965  df-sdom 8966  df-fin 8967  df-fsupp 9386  df-fi 9434  df-sup 9465  df-inf 9466  df-oi 9533  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-7 12310  df-8 12311  df-9 12312  df-n0 12503  df-z 12589  df-dec 12708  df-uz 12853  df-q 12963  df-rp 13007  df-xneg 13124  df-xadd 13125  df-xmul 13126  df-ioo 13360  df-ico 13362  df-icc 13363  df-fz 13517  df-fzo 13660  df-fl 13789  df-seq 13999  df-exp 14059  df-hash 14322  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215  df-clim 15464  df-sum 15665  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-ress 17209  df-plusg 17245  df-mulr 17246  df-starv 17247  df-sca 17248  df-vsca 17249  df-ip 17250  df-tset 17251  df-ple 17252  df-ds 17254  df-unif 17255  df-hom 17256  df-cco 17257  df-rest 17403  df-topn 17404  df-0g 17422  df-gsum 17423  df-topgen 17424  df-pt 17425  df-prds 17428  df-xrs 17483  df-qtop 17488  df-imas 17489  df-xps 17491  df-mre 17565  df-mrc 17566  df-acs 17568  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18740  df-mulg 19023  df-cntz 19267  df-cmn 19736  df-psmet 21270  df-xmet 21271  df-met 21272  df-bl 21273  df-mopn 21274  df-fbas 21275  df-fg 21276  df-cnfld 21279  df-top 22795  df-topon 22812  df-topsp 22834  df-bases 22848  df-cld 22922  df-ntr 22923  df-cls 22924  df-nei 23001  df-lp 23039  df-perf 23040  df-cn 23130  df-cnp 23131  df-haus 23218  df-cmp 23290  df-tx 23465  df-hmeo 23658  df-fil 23749  df-fm 23841  df-flim 23842  df-flf 23843  df-xms 24225  df-ms 24226  df-tms 24227  df-cncf 24797  df-limc 25794  df-dv 25795
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator