Step | Hyp | Ref
| Expression |
1 | | c1liplem1.k |
. . 3
⊢ 𝐾 = sup((abs “ ((ℝ D
𝐹) “ (𝐴[,]𝐵))), ℝ, < ) |
2 | | imassrn 5940 |
. . . . . 6
⊢ (abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵))) ⊆ ran
abs |
3 | | absf 14901 |
. . . . . . 7
⊢
abs:ℂ⟶ℝ |
4 | | frn 6552 |
. . . . . . 7
⊢
(abs:ℂ⟶ℝ → ran abs ⊆
ℝ) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢ ran abs
⊆ ℝ |
6 | 2, 5 | sstri 3910 |
. . . . 5
⊢ (abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵))) ⊆
ℝ |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝜑 → (abs “ ((ℝ D
𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ) |
8 | | dvf 24804 |
. . . . . . . 8
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
9 | | ffun 6548 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun
(ℝ D 𝐹)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
⊢ Fun
(ℝ D 𝐹) |
11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝜑 → Fun (ℝ D 𝐹)) |
12 | | c1liplem1.dv |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
13 | | cncff 23790 |
. . . . . . . 8
⊢
(((ℝ D 𝐹)
↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ) |
14 | | fdm 6554 |
. . . . . . . 8
⊢
(((ℝ D 𝐹)
↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ → dom ((ℝ D
𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵)) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵)) |
16 | | ssdmres 5874 |
. . . . . . 7
⊢ ((𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵)) |
17 | 15, 16 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) |
18 | | c1liplem1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
19 | 18 | rexrd 10883 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
20 | | c1liplem1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
21 | 20 | rexrd 10883 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
22 | | c1liplem1.le |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
23 | | lbicc2 13052 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
24 | 19, 21, 22, 23 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
25 | | funfvima2 7047 |
. . . . . . 7
⊢ ((Fun
(ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) → (𝐴 ∈ (𝐴[,]𝐵) → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
26 | 25 | imp 410 |
. . . . . 6
⊢ (((Fun
(ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) ∧ 𝐴 ∈ (𝐴[,]𝐵)) → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
27 | 11, 17, 24, 26 | syl21anc 838 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
28 | | ffun 6548 |
. . . . . . 7
⊢
(abs:ℂ⟶ℝ → Fun abs) |
29 | 3, 28 | ax-mp 5 |
. . . . . 6
⊢ Fun
abs |
30 | | imassrn 5940 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹) “ (𝐴[,]𝐵)) ⊆ ran (ℝ D 𝐹) |
31 | | frn 6552 |
. . . . . . . . 9
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → ran
(ℝ D 𝐹) ⊆
ℂ) |
32 | 8, 31 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(ℝ D 𝐹) ⊆
ℂ |
33 | 30, 32 | sstri 3910 |
. . . . . . 7
⊢ ((ℝ
D 𝐹) “ (𝐴[,]𝐵)) ⊆ ℂ |
34 | 3 | fdmi 6557 |
. . . . . . 7
⊢ dom abs =
ℂ |
35 | 33, 34 | sseqtrri 3938 |
. . . . . 6
⊢ ((ℝ
D 𝐹) “ (𝐴[,]𝐵)) ⊆ dom abs |
36 | | funfvima2 7047 |
. . . . . 6
⊢ ((Fun abs
∧ ((ℝ D 𝐹)
“ (𝐴[,]𝐵)) ⊆ dom abs) →
(((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))) |
37 | 29, 35, 36 | mp2an 692 |
. . . . 5
⊢
(((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
38 | | ne0i 4249 |
. . . . 5
⊢
((abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅) |
39 | 27, 37, 38 | 3syl 18 |
. . . 4
⊢ (𝜑 → (abs “ ((ℝ D
𝐹) “ (𝐴[,]𝐵))) ≠ ∅) |
40 | | ax-resscn 10786 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
41 | | ssid 3923 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
42 | | cncfss 23796 |
. . . . . . . 8
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ)) |
43 | 40, 41, 42 | mp2an 692 |
. . . . . . 7
⊢ ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ) |
44 | 43, 12 | sseldi 3899 |
. . . . . 6
⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
45 | | cniccbdd 24358 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ((ℝ
D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) |
46 | 18, 20, 44, 45 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) |
47 | | fvelima 6778 |
. . . . . . . . . 10
⊢ ((Fun abs
∧ 𝑏 ∈ (abs “
((ℝ D 𝐹) “
(𝐴[,]𝐵)))) → ∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏) |
48 | 29, 47 | mpan 690 |
. . . . . . . . 9
⊢ (𝑏 ∈ (abs “ ((ℝ D
𝐹) “ (𝐴[,]𝐵))) → ∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏) |
49 | | fvres 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ (𝐴[,]𝐵) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏) = ((ℝ D 𝐹)‘𝑏)) |
50 | 49 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
(𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏) = ((ℝ D 𝐹)‘𝑏)) |
51 | 50 | fveq2d 6721 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
(𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) = (abs‘((ℝ D 𝐹)‘𝑏))) |
52 | | 2fveq3 6722 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑏 → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) = (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏))) |
53 | 52 | breq1d 5063 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑏 → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ↔ (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) ≤ 𝑎)) |
54 | 53 | rspccva 3536 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
(𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) ≤ 𝑎) |
55 | 51, 54 | eqbrtrrd 5077 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
(𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎) |
56 | 55 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎) |
57 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘((ℝ D 𝐹)‘𝑏)) = (abs‘𝑦)) |
58 | 57 | breq1d 5063 |
. . . . . . . . . . . . . 14
⊢
(((ℝ D 𝐹)‘𝑏) = 𝑦 → ((abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎 ↔ (abs‘𝑦) ≤ 𝑎)) |
59 | 56, 58 | syl5ibcom 248 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘𝑦) ≤ 𝑎)) |
60 | 59 | rexlimdva 3203 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘𝑦) ≤ 𝑎)) |
61 | | fvelima 6778 |
. . . . . . . . . . . . 13
⊢ ((Fun
(ℝ D 𝐹) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → ∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦) |
62 | 10, 61 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → ∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦) |
63 | 60, 62 | impel 509 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs‘𝑦) ≤ 𝑎) |
64 | | breq1 5056 |
. . . . . . . . . . 11
⊢
((abs‘𝑦) =
𝑏 → ((abs‘𝑦) ≤ 𝑎 ↔ 𝑏 ≤ 𝑎)) |
65 | 63, 64 | syl5ibcom 248 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → ((abs‘𝑦) = 𝑏 → 𝑏 ≤ 𝑎)) |
66 | 65 | rexlimdva 3203 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏 → 𝑏 ≤ 𝑎)) |
67 | 48, 66 | syl5 34 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → 𝑏 ≤ 𝑎)) |
68 | 67 | ralrimiv 3104 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) |
69 | 68 | ex 416 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 → ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎)) |
70 | 69 | reximdva 3193 |
. . . . 5
⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎)) |
71 | 46, 70 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) |
72 | 7, 39, 71 | suprcld 11795 |
. . 3
⊢ (𝜑 → sup((abs “ ((ℝ
D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ) ∈
ℝ) |
73 | 1, 72 | eqeltrid 2842 |
. 2
⊢ (𝜑 → 𝐾 ∈ ℝ) |
74 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (𝐴[,]𝐵)) |
75 | 74 | fvresd 6737 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) = (𝐹‘𝑦)) |
76 | | c1liplem1.cn |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
77 | | cncff 23790 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ) |
79 | 78 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ) |
80 | 79, 74 | ffvelrnd 6905 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) ∈ ℝ) |
81 | 80 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) ∈ ℂ) |
82 | 75, 81 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑦) ∈ ℂ) |
83 | | simplrl 777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (𝐴[,]𝐵)) |
84 | 83 | fvresd 6737 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) = (𝐹‘𝑥)) |
85 | 79, 83 | ffvelrnd 6905 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) ∈ ℝ) |
86 | 85 | recnd 10861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) ∈ ℂ) |
87 | 84, 86 | eqeltrrd 2839 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑥) ∈ ℂ) |
88 | 82, 87 | subcld 11189 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹‘𝑦) − (𝐹‘𝑥)) ∈ ℂ) |
89 | | iccssre 13017 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
90 | 18, 20, 89 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
91 | 90 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐴[,]𝐵) ⊆ ℝ) |
92 | 91, 74 | sseldd 3902 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ) |
93 | 91, 83 | sseldd 3902 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ) |
94 | 92, 93 | resubcld 11260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈ ℝ) |
95 | 94 | recnd 10861 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈ ℂ) |
96 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦) |
97 | | difrp 12624 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈
ℝ+)) |
98 | 93, 92, 97 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈
ℝ+)) |
99 | 96, 98 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈
ℝ+) |
100 | 99 | rpne0d 12633 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ≠ 0) |
101 | 88, 95, 100 | absdivd 15019 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥)))) |
102 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ) |
103 | 39 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅) |
104 | 71 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) |
105 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → Fun abs) |
106 | 88, 95, 100 | divcld 11608 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ℂ) |
107 | 106, 34 | eleqtrrdi 2849 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs) |
108 | 93 | rexrd 10883 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ*) |
109 | 92 | rexrd 10883 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ*) |
110 | 93, 92, 96 | ltled 10980 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ≤ 𝑦) |
111 | | ubicc2 13053 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑥
≤ 𝑦) → 𝑦 ∈ (𝑥[,]𝑦)) |
112 | 108, 109,
110, 111 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (𝑥[,]𝑦)) |
113 | 112 | fvresd 6737 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) = (𝐹‘𝑦)) |
114 | | lbicc2 13052 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑥
≤ 𝑦) → 𝑥 ∈ (𝑥[,]𝑦)) |
115 | 108, 109,
110, 114 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (𝑥[,]𝑦)) |
116 | 115 | fvresd 6737 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥) = (𝐹‘𝑥)) |
117 | 113, 116 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) = ((𝐹‘𝑦) − (𝐹‘𝑥))) |
118 | 117 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) |
119 | | iccss2 13006 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥[,]𝑦) ⊆ (𝐴[,]𝐵)) |
120 | 119 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥[,]𝑦) ⊆ (𝐴[,]𝐵)) |
121 | 120 | resabs1d 5882 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) = (𝐹 ↾ (𝑥[,]𝑦))) |
122 | 76 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
123 | | rescncf 23794 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥[,]𝑦) ⊆ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ))) |
124 | 120, 122,
123 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ)) |
125 | 121, 124 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ)) |
126 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ℝ ⊆
ℂ) |
127 | | c1liplem1.f |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
128 | 127 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
129 | | cnex 10810 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ
∈ V |
130 | | reex 10820 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℝ
∈ V |
131 | 129, 130 | elpm2 8555 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (ℂ
↑pm ℝ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
132 | 131 | simplbi 501 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (ℂ
↑pm ℝ) → 𝐹:dom 𝐹⟶ℂ) |
133 | 128, 132 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐹:dom 𝐹⟶ℂ) |
134 | 131 | simprbi 500 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (ℂ
↑pm ℝ) → dom 𝐹 ⊆ ℝ) |
135 | 128, 134 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom 𝐹 ⊆ ℝ) |
136 | | iccssre 13017 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥[,]𝑦) ⊆ ℝ) |
137 | 93, 92, 136 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥[,]𝑦) ⊆ ℝ) |
138 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
139 | 138 | tgioo2 23700 |
. . . . . . . . . . . . . . . . . 18
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
140 | 138, 139 | dvres 24808 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:dom 𝐹⟶ℂ) ∧ (dom 𝐹 ⊆ ℝ ∧ (𝑥[,]𝑦) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑥[,]𝑦)))) |
141 | 126, 133,
135, 137, 140 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑥[,]𝑦)))) |
142 | | iccntr 23718 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦)) = (𝑥(,)𝑦)) |
143 | 93, 92, 142 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((int‘(topGen‘ran
(,)))‘(𝑥[,]𝑦)) = (𝑥(,)𝑦)) |
144 | 143 | reseq2d 5851 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ (𝑥(,)𝑦))) |
145 | 141, 144 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ (𝑥(,)𝑦))) |
146 | 145 | dmeqd 5774 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦))) |
147 | | ioossicc 13021 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥(,)𝑦) ⊆ (𝑥[,]𝑦) |
148 | 147, 120 | sstrid 3912 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥(,)𝑦) ⊆ (𝐴[,]𝐵)) |
149 | 17 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) |
150 | 148, 149 | sstrd 3911 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥(,)𝑦) ⊆ dom (ℝ D 𝐹)) |
151 | | ssdmres 5874 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥(,)𝑦) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)) = (𝑥(,)𝑦)) |
152 | 150, 151 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)) = (𝑥(,)𝑦)) |
153 | 146, 152 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = (𝑥(,)𝑦)) |
154 | 93, 92, 96, 125, 153 | mvth 24889 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ∃𝑎 ∈ (𝑥(,)𝑦)((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥))) |
155 | 145 | fveq1d 6719 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎)) |
156 | 155 | adantrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎)) |
157 | | fvres 6736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ (𝑥(,)𝑦) → (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎) = ((ℝ D 𝐹)‘𝑎)) |
158 | 157 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎) = ((ℝ D 𝐹)‘𝑎)) |
159 | 156, 158 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((ℝ D 𝐹)‘𝑎)) |
160 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → Fun (ℝ D 𝐹)) |
161 | 17 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) |
162 | 148 | sseld 3900 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑎 ∈ (𝑥(,)𝑦) → 𝑎 ∈ (𝐴[,]𝐵))) |
163 | 162 | impr 458 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → 𝑎 ∈ (𝐴[,]𝐵)) |
164 | | funfvima2 7047 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
(ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) → (𝑎 ∈ (𝐴[,]𝐵) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
165 | 164 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((Fun
(ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) ∧ 𝑎 ∈ (𝐴[,]𝐵)) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
166 | 160, 161,
163, 165 | syl21anc 838 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
167 | 159, 166 | eqeltrd 2838 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
168 | | eleq1 2825 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ D (𝐹
↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) ↔ ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
169 | 167, 168 | syl5ibcom 248 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
170 | 169 | expr 460 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑎 ∈ (𝑥(,)𝑦) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))) |
171 | 170 | rexlimdv 3202 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (∃𝑎 ∈ (𝑥(,)𝑦)((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
172 | 154, 171 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
173 | 118, 172 | eqeltrrd 2839 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
174 | | funfvima 7046 |
. . . . . . . . . . 11
⊢ ((Fun abs
∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs) → ((((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))) |
175 | 174 | imp 410 |
. . . . . . . . . 10
⊢ (((Fun
abs ∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs) ∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
176 | 105, 107,
173, 175 | syl21anc 838 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
177 | 102, 103,
104, 176 | suprubd 11794 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ≤ sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < )) |
178 | 177, 1 | breqtrrdi 5095 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ≤ 𝐾) |
179 | 101, 178 | eqbrtrrd 5077 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥))) ≤ 𝐾) |
180 | 88 | abscld 15000 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ∈ ℝ) |
181 | 73 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐾 ∈ ℝ) |
182 | 95, 100 | absrpcld 15012 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(𝑦 − 𝑥)) ∈
ℝ+) |
183 | 180, 181,
182 | ledivmuld 12681 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥))) ≤ 𝐾 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ ((abs‘(𝑦 − 𝑥)) · 𝐾))) |
184 | 179, 183 | mpbid 235 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ ((abs‘(𝑦 − 𝑥)) · 𝐾)) |
185 | 182 | rpcnd 12630 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(𝑦 − 𝑥)) ∈ ℂ) |
186 | 181 | recnd 10861 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐾 ∈ ℂ) |
187 | 185, 186 | mulcomd 10854 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((abs‘(𝑦 − 𝑥)) · 𝐾) = (𝐾 · (abs‘(𝑦 − 𝑥)))) |
188 | 184, 187 | breqtrd 5079 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥)))) |
189 | 188 | ex 416 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))) |
190 | 189 | ralrimivva 3112 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))) |
191 | 73, 190 | jca 515 |
1
⊢ (𝜑 → (𝐾 ∈ ℝ ∧ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥)))))) |