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	$⊢ φ \to A \in ℝ$
	dveq0.b	$⊢ φ \to B \in ℝ$
	dveq0.c	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
	dveq0.d	$⊢ φ \to ℝ D F = (A, B) \times \{0\}$
Assertion	dveq0	$⊢ φ \to F = [A, B] \times \{F (A)\}$

Proof

Step	Hyp	Ref	Expression
1		dveq0.a	$⊢ φ \to A \in ℝ$
2		dveq0.b	$⊢ φ \to B \in ℝ$
3		dveq0.c	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
4		dveq0.d	$⊢ φ \to ℝ D F = (A, B) \times \{0\}$
5		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
6	3 5	syl	$⊢ φ \to F : [A, B] ⟶ ℂ$
7	6	ffnd	$⊢ φ \to F Fn [A, B]$
8		fvex	$⊢ F (A) \in V$
9		fnconstg	$⊢ F (A) \in V \to ([A, B] \times \{F (A)\}) Fn [A, B]$
10	8 9	mp1i	$⊢ φ \to ([A, B] \times \{F (A)\}) Fn [A, B]$
11	8	fvconst2	$⊢ x \in [A, B] \to ([A, B] \times \{F (A)\}) (x) = F (A)$
12	11	adantl	$⊢ (φ \land x \in [A, B]) \to ([A, B] \times \{F (A)\}) (x) = F (A)$
13	6	adantr	$⊢ (φ \land x \in [A, B]) \to F : [A, B] ⟶ ℂ$
14	1	adantr	$⊢ (φ \land x \in [A, B]) \to A \in ℝ$
15	14	rexrd	$⊢ (φ \land x \in [A, B]) \to A \in ℝ^{*}$
16	2	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
17	16	rexrd	$⊢ (φ \land x \in [A, B]) \to B \in ℝ^{*}$
18		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
19	1 2 18	syl2anc	$⊢ φ \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
20	19	biimpa	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land A \leq x \land x \leq B)$
21	20	simp1d	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
22	20	simp2d	$⊢ (φ \land x \in [A, B]) \to A \leq x$
23	20	simp3d	$⊢ (φ \land x \in [A, B]) \to x \leq B$
24	14 21 16 22 23	letrd	$⊢ (φ \land x \in [A, B]) \to A \leq B$
25		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
26	15 17 24 25	syl3anc	$⊢ (φ \land x \in [A, B]) \to A \in [A, B]$
27	13 26	ffvelrnd	$⊢ (φ \land x \in [A, B]) \to F (A) \in ℂ$
28	6	ffvelrnda	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℂ$
29	27 28	subcld	$⊢ (φ \land x \in [A, B]) \to F (A) - F (x) \in ℂ$
30		simpr	$⊢ (φ \land x \in [A, B]) \to x \in [A, B]$
31	26 30	jca	$⊢ (φ \land x \in [A, B]) \to (A \in [A, B] \land x \in [A, B])$
32	4	dmeqd	$⊢ φ \to dom F_{ℝ}^{'} = dom ((A, B) \times \{0\})$
33		c0ex	$⊢ 0 \in V$
34	33	snnz	$⊢ \{0\} \neq \emptyset$
35		dmxp	$⊢ \{0\} \neq \emptyset \to dom ((A, B) \times \{0\}) = (A, B)$
36	34 35	ax-mp	$⊢ dom ((A, B) \times \{0\}) = (A, B)$
37	32 36	eqtrdi	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
38		0red	$⊢ φ \to 0 \in ℝ$
39	4	fveq1d	$⊢ φ \to F_{ℝ}^{'} (y) = ((A, B) \times \{0\}) (y)$
40	33	fvconst2	$⊢ y \in (A, B) \to ((A, B) \times \{0\}) (y) = 0$
41	39 40	sylan9eq	$⊢ (φ \land y \in (A, B)) \to F_{ℝ}^{'} (y) = 0$
42	41	abs00bd	$⊢ (φ \land y \in (A, B)) \to \|F_{ℝ}^{'} (y)\| = 0$
43		0le0	$⊢ 0 \leq 0$
44	42 43	eqbrtrdi	$⊢ (φ \land y \in (A, B)) \to \|F_{ℝ}^{'} (y)\| \leq 0$
45	1 2 3 37 38 44	dvlip	$⊢ (φ \land (A \in [A, B] \land x \in [A, B])) \to \|F (A) - F (x)\| \leq 0 \cdot \|A - x\|$
46	31 45	syldan	$⊢ (φ \land x \in [A, B]) \to \|F (A) - F (x)\| \leq 0 \cdot \|A - x\|$
47	14	recnd	$⊢ (φ \land x \in [A, B]) \to A \in ℂ$
48	21	recnd	$⊢ (φ \land x \in [A, B]) \to x \in ℂ$
49	47 48	subcld	$⊢ (φ \land x \in [A, B]) \to A - x \in ℂ$
50	49	abscld	$⊢ (φ \land x \in [A, B]) \to \|A - x\| \in ℝ$
51	50	recnd	$⊢ (φ \land x \in [A, B]) \to \|A - x\| \in ℂ$
52	51	mul02d	$⊢ (φ \land x \in [A, B]) \to 0 \cdot \|A - x\| = 0$
53	46 52	breqtrd	$⊢ (φ \land x \in [A, B]) \to \|F (A) - F (x)\| \leq 0$
54	29	absge0d	$⊢ (φ \land x \in [A, B]) \to 0 \leq \|F (A) - F (x)\|$
55	29	abscld	$⊢ (φ \land x \in [A, B]) \to \|F (A) - F (x)\| \in ℝ$
56		0re	$⊢ 0 \in ℝ$
57		letri3	$⊢ (\|F (A) - F (x)\| \in ℝ \land 0 \in ℝ) \to (\|F (A) - F (x)\| = 0 \leftrightarrow (\|F (A) - F (x)\| \leq 0 \land 0 \leq \|F (A) - F (x)\|))$
58	55 56 57	sylancl	$⊢ (φ \land x \in [A, B]) \to (\|F (A) - F (x)\| = 0 \leftrightarrow (\|F (A) - F (x)\| \leq 0 \land 0 \leq \|F (A) - F (x)\|))$
59	53 54 58	mpbir2and	$⊢ (φ \land x \in [A, B]) \to \|F (A) - F (x)\| = 0$
60	29 59	abs00d	$⊢ (φ \land x \in [A, B]) \to F (A) - F (x) = 0$
61	27 28 60	subeq0d	$⊢ (φ \land x \in [A, B]) \to F (A) = F (x)$
62	12 61	eqtr2d	$⊢ (φ \land x \in [A, B]) \to F (x) = ([A, B] \times \{F (A)\}) (x)$
63	7 10 62	eqfnfvd	$⊢ φ \to F = [A, B] \times \{F (A)\}$

Metamath Proof Explorer

Theorem dveq0

Proof