| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mvth.a | . . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 2 |  | mvth.b | . . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 3 |  | mvth.lt | . . 3
⊢ (𝜑 → 𝐴 < 𝐵) | 
| 4 |  | mvth.f | . . 3
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) | 
| 5 |  | mptresid 6069 | . . . 4
⊢ ( I
↾ (𝐴[,]𝐵)) = (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧) | 
| 6 |  | iccssre 13469 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 7 | 1, 2, 6 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | 
| 8 |  | ax-resscn 11212 | . . . . 5
⊢ ℝ
⊆ ℂ | 
| 9 |  | cncfmptid 24939 | . . . . 5
⊢ (((𝐴[,]𝐵) ⊆ ℝ ∧ ℝ ⊆
ℂ) → (𝑧 ∈
(𝐴[,]𝐵) ↦ 𝑧) ∈ ((𝐴[,]𝐵)–cn→ℝ)) | 
| 10 | 7, 8, 9 | sylancl 586 | . . . 4
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧) ∈ ((𝐴[,]𝐵)–cn→ℝ)) | 
| 11 | 5, 10 | eqeltrid 2845 | . . 3
⊢ (𝜑 → ( I ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) | 
| 12 |  | mvth.d | . . 3
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) | 
| 13 | 5 | eqcomi 2746 | . . . . . . 7
⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧) = ( I ↾ (𝐴[,]𝐵)) | 
| 14 | 13 | oveq2i 7442 | . . . . . 6
⊢ (ℝ
D (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧)) = (ℝ D ( I ↾ (𝐴[,]𝐵))) | 
| 15 |  | reelprrecn 11247 | . . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} | 
| 16 | 15 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) | 
| 17 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ) | 
| 18 | 17 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℂ) | 
| 19 |  | 1red 11262 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 1 ∈
ℝ) | 
| 20 | 16 | dvmptid 25995 | . . . . . . 7
⊢ (𝜑 → (ℝ D (𝑧 ∈ ℝ ↦ 𝑧)) = (𝑧 ∈ ℝ ↦ 1)) | 
| 21 |  | tgioo4 24826 | . . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 22 |  | eqid 2737 | . . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 23 |  | iccntr 24843 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | 
| 24 | 1, 2, 23 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | 
| 25 | 16, 18, 19, 20, 7, 21, 22, 24 | dvmptres2 26000 | . . . . . 6
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ 𝑧)) = (𝑧 ∈ (𝐴(,)𝐵) ↦ 1)) | 
| 26 | 14, 25 | eqtr3id 2791 | . . . . 5
⊢ (𝜑 → (ℝ D ( I ↾
(𝐴[,]𝐵))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ 1)) | 
| 27 | 26 | dmeqd 5916 | . . . 4
⊢ (𝜑 → dom (ℝ D ( I ↾
(𝐴[,]𝐵))) = dom (𝑧 ∈ (𝐴(,)𝐵) ↦ 1)) | 
| 28 |  | 1ex 11257 | . . . . 5
⊢ 1 ∈
V | 
| 29 |  | eqid 2737 | . . . . 5
⊢ (𝑧 ∈ (𝐴(,)𝐵) ↦ 1) = (𝑧 ∈ (𝐴(,)𝐵) ↦ 1) | 
| 30 | 28, 29 | dmmpti 6712 | . . . 4
⊢ dom
(𝑧 ∈ (𝐴(,)𝐵) ↦ 1) = (𝐴(,)𝐵) | 
| 31 | 27, 30 | eqtrdi 2793 | . . 3
⊢ (𝜑 → dom (ℝ D ( I ↾
(𝐴[,]𝐵))) = (𝐴(,)𝐵)) | 
| 32 | 1, 2, 3, 4, 11, 12, 31 | cmvth 26029 | . 2
⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) | 
| 33 | 1 | rexrd 11311 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 34 | 2 | rexrd 11311 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 35 | 1, 2, 3 | ltled 11409 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ 𝐵) | 
| 36 |  | ubicc2 13505 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) | 
| 37 | 33, 34, 35, 36 | syl3anc 1373 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) | 
| 38 |  | fvresi 7193 | . . . . . . . . . 10
⊢ (𝐵 ∈ (𝐴[,]𝐵) → (( I ↾ (𝐴[,]𝐵))‘𝐵) = 𝐵) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (( I ↾ (𝐴[,]𝐵))‘𝐵) = 𝐵) | 
| 40 |  | lbicc2 13504 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 41 | 33, 34, 35, 40 | syl3anc 1373 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 42 |  | fvresi 7193 | . . . . . . . . . 10
⊢ (𝐴 ∈ (𝐴[,]𝐵) → (( I ↾ (𝐴[,]𝐵))‘𝐴) = 𝐴) | 
| 43 | 41, 42 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (( I ↾ (𝐴[,]𝐵))‘𝐴) = 𝐴) | 
| 44 | 39, 43 | oveq12d 7449 | . . . . . . . 8
⊢ (𝜑 → ((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) = (𝐵 − 𝐴)) | 
| 45 | 44 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) = (𝐵 − 𝐴)) | 
| 46 | 45 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) = ((𝐵 − 𝐴) · ((ℝ D 𝐹)‘𝑥))) | 
| 47 | 26 | fveq1d 6908 | . . . . . . . . 9
⊢ (𝜑 → ((ℝ D ( I ↾
(𝐴[,]𝐵)))‘𝑥) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ 1)‘𝑥)) | 
| 48 |  | eqidd 2738 | . . . . . . . . . 10
⊢ (𝑧 = 𝑥 → 1 = 1) | 
| 49 | 48, 29, 28 | fvmpt3i 7021 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ 1)‘𝑥) = 1) | 
| 50 | 47, 49 | sylan9eq 2797 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥) = 1) | 
| 51 | 50 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · 1)) | 
| 52 |  | cncff 24919 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ) | 
| 53 | 4, 52 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) | 
| 54 | 53, 37 | ffvelcdmd 7105 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) | 
| 55 | 53, 41 | ffvelcdmd 7105 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) | 
| 56 | 54, 55 | resubcld 11691 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ) | 
| 57 | 56 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ) | 
| 58 | 57 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ) | 
| 59 | 58 | mulridd 11278 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · 1) = ((𝐹‘𝐵) − (𝐹‘𝐴))) | 
| 60 | 51, 59 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) | 
| 61 | 46, 60 | eqeq12d 2753 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) ↔ ((𝐵 − 𝐴) · ((ℝ D 𝐹)‘𝑥)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))) | 
| 62 | 2, 1 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) | 
| 63 | 62 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) | 
| 64 | 63 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐵 − 𝐴) ∈ ℂ) | 
| 65 |  | dvf 25942 | . . . . . . . 8
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ | 
| 66 | 12 | feq2d 6722 | . . . . . . . 8
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℂ)) | 
| 67 | 65, 66 | mpbii 233 | . . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) | 
| 68 | 67 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) | 
| 69 | 1, 2 | posdifd 11850 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) | 
| 70 | 3, 69 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) | 
| 71 | 70 | gt0ne0d 11827 | . . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) | 
| 72 | 71 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐵 − 𝐴) ≠ 0) | 
| 73 | 58, 64, 68, 72 | divmuld 12065 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)) = ((ℝ D 𝐹)‘𝑥) ↔ ((𝐵 − 𝐴) · ((ℝ D 𝐹)‘𝑥)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))) | 
| 74 | 61, 73 | bitr4d 282 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) ↔ (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)) = ((ℝ D 𝐹)‘𝑥))) | 
| 75 |  | eqcom 2744 | . . . 4
⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) ↔ (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥))) | 
| 76 |  | eqcom 2744 | . . . 4
⊢
(((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)) ↔ (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)) = ((ℝ D 𝐹)‘𝑥)) | 
| 77 | 74, 75, 76 | 3bitr4g 314 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) ↔ ((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)))) | 
| 78 | 77 | rexbidva 3177 | . 2
⊢ (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D ( I ↾ (𝐴[,]𝐵)))‘𝑥)) = (((( I ↾ (𝐴[,]𝐵))‘𝐵) − (( I ↾ (𝐴[,]𝐵))‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴)))) | 
| 79 | 32, 78 | mpbid 232 | 1
⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = (((𝐹‘𝐵) − (𝐹‘𝐴)) / (𝐵 − 𝐴))) |