Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑇(,)+∞) |
2 | | ioossre 12106 |
. . . . . . . . 9
⊢ (𝑇(,)+∞) ⊆
ℝ |
3 | 1, 2 | eqsstri 3598 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℝ |
4 | | dvfsumlem1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
5 | 3, 4 | sseldi 3566 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) |
6 | | dvfsumlem1.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
7 | 6, 1 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝑇(,)+∞)) |
8 | | dvfsum.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℝ) |
9 | 8 | rexrd 9968 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈
ℝ*) |
10 | | elioopnf 12138 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ ℝ*
→ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
12 | 7, 11 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)) |
13 | 12 | simpld 474 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℝ) |
14 | | reflcl 12459 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ∈
ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (⌊‘𝑋) ∈
ℝ) |
16 | 5, 15 | resubcld 10337 |
. . . . . 6
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℝ) |
17 | 13 | rexrd 9968 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
18 | 5 | rexrd 9968 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
19 | | dvfsumlem1.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
20 | | ubicc2 12160 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
21 | 17, 18, 19, 20 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
22 | | pnfxr 9971 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
23 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → +∞ ∈
ℝ*) |
24 | 12 | simprd 478 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 < 𝑋) |
25 | | ltpnf 11830 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ ℝ → 𝑌 < +∞) |
26 | 5, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 < +∞) |
27 | | iccssioo 12113 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋 ∧ 𝑌 < +∞)) → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞)) |
28 | 9, 23, 24, 26, 27 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞)) |
29 | 28, 1 | syl6sseqr 3615 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ 𝑆) |
30 | 29 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ 𝑆) |
31 | 3 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
32 | | dvfsum.a |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
33 | | dvfsum.b1 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
34 | | dvfsum.b3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
35 | 31, 32, 33, 34 | dvmptrecl 23591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
36 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑥 ∈ 𝑆 ↦ 𝐵) |
37 | 35, 36 | fmptd 6292 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
38 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝐵 |
39 | | nfcsb1v 3515 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
40 | | csbeq1a 3508 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
41 | 38, 39, 40 | cbvmpt 4677 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐵) |
42 | 41 | fmpt 6289 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑆 ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
43 | 37, 42 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
44 | 43 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
45 | 30, 44 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
46 | 45 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
47 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
48 | 47 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → (⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) |
49 | 48 | rspcv 3278 |
. . . . . . 7
⊢ (𝑌 ∈ (𝑋[,]𝑌) → (∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) |
50 | 21, 46, 49 | sylc 63 |
. . . . . 6
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) |
51 | 16, 50 | remulcld 9949 |
. . . . 5
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
52 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑆 ↦ 𝐴) = (𝑥 ∈ 𝑆 ↦ 𝐴) |
53 | 32, 52 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ) |
54 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦𝐴 |
55 | | nfcsb1v 3515 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 |
56 | | csbeq1a 3508 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴) |
57 | 54, 55, 56 | cbvmpt 4677 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑆 ↦ 𝐴) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) |
58 | 57 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑆 ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ) |
59 | 53, 58 | sylibr 223 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
60 | 59 | r19.21bi 2916 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
61 | 30, 60 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
62 | 61 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
63 | | csbeq1 3502 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑌 / 𝑥⦌𝐴) |
64 | 63 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) |
65 | 64 | rspcv 3278 |
. . . . . 6
⊢ (𝑌 ∈ (𝑋[,]𝑌) → (∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) |
66 | 21, 62, 65 | sylc 63 |
. . . . 5
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ) |
67 | 51, 66 | resubcld 10337 |
. . . 4
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
68 | 13, 15 | resubcld 10337 |
. . . . . 6
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ) |
69 | | lbicc2 12159 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
70 | 17, 18, 19, 69 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
71 | | csbeq1 3502 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
72 | 71 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
73 | 72 | rspcv 3278 |
. . . . . . 7
⊢ (𝑋 ∈ (𝑋[,]𝑌) → (∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
74 | 70, 46, 73 | sylc 63 |
. . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) |
75 | 68, 74 | remulcld 9949 |
. . . . 5
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
76 | | csbeq1 3502 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑋 / 𝑥⦌𝐴) |
77 | 76 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) |
78 | 77 | rspcv 3278 |
. . . . . 6
⊢ (𝑋 ∈ (𝑋[,]𝑌) → (∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) |
79 | 70, 62, 78 | sylc 63 |
. . . . 5
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ) |
80 | 75, 79 | resubcld 10337 |
. . . 4
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
81 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin) |
82 | | dvfsum.b2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
83 | 82 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ) |
84 | | elfzuz 12209 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
85 | | dvfsum.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
86 | 84, 85 | syl6eleqr 2699 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍) |
87 | | dvfsum.c |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
88 | 87 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
89 | 88 | rspccva 3281 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ) |
90 | 83, 86, 89 | syl2an 493 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ) |
91 | 81, 90 | fsumrecl 14312 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ) |
92 | 68, 50 | remulcld 9949 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
93 | 92, 79 | resubcld 10337 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
94 | 5, 13 | resubcld 10337 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℝ) |
95 | 50, 94 | remulcld 9949 |
. . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℝ) |
96 | 50 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
97 | 5 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℂ) |
98 | 13 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
99 | 96, 97, 98 | subdid 10365 |
. . . . . . . . 9
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) = ((⦋𝑌 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑌 / 𝑥⦌𝐵 · 𝑋))) |
100 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
101 | 100 | mulcn 22478 |
. . . . . . . . . . 11
⊢ ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
102 | 28, 2 | syl6ss 3580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
103 | | ax-resscn 9872 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℂ |
104 | 102, 103 | syl6ss 3580 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℂ) |
105 | 103 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ⊆
ℂ) |
106 | | cncfmptc 22522 |
. . . . . . . . . . . 12
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
107 | 50, 104, 105, 106 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
108 | | cncfmptid 22523 |
. . . . . . . . . . . 12
⊢ (((𝑋[,]𝑌) ⊆ ℝ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
109 | 102, 103,
108 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
110 | | remulcl 9900 |
. . . . . . . . . . 11
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑌 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ) |
111 | 100, 101,
107, 109, 103, 110 | cncfmpt2ss 22526 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
112 | | reelprrecn 9907 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
113 | 112 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
114 | | ioossicc 12130 |
. . . . . . . . . . . . . . 15
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
115 | 114, 102 | syl5ss 3579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ ℝ) |
116 | 115 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ) |
117 | 116 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ) |
118 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 1 ∈ ℂ) |
119 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
120 | 119 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
121 | | 1cnd 9935 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
122 | 113 | dvmptid 23526 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
123 | 100 | tgioo2 22414 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
124 | | iooretop 22379 |
. . . . . . . . . . . . . 14
⊢ (𝑋(,)𝑌) ∈ (topGen‘ran
(,)) |
125 | 124 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋(,)𝑌) ∈ (topGen‘ran
(,))) |
126 | 113, 120,
121, 122, 115, 123, 100, 125 | dvmptres 23532 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 1)) |
127 | 113, 117,
118, 126, 96 | dvmptcmul 23533 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 1))) |
128 | 96 | mulid1d 9936 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · 1) = ⦋𝑌 / 𝑥⦌𝐵) |
129 | 128 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵)) |
130 | 127, 129 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵)) |
131 | 29 | resmptd 5371 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) = (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴)) |
132 | 32 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
133 | 132, 52 | fmptd 6292 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
134 | 34 | dmeqd 5248 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = dom (𝑥 ∈ 𝑆 ↦ 𝐵)) |
135 | 33 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ 𝑉) |
136 | | dmmptg 5549 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
𝑆 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑆 ↦ 𝐵) = 𝑆) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑥 ∈ 𝑆 ↦ 𝐵) = 𝑆) |
138 | 134, 137 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = 𝑆) |
139 | | dvcn 23490 |
. . . . . . . . . . . . . . . 16
⊢
(((ℝ ⊆ ℂ ∧ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ ∧ 𝑆 ⊆ ℝ) ∧ dom (ℝ D
(𝑥 ∈ 𝑆 ↦ 𝐴)) = 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) |
140 | 105, 133,
31, 138, 139 | syl31anc 1321 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) |
141 | | cncffvrn 22509 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) → ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ)) |
142 | 103, 140,
141 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ)) |
143 | 53, 142 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ)) |
144 | 57, 143 | syl5eqelr 2693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ (𝑆–cn→ℝ)) |
145 | | rescncf 22508 |
. . . . . . . . . . . 12
⊢ ((𝑋[,]𝑌) ⊆ 𝑆 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ (𝑆–cn→ℝ) → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ))) |
146 | 29, 144, 145 | sylc 63 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
147 | 131, 146 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
148 | 60 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
149 | 57 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢ (ℝ
D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴)) |
150 | 34, 149, 41 | 3eqtr3g 2667 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐵)) |
151 | 114, 29 | syl5ss 3579 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ 𝑆) |
152 | 113, 148,
44, 150, 151, 123, 100, 125 | dvmptres 23532 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐵)) |
153 | 114 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋(,)𝑌) → 𝑦 ∈ (𝑋[,]𝑌)) |
154 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝜑) |
155 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈ 𝑆) |
156 | | dvfsum.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ ℝ) |
157 | 156 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ∈ ℝ) |
158 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ ℝ) |
159 | | elicc2 12109 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌))) |
160 | 13, 5, 159 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌))) |
161 | 160 | biimpa 500 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌)) |
162 | 161 | simp1d 1066 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ) |
163 | | dvfsumlem1.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ≤ 𝑋) |
164 | 163 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ≤ 𝑋) |
165 | 161 | simp2d 1067 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ≤ 𝑦) |
166 | 157, 158,
162, 164, 165 | letrd 10073 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ≤ 𝑦) |
167 | 161 | simp3d 1068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ≤ 𝑌) |
168 | | dvfsumlem1.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ≤ 𝑈) |
169 | 168 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ≤ 𝑈) |
170 | | simp2r 1081 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 𝑌 ∈ 𝑆) |
171 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑘 ∈ 𝑆 ↔ 𝑌 ∈ 𝑆)) |
172 | 171 | anbi2d 736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → ((𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆))) |
173 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑦 ≤ 𝑘 ↔ 𝑦 ≤ 𝑌)) |
174 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑘 ≤ 𝑈 ↔ 𝑌 ≤ 𝑈)) |
175 | 173, 174 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → ((𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈))) |
176 | 172, 175 | 3anbi23d 1394 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑌 → ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)))) |
177 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑘 ∈ V |
178 | 177, 87 | csbie 3525 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝑘 /
𝑥⦌𝐵 = 𝐶 |
179 | | csbeq1 3502 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → ⦋𝑘 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
180 | 178, 179 | syl5eqr 2658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → 𝐶 = ⦋𝑌 / 𝑥⦌𝐵) |
181 | 180 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑌 → (𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵 ↔ ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
182 | 176, 181 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑌 → (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) ↔ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵))) |
183 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) |
184 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐶 |
185 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥
≤ |
186 | 184, 185,
39 | nfbr 4629 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵 |
187 | 183, 186 | nfim 1813 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
188 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆)) |
189 | 188 | anbi1d 737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆))) |
190 | | breq2 4587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑦)) |
191 | | breq1 4586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑘 ↔ 𝑦 ≤ 𝑘)) |
192 | 190, 191 | 3anbi12d 1392 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈))) |
193 | 189, 192 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)))) |
194 | 40 | breq2d 4595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
195 | 193, 194 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵))) |
196 | | dvfsum.l |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) |
197 | 187, 195,
196 | chvar 2250 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
198 | 182, 197 | vtoclg 3239 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝑆 → ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
199 | 170, 198 | mpcom 37 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
200 | 154, 30, 155, 166, 167, 169, 199 | syl123anc 1335 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
201 | 153, 200 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
202 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑋)) |
203 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑌)) |
204 | 13, 5, 111, 130, 147, 152, 201, 70, 21, 19, 202, 76, 203, 63 | dvle 23574 |
. . . . . . . . 9
⊢ (𝜑 → ((⦋𝑌 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑌 / 𝑥⦌𝐵 · 𝑋)) ≤ (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴)) |
205 | 99, 204 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ≤ (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴)) |
206 | 95, 66, 79, 205 | lesubd 10510 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ≤ (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
207 | 92 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
208 | 51 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
209 | 66 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ) |
210 | 207, 208,
209 | subsubd 10299 |
. . . . . . . 8
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴)) |
211 | 208, 207 | negsubdi2d 10287 |
. . . . . . . . . . 11
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵))) |
212 | 15 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘𝑋) ∈
ℂ) |
213 | 97, 98, 212 | nnncan2d 10306 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) = (𝑌 − 𝑋)) |
214 | 213 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · ⦋𝑌 / 𝑥⦌𝐵) = ((𝑌 − 𝑋) · ⦋𝑌 / 𝑥⦌𝐵)) |
215 | 16 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℂ) |
216 | 68 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ) |
217 | 215, 216,
96 | subdird 10366 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵))) |
218 | 94 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℂ) |
219 | 218, 96 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − 𝑋) · ⦋𝑌 / 𝑥⦌𝐵) = (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
220 | 214, 217,
219 | 3eqtr3d 2652 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
221 | 220 | negeqd 10154 |
. . . . . . . . . . 11
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = -(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
222 | 211, 221 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = -(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
223 | 222 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = (-(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) + ⦋𝑌 / 𝑥⦌𝐴)) |
224 | 95 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℂ) |
225 | 224, 209 | negsubdid 10286 |
. . . . . . . . 9
⊢ (𝜑 → -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴) = (-(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) + ⦋𝑌 / 𝑥⦌𝐴)) |
226 | 223, 225 | eqtr4d 2647 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴)) |
227 | 224, 209 | negsubdi2d 10287 |
. . . . . . . 8
⊢ (𝜑 → -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
228 | 210, 226,
227 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
229 | 206, 228 | breqtrrd 4611 |
. . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴))) |
230 | 79, 92, 67, 229 | lesubd 10510 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
231 | | flle 12462 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ≤
𝑋) |
232 | 13, 231 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘𝑋) ≤ 𝑋) |
233 | 13, 15 | subge0d 10496 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝑋 − (⌊‘𝑋)) ↔ (⌊‘𝑋) ≤ 𝑋)) |
234 | 232, 233 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋))) |
235 | 200 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
236 | 71 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → (⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵 ↔ ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
237 | 236 | rspcv 3278 |
. . . . . . . 8
⊢ (𝑋 ∈ (𝑋[,]𝑌) → (∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
238 | 70, 235, 237 | sylc 63 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
239 | 50, 74, 68, 234, 238 | lemul2ad 10843 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵)) |
240 | 92, 75, 79, 239 | lesub1dd 10522 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
241 | 67, 93, 80, 230, 240 | letrd 10073 |
. . . 4
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
242 | 67, 80, 91, 241 | leadd1dd 10520 |
. . 3
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
243 | | dvfsum.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
244 | | dvfsum.md |
. . . 4
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) |
245 | | dvfsum.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
246 | | dvfsum.h |
. . . 4
⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) |
247 | | dvfsumlem1.6 |
. . . 4
⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) |
248 | 1, 85, 243, 156, 244, 8, 32, 33, 82, 34, 87, 245, 196, 246, 6, 4, 163, 19, 168, 247 | dvfsumlem1 23593 |
. . 3
⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
249 | 13 | leidd 10473 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑋) |
250 | 17, 18, 245, 19, 168 | xrletrd 11869 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑈) |
251 | | fllep1 12464 |
. . . . 5
⊢ (𝑋 ∈ ℝ → 𝑋 ≤ ((⌊‘𝑋) + 1)) |
252 | 13, 251 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ ((⌊‘𝑋) + 1)) |
253 | 1, 85, 243, 156, 244, 8, 32, 33, 82, 34, 87, 245, 196, 246, 6, 6, 163, 249, 250, 252 | dvfsumlem1 23593 |
. . 3
⊢ (𝜑 → (𝐻‘𝑋) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
254 | 242, 248,
253 | 3brtr4d 4615 |
. 2
⊢ (𝜑 → (𝐻‘𝑌) ≤ (𝐻‘𝑋)) |
255 | 80, 74 | resubcld 10337 |
. . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
256 | 67, 50 | resubcld 10337 |
. . . . 5
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
257 | | peano2rem 10227 |
. . . . . . . . . . 11
⊢ ((𝑋 − (⌊‘𝑋)) ∈ ℝ → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℝ) |
258 | 68, 257 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℝ) |
259 | 258, 74 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
260 | 259, 79 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
261 | | peano2rem 10227 |
. . . . . . . . . . 11
⊢ ((𝑌 − (⌊‘𝑋)) ∈ ℝ → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
262 | 16, 261 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
263 | 262, 74 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
264 | 263, 66 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
265 | 262, 50 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
266 | 265, 66 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
267 | 259 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
268 | 263 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
269 | 267, 268 | subcld 10271 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) ∈ ℂ) |
270 | 269, 209 | addcomd 10117 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
271 | 267, 268,
209 | subsubd 10299 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴)) |
272 | 209, 268,
267 | subsub2d 10300 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) = (⦋𝑌 / 𝑥⦌𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
273 | 270, 271,
272 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
274 | | 1cnd 9935 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℂ) |
275 | 215, 216,
274 | nnncan2d 10306 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋)))) |
276 | 275, 213 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = (𝑌 − 𝑋)) |
277 | 276 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · ⦋𝑋 / 𝑥⦌𝐵) = ((𝑌 − 𝑋) · ⦋𝑋 / 𝑥⦌𝐵)) |
278 | 262 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℂ) |
279 | 258 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℂ) |
280 | 74 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) |
281 | 278, 279,
280 | subdird 10366 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) |
282 | 218, 280 | mulcomd 9940 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − 𝑋) · ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
283 | 277, 281,
282 | 3eqtr3d 2652 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) = (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
284 | 283 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
285 | 273, 284 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
286 | 74, 94 | remulcld 9949 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℝ) |
287 | | cncfmptc 22522 |
. . . . . . . . . . . . . . 15
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
288 | 74, 104, 105, 287 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
289 | | remulcl 9900 |
. . . . . . . . . . . . . 14
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑋 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ) |
290 | 100, 101,
288, 109, 103, 289 | cncfmpt2ss 22526 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
291 | 113, 117,
118, 126, 280 | dvmptcmul 23533 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 1))) |
292 | 280 | mulid1d 9936 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · 1) = ⦋𝑋 / 𝑥⦌𝐵) |
293 | 292 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵)) |
294 | 291, 293 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵)) |
295 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ 𝑆) |
296 | 162 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ*) |
297 | 18 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈
ℝ*) |
298 | 245 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑈 ∈
ℝ*) |
299 | 296, 297,
298, 167, 169 | xrletrd 11869 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ≤ 𝑈) |
300 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
301 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆)) |
302 | 301 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆))) |
303 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑋 ≤ 𝑘 ↔ 𝑋 ≤ 𝑦)) |
304 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 ≤ 𝑈 ↔ 𝑦 ≤ 𝑈)) |
305 | 303, 304 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈))) |
306 | 302, 305 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)))) |
307 | | csbeq1 3502 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → ⦋𝑘 / 𝑥⦌𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
308 | 178, 307 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐵) |
309 | 308 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → (𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
310 | 306, 309 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
311 | | simp2l 1080 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑋 ∈ 𝑆) |
312 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) |
313 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵 |
314 | 184, 185,
313 | nfbr 4629 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵 |
315 | 312, 314 | nfim 1813 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
316 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆)) |
317 | 316 | anbi1d 737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → ((𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆))) |
318 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋)) |
319 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑘 ↔ 𝑋 ≤ 𝑘)) |
320 | 318, 319 | 3anbi12d 1392 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈))) |
321 | 317, 320 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)))) |
322 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
323 | 322 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → (𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
324 | 321, 323 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
325 | 315, 324,
196 | vtoclg1f 3238 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝑆 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
326 | 311, 325 | mpcom 37 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
327 | 300, 310,
326 | vtocl 3232 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
328 | 154, 295,
30, 164, 165, 299, 327 | syl123anc 1335 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
329 | 153, 328 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
330 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑋)) |
331 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑌)) |
332 | 13, 5, 147, 152, 290, 294, 329, 70, 21, 19, 76, 330, 63, 331 | dvle 23574 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((⦋𝑋 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑋 / 𝑥⦌𝐵 · 𝑋))) |
333 | 280, 97, 98 | subdid 10365 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) = ((⦋𝑋 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑋 / 𝑥⦌𝐵 · 𝑋))) |
334 | 332, 333 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
335 | 66, 79, 286, 334 | subled 10509 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐴) |
336 | 285, 335 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ⦋𝑋 / 𝑥⦌𝐴) |
337 | 259, 264,
79, 336 | subled 10509 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
338 | 262 | renegcld 10336 |
. . . . . . . . . . . 12
⊢ (𝜑 → -((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
339 | | 1red 9934 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
340 | 5, 15, 339 | lesubadd2d 10505 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) ≤ 1 ↔ 𝑌 ≤ ((⌊‘𝑋) + 1))) |
341 | 247, 340 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ≤ 1) |
342 | 16, 339 | suble0d 10497 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ (𝑌 − (⌊‘𝑋)) ≤ 1)) |
343 | 341, 342 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ≤ 0) |
344 | 262 | le0neg1d 10478 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1))) |
345 | 343, 344 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1)) |
346 | 50, 74, 338, 345, 238 | lemul2ad 10843 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
347 | 278, 96 | mulneg1d 10362 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵)) |
348 | 278, 280 | mulneg1d 10362 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
349 | 346, 347,
348 | 3brtr3d 4614 |
. . . . . . . . . 10
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
350 | 263, 265 | lenegd 10485 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ↔ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) |
351 | 349, 350 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵)) |
352 | 263, 265,
66, 351 | lesub1dd 10522 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
353 | 260, 264,
266, 337, 352 | letrd 10073 |
. . . . . . 7
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
354 | 216, 274,
280 | subdird 10366 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − (1 · ⦋𝑋 / 𝑥⦌𝐵))) |
355 | 280 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵) |
356 | 355 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − (1 · ⦋𝑋 / 𝑥⦌𝐵)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵)) |
357 | 354, 356 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵)) |
358 | 357 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
359 | 215, 274,
96 | subdird 10366 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵))) |
360 | 96 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
⦋𝑌 / 𝑥⦌𝐵) = ⦋𝑌 / 𝑥⦌𝐵) |
361 | 360 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
362 | 359, 361 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
363 | 362 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
364 | 353, 358,
363 | 3brtr3d 4614 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
365 | 75 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
366 | 79 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ) |
367 | 365, 366,
280 | sub32d 10303 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
368 | 208, 209,
96 | sub32d 10303 |
. . . . . 6
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
369 | 364, 367,
368 | 3brtr4d 4615 |
. . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵)) |
370 | 255, 256,
91, 369 | leadd1dd 10520 |
. . . 4
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
371 | 80 | recnd 9947 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ) |
372 | 91 | recnd 9947 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ) |
373 | 371, 372,
280 | addsubd 10292 |
. . . 4
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵) = (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
374 | 67 | recnd 9947 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ) |
375 | 374, 372,
96 | addsubd 10292 |
. . . 4
⊢ (𝜑 → (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵) = (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
376 | 370, 373,
375 | 3brtr4d 4615 |
. . 3
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵)) |
377 | 253 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) = (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵)) |
378 | 248 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵) = (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵)) |
379 | 376, 377,
378 | 3brtr4d 4615 |
. 2
⊢ (𝜑 → ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)) |
380 | 254, 379 | jca 553 |
1
⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) |