dvferm

Description: Fermat's theorem on stationary points. A point U which is a local maximum has derivative equal to zero. (Contributed by Mario Carneiro, 1-Sep-2014)

	Ref	Expression
Hypotheses	dvferm.a	$⊢ φ \to F : X ⟶ ℝ$
	dvferm.b	$⊢ φ \to X \subseteq ℝ$
	dvferm.u	$⊢ φ \to U \in (A, B)$
	dvferm.s	$⊢ φ \to (A, B) \subseteq X$
	dvferm.d	$⊢ φ \to U \in dom F_{ℝ}^{'}$
	dvferm.r	$⊢ φ \to \forall y \in (A, B) F (y) \leq F (U)$
Assertion	dvferm	$⊢ φ \to F_{ℝ}^{'} (U) = 0$

Proof

Step	Hyp	Ref	Expression
1		dvferm.a	$⊢ φ \to F : X ⟶ ℝ$
2		dvferm.b	$⊢ φ \to X \subseteq ℝ$
3		dvferm.u	$⊢ φ \to U \in (A, B)$
4		dvferm.s	$⊢ φ \to (A, B) \subseteq X$
5		dvferm.d	$⊢ φ \to U \in dom F_{ℝ}^{'}$
6		dvferm.r	$⊢ φ \to \forall y \in (A, B) F (y) \leq F (U)$
7		ne0i	$⊢ U \in (A, B) \to (A, B) \neq \emptyset$
8		ndmioo	$⊢ \neg (A \in ℝ^{} \land B \in ℝ^{}) \to (A, B) = \emptyset$
9	8	necon1ai	$⊢ (A, B) \neq \emptyset \to (A \in ℝ^{} \land B \in ℝ^{})$
10	3 7 9	3syl	$⊢ φ \to (A \in ℝ^{} \land B \in ℝ^{})$
11	10	simpld	$⊢ φ \to A \in ℝ^{*}$
12		ioossre	$⊢ (A, B) \subseteq ℝ$
13	12 3	sseldi	$⊢ φ \to U \in ℝ$
14	13	rexrd	$⊢ φ \to U \in ℝ^{*}$
15		eliooord	$⊢ U \in (A, B) \to (A < U \land U < B)$
16	3 15	syl	$⊢ φ \to (A < U \land U < B)$
17	16	simpld	$⊢ φ \to A < U$
18	11 14 17	xrltled	$⊢ φ \to A \leq U$
19		iooss1	$⊢ (A \in ℝ^{*} \land A \leq U) \to (U, B) \subseteq (A, B)$
20	11 18 19	syl2anc	$⊢ φ \to (U, B) \subseteq (A, B)$
21		ssralv	$⊢ (U, B) \subseteq (A, B) \to (\forall y \in (A, B) F (y) \leq F (U) \to \forall y \in (U, B) F (y) \leq F (U))$
22	20 6 21	sylc	$⊢ φ \to \forall y \in (U, B) F (y) \leq F (U)$
23	1 2 3 4 5 22	dvferm1	$⊢ φ \to F_{ℝ}^{'} (U) \leq 0$
24	10	simprd	$⊢ φ \to B \in ℝ^{*}$
25	16	simprd	$⊢ φ \to U < B$
26	14 24 25	xrltled	$⊢ φ \to U \leq B$
27		iooss2	$⊢ (B \in ℝ^{*} \land U \leq B) \to (A, U) \subseteq (A, B)$
28	24 26 27	syl2anc	$⊢ φ \to (A, U) \subseteq (A, B)$
29		ssralv	$⊢ (A, U) \subseteq (A, B) \to (\forall y \in (A, B) F (y) \leq F (U) \to \forall y \in (A, U) F (y) \leq F (U))$
30	28 6 29	sylc	$⊢ φ \to \forall y \in (A, U) F (y) \leq F (U)$
31	1 2 3 4 5 30	dvferm2	$⊢ φ \to 0 \leq F_{ℝ}^{'} (U)$
32		dvfre	$⊢ (F : X ⟶ ℝ \land X \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
33	1 2 32	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
34	33 5	ffvelrnd	$⊢ φ \to F_{ℝ}^{'} (U) \in ℝ$
35		0re	$⊢ 0 \in ℝ$
36		letri3	$⊢ (F_{ℝ}^{'} (U) \in ℝ \land 0 \in ℝ) \to (F_{ℝ}^{'} (U) = 0 \leftrightarrow (F_{ℝ}^{'} (U) \leq 0 \land 0 \leq F_{ℝ}^{'} (U)))$
37	34 35 36	sylancl	$⊢ φ \to (F_{ℝ}^{'} (U) = 0 \leftrightarrow (F_{ℝ}^{'} (U) \leq 0 \land 0 \leq F_{ℝ}^{'} (U)))$
38	23 31 37	mpbir2and	$⊢ φ \to F_{ℝ}^{'} (U) = 0$

Metamath Proof Explorer

Theorem dvferm

Proof