Step | Hyp | Ref
| Expression |
1 | | cmvth.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | cmvth.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | cmvth.lt |
. . 3
⊢ (𝜑 → 𝐴 < 𝐵) |
4 | | eqid 2610 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
5 | 4 | subcn 22477 |
. . . 4
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
6 | 4 | mulcn 22478 |
. . . . 5
⊢ ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
7 | | cmvth.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
8 | | cncff 22504 |
. . . . . . . . 9
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) |
10 | 1 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
11 | 2 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
12 | 1, 2, 3 | ltled 10064 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
13 | | ubicc2 12160 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
14 | 10, 11, 12, 13 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
15 | 9, 14 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
16 | | lbicc2 12159 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
17 | 10, 11, 12, 16 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
18 | 9, 17 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
19 | 15, 18 | resubcld 10337 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ) |
20 | | iccssre 12126 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
21 | 1, 2, 20 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
22 | | ax-resscn 9872 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
23 | 21, 22 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
24 | 22 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
25 | | cncfmptc 22522 |
. . . . . 6
⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑧 ∈
(𝐴[,]𝐵) ↦ ((𝐹‘𝐵) − (𝐹‘𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
26 | 19, 23, 24, 25 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹‘𝐵) − (𝐹‘𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
27 | | cmvth.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
28 | | cncff 22504 |
. . . . . . . 8
⊢ (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐺:(𝐴[,]𝐵)⟶ℝ) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℝ) |
30 | 29 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺‘𝑧))) |
31 | 30, 27 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺‘𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
32 | | remulcl 9900 |
. . . . 5
⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐺‘𝑧) ∈ ℝ) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) ∈ ℝ) |
33 | 4, 6, 26, 31, 22, 32 | cncfmpt2ss 22526 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
34 | 29, 14 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℝ) |
35 | 29, 17 | ffvelrnd 6268 |
. . . . . . 7
⊢ (𝜑 → (𝐺‘𝐴) ∈ ℝ) |
36 | 34, 35 | resubcld 10337 |
. . . . . 6
⊢ (𝜑 → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ) |
37 | | cncfmptc 22522 |
. . . . . 6
⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑧 ∈
(𝐴[,]𝐵) ↦ ((𝐺‘𝐵) − (𝐺‘𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
38 | 36, 23, 24, 37 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺‘𝐵) − (𝐺‘𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
39 | 9 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑧))) |
40 | 39, 7 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
41 | | remulcl 9900 |
. . . . 5
⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℝ) |
42 | 4, 6, 38, 40, 22, 41 | cncfmpt2ss 22526 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
43 | | resubcl 10224 |
. . . 4
⊢
(((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) ∈ ℝ ∧ (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℝ) → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) ∈ ℝ) |
44 | 4, 5, 33, 42, 22, 43 | cncfmpt2ss 22526 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))) ∈ ((𝐴[,]𝐵)–cn→ℝ)) |
45 | 19 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ) |
46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ) |
47 | 29 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑧) ∈ ℝ) |
48 | 47 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑧) ∈ ℂ) |
49 | 46, 48 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) ∈ ℂ) |
50 | 36 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ) |
51 | 9 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑧) ∈ ℝ) |
52 | 50, 51 | remulcld 9949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℝ) |
53 | 52 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℂ) |
54 | 49, 53 | subcld 10271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) ∈ ℂ) |
55 | 4 | tgioo2 22414 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
56 | | iccntr 22432 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
57 | 1, 2, 56 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
58 | 24, 21, 54, 55, 4, 57 | dvmptntr 23540 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))) |
59 | | reelprrecn 9907 |
. . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
61 | | ioossicc 12130 |
. . . . . . . . 9
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
62 | 61 | sseli 3564 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ (𝐴[,]𝐵)) |
63 | 62, 49 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) ∈ ℂ) |
64 | | ovex 6577 |
. . . . . . . 8
⊢ (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V |
65 | 64 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V) |
66 | 62, 48 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℂ) |
67 | | fvex 6113 |
. . . . . . . . 9
⊢ ((ℝ
D 𝐺)‘𝑧) ∈ V |
68 | 67 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ V) |
69 | 30 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺‘𝑧)))) |
70 | | dvf 23477 |
. . . . . . . . . . 11
⊢ (ℝ
D 𝐺):dom (ℝ D 𝐺)⟶ℂ |
71 | | cmvth.dg |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵)) |
72 | 71 | feq2d 5944 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ
D 𝐺):(𝐴(,)𝐵)⟶ℂ)) |
73 | 70, 72 | mpbii 222 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ) |
74 | 73 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐺) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧))) |
75 | 24, 21, 48, 55, 4, 57 | dvmptntr 23540 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺‘𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑧)))) |
76 | 69, 74, 75 | 3eqtr3rd 2653 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧))) |
77 | 60, 66, 68, 76, 45 | dvmptcmul 23533 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)))) |
78 | 62, 53 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℂ) |
79 | | ovex 6577 |
. . . . . . . 8
⊢ (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V |
80 | 79 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V) |
81 | 51 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑧) ∈ ℂ) |
82 | 62, 81 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℂ) |
83 | | fvex 6113 |
. . . . . . . . 9
⊢ ((ℝ
D 𝐹)‘𝑧) ∈ V |
84 | 83 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ V) |
85 | 39 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑧)))) |
86 | | dvf 23477 |
. . . . . . . . . . 11
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
87 | | cmvth.df |
. . . . . . . . . . . 12
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
88 | 87 | feq2d 5944 |
. . . . . . . . . . 11
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℂ)) |
89 | 86, 88 | mpbii 222 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
90 | 89 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧))) |
91 | 24, 21, 81, 55, 4, 57 | dvmptntr 23540 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑧)))) |
92 | 85, 90, 91 | 3eqtr3rd 2653 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧))) |
93 | 36 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℂ) |
94 | 60, 82, 84, 92, 93 | dvmptcmul 23533 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))) |
95 | 60, 63, 65, 77, 78, 80, 94 | dvmptsub 23536 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))) |
96 | 58, 95 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))) |
97 | 96 | dmeqd 5248 |
. . . 4
⊢ (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))) |
98 | | ovex 6577 |
. . . . 5
⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))) ∈ V |
99 | | eqid 2610 |
. . . . 5
⊢ (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))) |
100 | 98, 99 | dmmpti 5936 |
. . . 4
⊢ dom
(𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝐴(,)𝐵) |
101 | 97, 100 | syl6eq 2660 |
. . 3
⊢ (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = (𝐴(,)𝐵)) |
102 | 15 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ) |
103 | 35 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝐴) ∈ ℂ) |
104 | 102, 103 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐵) · (𝐺‘𝐴)) ∈ ℂ) |
105 | 18 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
106 | 34 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝐵) ∈ ℂ) |
107 | 105, 106 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐴) · (𝐺‘𝐵)) ∈ ℂ) |
108 | 105, 103 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐴) · (𝐺‘𝐴)) ∈ ℂ) |
109 | 104, 107,
108 | nnncan2d 10306 |
. . . . . 6
⊢ (𝜑 → ((((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐴))) − (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴)))) = (((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐵)))) |
110 | 102, 106 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐵) · (𝐺‘𝐵)) ∈ ℂ) |
111 | 110, 107,
104 | nnncan1d 10305 |
. . . . . 6
⊢ (𝜑 → ((((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐵))) − (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴)))) = (((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐵)))) |
112 | 109, 111 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → ((((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐴))) − (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴)))) = ((((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐵))) − (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴))))) |
113 | 102, 105,
103 | subdird 10366 |
. . . . . 6
⊢ (𝜑 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) = (((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐴)))) |
114 | 93, 105 | mulcomd 9940 |
. . . . . . 7
⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴)) = ((𝐹‘𝐴) · ((𝐺‘𝐵) − (𝐺‘𝐴)))) |
115 | 105, 106,
103 | subdid 10365 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐴) · ((𝐺‘𝐵) − (𝐺‘𝐴))) = (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴)))) |
116 | 114, 115 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴)) = (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴)))) |
117 | 113, 116 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴))) = ((((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐴))) − (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴))))) |
118 | 102, 105,
106 | subdird 10366 |
. . . . . 6
⊢ (𝜑 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) = (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐵)))) |
119 | 93, 102 | mulcomd 9940 |
. . . . . . 7
⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)) = ((𝐹‘𝐵) · ((𝐺‘𝐵) − (𝐺‘𝐴)))) |
120 | 102, 106,
103 | subdid 10365 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐵) · ((𝐺‘𝐵) − (𝐺‘𝐴))) = (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴)))) |
121 | 119, 120 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)) = (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴)))) |
122 | 118, 121 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵))) = ((((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐵))) − (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴))))) |
123 | 112, 117,
122 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴))) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)))) |
124 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (𝐺‘𝑧) = (𝐺‘𝐴)) |
125 | 124 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴))) |
126 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (𝐹‘𝑧) = (𝐹‘𝐴)) |
127 | 126 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴))) |
128 | 125, 127 | oveq12d 6567 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴)))) |
129 | | eqid 2610 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))) = (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))) |
130 | | ovex 6577 |
. . . . . 6
⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) ∈ V |
131 | 128, 129,
130 | fvmpt3i 6196 |
. . . . 5
⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐴) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴)))) |
132 | 17, 131 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐴) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴)))) |
133 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝐺‘𝑧) = (𝐺‘𝐵)) |
134 | 133 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵))) |
135 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝐹‘𝑧) = (𝐹‘𝐵)) |
136 | 135 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵))) |
137 | 134, 136 | oveq12d 6567 |
. . . . . 6
⊢ (𝑧 = 𝐵 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)))) |
138 | 137, 129,
130 | fvmpt3i 6196 |
. . . . 5
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐵) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)))) |
139 | 14, 138 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐵) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)))) |
140 | 123, 132,
139 | 3eqtr4d 2654 |
. . 3
⊢ (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐴) = ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐵)) |
141 | 1, 2, 3, 44, 101, 140 | rolle 23557 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = 0) |
142 | 96 | fveq1d 6105 |
. . . . . 6
⊢ (𝜑 → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥)) |
143 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘𝑥)) |
144 | 143 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥))) |
145 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘𝑥)) |
146 | 145 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) |
147 | 144, 146 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))) |
148 | 147, 99, 98 | fvmpt3i 6196 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))) |
149 | 142, 148 | sylan9eq 2664 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))) |
150 | 149 | eqeq1d 2612 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = 0 ↔ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0)) |
151 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ) |
152 | 73 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑥) ∈ ℂ) |
153 | 151, 152 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) ∈ ℂ) |
154 | 93 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℂ) |
155 | 89 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
156 | 154, 155 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) ∈ ℂ) |
157 | 153, 156 | subeq0ad 10281 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0 ↔ (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))) |
158 | 150, 157 | bitrd 267 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = 0 ↔ (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))) |
159 | 158 | rexbidva 3031 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))) |
160 | 141, 159 | mpbid 221 |
1
⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) |