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		tgioo4	⊢ ( 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 𝐹 ) ‘ 𝑥 ) ) )

Metamath Proof Explorer

Theorem cmvth

Proof