rollelem

	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.r	$⊢ φ \to \forall y \in [A, B] F (y) \leq F (U)$
	rolle.u	$⊢ φ \to U \in [A, B]$
	rolle.n	$⊢ φ \to \neg U \in \{A, B\}$
Assertion	rollelem	$⊢ φ \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.r	$⊢ φ \to \forall y \in [A, B] F (y) \leq F (U)$
7		rolle.u	$⊢ φ \to U \in [A, B]$
8		rolle.n	$⊢ φ \to \neg U \in \{A, B\}$
9	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
10	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
11	1 2 3	ltled	$⊢ φ \to A \leq B$
12		prunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$
13	9 10 11 12	syl3anc	$⊢ φ \to (A, B) \cup \{A, B\} = [A, B]$
14	7 13	eleqtrrd	$⊢ φ \to U \in ((A, B) \cup \{A, B\})$
15		elun	$⊢ U \in ((A, B) \cup \{A, B\}) \leftrightarrow (U \in (A, B) \lor U \in \{A, B\})$
16	14 15	sylib	$⊢ φ \to (U \in (A, B) \lor U \in \{A, B\})$
17	16	ord	$⊢ φ \to (\neg U \in (A, B) \to U \in \{A, B\})$
18	8 17	mt3d	$⊢ φ \to U \in (A, B)$
19		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
20	4 19	syl	$⊢ φ \to F : [A, B] ⟶ ℝ$
21		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
22	1 2 21	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
23		ioossicc	$⊢ (A, B) \subseteq [A, B]$
24	23	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
25	18 5	eleqtrrd	$⊢ φ \to U \in dom F_{ℝ}^{'}$
26		ssralv	$⊢ (A, B) \subseteq [A, B] \to (\forall y \in [A, B] F (y) \leq F (U) \to \forall y \in (A, B) F (y) \leq F (U))$
27	24 6 26	sylc	$⊢ φ \to \forall y \in (A, B) F (y) \leq F (U)$
28	20 22 18 24 25 27	dvferm	$⊢ φ \to F_{ℝ}^{'} (U) = 0$
29		fveqeq2	$⊢ x = U \to (F_{ℝ}^{'} (x) = 0 \leftrightarrow F_{ℝ}^{'} (U) = 0)$
30	29	rspcev	$⊢ (U \in (A, B) \land F_{ℝ}^{'} (U) = 0) \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$
31	18 28 30	syl2anc	$⊢ φ \to \exists x \in (A, B) F_{ℝ}^{'} (x) = 0$

Metamath Proof Explorer

Theorem rollelem

Proof