This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmvthOLD

Description: Obsolete version of cmvth as of 16-Apr-2025. (Contributed by Mario Carneiro, 29-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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