ftalem7

Description: Lemma for fta . Shift the minimum away from zero by a change of variables. (Contributed by Mario Carneiro, 14-Sep-2014)

	Ref	Expression
Hypotheses	ftalem.1	$⊢ A = coeff (F)$
	ftalem.2	$⊢ N = \deg (F)$
	ftalem.3	$⊢ φ \to F \in Poly (S)$
	ftalem.4	$⊢ φ \to N \in ℕ$
	ftalem7.5	$⊢ φ \to X \in ℂ$
	ftalem7.6	$⊢ φ \to F (X) \neq 0$
Assertion	ftalem7	$⊢ φ \to \neg \forall x \in ℂ \|F (X)\| \leq \|F (x)\|$

Proof

Step	Hyp	Ref	Expression
1		ftalem.1	$⊢ A = coeff (F)$
2		ftalem.2	$⊢ N = \deg (F)$
3		ftalem.3	$⊢ φ \to F \in Poly (S)$
4		ftalem.4	$⊢ φ \to N \in ℕ$
5		ftalem7.5	$⊢ φ \to X \in ℂ$
6		ftalem7.6	$⊢ φ \to F (X) \neq 0$
7		eqid	$⊢ coeff ((z \in ℂ ⟼ F (z + X))) = coeff ((z \in ℂ ⟼ F (z + X)))$
8		eqid	$⊢ \deg ((z \in ℂ ⟼ F (z + X))) = \deg ((z \in ℂ ⟼ F (z + X)))$
9		simpr	$⊢ (φ \land z \in ℂ) \to z \in ℂ$
10	5	adantr	$⊢ (φ \land z \in ℂ) \to X \in ℂ$
11	9 10	addcld	$⊢ (φ \land z \in ℂ) \to z + X \in ℂ$
12		cnex	$⊢ ℂ \in V$
13	12	a1i	$⊢ φ \to ℂ \in V$
14	5	negcld	$⊢ φ \to - X \in ℂ$
15	14	adantr	$⊢ (φ \land z \in ℂ) \to - X \in ℂ$
16		df-idp	$⊢ X^{p} = {I ↾}_{ℂ}$
17		mptresid	$⊢ {I ↾}_{ℂ} = (z \in ℂ ⟼ z)$
18	16 17	eqtri	$⊢ X^{p} = (z \in ℂ ⟼ z)$
19	18	a1i	$⊢ φ \to X^{p} = (z \in ℂ ⟼ z)$
20		fconstmpt	$⊢ ℂ \times \{- X\} = (z \in ℂ ⟼ - X)$
21	20	a1i	$⊢ φ \to ℂ \times \{- X\} = (z \in ℂ ⟼ - X)$
22	13 9 15 19 21	offval2	$⊢ φ \to X^{p} -_{f} (ℂ \times \{- X\}) = (z \in ℂ ⟼ z - (- X))$
23		id	$⊢ z \in ℂ \to z \in ℂ$
24		subneg	$⊢ (z \in ℂ \land X \in ℂ) \to z - (- X) = z + X$
25	23 5 24	syl2anr	$⊢ (φ \land z \in ℂ) \to z - (- X) = z + X$
26	25	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ z - (- X)) = (z \in ℂ ⟼ z + X)$
27	22 26	eqtrd	$⊢ φ \to X^{p} -_{f} (ℂ \times \{- X\}) = (z \in ℂ ⟼ z + X)$
28		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
29	3 28	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
30	29	feqmptd	$⊢ φ \to F = (y \in ℂ ⟼ F (y))$
31		fveq2	$⊢ y = z + X \to F (y) = F (z + X)$
32	11 27 30 31	fmptco	$⊢ φ \to F \circ (X^{p} -_{f} (ℂ \times \{- X\})) = (z \in ℂ ⟼ F (z + X))$
33		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
34	33 3	sselid	$⊢ φ \to F \in Poly (ℂ)$
35		eqid	$⊢ X^{p} -_{f} (ℂ \times \{- X\}) = X^{p} -_{f} (ℂ \times \{- X\})$
36	35	plyremlem	$⊢ - X \in ℂ \to (X^{p} -_{f} (ℂ \times \{- X\}) \in Poly (ℂ) \land \deg (X^{p} -_{f} (ℂ \times \{- X\})) = 1 \land {(X^{p} -_{f} (ℂ \times \{- X\}))}^{-1} [\{0\}] = \{- X\})$
37	14 36	syl	$⊢ φ \to (X^{p} -_{f} (ℂ \times \{- X\}) \in Poly (ℂ) \land \deg (X^{p} -_{f} (ℂ \times \{- X\})) = 1 \land {(X^{p} -_{f} (ℂ \times \{- X\}))}^{-1} [\{0\}] = \{- X\})$
38	37	simp1d	$⊢ φ \to X^{p} -_{f} (ℂ \times \{- X\}) \in Poly (ℂ)$
39		addcl	$⊢ (z \in ℂ \land w \in ℂ) \to z + w \in ℂ$
40	39	adantl	$⊢ (φ \land (z \in ℂ \land w \in ℂ)) \to z + w \in ℂ$
41		mulcl	$⊢ (z \in ℂ \land w \in ℂ) \to z w \in ℂ$
42	41	adantl	$⊢ (φ \land (z \in ℂ \land w \in ℂ)) \to z w \in ℂ$
43	34 38 40 42	plyco	$⊢ φ \to F \circ (X^{p} -_{f} (ℂ \times \{- X\})) \in Poly (ℂ)$
44	32 43	eqeltrrd	$⊢ φ \to (z \in ℂ ⟼ F (z + X)) \in Poly (ℂ)$
45	32	fveq2d	$⊢ φ \to \deg (F \circ (X^{p} -_{f} (ℂ \times \{- X\}))) = \deg ((z \in ℂ ⟼ F (z + X)))$
46		eqid	$⊢ \deg (X^{p} -_{f} (ℂ \times \{- X\})) = \deg (X^{p} -_{f} (ℂ \times \{- X\}))$
47	2 46 34 38	dgrco	$⊢ φ \to \deg (F \circ (X^{p} -_{f} (ℂ \times \{- X\}))) = N \deg (X^{p} -_{f} (ℂ \times \{- X\}))$
48	37	simp2d	$⊢ φ \to \deg (X^{p} -_{f} (ℂ \times \{- X\})) = 1$
49		1nn	$⊢ 1 \in ℕ$
50	48 49	eqeltrdi	$⊢ φ \to \deg (X^{p} -_{f} (ℂ \times \{- X\})) \in ℕ$
51	4 50	nnmulcld	$⊢ φ \to N \deg (X^{p} -_{f} (ℂ \times \{- X\})) \in ℕ$
52	47 51	eqeltrd	$⊢ φ \to \deg (F \circ (X^{p} -_{f} (ℂ \times \{- X\}))) \in ℕ$
53	45 52	eqeltrrd	$⊢ φ \to \deg ((z \in ℂ ⟼ F (z + X))) \in ℕ$
54		0cn	$⊢ 0 \in ℂ$
55		fvoveq1	$⊢ z = 0 \to F (z + X) = F (0 + X)$
56		eqid	$⊢ (z \in ℂ ⟼ F (z + X)) = (z \in ℂ ⟼ F (z + X))$
57		fvex	$⊢ F (0 + X) \in V$
58	55 56 57	fvmpt	$⊢ 0 \in ℂ \to (z \in ℂ ⟼ F (z + X)) (0) = F (0 + X)$
59	54 58	ax-mp	$⊢ (z \in ℂ ⟼ F (z + X)) (0) = F (0 + X)$
60	5	addlidd	$⊢ φ \to 0 + X = X$
61	60	fveq2d	$⊢ φ \to F (0 + X) = F (X)$
62	59 61	eqtrid	$⊢ φ \to (z \in ℂ ⟼ F (z + X)) (0) = F (X)$
63	62 6	eqnetrd	$⊢ φ \to (z \in ℂ ⟼ F (z + X)) (0) \neq 0$
64	7 8 44 53 63	ftalem6	$⊢ φ \to \exists y \in ℂ \|(z \in ℂ ⟼ F (z + X)) (y)\| < \|(z \in ℂ ⟼ F (z + X)) (0)\|$
65		id	$⊢ y \in ℂ \to y \in ℂ$
66		addcl	$⊢ (y \in ℂ \land X \in ℂ) \to y + X \in ℂ$
67	65 5 66	syl2anr	$⊢ (φ \land y \in ℂ) \to y + X \in ℂ$
68		fvoveq1	$⊢ z = y \to F (z + X) = F (y + X)$
69		fvex	$⊢ F (y + X) \in V$
70	68 56 69	fvmpt	$⊢ y \in ℂ \to (z \in ℂ ⟼ F (z + X)) (y) = F (y + X)$
71	70	adantl	$⊢ (φ \land y \in ℂ) \to (z \in ℂ ⟼ F (z + X)) (y) = F (y + X)$
72	71	fveq2d	$⊢ (φ \land y \in ℂ) \to \|(z \in ℂ ⟼ F (z + X)) (y)\| = \|F (y + X)\|$
73	62	adantr	$⊢ (φ \land y \in ℂ) \to (z \in ℂ ⟼ F (z + X)) (0) = F (X)$
74	73	fveq2d	$⊢ (φ \land y \in ℂ) \to \|(z \in ℂ ⟼ F (z + X)) (0)\| = \|F (X)\|$
75	72 74	breq12d	$⊢ (φ \land y \in ℂ) \to (\|(z \in ℂ ⟼ F (z + X)) (y)\| < \|(z \in ℂ ⟼ F (z + X)) (0)\| \leftrightarrow \|F (y + X)\| < \|F (X)\|)$
76	29	adantr	$⊢ (φ \land y \in ℂ) \to F : ℂ ⟶ ℂ$
77	76 67	ffvelcdmd	$⊢ (φ \land y \in ℂ) \to F (y + X) \in ℂ$
78	77	abscld	$⊢ (φ \land y \in ℂ) \to \|F (y + X)\| \in ℝ$
79	29 5	ffvelcdmd	$⊢ φ \to F (X) \in ℂ$
80	79	abscld	$⊢ φ \to \|F (X)\| \in ℝ$
81	80	adantr	$⊢ (φ \land y \in ℂ) \to \|F (X)\| \in ℝ$
82	78 81	ltnled	$⊢ (φ \land y \in ℂ) \to (\|F (y + X)\| < \|F (X)\| \leftrightarrow \neg \|F (X)\| \leq \|F (y + X)\|)$
83	75 82	bitrd	$⊢ (φ \land y \in ℂ) \to (\|(z \in ℂ ⟼ F (z + X)) (y)\| < \|(z \in ℂ ⟼ F (z + X)) (0)\| \leftrightarrow \neg \|F (X)\| \leq \|F (y + X)\|)$
84	83	biimpd	$⊢ (φ \land y \in ℂ) \to (\|(z \in ℂ ⟼ F (z + X)) (y)\| < \|(z \in ℂ ⟼ F (z + X)) (0)\| \to \neg \|F (X)\| \leq \|F (y + X)\|)$
85		2fveq3	$⊢ x = y + X \to \|F (x)\| = \|F (y + X)\|$
86	85	breq2d	$⊢ x = y + X \to (\|F (X)\| \leq \|F (x)\| \leftrightarrow \|F (X)\| \leq \|F (y + X)\|)$
87	86	notbid	$⊢ x = y + X \to (\neg \|F (X)\| \leq \|F (x)\| \leftrightarrow \neg \|F (X)\| \leq \|F (y + X)\|)$
88	87	rspcev	$⊢ (y + X \in ℂ \land \neg \|F (X)\| \leq \|F (y + X)\|) \to \exists x \in ℂ \neg \|F (X)\| \leq \|F (x)\|$
89	67 84 88	syl6an	$⊢ (φ \land y \in ℂ) \to (\|(z \in ℂ ⟼ F (z + X)) (y)\| < \|(z \in ℂ ⟼ F (z + X)) (0)\| \to \exists x \in ℂ \neg \|F (X)\| \leq \|F (x)\|)$
90	89	rexlimdva	$⊢ φ \to (\exists y \in ℂ \|(z \in ℂ ⟼ F (z + X)) (y)\| < \|(z \in ℂ ⟼ F (z + X)) (0)\| \to \exists x \in ℂ \neg \|F (X)\| \leq \|F (x)\|)$
91	64 90	mpd	$⊢ φ \to \exists x \in ℂ \neg \|F (X)\| \leq \|F (x)\|$
92		rexnal	$⊢ \exists x \in ℂ \neg \|F (X)\| \leq \|F (x)\| \leftrightarrow \neg \forall x \in ℂ \|F (X)\| \leq \|F (x)\|$
93	91 92	sylib	$⊢ φ \to \neg \forall x \in ℂ \|F (X)\| \leq \|F (x)\|$

Metamath Proof Explorer

Theorem ftalem7

Proof