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