Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑇(,)+∞) |
2 | | ioossre 12547 |
. . . . . . . . 9
⊢ (𝑇(,)+∞) ⊆
ℝ |
3 | 1, 2 | eqsstri 3853 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℝ |
4 | | dvfsumlem1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
5 | 3, 4 | sseldi 3818 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) |
6 | | dvfsumlem1.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
7 | 6, 1 | syl6eleq 2868 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝑇(,)+∞)) |
8 | | dvfsum.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℝ) |
9 | 8 | rexrd 10426 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈
ℝ*) |
10 | | elioopnf 12580 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ ℝ*
→ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
12 | 7, 11 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)) |
13 | 12 | simpld 490 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℝ) |
14 | | reflcl 12916 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ∈
ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (⌊‘𝑋) ∈
ℝ) |
16 | 5, 15 | resubcld 10803 |
. . . . . 6
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℝ) |
17 | | csbeq1 3753 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
18 | 17 | eleq1d 2843 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) |
19 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
20 | | dvfsum.a |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
21 | | dvfsum.b1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
22 | | dvfsum.b3 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
23 | 19, 20, 21, 22 | dvmptrecl 24224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
24 | 23 | fmpttd 6649 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
25 | | nfcv 2933 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝐵 |
26 | | nfcsb1v 3766 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
27 | | csbeq1a 3759 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
28 | 25, 26, 27 | cbvmpt 4984 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐵) |
29 | 28 | fmpt 6644 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑆 ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
30 | 24, 29 | sylibr 226 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
31 | 18, 30, 4 | rspcdva 3516 |
. . . . . 6
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) |
32 | 16, 31 | remulcld 10407 |
. . . . 5
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
33 | | csbeq1 3753 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑌 / 𝑥⦌𝐴) |
34 | 33 | eleq1d 2843 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) |
35 | 20 | fmpttd 6649 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ) |
36 | | nfcv 2933 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐴 |
37 | | nfcsb1v 3766 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 |
38 | | csbeq1a 3759 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴) |
39 | 36, 37, 38 | cbvmpt 4984 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑆 ↦ 𝐴) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) |
40 | 39 | fmpt 6644 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑆 ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ) |
41 | 35, 40 | sylibr 226 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
42 | 34, 41, 4 | rspcdva 3516 |
. . . . 5
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ) |
43 | 32, 42 | resubcld 10803 |
. . . 4
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
44 | 13, 15 | resubcld 10803 |
. . . . . 6
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ) |
45 | | csbeq1 3753 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
46 | 45 | eleq1d 2843 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
47 | 46, 30, 6 | rspcdva 3516 |
. . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) |
48 | 44, 47 | remulcld 10407 |
. . . . 5
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
49 | | csbeq1 3753 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑋 / 𝑥⦌𝐴) |
50 | 49 | eleq1d 2843 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) |
51 | 50, 41, 6 | rspcdva 3516 |
. . . . 5
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ) |
52 | 48, 51 | resubcld 10803 |
. . . 4
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
53 | | fzfid 13091 |
. . . . 5
⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin) |
54 | | dvfsum.b2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
55 | 54 | ralrimiva 3147 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ) |
56 | | elfzuz 12655 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
57 | | dvfsum.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
58 | 56, 57 | syl6eleqr 2869 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍) |
59 | | dvfsum.c |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
60 | 59 | eleq1d 2843 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
61 | 60 | rspccva 3509 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ) |
62 | 55, 58, 61 | syl2an 589 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ) |
63 | 53, 62 | fsumrecl 14872 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ) |
64 | 44, 31 | remulcld 10407 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
65 | 64, 51 | resubcld 10803 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
66 | 5, 13 | resubcld 10803 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℝ) |
67 | 31, 66 | remulcld 10407 |
. . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℝ) |
68 | 31 | recnd 10405 |
. . . . . . . . . 10
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
69 | 5 | recnd 10405 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℂ) |
70 | 13 | recnd 10405 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
71 | 68, 69, 70 | subdid 10831 |
. . . . . . . . 9
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) = ((⦋𝑌 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑌 / 𝑥⦌𝐵 · 𝑋))) |
72 | | eqid 2777 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
73 | 72 | mulcn 23078 |
. . . . . . . . . . 11
⊢ ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
74 | | pnfxr 10430 |
. . . . . . . . . . . . . . . 16
⊢ +∞
∈ ℝ* |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → +∞ ∈
ℝ*) |
76 | 12 | simprd 491 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 < 𝑋) |
77 | | ltpnf 12265 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ∈ ℝ → 𝑌 < +∞) |
78 | 5, 77 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 < +∞) |
79 | | iccssioo 12554 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋 ∧ 𝑌 < +∞)) → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞)) |
80 | 9, 75, 76, 78, 79 | syl22anc 829 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞)) |
81 | 80, 2 | syl6ss 3832 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
82 | | ax-resscn 10329 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
83 | 81, 82 | syl6ss 3832 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℂ) |
84 | 82 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ⊆
ℂ) |
85 | | cncfmptc 23122 |
. . . . . . . . . . . 12
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
86 | 31, 83, 84, 85 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
87 | | cncfmptid 23123 |
. . . . . . . . . . . 12
⊢ (((𝑋[,]𝑌) ⊆ ℝ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
88 | 81, 82, 87 | sylancl 580 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
89 | | remulcl 10357 |
. . . . . . . . . . 11
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑌 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ) |
90 | 72, 73, 86, 88, 82, 89 | cncfmpt2ss 23126 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
91 | | reelprrecn 10364 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
92 | 91 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
93 | | ioossicc 12571 |
. . . . . . . . . . . . . . 15
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
94 | 93, 81 | syl5ss 3831 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ ℝ) |
95 | 94 | sselda 3820 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ) |
96 | 95 | recnd 10405 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ) |
97 | | 1cnd 10371 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 1 ∈ ℂ) |
98 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
99 | 98 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
100 | | 1cnd 10371 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
101 | 92 | dvmptid 24157 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
102 | 72 | tgioo2 23014 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
103 | | iooretop 22977 |
. . . . . . . . . . . . . 14
⊢ (𝑋(,)𝑌) ∈ (topGen‘ran
(,)) |
104 | 103 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋(,)𝑌) ∈ (topGen‘ran
(,))) |
105 | 92, 99, 100, 101, 94, 102, 72, 104 | dvmptres 24163 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 1)) |
106 | 92, 96, 97, 105, 68 | dvmptcmul 24164 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 1))) |
107 | 68 | mulid1d 10394 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · 1) = ⦋𝑌 / 𝑥⦌𝐵) |
108 | 107 | mpteq2dv 4980 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵)) |
109 | 106, 108 | eqtrd 2813 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵)) |
110 | 80, 1 | syl6sseqr 3870 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ 𝑆) |
111 | 110 | resmptd 5702 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) = (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴)) |
112 | 20 | recnd 10405 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
113 | 112 | fmpttd 6649 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
114 | 22 | dmeqd 5571 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = dom (𝑥 ∈ 𝑆 ↦ 𝐵)) |
115 | 21 | ralrimiva 3147 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ 𝑉) |
116 | | dmmptg 5886 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
𝑆 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑆 ↦ 𝐵) = 𝑆) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑥 ∈ 𝑆 ↦ 𝐵) = 𝑆) |
118 | 114, 117 | eqtrd 2813 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = 𝑆) |
119 | | dvcn 24121 |
. . . . . . . . . . . . . . . 16
⊢
(((ℝ ⊆ ℂ ∧ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ ∧ 𝑆 ⊆ ℝ) ∧ dom (ℝ D
(𝑥 ∈ 𝑆 ↦ 𝐴)) = 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) |
120 | 84, 113, 19, 118, 119 | syl31anc 1441 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) |
121 | | cncffvrn 23109 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) → ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ)) |
122 | 82, 120, 121 | sylancr 581 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ)) |
123 | 35, 122 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ)) |
124 | 39, 123 | syl5eqelr 2863 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ (𝑆–cn→ℝ)) |
125 | | rescncf 23108 |
. . . . . . . . . . . 12
⊢ ((𝑋[,]𝑌) ⊆ 𝑆 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ (𝑆–cn→ℝ) → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ))) |
126 | 110, 124,
125 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
127 | 111, 126 | eqeltrrd 2859 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
128 | 41 | r19.21bi 3113 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
129 | 128 | recnd 10405 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
130 | 30 | r19.21bi 3113 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
131 | 39 | oveq2i 6933 |
. . . . . . . . . . . 12
⊢ (ℝ
D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴)) |
132 | 22, 131, 28 | 3eqtr3g 2836 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐵)) |
133 | 93, 110 | syl5ss 3831 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ 𝑆) |
134 | 92, 129, 130, 132, 133, 102, 72, 104 | dvmptres 24163 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐵)) |
135 | 93 | sseli 3816 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋(,)𝑌) → 𝑦 ∈ (𝑋[,]𝑌)) |
136 | | simpl 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝜑) |
137 | 110 | sselda 3820 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ 𝑆) |
138 | 4 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈ 𝑆) |
139 | | dvfsum.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ ℝ) |
140 | 139 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ∈ ℝ) |
141 | 13 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ ℝ) |
142 | | elicc2 12550 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌))) |
143 | 13, 5, 142 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌))) |
144 | 143 | biimpa 470 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌)) |
145 | 144 | simp1d 1133 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ) |
146 | | dvfsumlem1.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ≤ 𝑋) |
147 | 146 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ≤ 𝑋) |
148 | 144 | simp2d 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ≤ 𝑦) |
149 | 140, 141,
145, 147, 148 | letrd 10533 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ≤ 𝑦) |
150 | 144 | simp3d 1135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ≤ 𝑌) |
151 | | dvfsumlem1.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ≤ 𝑈) |
152 | 151 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ≤ 𝑈) |
153 | | simp2r 1214 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 𝑌 ∈ 𝑆) |
154 | | eleq1 2846 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑘 ∈ 𝑆 ↔ 𝑌 ∈ 𝑆)) |
155 | 154 | anbi2d 622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → ((𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆))) |
156 | | breq2 4890 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑦 ≤ 𝑘 ↔ 𝑦 ≤ 𝑌)) |
157 | | breq1 4889 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑘 ≤ 𝑈 ↔ 𝑌 ≤ 𝑈)) |
158 | 156, 157 | 3anbi23d 1512 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → ((𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈))) |
159 | 155, 158 | 3anbi23d 1512 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑌 → ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)))) |
160 | | vex 3400 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑘 ∈ V |
161 | 160, 59 | csbie 3776 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝑘 /
𝑥⦌𝐵 = 𝐶 |
162 | | csbeq1 3753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → ⦋𝑘 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
163 | 161, 162 | syl5eqr 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → 𝐶 = ⦋𝑌 / 𝑥⦌𝐵) |
164 | 163 | breq1d 4896 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑌 → (𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵 ↔ ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
165 | 159, 164 | imbi12d 336 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑌 → (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) ↔ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵))) |
166 | | nfv 1957 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) |
167 | | nfcv 2933 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐶 |
168 | | nfcv 2933 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥
≤ |
169 | 167, 168,
26 | nfbr 4933 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵 |
170 | 166, 169 | nfim 1943 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
171 | | eleq1 2846 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆)) |
172 | 171 | anbi1d 623 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆))) |
173 | | breq2 4890 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑦)) |
174 | | breq1 4889 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑘 ↔ 𝑦 ≤ 𝑘)) |
175 | 173, 174 | 3anbi12d 1510 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈))) |
176 | 172, 175 | 3anbi23d 1512 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)))) |
177 | 27 | breq2d 4898 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
178 | 176, 177 | imbi12d 336 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵))) |
179 | | dvfsum.l |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) |
180 | 170, 178,
179 | chvar 2359 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
181 | 165, 180 | vtoclg 3466 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝑆 → ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
182 | 153, 181 | mpcom 38 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
183 | 136, 137,
138, 149, 150, 152, 182 | syl123anc 1455 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
184 | 135, 183 | sylan2 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
185 | 13 | rexrd 10426 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
186 | 5 | rexrd 10426 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
187 | | dvfsumlem1.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
188 | | lbicc2 12602 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
189 | 185, 186,
187, 188 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
190 | | ubicc2 12603 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
191 | 185, 186,
187, 190 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
192 | | oveq2 6930 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑋)) |
193 | | oveq2 6930 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑌)) |
194 | 13, 5, 90, 109, 127, 134, 184, 189, 191, 187, 192, 49, 193, 33 | dvle 24207 |
. . . . . . . . 9
⊢ (𝜑 → ((⦋𝑌 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑌 / 𝑥⦌𝐵 · 𝑋)) ≤ (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴)) |
195 | 71, 194 | eqbrtrd 4908 |
. . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ≤ (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴)) |
196 | 67, 42, 51, 195 | lesubd 10979 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ≤ (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
197 | 64 | recnd 10405 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
198 | 32 | recnd 10405 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
199 | 42 | recnd 10405 |
. . . . . . . . 9
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ) |
200 | 197, 198,
199 | subsubd 10762 |
. . . . . . . 8
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴)) |
201 | 198, 197 | negsubdi2d 10750 |
. . . . . . . . . . 11
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵))) |
202 | 15 | recnd 10405 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘𝑋) ∈
ℂ) |
203 | 69, 70, 202 | nnncan2d 10769 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) = (𝑌 − 𝑋)) |
204 | 203 | oveq1d 6937 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · ⦋𝑌 / 𝑥⦌𝐵) = ((𝑌 − 𝑋) · ⦋𝑌 / 𝑥⦌𝐵)) |
205 | 16 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℂ) |
206 | 44 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ) |
207 | 205, 206,
68 | subdird 10832 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵))) |
208 | 66 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℂ) |
209 | 208, 68 | mulcomd 10398 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − 𝑋) · ⦋𝑌 / 𝑥⦌𝐵) = (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
210 | 204, 207,
209 | 3eqtr3d 2821 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
211 | 210 | negeqd 10616 |
. . . . . . . . . . 11
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = -(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
212 | 201, 211 | eqtr3d 2815 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = -(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
213 | 212 | oveq1d 6937 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = (-(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) + ⦋𝑌 / 𝑥⦌𝐴)) |
214 | 67 | recnd 10405 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℂ) |
215 | 214, 199 | negsubdid 10749 |
. . . . . . . . 9
⊢ (𝜑 → -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴) = (-(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) + ⦋𝑌 / 𝑥⦌𝐴)) |
216 | 213, 215 | eqtr4d 2816 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴)) |
217 | 214, 199 | negsubdi2d 10750 |
. . . . . . . 8
⊢ (𝜑 → -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
218 | 200, 216,
217 | 3eqtrd 2817 |
. . . . . . 7
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
219 | 196, 218 | breqtrrd 4914 |
. . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴))) |
220 | 51, 64, 43, 219 | lesubd 10979 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
221 | | flle 12919 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ≤
𝑋) |
222 | 13, 221 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘𝑋) ≤ 𝑋) |
223 | 13, 15 | subge0d 10965 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝑋 − (⌊‘𝑋)) ↔ (⌊‘𝑋) ≤ 𝑋)) |
224 | 222, 223 | mpbird 249 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋))) |
225 | 45 | breq2d 4898 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → (⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵 ↔ ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
226 | 183 | ralrimiva 3147 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
227 | 225, 226,
189 | rspcdva 3516 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
228 | 31, 47, 44, 224, 227 | lemul2ad 11318 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵)) |
229 | 64, 48, 51, 228 | lesub1dd 10991 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
230 | 43, 65, 52, 220, 229 | letrd 10533 |
. . . 4
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
231 | 43, 52, 63, 230 | leadd1dd 10989 |
. . 3
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
232 | | dvfsum.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
233 | | dvfsum.md |
. . . 4
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) |
234 | | dvfsum.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
235 | | dvfsum.h |
. . . 4
⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) |
236 | | dvfsumlem1.6 |
. . . 4
⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) |
237 | 1, 57, 232, 139, 233, 8, 20, 21, 54, 22, 59, 234, 179, 235, 6, 4, 146, 187, 151, 236 | dvfsumlem1 24226 |
. . 3
⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
238 | 13 | leidd 10941 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑋) |
239 | 185, 186,
234, 187, 151 | xrletrd 12305 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑈) |
240 | | fllep1 12921 |
. . . . 5
⊢ (𝑋 ∈ ℝ → 𝑋 ≤ ((⌊‘𝑋) + 1)) |
241 | 13, 240 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ ((⌊‘𝑋) + 1)) |
242 | 1, 57, 232, 139, 233, 8, 20, 21, 54, 22, 59, 234, 179, 235, 6, 6, 146, 238, 239, 241 | dvfsumlem1 24226 |
. . 3
⊢ (𝜑 → (𝐻‘𝑋) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
243 | 231, 237,
242 | 3brtr4d 4918 |
. 2
⊢ (𝜑 → (𝐻‘𝑌) ≤ (𝐻‘𝑋)) |
244 | 52, 47 | resubcld 10803 |
. . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
245 | 43, 31 | resubcld 10803 |
. . . . 5
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
246 | | peano2rem 10690 |
. . . . . . . . . . 11
⊢ ((𝑋 − (⌊‘𝑋)) ∈ ℝ → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℝ) |
247 | 44, 246 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℝ) |
248 | 247, 47 | remulcld 10407 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
249 | 248, 51 | resubcld 10803 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
250 | | peano2rem 10690 |
. . . . . . . . . . 11
⊢ ((𝑌 − (⌊‘𝑋)) ∈ ℝ → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
251 | 16, 250 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
252 | 251, 47 | remulcld 10407 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
253 | 252, 42 | resubcld 10803 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
254 | 251, 31 | remulcld 10407 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
255 | 254, 42 | resubcld 10803 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
256 | 248 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
257 | 252 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
258 | 256, 257 | subcld 10734 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) ∈ ℂ) |
259 | 258, 199 | addcomd 10578 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
260 | 256, 257,
199 | subsubd 10762 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴)) |
261 | 199, 257,
256 | subsub2d 10763 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) = (⦋𝑌 / 𝑥⦌𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
262 | 259, 260,
261 | 3eqtr4d 2823 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
263 | | 1cnd 10371 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℂ) |
264 | 205, 206,
263 | nnncan2d 10769 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋)))) |
265 | 264, 203 | eqtrd 2813 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = (𝑌 − 𝑋)) |
266 | 265 | oveq1d 6937 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · ⦋𝑋 / 𝑥⦌𝐵) = ((𝑌 − 𝑋) · ⦋𝑋 / 𝑥⦌𝐵)) |
267 | 251 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℂ) |
268 | 247 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℂ) |
269 | 47 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) |
270 | 267, 268,
269 | subdird 10832 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) |
271 | 208, 269 | mulcomd 10398 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − 𝑋) · ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
272 | 266, 270,
271 | 3eqtr3d 2821 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) = (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
273 | 272 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
274 | 262, 273 | eqtrd 2813 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
275 | 47, 66 | remulcld 10407 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℝ) |
276 | | cncfmptc 23122 |
. . . . . . . . . . . . . . 15
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
277 | 47, 83, 84, 276 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
278 | | remulcl 10357 |
. . . . . . . . . . . . . 14
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑋 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ) |
279 | 72, 73, 277, 88, 82, 278 | cncfmpt2ss 23126 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
280 | 92, 96, 97, 105, 269 | dvmptcmul 24164 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 1))) |
281 | 269 | mulid1d 10394 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · 1) = ⦋𝑋 / 𝑥⦌𝐵) |
282 | 281 | mpteq2dv 4980 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵)) |
283 | 280, 282 | eqtrd 2813 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵)) |
284 | 6 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ 𝑆) |
285 | 145 | rexrd 10426 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ*) |
286 | 186 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈
ℝ*) |
287 | 234 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑈 ∈
ℝ*) |
288 | 285, 286,
287, 150, 152 | xrletrd 12305 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ≤ 𝑈) |
289 | | vex 3400 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
290 | | eleq1 2846 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆)) |
291 | 290 | anbi2d 622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆))) |
292 | | breq2 4890 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑋 ≤ 𝑘 ↔ 𝑋 ≤ 𝑦)) |
293 | | breq1 4889 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 ≤ 𝑈 ↔ 𝑦 ≤ 𝑈)) |
294 | 292, 293 | 3anbi23d 1512 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈))) |
295 | 291, 294 | 3anbi23d 1512 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)))) |
296 | | csbeq1 3753 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → ⦋𝑘 / 𝑥⦌𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
297 | 161, 296 | syl5eqr 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐵) |
298 | 297 | breq1d 4896 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → (𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
299 | 295, 298 | imbi12d 336 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
300 | | simp2l 1213 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑋 ∈ 𝑆) |
301 | | nfv 1957 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) |
302 | | nfcsb1v 3766 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵 |
303 | 167, 168,
302 | nfbr 4933 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵 |
304 | 301, 303 | nfim 1943 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
305 | | eleq1 2846 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆)) |
306 | 305 | anbi1d 623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → ((𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆))) |
307 | | breq2 4890 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋)) |
308 | | breq1 4889 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑘 ↔ 𝑋 ≤ 𝑘)) |
309 | 307, 308 | 3anbi12d 1510 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈))) |
310 | 306, 309 | 3anbi23d 1512 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)))) |
311 | | csbeq1a 3759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
312 | 311 | breq2d 4898 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → (𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
313 | 310, 312 | imbi12d 336 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
314 | 304, 313,
179 | vtoclg1f 3465 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝑆 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
315 | 300, 314 | mpcom 38 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
316 | 289, 299,
315 | vtocl 3459 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
317 | 136, 284,
137, 147, 148, 288, 316 | syl123anc 1455 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
318 | 135, 317 | sylan2 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
319 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑋)) |
320 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑌)) |
321 | 13, 5, 127, 134, 279, 283, 318, 189, 191, 187, 49, 319, 33, 320 | dvle 24207 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((⦋𝑋 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑋 / 𝑥⦌𝐵 · 𝑋))) |
322 | 269, 69, 70 | subdid 10831 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) = ((⦋𝑋 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑋 / 𝑥⦌𝐵 · 𝑋))) |
323 | 321, 322 | breqtrrd 4914 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
324 | 42, 51, 275, 323 | subled 10978 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐴) |
325 | 274, 324 | eqbrtrd 4908 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ⦋𝑋 / 𝑥⦌𝐴) |
326 | 248, 253,
51, 325 | subled 10978 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
327 | 251 | renegcld 10802 |
. . . . . . . . . . . 12
⊢ (𝜑 → -((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
328 | | 1red 10377 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
329 | 5, 15, 328 | lesubadd2d 10974 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) ≤ 1 ↔ 𝑌 ≤ ((⌊‘𝑋) + 1))) |
330 | 236, 329 | mpbird 249 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ≤ 1) |
331 | 16, 328 | suble0d 10966 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ (𝑌 − (⌊‘𝑋)) ≤ 1)) |
332 | 330, 331 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ≤ 0) |
333 | 251 | le0neg1d 10946 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1))) |
334 | 332, 333 | mpbid 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1)) |
335 | 31, 47, 327, 334, 227 | lemul2ad 11318 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
336 | 267, 68 | mulneg1d 10828 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵)) |
337 | 267, 269 | mulneg1d 10828 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
338 | 335, 336,
337 | 3brtr3d 4917 |
. . . . . . . . . 10
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
339 | 252, 254 | lenegd 10954 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ↔ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) |
340 | 338, 339 | mpbird 249 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵)) |
341 | 252, 254,
42, 340 | lesub1dd 10991 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
342 | 249, 253,
255, 326, 341 | letrd 10533 |
. . . . . . 7
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
343 | 206, 263,
269 | subdird 10832 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − (1 · ⦋𝑋 / 𝑥⦌𝐵))) |
344 | 269 | mulid2d 10395 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵) |
345 | 344 | oveq2d 6938 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − (1 · ⦋𝑋 / 𝑥⦌𝐵)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵)) |
346 | 343, 345 | eqtrd 2813 |
. . . . . . . 8
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵)) |
347 | 346 | oveq1d 6937 |
. . . . . . 7
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
348 | 205, 263,
68 | subdird 10832 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵))) |
349 | 68 | mulid2d 10395 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
⦋𝑌 / 𝑥⦌𝐵) = ⦋𝑌 / 𝑥⦌𝐵) |
350 | 349 | oveq2d 6938 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
351 | 348, 350 | eqtrd 2813 |
. . . . . . . 8
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
352 | 351 | oveq1d 6937 |
. . . . . . 7
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
353 | 342, 347,
352 | 3brtr3d 4917 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
354 | 48 | recnd 10405 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
355 | 51 | recnd 10405 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ) |
356 | 354, 355,
269 | sub32d 10766 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
357 | 198, 199,
68 | sub32d 10766 |
. . . . . 6
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
358 | 353, 356,
357 | 3brtr4d 4918 |
. . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵)) |
359 | 244, 245,
63, 358 | leadd1dd 10989 |
. . . 4
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
360 | 52 | recnd 10405 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ) |
361 | 63 | recnd 10405 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ) |
362 | 360, 361,
269 | addsubd 10755 |
. . . 4
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵) = (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
363 | 43 | recnd 10405 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ) |
364 | 363, 361,
68 | addsubd 10755 |
. . . 4
⊢ (𝜑 → (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵) = (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
365 | 359, 362,
364 | 3brtr4d 4918 |
. . 3
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵)) |
366 | 242 | oveq1d 6937 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) = (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵)) |
367 | 237 | oveq1d 6937 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵) = (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵)) |
368 | 365, 366,
367 | 3brtr4d 4918 |
. 2
⊢ (𝜑 → ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)) |
369 | 243, 368 | jca 507 |
1
⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) |