Step | Hyp | Ref
| Expression |
1 | | dvfsum.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑇(,)+∞) |
2 | | ioossre 13382 |
. . . . . . . . 9
⊢ (𝑇(,)+∞) ⊆
ℝ |
3 | 1, 2 | eqsstri 4008 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℝ |
4 | | dvfsumlem1.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
5 | 3, 4 | sselid 3972 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) |
6 | | dvfsumlem1.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
7 | 6, 1 | eleqtrdi 2835 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝑇(,)+∞)) |
8 | | dvfsum.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℝ) |
9 | 8 | rexrd 11261 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈
ℝ*) |
10 | | elioopnf 13417 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ ℝ*
→ (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))) |
12 | 7, 11 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)) |
13 | 12 | simpld 494 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℝ) |
14 | | reflcl 13758 |
. . . . . . . 8
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ∈
ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (⌊‘𝑋) ∈
ℝ) |
16 | 5, 15 | resubcld 11639 |
. . . . . 6
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℝ) |
17 | | csbeq1 3888 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
18 | 17 | eleq1d 2810 |
. . . . . . 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 25880 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
24 | 23 | fmpttd 7106 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
25 | | nfcv 2895 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝐵 |
26 | | nfcsb1v 3910 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
27 | | csbeq1a 3899 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
28 | 25, 26, 27 | cbvmpt 5249 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐵) |
29 | 28 | fmpt 7101 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑆 ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
30 | 24, 29 | sylibr 233 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
31 | 18, 30, 4 | rspcdva 3605 |
. . . . . 6
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) |
32 | 16, 31 | remulcld 11241 |
. . . . 5
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
33 | | csbeq1 3888 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑌 / 𝑥⦌𝐴) |
34 | 33 | eleq1d 2810 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ)) |
35 | 20 | fmpttd 7106 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ) |
36 | | nfcv 2895 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐴 |
37 | | nfcsb1v 3910 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 |
38 | | csbeq1a 3899 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴) |
39 | 36, 37, 38 | cbvmpt 5249 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝑆 ↦ 𝐴) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) |
40 | 39 | fmpt 7101 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑆 ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ) |
41 | 35, 40 | sylibr 233 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
42 | 34, 41, 4 | rspcdva 3605 |
. . . . 5
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℝ) |
43 | 32, 42 | resubcld 11639 |
. . . 4
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
44 | 13, 15 | resubcld 11639 |
. . . . . 6
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℝ) |
45 | | csbeq1 3888 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
46 | 45 | eleq1d 2810 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ)) |
47 | 46, 30, 6 | rspcdva 3605 |
. . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) |
48 | 44, 47 | remulcld 11241 |
. . . . 5
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
49 | | csbeq1 3888 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑋 / 𝑥⦌𝐴) |
50 | 49 | eleq1d 2810 |
. . . . . 6
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ)) |
51 | 50, 41, 6 | rspcdva 3605 |
. . . . 5
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℝ) |
52 | 48, 51 | resubcld 11639 |
. . . 4
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
53 | | fzfid 13935 |
. . . . 5
⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin) |
54 | | dvfsum.b2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
55 | 54 | ralrimiva 3138 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℝ) |
56 | | elfzuz 13494 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
57 | | dvfsum.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
58 | 56, 57 | eleqtrrdi 2836 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍) |
59 | | dvfsum.c |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
60 | 59 | eleq1d 2810 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ)) |
61 | 60 | rspccva 3603 |
. . . . . 6
⊢
((∀𝑥 ∈
𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℝ) |
62 | 55, 58, 61 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℝ) |
63 | 53, 62 | fsumrecl 15677 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℝ) |
64 | 44, 31 | remulcld 11241 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
65 | 64, 51 | resubcld 11639 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
66 | 5, 13 | resubcld 11639 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℝ) |
67 | 31, 66 | remulcld 11241 |
. . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℝ) |
68 | 31 | recnd 11239 |
. . . . . . . . . 10
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
69 | 5 | recnd 11239 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℂ) |
70 | 13 | recnd 11239 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
71 | 68, 69, 70 | subdid 11667 |
. . . . . . . . 9
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) = ((⦋𝑌 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑌 / 𝑥⦌𝐵 · 𝑋))) |
72 | | eqid 2724 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
73 | 72 | mpomulcn 24707 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
74 | | csbeq1 3888 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑌 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
75 | 74 | eleq1d 2810 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑌 → (⦋𝑧 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) |
76 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑧𝐵 |
77 | | nfcsb1v 3910 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
78 | | csbeq1a 3899 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
79 | 76, 77, 78 | cbvmpt 5249 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑧 ∈ 𝑆 ↦ ⦋𝑧 / 𝑥⦌𝐵) |
80 | 79 | fmpt 7101 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧 ∈
𝑆 ⦋𝑧 / 𝑥⦌𝐵 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
81 | 24, 80 | sylibr 233 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 ⦋𝑧 / 𝑥⦌𝐵 ∈ ℝ) |
82 | 75, 81, 4 | rspcdva 3605 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) |
83 | | pnfxr 11265 |
. . . . . . . . . . . . . . . . . 18
⊢ +∞
∈ ℝ* |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → +∞ ∈
ℝ*) |
85 | 12 | simprd 495 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 < 𝑋) |
86 | 5 | ltpnfd 13098 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑌 < +∞) |
87 | | iccssioo 13390 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ ℝ*
∧ +∞ ∈ ℝ*) ∧ (𝑇 < 𝑋 ∧ 𝑌 < +∞)) → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞)) |
88 | 9, 84, 85, 86, 87 | syl22anc 836 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ (𝑇(,)+∞)) |
89 | 88, 2 | sstrdi 3986 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
90 | | ax-resscn 11163 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
91 | 89, 90 | sstrdi 3986 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℂ) |
92 | 90 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℝ ⊆
ℂ) |
93 | | cncfmptc 24754 |
. . . . . . . . . . . . . 14
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
94 | 82, 91, 92, 93 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
95 | | cncfmptid 24755 |
. . . . . . . . . . . . . 14
⊢ (((𝑋[,]𝑌) ⊆ ℝ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
96 | 89, 90, 95 | sylancl 585 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ 𝑦) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
97 | | remulcl 11191 |
. . . . . . . . . . . . . 14
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑌 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ) |
98 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) |
99 | 98 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
100 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ) |
101 | 100 | recnd 11239 |
. . . . . . . . . . . . . . . . . 18
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℂ) |
102 | 99, 101 | jca 511 |
. . . . . . . . . . . . . . . . 17
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
103 | | ovmpot 7561 |
. . . . . . . . . . . . . . . . . 18
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) |
104 | 103 | eqcomd 2730 |
. . . . . . . . . . . . . . . . 17
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) |
105 | 102, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) |
106 | 105 | eleq1d 2810 |
. . . . . . . . . . . . . . 15
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((⦋𝑌 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ ↔ (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ)) |
107 | 106 | biimpd 228 |
. . . . . . . . . . . . . 14
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((⦋𝑌 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ → (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ)) |
108 | 97, 107 | mpd 15 |
. . . . . . . . . . . . 13
⊢
((⦋𝑌 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ) |
109 | 72, 73, 94, 96, 90, 108 | cncfmpt2ss 24758 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
110 | | df-mpt 5222 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} |
111 | 110 | eleq1i 2816 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ) ↔ {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
112 | 111 | biimpi 215 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ) → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
113 | 109, 112 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
114 | | idd 24 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → 𝑦 ∈ (𝑋[,]𝑌))) |
115 | 114 | a1dd 50 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑦 ∈ (𝑋[,]𝑌)))) |
116 | 115 | impd 410 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → 𝑦 ∈ (𝑋[,]𝑌))) |
117 | | csbeq1 3888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑚 = 𝑌 → ⦋𝑚 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
118 | 117 | eleq1d 2810 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑚 = 𝑌 → (⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) |
119 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎ𝑚𝐵 |
120 | | nfcsb1v 3910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎ𝑥⦋𝑚 / 𝑥⦌𝐵 |
121 | | csbeq1a 3899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑥⦌𝐵) |
122 | 119, 120,
121 | cbvmpt 5249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑚 ∈ 𝑆 ↦ ⦋𝑚 / 𝑥⦌𝐵) |
123 | 122 | fmpt 7101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑚 ∈
𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
124 | 24, 123 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∀𝑚 ∈ 𝑆 ⦋𝑚 / 𝑥⦌𝐵 ∈ ℝ) |
125 | 118, 124,
4 | rspcdva 3605 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) |
126 | 125 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
127 | 126 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
128 | | elicc2 13386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌))) |
129 | 13, 5, 128 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↔ (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌))) |
130 | 129 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌)) |
131 | 130 | simp1d 1139 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ) |
132 | 131 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℂ) |
133 | 127, 132 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
134 | 133, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) |
135 | 134 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ↔ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) |
136 | 135 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) |
137 | 136 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)))) |
138 | 137 | impd 410 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) |
139 | 116, 138 | jcad 512 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)))) |
140 | 114 | a1dd 50 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) → 𝑦 ∈ (𝑋[,]𝑌)))) |
141 | 140 | impd 410 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) → 𝑦 ∈ (𝑋[,]𝑌))) |
142 | | csbeq1 3888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 = 𝑌 → ⦋𝑘 / 𝑥⦌𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
143 | 142 | eleq1d 2810 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 = 𝑌 → (⦋𝑘 / 𝑥⦌𝐵 ∈ ℝ ↔ ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ)) |
144 | | nfcv 2895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎ𝑘𝐵 |
145 | | nfcsb1v 3910 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎ𝑥⦋𝑘 / 𝑥⦌𝐵 |
146 | | csbeq1a 3899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑥⦌𝐵) |
147 | 144, 145,
146 | cbvmpt 5249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ 𝑆 ↦ 𝐵) = (𝑘 ∈ 𝑆 ↦ ⦋𝑘 / 𝑥⦌𝐵) |
148 | 147 | fmpt 7101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑘 ∈
𝑆 ⦋𝑘 / 𝑥⦌𝐵 ∈ ℝ ↔ (𝑥 ∈ 𝑆 ↦ 𝐵):𝑆⟶ℝ) |
149 | 24, 148 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∀𝑘 ∈ 𝑆 ⦋𝑘 / 𝑥⦌𝐵 ∈ ℝ) |
150 | 143, 149,
4 | rspcdva 3605 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℝ) |
151 | 150 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
152 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
153 | 152, 132 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
154 | 153, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) |
155 | 154 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) ↔ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))) |
156 | 155 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) → 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))) |
157 | 156 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) → 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))) |
158 | 157 | impd 410 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) → 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))) |
159 | 141, 158 | jcad 512 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) → (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))) |
160 | 139, 159 | impbid 211 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)))) |
161 | 160 | opabbidv 5204 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))}) |
162 | | df-mpt 5222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))} |
163 | 162 | eqcomi 2733 |
. . . . . . . . . . . . . . . 16
⊢
{〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) |
164 | 163 | eqeq2i 2737 |
. . . . . . . . . . . . . . 15
⊢
({〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))} ↔ {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) |
165 | 164 | biimpi 215 |
. . . . . . . . . . . . . 14
⊢
({〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))} → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) |
166 | 161, 165 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) |
167 | 166 | eleq1d 2810 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ) ↔ (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))) |
168 | 167 | biimpd 228 |
. . . . . . . . . . 11
⊢ (𝜑 → ({〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑌 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))) |
169 | 113, 168 | mpd 15 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
170 | | reelprrecn 11198 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ {ℝ, ℂ} |
171 | 170 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
172 | | ioossicc 13407 |
. . . . . . . . . . . . . . 15
⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) |
173 | 172, 89 | sstrid 3985 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ ℝ) |
174 | 173 | sselda 3974 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℝ) |
175 | 174 | recnd 11239 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 𝑦 ∈ ℂ) |
176 | | 1cnd 11206 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → 1 ∈ ℂ) |
177 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ) |
178 | 177 | recnd 11239 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) |
179 | | 1cnd 11206 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) |
180 | 171 | dvmptid 25811 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) |
181 | 72 | tgioo2 24641 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
182 | | iooretop 24604 |
. . . . . . . . . . . . . 14
⊢ (𝑋(,)𝑌) ∈ (topGen‘ran
(,)) |
183 | 182 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋(,)𝑌) ∈ (topGen‘ran
(,))) |
184 | 171, 178,
179, 180, 173, 181, 72, 183 | dvmptres 25817 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ 𝑦)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ 1)) |
185 | 171, 175,
176, 184, 68 | dvmptcmul 25818 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 1))) |
186 | 68 | mulridd 11228 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · 1) = ⦋𝑌 / 𝑥⦌𝐵) |
187 | 186 | mpteq2dv 5240 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵)) |
188 | 185, 187 | eqtrd 2764 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑌 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑌 / 𝑥⦌𝐵)) |
189 | 88, 1 | sseqtrrdi 4025 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ 𝑆) |
190 | 189 | resmptd 6030 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) = (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴)) |
191 | 20 | recnd 11239 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
192 | 191 | fmpttd 7106 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ) |
193 | 22 | dmeqd 5895 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = dom (𝑥 ∈ 𝑆 ↦ 𝐵)) |
194 | 21 | ralrimiva 3138 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ 𝑉) |
195 | | dmmptg 6231 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
𝑆 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝑆 ↦ 𝐵) = 𝑆) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom (𝑥 ∈ 𝑆 ↦ 𝐵) = 𝑆) |
197 | 193, 196 | eqtrd 2764 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = 𝑆) |
198 | | dvcn 25773 |
. . . . . . . . . . . . . . . 16
⊢
(((ℝ ⊆ ℂ ∧ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℂ ∧ 𝑆 ⊆ ℝ) ∧ dom (ℝ D
(𝑥 ∈ 𝑆 ↦ 𝐴)) = 𝑆) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) |
199 | 92, 192, 19, 197, 198 | syl31anc 1370 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) |
200 | | cncfcdm 24740 |
. . . . . . . . . . . . . . 15
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℂ)) → ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ)) |
201 | 90, 199, 200 | sylancr 586 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ) ↔ (𝑥 ∈ 𝑆 ↦ 𝐴):𝑆⟶ℝ)) |
202 | 35, 201 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→ℝ)) |
203 | 39, 202 | eqeltrrid 2830 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ (𝑆–cn→ℝ)) |
204 | | rescncf 24739 |
. . . . . . . . . . . 12
⊢ ((𝑋[,]𝑌) ⊆ 𝑆 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ (𝑆–cn→ℝ) → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ))) |
205 | 189, 203,
204 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴) ↾ (𝑋[,]𝑌)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
206 | 190, 205 | eqeltrrd 2826 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
207 | 41 | r19.21bi 3240 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) |
208 | 207 | recnd 11239 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) |
209 | 30 | r19.21bi 3240 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) |
210 | 39 | oveq2i 7412 |
. . . . . . . . . . . 12
⊢ (ℝ
D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴)) |
211 | 22, 210, 28 | 3eqtr3g 2787 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ 𝑆 ↦ ⦋𝑦 / 𝑥⦌𝐵)) |
212 | 172, 189 | sstrid 3985 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ 𝑆) |
213 | 171, 208,
209, 211, 212, 181, 72, 183 | dvmptres 25817 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑦 / 𝑥⦌𝐵)) |
214 | 172 | sseli 3970 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑋(,)𝑌) → 𝑦 ∈ (𝑋[,]𝑌)) |
215 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝜑) |
216 | 189 | sselda 3974 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ 𝑆) |
217 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈ 𝑆) |
218 | | dvfsum.d |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ ℝ) |
219 | 218 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ∈ ℝ) |
220 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ ℝ) |
221 | | dvfsumlem1.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ≤ 𝑋) |
222 | 221 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ≤ 𝑋) |
223 | 130 | simp2d 1140 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ≤ 𝑦) |
224 | 219, 220,
131, 222, 223 | letrd 11368 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝐷 ≤ 𝑦) |
225 | 130 | simp3d 1141 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ≤ 𝑌) |
226 | | dvfsumlem1.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ≤ 𝑈) |
227 | 226 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ≤ 𝑈) |
228 | | simp2r 1197 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → 𝑌 ∈ 𝑆) |
229 | | eleq1 2813 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑘 ∈ 𝑆 ↔ 𝑌 ∈ 𝑆)) |
230 | 229 | anbi2d 628 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → ((𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆))) |
231 | | breq2 5142 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑦 ≤ 𝑘 ↔ 𝑦 ≤ 𝑌)) |
232 | | breq1 5141 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑌 → (𝑘 ≤ 𝑈 ↔ 𝑌 ≤ 𝑈)) |
233 | 231, 232 | 3anbi23d 1435 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → ((𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈))) |
234 | 230, 233 | 3anbi23d 1435 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑌 → ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)))) |
235 | | vex 3470 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑘 ∈ V |
236 | 235, 59 | csbie 3921 |
. . . . . . . . . . . . . . . . 17
⊢
⦋𝑘 /
𝑥⦌𝐵 = 𝐶 |
237 | 236, 142 | eqtr3id 2778 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑌 → 𝐶 = ⦋𝑌 / 𝑥⦌𝐵) |
238 | 237 | breq1d 5148 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑌 → (𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵 ↔ ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
239 | 234, 238 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑌 → (((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) ↔ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵))) |
240 | | nfv 1909 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) |
241 | | nfcv 2895 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐶 |
242 | | nfcv 2895 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥
≤ |
243 | 241, 242,
26 | nfbr 5185 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵 |
244 | 240, 243 | nfim 1891 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
245 | | eleq1 2813 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆)) |
246 | 245 | anbi1d 629 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆))) |
247 | | breq2 5142 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑦)) |
248 | | breq1 5141 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑘 ↔ 𝑦 ≤ 𝑘)) |
249 | 247, 248 | 3anbi12d 1433 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈))) |
250 | 246, 249 | 3anbi23d 1435 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)))) |
251 | 27 | breq2d 5150 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
252 | 250, 251 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵))) |
253 | | dvfsum.l |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) |
254 | 244, 252,
253 | chvarfv 2225 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
255 | 239, 254 | vtoclg 3535 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ 𝑆 → ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵)) |
256 | 228, 255 | mpcom 38 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝐷 ≤ 𝑦 ∧ 𝑦 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
257 | 215, 216,
217, 224, 225, 227, 256 | syl123anc 1384 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
258 | 214, 257 | sylan2 592 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
259 | 13 | rexrd 11261 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
260 | 5 | rexrd 11261 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
261 | | dvfsumlem1.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
262 | | lbicc2 13438 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑋 ∈ (𝑋[,]𝑌)) |
263 | 259, 260,
261, 262 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ (𝑋[,]𝑌)) |
264 | | ubicc2 13439 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ* ∧ 𝑋
≤ 𝑌) → 𝑌 ∈ (𝑋[,]𝑌)) |
265 | 259, 260,
261, 264 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑋[,]𝑌)) |
266 | | oveq2 7409 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑋)) |
267 | | oveq2 7409 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (⦋𝑌 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑌 / 𝑥⦌𝐵 · 𝑌)) |
268 | 13, 5, 169, 188, 206, 213, 258, 263, 265, 261, 266, 49, 267, 33 | dvle 25862 |
. . . . . . . . 9
⊢ (𝜑 → ((⦋𝑌 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑌 / 𝑥⦌𝐵 · 𝑋)) ≤ (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴)) |
269 | 71, 268 | eqbrtrd 5160 |
. . . . . . . 8
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ≤ (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴)) |
270 | 67, 42, 51, 269 | lesubd 11815 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ≤ (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
271 | 64 | recnd 11239 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
272 | 32 | recnd 11239 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
273 | 42 | recnd 11239 |
. . . . . . . . 9
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ) |
274 | 271, 272,
273 | subsubd 11596 |
. . . . . . . 8
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴)) |
275 | 272, 271 | negsubdi2d 11584 |
. . . . . . . . . . 11
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵))) |
276 | 15 | recnd 11239 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘𝑋) ∈
ℂ) |
277 | 69, 70, 276 | nnncan2d 11603 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) = (𝑌 − 𝑋)) |
278 | 277 | oveq1d 7416 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · ⦋𝑌 / 𝑥⦌𝐵) = ((𝑌 − 𝑋) · ⦋𝑌 / 𝑥⦌𝐵)) |
279 | 16 | recnd 11239 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℂ) |
280 | 44 | recnd 11239 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 − (⌊‘𝑋)) ∈ ℂ) |
281 | 279, 280,
68 | subdird 11668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋))) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵))) |
282 | 66 | recnd 11239 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℂ) |
283 | 282, 68 | mulcomd 11232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − 𝑋) · ⦋𝑌 / 𝑥⦌𝐵) = (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
284 | 278, 281,
283 | 3eqtr3d 2772 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
285 | 284 | negeqd 11451 |
. . . . . . . . . . 11
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = -(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
286 | 275, 285 | eqtr3d 2766 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) = -(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
287 | 286 | oveq1d 7416 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = (-(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) + ⦋𝑌 / 𝑥⦌𝐴)) |
288 | 67 | recnd 11239 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℂ) |
289 | 288, 273 | negsubdid 11583 |
. . . . . . . . 9
⊢ (𝜑 → -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴) = (-(⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) + ⦋𝑌 / 𝑥⦌𝐴)) |
290 | 287, 289 | eqtr4d 2767 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴)) |
291 | 288, 273 | negsubdi2d 11584 |
. . . . . . . 8
⊢ (𝜑 → -((⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) − ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
292 | 274, 290,
291 | 3eqtrd 2768 |
. . . . . . 7
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑌 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
293 | 270, 292 | breqtrrd 5166 |
. . . . . 6
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴))) |
294 | 51, 64, 43, 293 | lesubd 11815 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
295 | | flle 13761 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ≤
𝑋) |
296 | 13, 295 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘𝑋) ≤ 𝑋) |
297 | 13, 15 | subge0d 11801 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝑋 − (⌊‘𝑋)) ↔ (⌊‘𝑋) ≤ 𝑋)) |
298 | 296, 297 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑋 − (⌊‘𝑋))) |
299 | 45 | breq2d 5150 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → (⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵 ↔ ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
300 | 257 | ralrimiva 3138 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ (𝑋[,]𝑌)⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑦 / 𝑥⦌𝐵) |
301 | 299, 300,
263 | rspcdva 3605 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
302 | 31, 47, 44, 298, 301 | lemul2ad 12151 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ≤ ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵)) |
303 | 64, 48, 51, 302 | lesub1dd 11827 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
304 | 43, 65, 52, 294, 303 | letrd 11368 |
. . . 4
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
305 | 43, 52, 63, 304 | leadd1dd 11825 |
. . 3
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
306 | | dvfsum.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
307 | | dvfsum.md |
. . . 4
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) |
308 | | dvfsum.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈
ℝ*) |
309 | | dvfsum.h |
. . . 4
⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) |
310 | | dvfsumlem1.6 |
. . . 4
⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) |
311 | 1, 57, 306, 218, 307, 8, 20, 21, 54, 22, 59, 308, 253, 309, 6, 4, 221, 261, 226, 310 | dvfsumlem1 25882 |
. . 3
⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
312 | 13 | leidd 11777 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑋) |
313 | 259, 260,
308, 261, 226 | xrletrd 13138 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ 𝑈) |
314 | | fllep1 13763 |
. . . . 5
⊢ (𝑋 ∈ ℝ → 𝑋 ≤ ((⌊‘𝑋) + 1)) |
315 | 13, 314 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑋 ≤ ((⌊‘𝑋) + 1)) |
316 | 1, 57, 306, 218, 307, 8, 20, 21, 54, 22, 59, 308, 253, 309, 6, 6, 221, 312, 313, 315 | dvfsumlem1 25882 |
. . 3
⊢ (𝜑 → (𝐻‘𝑋) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
317 | 305, 311,
316 | 3brtr4d 5170 |
. 2
⊢ (𝜑 → (𝐻‘𝑌) ≤ (𝐻‘𝑋)) |
318 | 52, 47 | resubcld 11639 |
. . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
319 | 43, 31 | resubcld 11639 |
. . . . 5
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
320 | | peano2rem 11524 |
. . . . . . . . . . 11
⊢ ((𝑋 − (⌊‘𝑋)) ∈ ℝ → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℝ) |
321 | 44, 320 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℝ) |
322 | 321, 47 | remulcld 11241 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
323 | 322, 51 | resubcld 11639 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℝ) |
324 | | peano2rem 11524 |
. . . . . . . . . . 11
⊢ ((𝑌 − (⌊‘𝑋)) ∈ ℝ → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
325 | 16, 324 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
326 | 325, 47 | remulcld 11241 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℝ) |
327 | 326, 42 | resubcld 11639 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
328 | 325, 31 | remulcld 11241 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℝ) |
329 | 328, 42 | resubcld 11639 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℝ) |
330 | 322 | recnd 11239 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
331 | 326 | recnd 11239 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
332 | 330, 331 | subcld 11568 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) ∈ ℂ) |
333 | 332, 273 | addcomd 11413 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴) = (⦋𝑌 / 𝑥⦌𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
334 | 330, 331,
273 | subsubd 11596 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) + ⦋𝑌 / 𝑥⦌𝐴)) |
335 | 273, 331,
330 | subsub2d 11597 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) = (⦋𝑌 / 𝑥⦌𝐴 + ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
336 | 333, 334,
335 | 3eqtr4d 2774 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)))) |
337 | | 1cnd 11206 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℂ) |
338 | 279, 280,
337 | nnncan2d 11603 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = ((𝑌 − (⌊‘𝑋)) − (𝑋 − (⌊‘𝑋)))) |
339 | 338, 277 | eqtrd 2764 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) = (𝑌 − 𝑋)) |
340 | 339 | oveq1d 7416 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · ⦋𝑋 / 𝑥⦌𝐵) = ((𝑌 − 𝑋) · ⦋𝑋 / 𝑥⦌𝐵)) |
341 | 325 | recnd 11239 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ∈
ℂ) |
342 | 321 | recnd 11239 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) − 1) ∈
ℂ) |
343 | 47 | recnd 11239 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) |
344 | 341, 342,
343 | subdird 11668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) − ((𝑋 − (⌊‘𝑋)) − 1)) · ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) |
345 | 282, 343 | mulcomd 11232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − 𝑋) · ⦋𝑋 / 𝑥⦌𝐵) = (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
346 | 340, 344,
345 | 3eqtr3d 2772 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) = (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
347 | 346 | oveq2d 7417 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
348 | 336, 347 | eqtrd 2764 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) = (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)))) |
349 | 47, 66 | remulcld 11241 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) ∈ ℝ) |
350 | | cncfmptc 24754 |
. . . . . . . . . . . . . . . . 17
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ (𝑋[,]𝑌) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑋[,]𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
351 | 47, 91, 92, 350 | syl3anc 1368 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
352 | | remulcl 11191 |
. . . . . . . . . . . . . . . . 17
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑋 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ) |
353 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
⦋𝑋 / 𝑥⦌𝐵 ∈ ℝ) |
354 | 353 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) |
355 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℝ) |
356 | 355 | recnd 11239 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈
ℂ) |
357 | 354, 356 | jca 511 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
358 | | ovmpot 7561 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) |
359 | 358 | eqcomd 2730 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
(⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) |
360 | 357, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) |
361 | 360 | eleq1d 2810 |
. . . . . . . . . . . . . . . . . 18
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((⦋𝑋 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ ↔ (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ)) |
362 | 361 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((⦋𝑋 / 𝑥⦌𝐵 · 𝑦) ∈ ℝ → (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ)) |
363 | 352, 362 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢
((⦋𝑋 /
𝑥⦌𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
(⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ) |
364 | 72, 73, 351, 96, 90, 363 | cncfmpt2ss 24758 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
365 | | df-mpt 5222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} |
366 | 365 | eleq1i 2816 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ) ↔ {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
367 | 366 | biimpi 215 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ) → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
368 | 364, 367 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
369 | 114 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑦 ∈ (𝑋[,]𝑌)))) |
370 | 369 | impd 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → 𝑦 ∈ (𝑋[,]𝑌))) |
371 | 343 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ) |
372 | 371, 132 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (⦋𝑋 / 𝑥⦌𝐵 ∈ ℂ ∧ 𝑦 ∈ ℂ)) |
373 | 372, 358 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) |
374 | 373 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ↔ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) |
375 | 374 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) |
376 | 375 | ex 412 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) → 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)))) |
377 | 376 | impd 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) |
378 | 370, 377 | jcad 512 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) → (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)))) |
379 | 114 | a1dd 50 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) → 𝑦 ∈ (𝑋[,]𝑌)))) |
380 | 379 | impd 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) → 𝑦 ∈ (𝑋[,]𝑌))) |
381 | 372, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) |
382 | 381 | eqeq2d 2735 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) ↔ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))) |
383 | 382 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → (𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) → 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))) |
384 | 383 | ex 412 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) → (𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) → 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))) |
385 | 384 | impd 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) → 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))) |
386 | 380, 385 | jcad 512 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) → (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)))) |
387 | 378, 386 | impbid 211 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)))) |
388 | 387 | opabbidv 5204 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))}) |
389 | | df-mpt 5222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))} |
390 | 389 | eqcomi 2733 |
. . . . . . . . . . . . . . . . . . 19
⊢
{〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) |
391 | 390 | eqeq2i 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
({〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))} ↔ {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) |
392 | 391 | biimpi 215 |
. . . . . . . . . . . . . . . . 17
⊢
({〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))} → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) |
393 | 388, 392 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) |
394 | 393 | eleq1d 2810 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ({〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ) ↔ (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))) |
395 | 394 | biimpd 228 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ({〈𝑦, 𝑤〉 ∣ (𝑦 ∈ (𝑋[,]𝑌) ∧ 𝑤 = (⦋𝑋 / 𝑥⦌𝐵(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑋[,]𝑌)–cn→ℝ) → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ))) |
396 | 368, 395 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ (𝑋[,]𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦)) ∈ ((𝑋[,]𝑌)–cn→ℝ)) |
397 | 171, 175,
176, 184, 343 | dvmptcmul 25818 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 1))) |
398 | 343 | mulridd 11228 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · 1) = ⦋𝑋 / 𝑥⦌𝐵) |
399 | 398 | mpteq2dv 5240 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 1)) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵)) |
400 | 397, 399 | eqtrd 2764 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝑋(,)𝑌) ↦ (⦋𝑋 / 𝑥⦌𝐵 · 𝑦))) = (𝑦 ∈ (𝑋(,)𝑌) ↦ ⦋𝑋 / 𝑥⦌𝐵)) |
401 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑋 ∈ 𝑆) |
402 | 131 | rexrd 11261 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ∈ ℝ*) |
403 | 260 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑌 ∈
ℝ*) |
404 | 308 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑈 ∈
ℝ*) |
405 | 402, 403,
404, 225, 227 | xrletrd 13138 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → 𝑦 ≤ 𝑈) |
406 | | vex 3470 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
407 | | eleq1 2813 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝑆 ↔ 𝑦 ∈ 𝑆)) |
408 | 407 | anbi2d 628 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆))) |
409 | | breq2 5142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑋 ≤ 𝑘 ↔ 𝑋 ≤ 𝑦)) |
410 | | breq1 5141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 ≤ 𝑈 ↔ 𝑦 ≤ 𝑈)) |
411 | 409, 410 | 3anbi23d 1435 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → ((𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈))) |
412 | 408, 411 | 3anbi23d 1435 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)))) |
413 | | csbeq1 3888 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → ⦋𝑘 / 𝑥⦌𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
414 | 236, 413 | eqtr3id 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐵) |
415 | 414 | breq1d 5148 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → (𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵 ↔ ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
416 | 412, 415 | imbi12d 344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
417 | | simp2l 1196 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝑋 ∈ 𝑆) |
418 | | nfv 1909 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) |
419 | | nfcsb1v 3910 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥⦋𝑋 / 𝑥⦌𝐵 |
420 | 241, 242,
419 | nfbr 5185 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵 |
421 | 418, 420 | nfim 1891 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
422 | | eleq1 2813 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆)) |
423 | 422 | anbi1d 629 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → ((𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ↔ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆))) |
424 | | breq2 5142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋)) |
425 | | breq1 5141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑘 ↔ 𝑋 ≤ 𝑘)) |
426 | 424, 425 | 3anbi12d 1433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → ((𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈) ↔ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈))) |
427 | 423, 426 | 3anbi23d 1435 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) ↔ (𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)))) |
428 | | csbeq1a 3899 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → 𝐵 = ⦋𝑋 / 𝑥⦌𝐵) |
429 | 428 | breq2d 5150 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → (𝐶 ≤ 𝐵 ↔ 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
430 | 427, 429 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ 𝐵) ↔ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵))) |
431 | 421, 430,
253 | vtoclg1f 3551 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ 𝑆 → ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵)) |
432 | 417, 431 | mpcom 38 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈)) → 𝐶 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
433 | 406, 416,
432 | vtocl 3538 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑦 ∧ 𝑦 ≤ 𝑈)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
434 | 215, 401,
216, 222, 223, 405, 433 | syl123anc 1384 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋[,]𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
435 | 214, 434 | sylan2 592 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋(,)𝑌)) → ⦋𝑦 / 𝑥⦌𝐵 ≤ ⦋𝑋 / 𝑥⦌𝐵) |
436 | | oveq2 7409 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑋)) |
437 | | oveq2 7409 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → (⦋𝑋 / 𝑥⦌𝐵 · 𝑦) = (⦋𝑋 / 𝑥⦌𝐵 · 𝑌)) |
438 | 13, 5, 206, 213, 396, 400, 435, 263, 265, 261, 49, 436, 33, 437 | dvle 25862 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((⦋𝑋 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑋 / 𝑥⦌𝐵 · 𝑋))) |
439 | 343, 69, 70 | subdid 11667 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋)) = ((⦋𝑋 / 𝑥⦌𝐵 · 𝑌) − (⦋𝑋 / 𝑥⦌𝐵 · 𝑋))) |
440 | 438, 439 | breqtrrd 5166 |
. . . . . . . . . . 11
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − ⦋𝑋 / 𝑥⦌𝐴) ≤ (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) |
441 | 42, 51, 349, 440 | subled 11814 |
. . . . . . . . . 10
⊢ (𝜑 → (⦋𝑌 / 𝑥⦌𝐴 − (⦋𝑋 / 𝑥⦌𝐵 · (𝑌 − 𝑋))) ≤ ⦋𝑋 / 𝑥⦌𝐴) |
442 | 348, 441 | eqbrtrd 5160 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) ≤ ⦋𝑋 / 𝑥⦌𝐴) |
443 | 322, 327,
51, 442 | subled 11814 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
444 | 325 | renegcld 11638 |
. . . . . . . . . . . 12
⊢ (𝜑 → -((𝑌 − (⌊‘𝑋)) − 1) ∈
ℝ) |
445 | | 1red 11212 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
446 | 5, 15, 445 | lesubadd2d 11810 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) ≤ 1 ↔ 𝑌 ≤ ((⌊‘𝑋) + 1))) |
447 | 310, 446 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ≤ 1) |
448 | 16, 445 | suble0d 11802 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ (𝑌 − (⌊‘𝑋)) ≤ 1)) |
449 | 447, 448 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) ≤ 0) |
450 | 325 | le0neg1d 11782 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) ≤ 0 ↔ 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1))) |
451 | 449, 450 | mpbid 231 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ -((𝑌 − (⌊‘𝑋)) − 1)) |
452 | 31, 47, 444, 451, 301 | lemul2ad 12151 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
453 | 341, 68 | mulneg1d 11664 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵)) |
454 | 341, 343 | mulneg1d 11664 |
. . . . . . . . . . 11
⊢ (𝜑 → (-((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
455 | 452, 453,
454 | 3brtr3d 5169 |
. . . . . . . . . 10
⊢ (𝜑 → -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵)) |
456 | 326, 328 | lenegd 11790 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ↔ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) ≤ -(((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵))) |
457 | 455, 456 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) ≤ (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵)) |
458 | 326, 328,
42, 457 | lesub1dd 11827 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
459 | 323, 327,
329, 443, 458 | letrd 11368 |
. . . . . . 7
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
460 | 280, 337,
343 | subdird 11668 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − (1 · ⦋𝑋 / 𝑥⦌𝐵))) |
461 | 343 | mullidd 11229 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
⦋𝑋 / 𝑥⦌𝐵) = ⦋𝑋 / 𝑥⦌𝐵) |
462 | 461 | oveq2d 7417 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − (1 · ⦋𝑋 / 𝑥⦌𝐵)) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵)) |
463 | 460, 462 | eqtrd 2764 |
. . . . . . . 8
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) = (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵)) |
464 | 463 | oveq1d 7416 |
. . . . . . 7
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) − 1) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
465 | 279, 337,
68 | subdird 11668 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵))) |
466 | 68 | mullidd 11229 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
⦋𝑌 / 𝑥⦌𝐵) = ⦋𝑌 / 𝑥⦌𝐵) |
467 | 466 | oveq2d 7417 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
468 | 465, 467 | eqtrd 2764 |
. . . . . . . 8
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
469 | 468 | oveq1d 7416 |
. . . . . . 7
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
470 | 459, 464,
469 | 3brtr3d 5169 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ≤ ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
471 | 48 | recnd 11239 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) ∈ ℂ) |
472 | 51 | recnd 11239 |
. . . . . . 7
⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 ∈ ℂ) |
473 | 471, 472,
343 | sub32d 11600 |
. . . . . 6
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) = ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴)) |
474 | 272, 273,
68 | sub32d 11600 |
. . . . . 6
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
475 | 470, 473,
474 | 3brtr4d 5170 |
. . . . 5
⊢ (𝜑 → ((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵)) |
476 | 318, 319,
63, 475 | leadd1dd 11825 |
. . . 4
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) ≤ (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
477 | 52 | recnd 11239 |
. . . . 5
⊢ (𝜑 → (((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) ∈ ℂ) |
478 | 63 | recnd 11239 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ) |
479 | 477, 478,
343 | addsubd 11589 |
. . . 4
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵) = (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) − ⦋𝑋 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
480 | 43 | recnd 11239 |
. . . . 5
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ) |
481 | 480, 478,
68 | addsubd 11589 |
. . . 4
⊢ (𝜑 → (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵) = (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) − ⦋𝑌 / 𝑥⦌𝐵) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |
482 | 476, 479,
481 | 3brtr4d 5170 |
. . 3
⊢ (𝜑 → (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵) ≤ (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵)) |
483 | 316 | oveq1d 7416 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) = (((((𝑋 − (⌊‘𝑋)) · ⦋𝑋 / 𝑥⦌𝐵) − ⦋𝑋 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑋 / 𝑥⦌𝐵)) |
484 | 311 | oveq1d 7416 |
. . 3
⊢ (𝜑 → ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵) = (((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) − ⦋𝑌 / 𝑥⦌𝐵)) |
485 | 482, 483,
484 | 3brtr4d 5170 |
. 2
⊢ (𝜑 → ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵)) |
486 | 317, 485 | jca 511 |
1
⊢ (𝜑 → ((𝐻‘𝑌) ≤ (𝐻‘𝑋) ∧ ((𝐻‘𝑋) − ⦋𝑋 / 𝑥⦌𝐵) ≤ ((𝐻‘𝑌) − ⦋𝑌 / 𝑥⦌𝐵))) |