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)

	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	8	mulcn	$⊢ \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
11		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
12	4 11	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
13	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
14	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
15	1 2 3	ltled	$⊢ φ \to A \leq B$
16		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
17	13 14 15 16	syl3anc	$⊢ φ \to B \in [A, B]$
18	12 17	ffvelrnd	$⊢ φ \to F (B) \in ℝ$
19		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
20	13 14 15 19	syl3anc	$⊢ φ \to A \in [A, B]$
21	12 20	ffvelrnd	$⊢ φ \to F (A) \in ℝ$
22	18 21	resubcld	$⊢ φ \to F (B) - F (A) \in ℝ$
23		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
24	1 2 23	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
25		ax-resscn	$⊢ ℝ \subseteq ℂ$
26	24 25	sstrdi	$⊢ φ \to [A, B] \subseteq ℂ$
27	25	a1i	$⊢ φ \to ℝ \subseteq ℂ$
28		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}{⟶} ℝ$
29	22 26 27 28	syl3anc	$⊢ φ \to (z \in [A, B] ⟼ F (B) - F (A)) : [A, B] \underset{cn}{⟶} ℝ$
30		cncff	$⊢ G : [A, B] \underset{cn}{⟶} ℝ \to G : [A, B] ⟶ ℝ$
31	5 30	syl	$⊢ φ \to G : [A, B] ⟶ ℝ$
32	31	feqmptd	$⊢ φ \to G = (z \in [A, B] ⟼ G (z))$
33	32 5	eqeltrrd	$⊢ φ \to (z \in [A, B] ⟼ G (z)) : [A, B] \underset{cn}{⟶} ℝ$
34		remulcl	$⊢ (F (B) - F (A) \in ℝ \land G (z) \in ℝ) \to (F (B) - F (A)) G (z) \in ℝ$
35	8 10 29 33 25 34	cncfmpt2ss	$⊢ φ \to (z \in [A, B] ⟼ (F (B) - F (A)) G (z)) : [A, B] \underset{cn}{⟶} ℝ$
36	31 17	ffvelrnd	$⊢ φ \to G (B) \in ℝ$
37	31 20	ffvelrnd	$⊢ φ \to G (A) \in ℝ$
38	36 37	resubcld	$⊢ φ \to G (B) - G (A) \in ℝ$
39		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}{⟶} ℝ$
40	38 26 27 39	syl3anc	$⊢ φ \to (z \in [A, B] ⟼ G (B) - G (A)) : [A, B] \underset{cn}{⟶} ℝ$
41	12	feqmptd	$⊢ φ \to F = (z \in [A, B] ⟼ F (z))$
42	41 4	eqeltrrd	$⊢ φ \to (z \in [A, B] ⟼ F (z)) : [A, B] \underset{cn}{⟶} ℝ$
43		remulcl	$⊢ (G (B) - G (A) \in ℝ \land F (z) \in ℝ) \to (G (B) - G (A)) F (z) \in ℝ$
44	8 10 40 42 25 43	cncfmpt2ss	$⊢ φ \to (z \in [A, B] ⟼ (G (B) - G (A)) F (z)) : [A, B] \underset{cn}{⟶} ℝ$
45		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 ℝ$
46	8 9 35 44 25 45	cncfmpt2ss	$⊢ φ \to (z \in [A, B] ⟼ (F (B) - F (A)) G (z) - (G (B) - G (A)) F (z)) : [A, B] \underset{cn}{⟶} ℝ$
47	22	recnd	$⊢ φ \to F (B) - F (A) \in ℂ$
48	47	adantr	$⊢ (φ \land z \in [A, B]) \to F (B) - F (A) \in ℂ$
49	31	ffvelrnda	$⊢ (φ \land z \in [A, B]) \to G (z) \in ℝ$
50	49	recnd	$⊢ (φ \land z \in [A, B]) \to G (z) \in ℂ$
51	48 50	mulcld	$⊢ (φ \land z \in [A, B]) \to (F (B) - F (A)) G (z) \in ℂ$
52	38	adantr	$⊢ (φ \land z \in [A, B]) \to G (B) - G (A) \in ℝ$
53	12	ffvelrnda	$⊢ (φ \land z \in [A, B]) \to F (z) \in ℝ$
54	52 53	remulcld	$⊢ (φ \land z \in [A, B]) \to (G (B) - G (A)) F (z) \in ℝ$
55	54	recnd	$⊢ (φ \land z \in [A, B]) \to (G (B) - G (A)) F (z) \in ℂ$
56	51 55	subcld	$⊢ (φ \land z \in [A, B]) \to (F (B) - F (A)) G (z) - (G (B) - G (A)) F (z) \in ℂ$
57	8	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
58		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
59	1 2 58	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
60	27 24 56 57 8 59	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}$
61		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
62	61	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
63		ioossicc	$⊢ (A, B) \subseteq [A, B]$
64	63	sseli	$⊢ z \in (A, B) \to z \in [A, B]$
65	64 51	sylan2	$⊢ (φ \land z \in (A, B)) \to (F (B) - F (A)) G (z) \in ℂ$
66		ovex	$⊢ (F (B) - F (A)) G_{ℝ}^{'} (z) \in V$
67	66	a1i	$⊢ (φ \land z \in (A, B)) \to (F (B) - F (A)) G_{ℝ}^{'} (z) \in V$
68	64 50	sylan2	$⊢ (φ \land z \in (A, B)) \to G (z) \in ℂ$
69		fvexd	$⊢ (φ \land z \in (A, B)) \to G_{ℝ}^{'} (z) \in V$
70	32	oveq2d	$⊢ φ \to ℝ D G = \frac{d (z \in [A, B]⟼ G (z))}{d_{ℝ} z}$
71		dvf	$⊢ G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ$
72	7	feq2d	$⊢ φ \to (G_{ℝ}^{'} : dom G_{ℝ}^{'} ⟶ ℂ \leftrightarrow G_{ℝ}^{'} : (A, B) ⟶ ℂ)$
73	71 72	mpbii	$⊢ φ \to G_{ℝ}^{'} : (A, B) ⟶ ℂ$
74	73	feqmptd	$⊢ φ \to ℝ D G = (z \in (A, B) ⟼ G_{ℝ}^{'} (z))$
75	27 24 50 57 8 59	dvmptntr	$⊢ φ \to \frac{d (z \in [A, B]⟼ G (z))}{d_{ℝ} z} = \frac{d (z \in (A, B)⟼ G (z))}{d_{ℝ} z}$
76	70 74 75	3eqtr3rd	$⊢ φ \to \frac{d (z \in (A, B)⟼ G (z))}{d_{ℝ} z} = (z \in (A, B) ⟼ G_{ℝ}^{'} (z))$
77	62 68 69 76 47	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))$
78	64 55	sylan2	$⊢ (φ \land z \in (A, B)) \to (G (B) - G (A)) F (z) \in ℂ$
79		ovex	$⊢ (G (B) - G (A)) F_{ℝ}^{'} (z) \in V$
80	79	a1i	$⊢ (φ \land z \in (A, B)) \to (G (B) - G (A)) F_{ℝ}^{'} (z) \in V$
81	53	recnd	$⊢ (φ \land z \in [A, B]) \to F (z) \in ℂ$
82	64 81	sylan2	$⊢ (φ \land z \in (A, B)) \to F (z) \in ℂ$
83		fvexd	$⊢ (φ \land z \in (A, B)) \to F_{ℝ}^{'} (z) \in V$
84	41	oveq2d	$⊢ φ \to ℝ D F = \frac{d (z \in [A, B]⟼ F (z))}{d_{ℝ} z}$
85		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
86	6	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℂ)$
87	85 86	mpbii	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
88	87	feqmptd	$⊢ φ \to ℝ D F = (z \in (A, B) ⟼ F_{ℝ}^{'} (z))$
89	27 24 81 57 8 59	dvmptntr	$⊢ φ \to \frac{d (z \in [A, B]⟼ F (z))}{d_{ℝ} z} = \frac{d (z \in (A, B)⟼ F (z))}{d_{ℝ} z}$
90	84 88 89	3eqtr3rd	$⊢ φ \to \frac{d (z \in (A, B)⟼ F (z))}{d_{ℝ} z} = (z \in (A, B) ⟼ F_{ℝ}^{'} (z))$
91	38	recnd	$⊢ φ \to G (B) - G (A) \in ℂ$
92	62 82 83 90 91	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))$
93	62 65 67 77 78 80 92	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))$
94	60 93	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))$
95	94	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))$
96		ovex	$⊢ (F (B) - F (A)) G_{ℝ}^{'} (z) - (G (B) - G (A)) F_{ℝ}^{'} (z) \in V$
97		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))$
98	96 97	dmmpti	$⊢ dom (z \in (A, B) ⟼ (F (B) - F (A)) G_{ℝ}^{'} (z) - (G (B) - G (A)) F_{ℝ}^{'} (z)) = (A, B)$
99	95 98	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)$
100	18	recnd	$⊢ φ \to F (B) \in ℂ$
101	37	recnd	$⊢ φ \to G (A) \in ℂ$
102	100 101	mulcld	$⊢ φ \to F (B) G (A) \in ℂ$
103	21	recnd	$⊢ φ \to F (A) \in ℂ$
104	36	recnd	$⊢ φ \to G (B) \in ℂ$
105	103 104	mulcld	$⊢ φ \to F (A) G (B) \in ℂ$
106	103 101	mulcld	$⊢ φ \to F (A) G (A) \in ℂ$
107	102 105 106	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)$
108	100 104	mulcld	$⊢ φ \to F (B) G (B) \in ℂ$
109	108 105 102	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)$
110	107 109	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))$
111	100 103 101	subdird	$⊢ φ \to (F (B) - F (A)) G (A) = F (B) G (A) - F (A) G (A)$
112	91 103	mulcomd	$⊢ φ \to (G (B) - G (A)) F (A) = F (A) (G (B) - G (A))$
113	103 104 101	subdid	$⊢ φ \to F (A) (G (B) - G (A)) = F (A) G (B) - F (A) G (A)$
114	112 113	eqtrd	$⊢ φ \to (G (B) - G (A)) F (A) = F (A) G (B) - F (A) G (A)$
115	111 114	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))$
116	100 103 104	subdird	$⊢ φ \to (F (B) - F (A)) G (B) = F (B) G (B) - F (A) G (B)$
117	91 100	mulcomd	$⊢ φ \to (G (B) - G (A)) F (B) = F (B) (G (B) - G (A))$
118	100 104 101	subdid	$⊢ φ \to F (B) (G (B) - G (A)) = F (B) G (B) - F (B) G (A)$
119	117 118	eqtrd	$⊢ φ \to (G (B) - G (A)) F (B) = F (B) G (B) - F (B) G (A)$
120	116 119	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))$
121	110 115 120	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)$
122		fveq2	$⊢ z = A \to G (z) = G (A)$
123	122	oveq2d	$⊢ z = A \to (F (B) - F (A)) G (z) = (F (B) - F (A)) G (A)$
124		fveq2	$⊢ z = A \to F (z) = F (A)$
125	124	oveq2d	$⊢ z = A \to (G (B) - G (A)) F (z) = (G (B) - G (A)) F (A)$
126	123 125	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)$
127		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))$
128		ovex	$⊢ (F (B) - F (A)) G (z) - (G (B) - G (A)) F (z) \in V$
129	126 127 128	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)$
130	20 129	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)$
131		fveq2	$⊢ z = B \to G (z) = G (B)$
132	131	oveq2d	$⊢ z = B \to (F (B) - F (A)) G (z) = (F (B) - F (A)) G (B)$
133		fveq2	$⊢ z = B \to F (z) = F (B)$
134	133	oveq2d	$⊢ z = B \to (G (B) - G (A)) F (z) = (G (B) - G (A)) F (B)$
135	132 134	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)$
136	135 127 128	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)$
137	17 136	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)$
138	121 130 137	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)$
139	1 2 3 46 99 138	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$
140	94	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)$
141		fveq2	$⊢ z = x \to G_{ℝ}^{'} (z) = G_{ℝ}^{'} (x)$
142	141	oveq2d	$⊢ z = x \to (F (B) - F (A)) G_{ℝ}^{'} (z) = (F (B) - F (A)) G_{ℝ}^{'} (x)$
143		fveq2	$⊢ z = x \to F_{ℝ}^{'} (z) = F_{ℝ}^{'} (x)$
144	143	oveq2d	$⊢ z = x \to (G (B) - G (A)) F_{ℝ}^{'} (z) = (G (B) - G (A)) F_{ℝ}^{'} (x)$
145	142 144	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)$
146	145 97 96	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)$
147	140 146	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)$
148	147	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)$
149	47	adantr	$⊢ (φ \land x \in (A, B)) \to F (B) - F (A) \in ℂ$
150	73	ffvelrnda	$⊢ (φ \land x \in (A, B)) \to G_{ℝ}^{'} (x) \in ℂ$
151	149 150	mulcld	$⊢ (φ \land x \in (A, B)) \to (F (B) - F (A)) G_{ℝ}^{'} (x) \in ℂ$
152	91	adantr	$⊢ (φ \land x \in (A, B)) \to G (B) - G (A) \in ℂ$
153	87	ffvelrnda	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
154	152 153	mulcld	$⊢ (φ \land x \in (A, B)) \to (G (B) - G (A)) F_{ℝ}^{'} (x) \in ℂ$
155	151 154	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))$
156	148 155	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))$
157	156	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))$
158	139 157	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