rolle

Description: Rolle's theorem. If F is a real continuous function on [ A , B ] which is differentiable on ( A , B ) , and F ( A ) = F ( B ) , then there is some x e. ( A , B ) such that ( RR _D F )x = 0 . (Contributed by Mario Carneiro, 1-Sep-2014)

	Ref	Expression
Hypotheses	rolle.a	$⊢ φ \to A \in ℝ$
	rolle.b	$⊢ φ \to B \in ℝ$
	rolle.lt	$⊢ φ \to A < B$
	rolle.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
	rolle.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	rolle.e	$⊢ φ \to F (A) = F (B)$
Assertion	rolle	$⊢ φ \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$

Proof

Step	Hyp	Ref	Expression
1		rolle.a	$⊢ φ \to A \in ℝ$
2		rolle.b	$⊢ φ \to B \in ℝ$
3		rolle.lt	$⊢ φ \to A < B$
4		rolle.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
5		rolle.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
6		rolle.e	$⊢ φ \to F (A) = F (B)$
7	1 2 3	ltled	$⊢ φ \to A \leq B$
8	1 2 7 4	evthicc	$⊢ φ \to (\exists u \in [A, B] \forall y \in [A, B] F (y) \leq F (u) \land \exists v \in [A, B] \forall y \in [A, B] F (v) \leq F (y))$
9		reeanv	$⊢ \exists u \in [A, B] \exists v \in [A, B] (\forall y \in [A, B] F (y) \leq F (u) \land \forall y \in [A, B] F (v) \leq F (y)) \leftrightarrow (\exists u \in [A, B] \forall y \in [A, B] F (y) \leq F (u) \land \exists v \in [A, B] \forall y \in [A, B] F (v) \leq F (y))$
10	8 9	sylibr	$⊢ φ \to \exists u \in [A, B] \exists v \in [A, B] (\forall y \in [A, B] F (y) \leq F (u) \land \forall y \in [A, B] F (v) \leq F (y))$
11		r19.26	$⊢ \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \leftrightarrow (\forall y \in [A, B] F (y) \leq F (u) \land \forall y \in [A, B] F (v) \leq F (y))$
12	1	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to A \in ℝ$
13	2	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to B \in ℝ$
14	3	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to A < B$
15	4	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to F : [A, B] \underset{cn}{⟶} ℝ$
16	5	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to dom F_{ℝ}^{'} = (A, B)$
17		simpl	$⊢ (F (y) \leq F (u) \land F (v) \leq F (y)) \to F (y) \leq F (u)$
18	17	ralimi	$⊢ \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \to \forall y \in [A, B] F (y) \leq F (u)$
19		fveq2	$⊢ y = t \to F (y) = F (t)$
20	19	breq1d	$⊢ y = t \to (F (y) \leq F (u) \leftrightarrow F (t) \leq F (u))$
21	20	cbvralvw	$⊢ \forall y \in [A, B] F (y) \leq F (u) \leftrightarrow \forall t \in [A, B] F (t) \leq F (u)$
22	18 21	sylib	$⊢ \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \to \forall t \in [A, B] F (t) \leq F (u)$
23	22	ad2antrl	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to \forall t \in [A, B] F (t) \leq F (u)$
24		simplrl	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to u \in [A, B]$
25		simprr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to \neg u \in \{A, B\}$
26	12 13 14 15 16 23 24 25	rollelem	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg u \in \{A, B\})) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$
27	26	expr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y))) \to (\neg u \in \{A, B\} \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
28	1	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to A \in ℝ$
29	2	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to B \in ℝ$
30	3	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to A < B$
31		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
32	4 31	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
33	32	ffvelrnda	$⊢ (φ \land u \in [A, B]) \to F (u) \in ℝ$
34	33	renegcld	$⊢ (φ \land u \in [A, B]) \to - F (u) \in ℝ$
35	34	fmpttd	$⊢ φ \to (u \in [A, B] ⟼ - F (u)) : [A, B] ⟶ ℝ$
36		ax-resscn	$⊢ ℝ \subseteq ℂ$
37		ssid	$⊢ ℂ \subseteq ℂ$
38		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
39	36 37 38	mp2an	$⊢ [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
40	39 4	sseldi	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
41		eqid	$⊢ (u \in [A, B] ⟼ - F (u)) = (u \in [A, B] ⟼ - F (u))$
42	41	negfcncf	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to (u \in [A, B] ⟼ - F (u)) : [A, B] \underset{cn}{⟶} ℂ$
43	40 42	syl	$⊢ φ \to (u \in [A, B] ⟼ - F (u)) : [A, B] \underset{cn}{⟶} ℂ$
44		cncffvrn	$⊢ (ℝ \subseteq ℂ \land (u \in [A, B] ⟼ - F (u)) : [A, B] \underset{cn}{⟶} ℂ) \to ((u \in [A, B] ⟼ - F (u)) : [A, B] \underset{cn}{⟶} ℝ \leftrightarrow (u \in [A, B] ⟼ - F (u)) : [A, B] ⟶ ℝ)$
45	36 43 44	sylancr	$⊢ φ \to ((u \in [A, B] ⟼ - F (u)) : [A, B] \underset{cn}{⟶} ℝ \leftrightarrow (u \in [A, B] ⟼ - F (u)) : [A, B] ⟶ ℝ)$
46	35 45	mpbird	$⊢ φ \to (u \in [A, B] ⟼ - F (u)) : [A, B] \underset{cn}{⟶} ℝ$
47	46	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to (u \in [A, B] ⟼ - F (u)) : [A, B] \underset{cn}{⟶} ℝ$
48	36	a1i	$⊢ φ \to ℝ \subseteq ℂ$
49		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
50	1 2 49	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
51		fss	$⊢ (F : [A, B] ⟶ ℝ \land ℝ \subseteq ℂ) \to F : [A, B] ⟶ ℂ$
52	32 36 51	sylancl	$⊢ φ \to F : [A, B] ⟶ ℂ$
53	52	ffvelrnda	$⊢ (φ \land u \in [A, B]) \to F (u) \in ℂ$
54	53	negcld	$⊢ (φ \land u \in [A, B]) \to - F (u) \in ℂ$
55		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
56	55	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
57		iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$
58	1 2 57	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([A, B]) = (A, B)$
59	48 50 54 56 55 58	dvmptntr	$⊢ φ \to \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} = \frac{d (u \in (A, B)⟼ - F (u))}{d_{ℝ} u}$
60		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
61	60	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
62		ioossicc	$⊢ (A, B) \subseteq [A, B]$
63	62	sseli	$⊢ u \in (A, B) \to u \in [A, B]$
64	63 53	sylan2	$⊢ (φ \land u \in (A, B)) \to F (u) \in ℂ$
65		fvexd	$⊢ (φ \land u \in (A, B)) \to F_{ℝ}^{'} (u) \in V$
66	32	feqmptd	$⊢ φ \to F = (u \in [A, B] ⟼ F (u))$
67	66	oveq2d	$⊢ φ \to ℝ D F = \frac{d (u \in [A, B]⟼ F (u))}{d_{ℝ} u}$
68		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
69	5	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℂ)$
70	68 69	mpbii	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
71	70	feqmptd	$⊢ φ \to ℝ D F = (u \in (A, B) ⟼ F_{ℝ}^{'} (u))$
72	48 50 53 56 55 58	dvmptntr	$⊢ φ \to \frac{d (u \in [A, B]⟼ F (u))}{d_{ℝ} u} = \frac{d (u \in (A, B)⟼ F (u))}{d_{ℝ} u}$
73	67 71 72	3eqtr3rd	$⊢ φ \to \frac{d (u \in (A, B)⟼ F (u))}{d_{ℝ} u} = (u \in (A, B) ⟼ F_{ℝ}^{'} (u))$
74	61 64 65 73	dvmptneg	$⊢ φ \to \frac{d (u \in (A, B)⟼ - F (u))}{d_{ℝ} u} = (u \in (A, B) ⟼ - F_{ℝ}^{'} (u))$
75	59 74	eqtrd	$⊢ φ \to \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} = (u \in (A, B) ⟼ - F_{ℝ}^{'} (u))$
76	75	dmeqd	$⊢ φ \to dom \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} = dom (u \in (A, B) ⟼ - F_{ℝ}^{'} (u))$
77		dmmptg	$⊢ \forall u \in (A, B) - F_{ℝ}^{'} (u) \in V \to dom (u \in (A, B) ⟼ - F_{ℝ}^{'} (u)) = (A, B)$
78		negex	$⊢ - F_{ℝ}^{'} (u) \in V$
79	78	a1i	$⊢ u \in (A, B) \to - F_{ℝ}^{'} (u) \in V$
80	77 79	mprg	$⊢ dom (u \in (A, B) ⟼ - F_{ℝ}^{'} (u)) = (A, B)$
81	76 80	eqtrdi	$⊢ φ \to dom \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} = (A, B)$
82	81	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to dom \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} = (A, B)$
83		simpr	$⊢ (F (y) \leq F (u) \land F (v) \leq F (y)) \to F (v) \leq F (y)$
84	32	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to F : [A, B] ⟶ ℝ$
85		simplrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to v \in [A, B]$
86	84 85	ffvelrnd	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to F (v) \in ℝ$
87	32	adantr	$⊢ (φ \land (u \in [A, B] \land v \in [A, B])) \to F : [A, B] ⟶ ℝ$
88	87	ffvelrnda	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to F (y) \in ℝ$
89	86 88	lenegd	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to (F (v) \leq F (y) \leftrightarrow - F (y) \leq - F (v))$
90		fveq2	$⊢ u = y \to F (u) = F (y)$
91	90	negeqd	$⊢ u = y \to - F (u) = - F (y)$
92		negex	$⊢ - F (y) \in V$
93	91 41 92	fvmpt	$⊢ y \in [A, B] \to (u \in [A, B] ⟼ - F (u)) (y) = - F (y)$
94	93	adantl	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to (u \in [A, B] ⟼ - F (u)) (y) = - F (y)$
95		fveq2	$⊢ u = v \to F (u) = F (v)$
96	95	negeqd	$⊢ u = v \to - F (u) = - F (v)$
97		negex	$⊢ - F (v) \in V$
98	96 41 97	fvmpt	$⊢ v \in [A, B] \to (u \in [A, B] ⟼ - F (u)) (v) = - F (v)$
99	85 98	syl	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to (u \in [A, B] ⟼ - F (u)) (v) = - F (v)$
100	94 99	breq12d	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to ((u \in [A, B] ⟼ - F (u)) (y) \leq (u \in [A, B] ⟼ - F (u)) (v) \leftrightarrow - F (y) \leq - F (v))$
101	89 100	bitr4d	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to (F (v) \leq F (y) \leftrightarrow (u \in [A, B] ⟼ - F (u)) (y) \leq (u \in [A, B] ⟼ - F (u)) (v))$
102	83 101	syl5ib	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to ((F (y) \leq F (u) \land F (v) \leq F (y)) \to (u \in [A, B] ⟼ - F (u)) (y) \leq (u \in [A, B] ⟼ - F (u)) (v))$
103	102	ralimdva	$⊢ (φ \land (u \in [A, B] \land v \in [A, B])) \to (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \to \forall y \in [A, B] (u \in [A, B] ⟼ - F (u)) (y) \leq (u \in [A, B] ⟼ - F (u)) (v))$
104	103	imp	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y))) \to \forall y \in [A, B] (u \in [A, B] ⟼ - F (u)) (y) \leq (u \in [A, B] ⟼ - F (u)) (v)$
105		fveq2	$⊢ y = t \to (u \in [A, B] ⟼ - F (u)) (y) = (u \in [A, B] ⟼ - F (u)) (t)$
106	105	breq1d	$⊢ y = t \to ((u \in [A, B] ⟼ - F (u)) (y) \leq (u \in [A, B] ⟼ - F (u)) (v) \leftrightarrow (u \in [A, B] ⟼ - F (u)) (t) \leq (u \in [A, B] ⟼ - F (u)) (v))$
107	106	cbvralvw	$⊢ \forall y \in [A, B] (u \in [A, B] ⟼ - F (u)) (y) \leq (u \in [A, B] ⟼ - F (u)) (v) \leftrightarrow \forall t \in [A, B] (u \in [A, B] ⟼ - F (u)) (t) \leq (u \in [A, B] ⟼ - F (u)) (v)$
108	104 107	sylib	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y))) \to \forall t \in [A, B] (u \in [A, B] ⟼ - F (u)) (t) \leq (u \in [A, B] ⟼ - F (u)) (v)$
109	108	adantrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to \forall t \in [A, B] (u \in [A, B] ⟼ - F (u)) (t) \leq (u \in [A, B] ⟼ - F (u)) (v)$
110		simplrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to v \in [A, B]$
111		simprr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to \neg v \in \{A, B\}$
112	28 29 30 47 82 109 110 111	rollelem	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to \exists x \in (A, B) \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} (x) = 0$
113	75	fveq1d	$⊢ φ \to \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} (x) = (u \in (A, B) ⟼ - F_{ℝ}^{'} (u)) (x)$
114		fveq2	$⊢ u = x \to F_{ℝ}^{'} (u) = F_{ℝ}^{'} (x)$
115	114	negeqd	$⊢ u = x \to - F_{ℝ}^{'} (u) = - F_{ℝ}^{'} (x)$
116		eqid	$⊢ (u \in (A, B) ⟼ - F_{ℝ}^{'} (u)) = (u \in (A, B) ⟼ - F_{ℝ}^{'} (u))$
117		negex	$⊢ - F_{ℝ}^{'} (x) \in V$
118	115 116 117	fvmpt	$⊢ x \in (A, B) \to (u \in (A, B) ⟼ - F_{ℝ}^{'} (u)) (x) = - F_{ℝ}^{'} (x)$
119	113 118	sylan9eq	$⊢ (φ \land x \in (A, B)) \to \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} (x) = - F_{ℝ}^{'} (x)$
120	119	eqeq1d	$⊢ (φ \land x \in (A, B)) \to (\frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} (x) = 0 \leftrightarrow - F_{ℝ}^{'} (x) = 0)$
121	5	eleq2d	$⊢ φ \to (x \in dom F_{ℝ}^{'} \leftrightarrow x \in (A, B))$
122	121	biimpar	$⊢ (φ \land x \in (A, B)) \to x \in dom F_{ℝ}^{'}$
123	68	ffvelrni	$⊢ x \in dom F_{ℝ}^{'} \to F_{ℝ}^{'} (x) \in ℂ$
124	122 123	syl	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
125	124	negeq0d	$⊢ (φ \land x \in (A, B)) \to (F_{ℝ}^{'} (x) = 0 \leftrightarrow - F_{ℝ}^{'} (x) = 0)$
126	120 125	bitr4d	$⊢ (φ \land x \in (A, B)) \to (\frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} (x) = 0 \leftrightarrow F_{ℝ}^{'} (x) = 0)$
127	126	rexbidva	$⊢ φ \to (\exists x \in (A, B) \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} (x) = 0 \leftrightarrow \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
128	127	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to (\exists x \in (A, B) \frac{d (u \in [A, B]⟼ - F (u))}{d_{ℝ} u} (x) = 0 \leftrightarrow \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
129	112 128	mpbid	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \land \neg v \in \{A, B\})) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$
130	129	expr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y))) \to (\neg v \in \{A, B\} \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
131		vex	$⊢ u \in V$
132	131	elpr	$⊢ u \in \{A, B\} \leftrightarrow (u = A \lor u = B)$
133		fveq2	$⊢ u = A \to F (u) = F (A)$
134	133	a1i	$⊢ φ \to (u = A \to F (u) = F (A))$
135	6	eqcomd	$⊢ φ \to F (B) = F (A)$
136		fveqeq2	$⊢ u = B \to (F (u) = F (A) \leftrightarrow F (B) = F (A))$
137	135 136	syl5ibrcom	$⊢ φ \to (u = B \to F (u) = F (A))$
138	134 137	jaod	$⊢ φ \to ((u = A \lor u = B) \to F (u) = F (A))$
139	132 138	syl5bi	$⊢ φ \to (u \in \{A, B\} \to F (u) = F (A))$
140		eleq1w	$⊢ u = v \to (u \in \{A, B\} \leftrightarrow v \in \{A, B\})$
141		fveqeq2	$⊢ u = v \to (F (u) = F (A) \leftrightarrow F (v) = F (A))$
142	140 141	imbi12d	$⊢ u = v \to ((u \in \{A, B\} \to F (u) = F (A)) \leftrightarrow (v \in \{A, B\} \to F (v) = F (A)))$
143	142	imbi2d	$⊢ u = v \to ((φ \to (u \in \{A, B\} \to F (u) = F (A))) \leftrightarrow (φ \to (v \in \{A, B\} \to F (v) = F (A))))$
144	143 139	chvarvv	$⊢ φ \to (v \in \{A, B\} \to F (v) = F (A))$
145	139 144	anim12d	$⊢ φ \to ((u \in \{A, B\} \land v \in \{A, B\}) \to (F (u) = F (A) \land F (v) = F (A)))$
146	145	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y))) \to ((u \in \{A, B\} \land v \in \{A, B\}) \to (F (u) = F (A) \land F (v) = F (A)))$
147	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
148	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
149		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
150	147 148 7 149	syl3anc	$⊢ φ \to A \in [A, B]$
151	32 150	ffvelrnd	$⊢ φ \to F (A) \in ℝ$
152	151	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to F (A) \in ℝ$
153	88 152	letri3d	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to (F (y) = F (A) \leftrightarrow (F (y) \leq F (A) \land F (A) \leq F (y)))$
154		breq2	$⊢ F (u) = F (A) \to (F (y) \leq F (u) \leftrightarrow F (y) \leq F (A))$
155		breq1	$⊢ F (v) = F (A) \to (F (v) \leq F (y) \leftrightarrow F (A) \leq F (y))$
156	154 155	bi2anan9	$⊢ (F (u) = F (A) \land F (v) = F (A)) \to ((F (y) \leq F (u) \land F (v) \leq F (y)) \leftrightarrow (F (y) \leq F (A) \land F (A) \leq F (y)))$
157	156	bibi2d	$⊢ (F (u) = F (A) \land F (v) = F (A)) \to ((F (y) = F (A) \leftrightarrow (F (y) \leq F (u) \land F (v) \leq F (y))) \leftrightarrow (F (y) = F (A) \leftrightarrow (F (y) \leq F (A) \land F (A) \leq F (y))))$
158	153 157	syl5ibrcom	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land y \in [A, B]) \to ((F (u) = F (A) \land F (v) = F (A)) \to (F (y) = F (A) \leftrightarrow (F (y) \leq F (u) \land F (v) \leq F (y))))$
159	158	impancom	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (F (u) = F (A) \land F (v) = F (A))) \to (y \in [A, B] \to (F (y) = F (A) \leftrightarrow (F (y) \leq F (u) \land F (v) \leq F (y))))$
160	159	imp	$⊢ (((φ \land (u \in [A, B] \land v \in [A, B])) \land (F (u) = F (A) \land F (v) = F (A))) \land y \in [A, B]) \to (F (y) = F (A) \leftrightarrow (F (y) \leq F (u) \land F (v) \leq F (y)))$
161	160	ralbidva	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (F (u) = F (A) \land F (v) = F (A))) \to (\forall y \in [A, B] F (y) = F (A) \leftrightarrow \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)))$
162	32	ffnd	$⊢ φ \to F Fn [A, B]$
163		fnconstg	$⊢ F (A) \in ℝ \to ([A, B] \times \{F (A)\}) Fn [A, B]$
164	151 163	syl	$⊢ φ \to ([A, B] \times \{F (A)\}) Fn [A, B]$
165		eqfnfv	$⊢ (F Fn [A, B] \land ([A, B] \times \{F (A)\}) Fn [A, B]) \to (F = [A, B] \times \{F (A)\} \leftrightarrow \forall y \in [A, B] F (y) = ([A, B] \times \{F (A)\}) (y))$
166	162 164 165	syl2anc	$⊢ φ \to (F = [A, B] \times \{F (A)\} \leftrightarrow \forall y \in [A, B] F (y) = ([A, B] \times \{F (A)\}) (y))$
167		fvex	$⊢ F (A) \in V$
168	167	fvconst2	$⊢ y \in [A, B] \to ([A, B] \times \{F (A)\}) (y) = F (A)$
169	168	eqeq2d	$⊢ y \in [A, B] \to (F (y) = ([A, B] \times \{F (A)\}) (y) \leftrightarrow F (y) = F (A))$
170	169	ralbiia	$⊢ \forall y \in [A, B] F (y) = ([A, B] \times \{F (A)\}) (y) \leftrightarrow \forall y \in [A, B] F (y) = F (A)$
171	166 170	bitrdi	$⊢ φ \to (F = [A, B] \times \{F (A)\} \leftrightarrow \forall y \in [A, B] F (y) = F (A))$
172		ioon0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ((A, B) \neq \emptyset \leftrightarrow A < B)$
173	147 148 172	syl2anc	$⊢ φ \to ((A, B) \neq \emptyset \leftrightarrow A < B)$
174	3 173	mpbird	$⊢ φ \to (A, B) \neq \emptyset$
175		fconstmpt	$⊢ [A, B] \times \{F (A)\} = (u \in [A, B] ⟼ F (A))$
176	175	eqeq2i	$⊢ F = [A, B] \times \{F (A)\} \leftrightarrow F = (u \in [A, B] ⟼ F (A))$
177	176	biimpi	$⊢ F = [A, B] \times \{F (A)\} \to F = (u \in [A, B] ⟼ F (A))$
178	177	oveq2d	$⊢ F = [A, B] \times \{F (A)\} \to ℝ D F = \frac{d (u \in [A, B]⟼ F (A))}{d_{ℝ} u}$
179	151	recnd	$⊢ φ \to F (A) \in ℂ$
180	179	adantr	$⊢ (φ \land u \in ℝ) \to F (A) \in ℂ$
181		0cnd	$⊢ (φ \land u \in ℝ) \to 0 \in ℂ$
182	61 179	dvmptc	$⊢ φ \to \frac{d (u \in ℝ⟼ F (A))}{d_{ℝ} u} = (u \in ℝ ⟼ 0)$
183	61 180 181 182 50 56 55 58	dvmptres2	$⊢ φ \to \frac{d (u \in [A, B]⟼ F (A))}{d_{ℝ} u} = (u \in (A, B) ⟼ 0)$
184	178 183	sylan9eqr	$⊢ (φ \land F = [A, B] \times \{F (A)\}) \to ℝ D F = (u \in (A, B) ⟼ 0)$
185	184	fveq1d	$⊢ (φ \land F = [A, B] \times \{F (A)\}) \to F_{ℝ}^{'} (x) = (u \in (A, B) ⟼ 0) (x)$
186		eqidd	$⊢ u = x \to 0 = 0$
187		eqid	$⊢ (u \in (A, B) ⟼ 0) = (u \in (A, B) ⟼ 0)$
188		c0ex	$⊢ 0 \in V$
189	186 187 188	fvmpt	$⊢ x \in (A, B) \to (u \in (A, B) ⟼ 0) (x) = 0$
190	185 189	sylan9eq	$⊢ ((φ \land F = [A, B] \times \{F (A)\}) \land x \in (A, B)) \to F_{ℝ}^{'} (x) = 0$
191	190	ralrimiva	$⊢ (φ \land F = [A, B] \times \{F (A)\}) \to \forall x \in (A, B) F_{ℝ}^{'} (x) = 0$
192		r19.2z	$⊢ ((A, B) \neq \emptyset \land \forall x \in (A, B) F_{ℝ}^{'} (x) = 0) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$
193	174 191 192	syl2an2r	$⊢ (φ \land F = [A, B] \times \{F (A)\}) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$
194	193	ex	$⊢ φ \to (F = [A, B] \times \{F (A)\} \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
195	171 194	sylbird	$⊢ φ \to (\forall y \in [A, B] F (y) = F (A) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
196	195	ad2antrr	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (F (u) = F (A) \land F (v) = F (A))) \to (\forall y \in [A, B] F (y) = F (A) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
197	161 196	sylbird	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land (F (u) = F (A) \land F (v) = F (A))) \to (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
198	197	impancom	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y))) \to ((F (u) = F (A) \land F (v) = F (A)) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
199	146 198	syld	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y))) \to ((u \in \{A, B\} \land v \in \{A, B\}) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
200	27 130 199	ecased	$⊢ ((φ \land (u \in [A, B] \land v \in [A, B])) \land \forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y))) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$
201	200	ex	$⊢ (φ \land (u \in [A, B] \land v \in [A, B])) \to (\forall y \in [A, B] (F (y) \leq F (u) \land F (v) \leq F (y)) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
202	11 201	syl5bir	$⊢ (φ \land (u \in [A, B] \land v \in [A, B])) \to ((\forall y \in [A, B] F (y) \leq F (u) \land \forall y \in [A, B] F (v) \leq F (y)) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
203	202	rexlimdvva	$⊢ φ \to (\exists u \in [A, B] \exists v \in [A, B] (\forall y \in [A, B] F (y) \leq F (u) \land \forall y \in [A, B] F (v) \leq F (y)) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0)$
204	10 203	mpd	$⊢ φ \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$

Metamath Proof Explorer

Theorem rolle

Proof