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

Metamath Proof Explorer

Theorem cmvthOLD

Proof