This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dveq0

Description: If a continuous function has zero derivative at all points on the interior of a closed interval, then it must be a constant function. (Contributed by Mario Carneiro, 2-Sep-2014) (Proof shortened by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses dveq0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dveq0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dveq0.c ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
dveq0.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ( 𝐴 (,) 𝐵 ) × { 0 } ) )
Assertion dveq0 ( 𝜑 → 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) )

Proof

Step Hyp Ref Expression
1 dveq0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dveq0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dveq0.c ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
4 dveq0.d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ( 𝐴 (,) 𝐵 ) × { 0 } ) )
5 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
6 3 5 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
7 6 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 [,] 𝐵 ) )
8 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
9 fnconstg ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ V → ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) Fn ( 𝐴 [,] 𝐵 ) )
10 8 9 mp1i ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) Fn ( 𝐴 [,] 𝐵 ) )
11 8 fvconst2 ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
13 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
14 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ )
15 14 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℝ* )
16 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
17 16 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ* )
18 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
19 1 2 18 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
20 19 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
21 20 simp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℝ )
22 20 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑥 )
23 20 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
24 14 21 16 22 23 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝐵 )
25 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
26 15 17 24 25 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
27 13 26 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
28 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
29 27 28 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
31 26 30 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) )
32 4 dmeqd ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = dom ( ( 𝐴 (,) 𝐵 ) × { 0 } ) )
33 c0ex ⊢ 0 ∈ V
34 33 snnz ⊢ { 0 } ≠ ∅
35 dmxp ⊢ ( { 0 } ≠ ∅ → dom ( ( 𝐴 (,) 𝐵 ) × { 0 } ) = ( 𝐴 (,) 𝐵 ) )
36 34 35 ax-mp ⊢ dom ( ( 𝐴 (,) 𝐵 ) × { 0 } ) = ( 𝐴 (,) 𝐵 )
37 32 36 eqtrdi ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
38 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
39 4 fveq1d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = ( ( ( 𝐴 (,) 𝐵 ) × { 0 } ) ‘ 𝑦 ) )
40 33 fvconst2 ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( 𝐴 (,) 𝐵 ) × { 0 } ) ‘ 𝑦 ) = 0 )
41 39 40 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑦 ) = 0 )
42 41 abs00bd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) = 0 )
43 0le0 ⊢ 0 ≤ 0
44 42 43 eqbrtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ 0 )
45 1 2 3 37 38 44 dvlip ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 0 · ( abs ‘ ( 𝐴 − 𝑥 ) ) ) )
46 31 45 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ ( 0 · ( abs ‘ ( 𝐴 − 𝑥 ) ) ) )
47 14 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ∈ ℂ )
48 21 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℂ )
49 47 48 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 − 𝑥 ) ∈ ℂ )
50 49 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( 𝐴 − 𝑥 ) ) ∈ ℝ )
51 50 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( 𝐴 − 𝑥 ) ) ∈ ℂ )
52 51 mul02d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 0 · ( abs ‘ ( 𝐴 − 𝑥 ) ) ) = 0 )
53 46 52 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ 0 )
54 29 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) )
55 29 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ )
56 0re ⊢ 0 ∈ ℝ
57 letri3 ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) = 0 ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
58 55 56 57 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) = 0 ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ≤ 0 ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
59 53 54 58 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) ) = 0 )
60 29 59 abs00d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐹 ‘ 𝑥 ) ) = 0 )
61 27 28 60 subeq0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝑥 ) )
62 12 61 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ( ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ‘ 𝑥 ) )
63 7 10 62 eqfnfvd ⊢ ( 𝜑 → 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) )