Metamath Proof Explorer

Theorem cmvth

Description: Cauchy's Mean Value Theorem. If F , G are real continuous functions on [ A , B ] differentiable on ( A , B ) , then there is some x e. ( A , B ) such that F ' ( x ) / G ' ( x ) = ( F ( A ) - F ( B ) ) / ( G ( A ) - G ( B ) ) . (We express the condition without division, so that we need no nonzero constraints.) (Contributed by Mario Carneiro, 29-Dec-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses cmvth.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
cmvth.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
cmvth.lt ⊢ ( 𝜑 → 𝐴 < 𝐵 )
cmvth.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
cmvth.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
cmvth.df ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
cmvth.dg ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
Assertion cmvth ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 cmvth.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 cmvth.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 cmvth.lt ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 cmvth.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5 cmvth.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
6 cmvth.df ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
7 cmvth.dg ⊢ ( 𝜑 → dom ( ℝ D 𝐺 ) = ( 𝐴 (,) 𝐵 ) )
8 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
9 8 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
10 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
11 4 10 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
12 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
13 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
14 1 2 3 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
15 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
16 12 13 14 15 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
17 11 16 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
18 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
19 12 13 14 18 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
20 11 19 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
21 17 20 resubcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
22 21 recnd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
24 cncff ⊢ ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
25 5 24 syl ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
26 25 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
27 26 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
28 ovmpot ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) )
29 23 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) )
30 29 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ↔ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) )
31 30 pm5.32da ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) ) )
32 31 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) } )
33 df-mpt ⊢ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) }
34 32 33 eqtr4di ⊢ ( 𝜑 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ) } = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) )
35 df-mpt ⊢ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ) }
36 8 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
37 1 2 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
38 ax-resscn ⊢ ℝ ⊆ ℂ
39 37 38 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
40 38 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
41 cncfmptc ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
42 21 39 40 41 syl3anc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
43 25 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐺 ‘ 𝑧 ) ) )
44 43 5 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
45 simpl ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ )
46 45 recnd ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
47 simpr ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
48 47 recnd ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
49 28 eqcomd ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) )
50 46 48 49 syl2anc ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) )
51 remulcl ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
52 50 51 eqeltrrd ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ )
53 8 36 42 44 38 52 cncfmpt2ss ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
54 35 53 eqeltrrid ⊢ ( 𝜑 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐺 ‘ 𝑧 ) ) ) } ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
55 34 54 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
56 25 16 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
57 25 19 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) ∈ ℝ )
58 56 57 resubcld ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ )
60 59 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ )
61 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
62 61 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
63 ovmpot ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) )
64 60 62 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) )
65 64 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ↔ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) )
66 65 pm5.32da ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ) ↔ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) )
67 66 opabbidv ⊢ ( 𝜑 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) } )
68 df-mpt ⊢ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) }
69 67 68 eqtr4di ⊢ ( 𝜑 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ) } = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) )
70 df-mpt ⊢ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ) }
71 cncfmptc ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
72 58 39 40 71 syl3anc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
73 11 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) )
74 73 4 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
75 simpl ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ )
76 75 recnd ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ )
77 simpr ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
78 77 recnd ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
79 63 eqcomd ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) )
80 76 78 79 syl2anc ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) )
81 remulcl ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
82 80 81 eqeltrrd ⊢ ( ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
83 8 36 72 74 38 82 cncfmpt2ss ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
84 70 83 eqeltrrid ⊢ ( 𝜑 → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝐹 ‘ 𝑧 ) ) ) } ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
85 69 84 eqeltrrd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
86 resubcl ⊢ ( ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℝ ∧ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ∈ ℝ )
87 8 9 55 85 38 86 cncfmpt2ss ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
88 23 27 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
89 59 61 remulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
90 89 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
91 88 90 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ∈ ℂ )
92 8 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
93 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
94 1 2 93 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
95 40 37 91 92 8 94 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) = ( ℝ D ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) )
96 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
97 96 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
98 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
99 98 sseli ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
100 99 88 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
101 ovexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ∈ V )
102 99 27 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
103 fvexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ∈ V )
104 43 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐺 ) = ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐺 ‘ 𝑧 ) ) ) )
105 dvf ⊢ ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ
106 7 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐺 ) : dom ( ℝ D 𝐺 ) ⟶ ℂ ↔ ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
107 105 106 mpbii ⊢ ( 𝜑 → ( ℝ D 𝐺 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
108 107 feqmptd ⊢ ( 𝜑 → ( ℝ D 𝐺 ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) )
109 40 37 27 92 8 94 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐺 ‘ 𝑧 ) ) ) = ( ℝ D ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑧 ) ) ) )
110 104 108 109 3eqtr3rd ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) )
111 97 102 103 110 22 dvmptcmul ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) ) )
112 99 90 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ∈ ℂ )
113 ovexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ∈ V )
114 99 62 sylan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
115 fvexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ∈ V )
116 73 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) ) )
117 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
118 6 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
119 117 118 mpbii ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
120 119 feqmptd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) )
121 40 37 62 92 8 94 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) ) = ( ℝ D ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) ) )
122 116 120 121 3eqtr3rd ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) )
123 58 recnd ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ )
124 97 114 115 122 123 dvmptcmul ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) )
125 97 100 101 111 112 113 124 dvmptsub ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) ) )
126 95 125 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) ) )
127 126 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) = dom ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) ) )
128 ovex ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) ∈ V
129 eqid ⊢ ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) )
130 128 129 dmmpti ⊢ dom ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) ) = ( 𝐴 (,) 𝐵 )
131 127 130 eqtrdi ⊢ ( 𝜑 → dom ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) = ( 𝐴 (,) 𝐵 ) )
132 17 recnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
133 57 recnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) ∈ ℂ )
134 132 133 mulcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ )
135 20 recnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
136 56 recnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℂ )
137 135 136 mulcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ∈ ℂ )
138 135 133 mulcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ )
139 134 137 138 nnncan2d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) − ( ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) ) = ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
140 132 136 mulcld ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) ∈ ℂ )
141 140 137 134 nnncan1d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) − ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) ) ) = ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
142 139 141 eqtr4d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) − ( ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) ) = ( ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) − ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) ) ) )
143 132 135 133 subdird ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐴 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) )
144 123 135 mulcomd ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐴 ) · ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
145 135 136 133 subdid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) · ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ) = ( ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) )
146 144 145 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐴 ) ) = ( ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) )
147 143 146 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐴 ) ) ) = ( ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) − ( ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐴 ) ) ) ) )
148 132 135 136 subdird ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐵 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
149 123 132 mulcomd ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐵 ) ) = ( ( 𝐹 ‘ 𝐵 ) · ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ) )
150 132 136 133 subdid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) · ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ) = ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) ) )
151 149 150 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐵 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) ) )
152 148 151 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐵 ) ) ) = ( ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) − ( ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( 𝐹 ‘ 𝐵 ) · ( 𝐺 ‘ 𝐴 ) ) ) ) )
153 142 147 152 3eqtr4d ⊢ ( 𝜑 → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐴 ) ) ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐵 ) ) ) )
154 fveq2 ⊢ ( 𝑧 = 𝐴 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐴 ) )
155 154 oveq2d ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐴 ) ) )
156 fveq2 ⊢ ( 𝑧 = 𝐴 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐴 ) )
157 156 oveq2d ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐴 ) ) )
158 155 157 oveq12d ⊢ ( 𝑧 = 𝐴 → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐴 ) ) ) )
159 eqid ⊢ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) )
160 ovex ⊢ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ∈ V
161 158 159 160 fvmpt3i ⊢ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝐴 ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐴 ) ) ) )
162 19 161 syl ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝐴 ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐴 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐴 ) ) ) )
163 fveq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐵 ) )
164 163 oveq2d ⊢ ( 𝑧 = 𝐵 → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐵 ) ) )
165 fveq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝐵 ) )
166 165 oveq2d ⊢ ( 𝑧 = 𝐵 → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐵 ) ) )
167 164 166 oveq12d ⊢ ( 𝑧 = 𝐵 → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐵 ) ) ) )
168 167 159 160 fvmpt3i ⊢ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝐵 ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐵 ) ) ) )
169 16 168 syl ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝐵 ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝐵 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝐵 ) ) ) )
170 153 162 169 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝐴 ) = ( ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ‘ 𝐵 ) )
171 1 2 3 87 131 170 rolle ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) ‘ 𝑥 ) = 0 )
172 126 fveq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) ‘ 𝑥 ) = ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) ) ‘ 𝑥 ) )
173 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( ℝ D 𝐺 ) ‘ 𝑧 ) = ( ( ℝ D 𝐺 ) ‘ 𝑥 ) )
174 173 oveq2d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) )
175 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( ℝ D 𝐹 ) ‘ 𝑧 ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
176 175 oveq2d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
177 174 176 oveq12d ⊢ ( 𝑧 = 𝑥 → ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
178 177 129 128 fvmpt3i ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑧 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑧 ) ) ) ) ‘ 𝑥 ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
179 172 178 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) ‘ 𝑥 ) = ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
180 179 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) ‘ 𝑥 ) = 0 ↔ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) = 0 ) )
181 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ )
182 107 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ∈ ℂ )
183 181 182 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) ∈ ℂ )
184 123 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) ∈ ℂ )
185 119 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
186 184 185 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ ℂ )
187 183 186 subeq0ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) = 0 ↔ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
188 180 187 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) ‘ 𝑥 ) = 0 ↔ ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
189 188 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( 𝐹 ‘ 𝑧 ) ) ) ) ) ‘ 𝑥 ) = 0 ↔ ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
190 171 189 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) · ( ( ℝ D 𝐺 ) ‘ 𝑥 ) ) = ( ( ( 𝐺 ‘ 𝐵 ) − ( 𝐺 ‘ 𝐴 ) ) · ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )