Theorem 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	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
	dvferm.b	⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
	dvferm.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 (,) 𝐵 ) )
	dvferm.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝑋 )
	dvferm.d	⊢ ( 𝜑 → 𝑈 ∈ dom ( ℝ D 𝐹 ) )
	dvferm.r	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
Assertion	dvferm	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		dvferm.a	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
2		dvferm.b	⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
3		dvferm.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐴 (,) 𝐵 ) )
4		dvferm.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝑋 )
5		dvferm.d	⊢ ( 𝜑 → 𝑈 ∈ dom ( ℝ D 𝐹 ) )
6		dvferm.r	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
7		ne0i	⊢ ( 𝑈 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
8		ndmioo	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 (,) 𝐵 ) = ∅ )
9	8	necon1ai	⊢ ( ( 𝐴 (,) 𝐵 ) ≠ ∅ → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
10	3 7 9	3syl	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
11	10	simpld	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
12		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
13	12 3	sselid	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
14	13	rexrd	⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
15		eliooord	⊢ ( 𝑈 ∈ ( 𝐴 (,) 𝐵 ) → ( 𝐴 < 𝑈 ∧ 𝑈 < 𝐵 ) )
16	3 15	syl	⊢ ( 𝜑 → ( 𝐴 < 𝑈 ∧ 𝑈 < 𝐵 ) )
17	16	simpld	⊢ ( 𝜑 → 𝐴 < 𝑈 )
18	11 14 17	xrltled	⊢ ( 𝜑 → 𝐴 ≤ 𝑈 )
19		iooss1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑈 ) → ( 𝑈 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
20	11 18 19	syl2anc	⊢ ( 𝜑 → ( 𝑈 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
21		ssralv	⊢ ( ( 𝑈 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) → ∀ 𝑦 ∈ ( 𝑈 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) ) )
22	20 6 21	sylc	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑈 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
23	1 2 3 4 5 22	dvferm1	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ≤ 0 )
24	10	simprd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
25	16	simprd	⊢ ( 𝜑 → 𝑈 < 𝐵 )
26	14 24 25	xrltled	⊢ ( 𝜑 → 𝑈 ≤ 𝐵 )
27		iooss2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑈 ≤ 𝐵 ) → ( 𝐴 (,) 𝑈 ) ⊆ ( 𝐴 (,) 𝐵 ) )
28	24 26 27	syl2anc	⊢ ( 𝜑 → ( 𝐴 (,) 𝑈 ) ⊆ ( 𝐴 (,) 𝐵 ) )
29		ssralv	⊢ ( ( 𝐴 (,) 𝑈 ) ⊆ ( 𝐴 (,) 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝑈 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) ) )
30	28 6 29	sylc	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝑈 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑈 ) )
31	1 2 3 4 5 30	dvferm2	⊢ ( 𝜑 → 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) )
32		dvfre	⊢ ( ( 𝐹 : 𝑋 ⟶ ℝ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
33	1 2 32	syl2anc	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
34	33 5	ffvelcdmd	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ )
35		0re	⊢ 0 ∈ ℝ
36		letri3	⊢ ( ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) = 0 ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ≤ 0 ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
37	34 35 36	sylancl	⊢ ( 𝜑 → ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) = 0 ↔ ( ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ≤ 0 ∧ 0 ≤ ( ( ℝ D 𝐹 ) ‘ 𝑈 ) ) ) )
38	23 31 37	mpbir2and	⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑈 ) = 0 )