Step | Hyp | Ref
| Expression |
1 | | c1liplem1.k |
. . 3
⊢ 𝐾 = sup((abs “ ((ℝ D
𝐹) “ (𝐴[,]𝐵))), ℝ, < ) |
2 | | imassrn 5396 |
. . . . . 6
⊢ (abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵))) ⊆ ran
abs |
3 | | absf 13925 |
. . . . . . 7
⊢
abs:ℂ⟶ℝ |
4 | | frn 5966 |
. . . . . . 7
⊢
(abs:ℂ⟶ℝ → ran abs ⊆
ℝ) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢ ran abs
⊆ ℝ |
6 | 2, 5 | sstri 3577 |
. . . . 5
⊢ (abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵))) ⊆
ℝ |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝜑 → (abs “ ((ℝ D
𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ) |
8 | | dvf 23477 |
. . . . . . . 8
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
9 | | ffun 5961 |
. . . . . . . 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 22504 |
. . . . . . . 8
⊢
(((ℝ D 𝐹)
↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ) |
14 | | fdm 5964 |
. . . . . . . 8
⊢
(((ℝ D 𝐹)
↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ → dom ((ℝ D
𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵)) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵)) |
16 | | ssdmres 5340 |
. . . . . . 7
⊢ ((𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) = (𝐴[,]𝐵)) |
17 | 15, 16 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) |
18 | | c1liplem1.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
19 | 18 | rexrd 9968 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
20 | | c1liplem1.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
21 | 20 | rexrd 9968 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
22 | | c1liplem1.le |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
23 | | lbicc2 12159 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
24 | 19, 21, 22, 23 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
25 | | funfvima2 6397 |
. . . . . . 7
⊢ ((Fun
(ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) → (𝐴 ∈ (𝐴[,]𝐵) → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
26 | 25 | imp 444 |
. . . . . 6
⊢ (((Fun
(ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) ∧ 𝐴 ∈ (𝐴[,]𝐵)) → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
27 | 11, 17, 24, 26 | syl21anc 1317 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
28 | | ffun 5961 |
. . . . . . 7
⊢
(abs:ℂ⟶ℝ → Fun abs) |
29 | 3, 28 | ax-mp 5 |
. . . . . 6
⊢ Fun
abs |
30 | | imassrn 5396 |
. . . . . . . 8
⊢ ((ℝ
D 𝐹) “ (𝐴[,]𝐵)) ⊆ ran (ℝ D 𝐹) |
31 | | frn 5966 |
. . . . . . . . 9
⊢ ((ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ → ran
(ℝ D 𝐹) ⊆
ℂ) |
32 | 8, 31 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(ℝ D 𝐹) ⊆
ℂ |
33 | 30, 32 | sstri 3577 |
. . . . . . 7
⊢ ((ℝ
D 𝐹) “ (𝐴[,]𝐵)) ⊆ ℂ |
34 | 3 | fdmi 5965 |
. . . . . . 7
⊢ dom abs =
ℂ |
35 | 33, 34 | sseqtr4i 3601 |
. . . . . 6
⊢ ((ℝ
D 𝐹) “ (𝐴[,]𝐵)) ⊆ dom abs |
36 | | funfvima2 6397 |
. . . . . 6
⊢ ((Fun abs
∧ ((ℝ D 𝐹)
“ (𝐴[,]𝐵)) ⊆ dom abs) →
(((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))) |
37 | 29, 35, 36 | mp2an 704 |
. . . . 5
⊢
(((ℝ D 𝐹)‘𝐴) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
38 | | ne0i 3880 |
. . . . 5
⊢
((abs‘((ℝ D 𝐹)‘𝐴)) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅) |
39 | 27, 37, 38 | 3syl 18 |
. . . 4
⊢ (𝜑 → (abs “ ((ℝ D
𝐹) “ (𝐴[,]𝐵))) ≠ ∅) |
40 | | ax-resscn 9872 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
41 | | ssid 3587 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
42 | | cncfss 22510 |
. . . . . . . 8
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ)) |
43 | 40, 41, 42 | mp2an 704 |
. . . . . . 7
⊢ ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ) |
44 | 43, 12 | sseldi 3566 |
. . . . . 6
⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
45 | | cniccbdd 23037 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ((ℝ
D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) |
46 | 18, 20, 44, 45 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) |
47 | | fvelima 6158 |
. . . . . . . . . 10
⊢ ((Fun abs
∧ 𝑏 ∈ (abs “
((ℝ D 𝐹) “
(𝐴[,]𝐵)))) → ∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏) |
48 | 29, 47 | mpan 702 |
. . . . . . . . 9
⊢ (𝑏 ∈ (abs “ ((ℝ D
𝐹) “ (𝐴[,]𝐵))) → ∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏) |
49 | | fvelima 6158 |
. . . . . . . . . . . . . 14
⊢ ((Fun
(ℝ D 𝐹) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → ∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦) |
50 | 10, 49 | mpan 702 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → ∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦) |
51 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ (𝐴[,]𝐵) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏) = ((ℝ D 𝐹)‘𝑏)) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑥 ∈
(𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏) = ((ℝ D 𝐹)‘𝑏)) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
(𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) = (abs‘((ℝ D 𝐹)‘𝑏))) |
54 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑏 → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥) = (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) |
55 | 54 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑏 → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) = (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏))) |
56 | 55 | breq1d 4593 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑏 → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ↔ (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) ≤ 𝑎)) |
57 | 56 | rspccva 3281 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
(𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑏)) ≤ 𝑎) |
58 | 53, 57 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
(𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎) |
59 | 58 | adantll 746 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎) |
60 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢
(((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘((ℝ D 𝐹)‘𝑏)) = (abs‘𝑦)) |
61 | 60 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ D 𝐹)‘𝑏) = 𝑦 → ((abs‘((ℝ D 𝐹)‘𝑏)) ≤ 𝑎 ↔ (abs‘𝑦) ≤ 𝑎)) |
62 | 59, 61 | syl5ibcom 234 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘𝑦) ≤ 𝑎)) |
63 | 62 | rexlimdva 3013 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (∃𝑏 ∈ (𝐴[,]𝐵)((ℝ D 𝐹)‘𝑏) = 𝑦 → (abs‘𝑦) ≤ 𝑎)) |
64 | 50, 63 | syl5 33 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘𝑦) ≤ 𝑎)) |
65 | 64 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs‘𝑦) ≤ 𝑎) |
66 | | breq1 4586 |
. . . . . . . . . . 11
⊢
((abs‘𝑦) =
𝑏 → ((abs‘𝑦) ≤ 𝑎 ↔ 𝑏 ≤ 𝑎)) |
67 | 65, 66 | syl5ibcom 234 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) ∧ 𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → ((abs‘𝑦) = 𝑏 → 𝑏 ≤ 𝑎)) |
68 | 67 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (∃𝑦 ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))(abs‘𝑦) = 𝑏 → 𝑏 ≤ 𝑎)) |
69 | 48, 68 | syl5 33 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → (𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → 𝑏 ≤ 𝑎)) |
70 | 69 | ralrimiv 2948 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎) → ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) |
71 | 70 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 → ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎)) |
72 | 71 | reximdva 3000 |
. . . . 5
⊢ (𝜑 → (∃𝑎 ∈ ℝ ∀𝑥 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑥)) ≤ 𝑎 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎)) |
73 | 46, 72 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) |
74 | | suprcl 10862 |
. . . 4
⊢ (((abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵))) ⊆ ℝ ∧ (abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵))) ≠ ∅ ∧
∃𝑎 ∈ ℝ
∀𝑏 ∈ (abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) → sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ) ∈
ℝ) |
75 | 7, 39, 73, 74 | syl3anc 1318 |
. . 3
⊢ (𝜑 → sup((abs “ ((ℝ
D 𝐹) “ (𝐴[,]𝐵))), ℝ, < ) ∈
ℝ) |
76 | 1, 75 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝐾 ∈ ℝ) |
77 | | simplrr 797 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (𝐴[,]𝐵)) |
78 | | fvres 6117 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) = (𝐹‘𝑦)) |
79 | 77, 78 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) = (𝐹‘𝑦)) |
80 | | c1liplem1.cn |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
81 | | cncff 22504 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ) |
83 | 82 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝐴[,]𝐵)):(𝐴[,]𝐵)⟶ℝ) |
84 | 83, 77 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) ∈ ℝ) |
85 | 84 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑦) ∈ ℂ) |
86 | 79, 85 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑦) ∈ ℂ) |
87 | | simplrl 796 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (𝐴[,]𝐵)) |
88 | | fvres 6117 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) = (𝐹‘𝑥)) |
89 | 87, 88 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) = (𝐹‘𝑥)) |
90 | 83, 87 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) ∈ ℝ) |
91 | 90 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝑥) ∈ ℂ) |
92 | 89, 91 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹‘𝑥) ∈ ℂ) |
93 | 86, 92 | subcld 10271 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹‘𝑦) − (𝐹‘𝑥)) ∈ ℂ) |
94 | | iccssre 12126 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
95 | 18, 20, 94 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
96 | 95 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐴[,]𝐵) ⊆ ℝ) |
97 | 96, 77 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ) |
98 | 96, 87 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ) |
99 | 97, 98 | resubcld 10337 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈ ℝ) |
100 | 99 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈ ℂ) |
101 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦) |
102 | | difrp 11744 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈
ℝ+)) |
103 | 98, 97, 102 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈
ℝ+)) |
104 | 101, 103 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ∈
ℝ+) |
105 | 104 | rpne0d 11753 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑦 − 𝑥) ≠ 0) |
106 | 93, 100, 105 | absdivd 14042 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) = ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥)))) |
107 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ⊆ ℝ) |
108 | 39 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) ≠ ∅) |
109 | 73 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ∃𝑎 ∈ ℝ ∀𝑏 ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) |
110 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → Fun abs) |
111 | 93, 100, 105 | divcld 10680 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ℂ) |
112 | 111, 34 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs) |
113 | 98 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ ℝ*) |
114 | 97 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ ℝ*) |
115 | 98, 97, 101 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ≤ 𝑦) |
116 | | ubicc2 12160 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑥
≤ 𝑦) → 𝑦 ∈ (𝑥[,]𝑦)) |
117 | 113, 114,
115, 116 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (𝑥[,]𝑦)) |
118 | | fvres 6117 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝑥[,]𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) = (𝐹‘𝑦)) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) = (𝐹‘𝑦)) |
120 | | lbicc2 12159 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ 𝑥
≤ 𝑦) → 𝑥 ∈ (𝑥[,]𝑦)) |
121 | 113, 114,
115, 120 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (𝑥[,]𝑦)) |
122 | | fvres 6117 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑥[,]𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥) = (𝐹‘𝑥)) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥) = (𝐹‘𝑥)) |
124 | 119, 123 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) = ((𝐹‘𝑦) − (𝐹‘𝑥))) |
125 | 124 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) = (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) |
126 | | iccss2 12115 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥[,]𝑦) ⊆ (𝐴[,]𝐵)) |
127 | 126 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥[,]𝑦) ⊆ (𝐴[,]𝐵)) |
128 | 127 | resabs1d 5348 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) = (𝐹 ↾ (𝑥[,]𝑦))) |
129 | 80 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
130 | | rescncf 22508 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥[,]𝑦) ⊆ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ))) |
131 | 127, 129,
130 | sylc 63 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((𝐹 ↾ (𝐴[,]𝐵)) ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ)) |
132 | 128, 131 | eqeltrrd 2689 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐹 ↾ (𝑥[,]𝑦)) ∈ ((𝑥[,]𝑦)–cn→ℝ)) |
133 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ℝ ⊆
ℂ) |
134 | | c1liplem1.f |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
135 | 134 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
136 | | cnex 9896 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℂ
∈ V |
137 | | reex 9906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℝ
∈ V |
138 | 136, 137 | elpm2 7775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 ∈ (ℂ
↑pm ℝ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
139 | 138 | simplbi 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (ℂ
↑pm ℝ) → 𝐹:dom 𝐹⟶ℂ) |
140 | 135, 139 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐹:dom 𝐹⟶ℂ) |
141 | 138 | simprbi 479 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (ℂ
↑pm ℝ) → dom 𝐹 ⊆ ℝ) |
142 | 135, 141 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom 𝐹 ⊆ ℝ) |
143 | | iccssre 12126 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥[,]𝑦) ⊆ ℝ) |
144 | 98, 97, 143 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥[,]𝑦) ⊆ ℝ) |
145 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
146 | 145 | tgioo2 22414 |
. . . . . . . . . . . . . . . . . 18
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
147 | 145, 146 | dvres 23481 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:dom 𝐹⟶ℂ) ∧ (dom 𝐹 ⊆ ℝ ∧ (𝑥[,]𝑦) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑥[,]𝑦)))) |
148 | 133, 140,
142, 144, 147 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑥[,]𝑦)))) |
149 | | iccntr 22432 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑥[,]𝑦)) = (𝑥(,)𝑦)) |
150 | 98, 97, 149 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((int‘(topGen‘ran
(,)))‘(𝑥[,]𝑦)) = (𝑥(,)𝑦)) |
151 | 150 | reseq2d 5317 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ (𝑥(,)𝑦))) |
152 | 148, 151 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = ((ℝ D 𝐹) ↾ (𝑥(,)𝑦))) |
153 | 152 | dmeqd 5248 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦))) |
154 | | ioossicc 12130 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥(,)𝑦) ⊆ (𝑥[,]𝑦) |
155 | 154, 127 | syl5ss 3579 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥(,)𝑦) ⊆ (𝐴[,]𝐵)) |
156 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) |
157 | 155, 156 | sstrd 3578 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑥(,)𝑦) ⊆ dom (ℝ D 𝐹)) |
158 | | ssdmres 5340 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥(,)𝑦) ⊆ dom (ℝ D 𝐹) ↔ dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)) = (𝑥(,)𝑦)) |
159 | 157, 158 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom ((ℝ D 𝐹) ↾ (𝑥(,)𝑦)) = (𝑥(,)𝑦)) |
160 | 153, 159 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → dom (ℝ D (𝐹 ↾ (𝑥[,]𝑦))) = (𝑥(,)𝑦)) |
161 | 98, 97, 101, 132, 160 | mvth 23559 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ∃𝑎 ∈ (𝑥(,)𝑦)((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥))) |
162 | 152 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎)) |
163 | 162 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎)) |
164 | | fvres 6117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ (𝑥(,)𝑦) → (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎) = ((ℝ D 𝐹)‘𝑎)) |
165 | 164 | ad2antll 761 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (((ℝ D 𝐹) ↾ (𝑥(,)𝑦))‘𝑎) = ((ℝ D 𝐹)‘𝑎)) |
166 | 163, 165 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((ℝ D 𝐹)‘𝑎)) |
167 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → Fun (ℝ D 𝐹)) |
168 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) |
169 | 155 | sseld 3567 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑎 ∈ (𝑥(,)𝑦) → 𝑎 ∈ (𝐴[,]𝐵))) |
170 | 169 | impr 647 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → 𝑎 ∈ (𝐴[,]𝐵)) |
171 | | funfvima2 6397 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
(ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) → (𝑎 ∈ (𝐴[,]𝐵) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
172 | 171 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ (((Fun
(ℝ D 𝐹) ∧ (𝐴[,]𝐵) ⊆ dom (ℝ D 𝐹)) ∧ 𝑎 ∈ (𝐴[,]𝐵)) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
173 | 167, 168,
170, 172 | syl21anc 1317 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D 𝐹)‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
174 | 166, 173 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → ((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
175 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ D (𝐹
↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) ↔ ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
176 | 174, 175 | syl5ibcom 234 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ (𝑥 < 𝑦 ∧ 𝑎 ∈ (𝑥(,)𝑦))) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
177 | 176 | expr 641 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (𝑎 ∈ (𝑥(,)𝑦) → (((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))) |
178 | 177 | rexlimdv 3012 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (∃𝑎 ∈ (𝑥(,)𝑦)((ℝ D (𝐹 ↾ (𝑥[,]𝑦)))‘𝑎) = ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
179 | 161, 178 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((((𝐹 ↾ (𝑥[,]𝑦))‘𝑦) − ((𝐹 ↾ (𝑥[,]𝑦))‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
180 | 125, 179 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) |
181 | | funfvima 6396 |
. . . . . . . . . . 11
⊢ ((Fun abs
∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs) → ((((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵)) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))))) |
182 | 181 | imp 444 |
. . . . . . . . . 10
⊢ (((Fun
abs ∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ dom abs) ∧ (((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥)) ∈ ((ℝ D 𝐹) “ (𝐴[,]𝐵))) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
183 | 110, 112,
180, 182 | syl21anc 1317 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) |
184 | | suprub 10863 |
. . . . . . . . 9
⊢ ((((abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵))) ⊆ ℝ ∧ (abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵))) ≠ ∅ ∧
∃𝑎 ∈ ℝ
∀𝑏 ∈ (abs
“ ((ℝ D 𝐹)
“ (𝐴[,]𝐵)))𝑏 ≤ 𝑎) ∧ (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ∈ (abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵)))) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ≤ sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < )) |
185 | 107, 108,
109, 183, 184 | syl31anc 1321 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ≤ sup((abs “ ((ℝ D 𝐹) “ (𝐴[,]𝐵))), ℝ, < )) |
186 | 185, 1 | syl6breqr 4625 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(((𝐹‘𝑦) − (𝐹‘𝑥)) / (𝑦 − 𝑥))) ≤ 𝐾) |
187 | 106, 186 | eqbrtrrd 4607 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥))) ≤ 𝐾) |
188 | 93 | abscld 14023 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ∈ ℝ) |
189 | 76 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐾 ∈ ℝ) |
190 | 100, 105 | absrpcld 14035 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(𝑦 − 𝑥)) ∈
ℝ+) |
191 | 188, 189,
190 | ledivmuld 11801 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) / (abs‘(𝑦 − 𝑥))) ≤ 𝐾 ↔ (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ ((abs‘(𝑦 − 𝑥)) · 𝐾))) |
192 | 187, 191 | mpbid 221 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ ((abs‘(𝑦 − 𝑥)) · 𝐾)) |
193 | 190 | rpcnd 11750 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘(𝑦 − 𝑥)) ∈ ℂ) |
194 | 189 | recnd 9947 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → 𝐾 ∈ ℂ) |
195 | 193, 194 | mulcomd 9940 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → ((abs‘(𝑦 − 𝑥)) · 𝐾) = (𝐾 · (abs‘(𝑦 − 𝑥)))) |
196 | 192, 195 | breqtrd 4609 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) ∧ 𝑥 < 𝑦) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥)))) |
197 | 196 | ex 449 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝐴[,]𝐵))) → (𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))) |
198 | 197 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥))))) |
199 | 76, 198 | jca 553 |
1
⊢ (𝜑 → (𝐾 ∈ ℝ ∧ ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝐾 · (abs‘(𝑦 − 𝑥)))))) |