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	$⊢ φ \to A \in ℝ$
	cmvth.b	$⊢ φ \to B \in ℝ$
	cmvth.lt	$⊢ φ \to A < B$
	cmvth.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	cmvth.g	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℝ$
	cmvth.df	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	cmvth.dg	$⊢ φ \to dom G_{ℝ}^{'} = (A, B)$
Assertion	cmvth	$⊢ φ \to \exists x \in (A, B) (F (B) - F (A)) G_{ℝ}^{'} (x) = (G (B) - G (A)) F_{ℝ}^{'} (x)$

Proof

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

Metamath Proof Explorer

Theorem cmvth

Proof