Step | Hyp | Ref
| Expression |
1 | | mvth.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | mvth.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | mvth.lt |
. . 3
⊢ (𝜑 → 𝐴 < 𝐵) |
4 | | mvth.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
5 | | mptresid 5712 |
. . . 4
⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧) = ( I ↾ (𝐴[,]𝐵)) |
6 | | iccssre 12567 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
7 | 1, 2, 6 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
8 | | ax-resscn 10329 |
. . . . 5
⊢ ℝ
⊆ ℂ |
9 | | cncfmptid 23123 |
. . . . 5
⊢ (((𝐴[,]𝐵) ⊆ ℝ ∧ ℝ ⊆
ℂ) → (𝑧 ∈
(𝐴[,]𝐵) ↦ 𝑧) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
10 | 7, 8, 9 | sylancl 580 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
11 | 5, 10 | syl5eqelr 2864 |
. . 3
⊢ (𝜑 → ( I ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
12 | | mvth.d |
. . 3
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
13 | 5 | oveq2i 6933 |
. . . . . 6
⊢ (ℝ
D (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧)) = (ℝ D ( I ↾ (𝐴[,]𝐵))) |
14 | | reelprrecn 10364 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
15 | 14 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
16 | | simpr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ) |
17 | 16 | recnd 10405 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℂ) |
18 | | 1red 10377 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 1 ∈
ℝ) |
19 | 15 | dvmptid 24157 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑧 ∈ ℝ ↦ 𝑧)) = (𝑧 ∈ ℝ ↦ 1)) |
20 | | eqid 2778 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
21 | 20 | tgioo2 23014 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
22 | | iccntr 23032 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
23 | 1, 2, 22 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
24 | 15, 17, 18, 19, 7, 21, 20, 23 | dvmptres2 24162 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧)) = (𝑧 ∈ (𝐴(,)𝐵) ↦ 1)) |
25 | 13, 24 | syl5eqr 2828 |
. . . . 5
⊢ (𝜑 → (ℝ D ( I ↾
(𝐴[,]𝐵))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ 1)) |
26 | 25 | dmeqd 5571 |
. . . 4
⊢ (𝜑 → dom (ℝ D ( I ↾
(𝐴[,]𝐵))) = dom (𝑧 ∈ (𝐴(,)𝐵) ↦ 1)) |
27 | | 1ex 10372 |
. . . . 5
⊢ 1 ∈
V |
28 | | eqid 2778 |
. . . . 5
⊢ (𝑧 ∈ (𝐴(,)𝐵) ↦ 1) = (𝑧 ∈ (𝐴(,)𝐵) ↦ 1) |
29 | 27, 28 | dmmpti 6269 |
. . . 4
⊢ dom
(𝑧 ∈ (𝐴(,)𝐵) ↦ 1) = (𝐴(,)𝐵) |
30 | 26, 29 | syl6eq 2830 |
. . 3
⊢ (𝜑 → dom (ℝ D ( I ↾
(𝐴[,]𝐵))) = (𝐴(,)𝐵)) |
31 | 1, 2, 3, 4, 11, 12, 30 | cmvth 24191 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) |
32 | 1 | rexrd 10426 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
33 | 2 | rexrd 10426 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
34 | 1, 2, 3 | ltled 10524 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
35 | | ubicc2 12603 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
36 | 32, 33, 34, 35 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
37 | | fvresi 6706 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (𝐴[,]𝐵) → (( I ↾ (𝐴[,]𝐵))‘𝐵) = 𝐵) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (( I ↾ (𝐴[,]𝐵))‘𝐵) = 𝐵) |
39 | | lbicc2 12602 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
40 | 32, 33, 34, 39 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
41 | | fvresi 6706 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝐴[,]𝐵) → (( I ↾ (𝐴[,]𝐵))‘𝐴) = 𝐴) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (( I ↾ (𝐴[,]𝐵))‘𝐴) = 𝐴) |
43 | 38, 42 | oveq12d 6940 |
. . . . . . . 8
⊢ (𝜑 → ((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) = (𝐵 − 𝐴)) |
44 | 43 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) = (𝐵 − 𝐴)) |
45 | 44 | oveq1d 6937 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) = ((𝐵 − 𝐴) · ((ℝ D 𝐹)‘𝑥))) |
46 | 25 | fveq1d 6448 |
. . . . . . . . 9
⊢ (𝜑 → ((ℝ D ( I ↾
(𝐴[,]𝐵)))‘𝑥) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ 1)‘𝑥)) |
47 | | eqidd 2779 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → 1 = 1) |
48 | 47, 28, 27 | fvmpt3i 6547 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ 1)‘𝑥) = 1) |
49 | 46, 48 | sylan9eq 2834 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥) = 1) |
50 | 49 | oveq2d 6938 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · 1)) |
51 | | cncff 23104 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
52 | 4, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
53 | 52, 36 | ffvelrnd 6624 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
54 | 52, 40 | ffvelrnd 6624 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
55 | 53, 54 | resubcld 10803 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ) |
56 | 55 | recnd 10405 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ) |
57 | 56 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ) |
58 | 57 | mulid1d 10394 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · 1) = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
59 | 50, 58 | eqtrd 2814 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
60 | 45, 59 | eqeq12d 2793 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) ↔ ((𝐵 − 𝐴) · ((ℝ D 𝐹)‘𝑥)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))) |
61 | 2, 1 | resubcld 10803 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
62 | 61 | recnd 10405 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
63 | 62 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐵 − 𝐴) ∈ ℂ) |
64 | | dvf 24108 |
. . . . . . . 8
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
65 | 12 | feq2d 6277 |
. . . . . . . 8
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℂ)) |
66 | 64, 65 | mpbii 225 |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
67 | 66 | ffvelrnda 6623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
68 | 1, 2 | posdifd 10962 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
69 | 3, 68 | mpbid 224 |
. . . . . . . 8
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
70 | 69 | gt0ne0d 10939 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) |
71 | 70 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐵 − 𝐴) ≠ 0) |
72 | 57, 63, 67, 71 | divmuld 11173 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)) = ((ℝ D 𝐹)‘𝑥) ↔ ((𝐵 − 𝐴) · ((ℝ D 𝐹)‘𝑥)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))) |
73 | 60, 72 | bitr4d 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) ↔ (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)) = ((ℝ D 𝐹)‘𝑥))) |
74 | | eqcom 2785 |
. . . 4
⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) ↔ (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥))) |
75 | | eqcom 2785 |
. . . 4
⊢
(((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)) ↔ (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)) = ((ℝ D 𝐹)‘𝑥)) |
76 | 73, 74, 75 | 3bitr4g 306 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) ↔ ((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)))) |
77 | 76 | rexbidva 3234 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)))) |
78 | 31, 77 | mpbid 224 |
1
⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴))) |