Theorem ftalem6

Description: Lemma for fta : Discharge the auxiliary variables in ftalem5 . (Contributed by Mario Carneiro, 20-Sep-2014) (Proof shortened by AV, 28-Sep-2020)

	Ref	Expression
Hypotheses	ftalem.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
	ftalem.2	$$⊢N=\mathrm{deg}\left(F\right)$$
	ftalem.3	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
	ftalem.4	$$⊢\phi \to N\in \mathbb{N}$$
	ftalem6.5	$$⊢\phi \to F\left(0\right)\ne 0$$
Assertion	ftalem6	$$⊢\phi \to \exists x\in ℂ\left|F\left(x\right)\right|<\left|F\left(0\right)\right|$$

Proof

Step	Hyp	Ref	Expression
1		ftalem.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
2		ftalem.2	$$⊢N=\mathrm{deg}\left(F\right)$$
3		ftalem.3	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
4		ftalem.4	$$⊢\phi \to N\in \mathbb{N}$$
5		ftalem6.5	$$⊢\phi \to F\left(0\right)\ne 0$$
6		fveq2	$$⊢k=n\to A\left(k\right)=A\left(n\right)$$
7	6	neeq1d	$$⊢k=n\to \left(A\left(k\right)\ne 0\leftrightarrow A\left(n\right)\ne 0\right)$$
8	7	cbvrabv	$$⊢\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\}=\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}$$
9	8	infeq1i	$$⊢inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)=inf\left(\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\},ℝ,<\right)$$
10		eqid	$$⊢{\left(-\left(\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}={\left(-\left(\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}$$
11		fveq2	$$⊢r=s\to A\left(r\right)=A\left(s\right)$$
12		oveq2	$$⊢r=s\to {\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r={\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^s$$
13	11 12	oveq12d	$$⊢r=s\to A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r=A\left(s\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^s$$
14	13	fveq2d	$$⊢r=s\to \left|A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r\right|=\left|A\left(s\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^s\right|$$
15	14	cbvsumv	$$⊢\sum _{r=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r\right|=\sum _{s=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(s\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^s\right|$$
16	15	oveq1i	$$⊢\sum _{r=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r\right|+1=\sum _{s=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(s\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^s\right|+1$$
17	16	oveq2i	$$⊢\frac{\left|F\left(0\right)\right|}{\sum _{r=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r\right|+1}=\frac{\left|F\left(0\right)\right|}{\sum _{s=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(s\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^s\right|+1}$$
18		eqid	$$⊢if\left(1\le \frac{\left|F\left(0\right)\right|}{\sum _{r=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r\right|+1},1,\frac{\left|F\left(0\right)\right|}{\sum _{r=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r\right|+1}\right)=if\left(1\le \frac{\left|F\left(0\right)\right|}{\sum _{r=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r\right|+1},1,\frac{\left|F\left(0\right)\right|}{\sum _{r=inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)+1}^N\left|A\left(r\right){\left({\left(-\frac{F\left(0\right)}{A\left(inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)\right)}\right)}^{\frac{1}{inf\left(\left\{k\in \mathbb{N}|A\left(k\right)\ne 0\right\},ℝ,<\right)}}\right)}^r\right|+1}\right)$$
19	1 2 3 4 5 9 10 17 18	ftalem5	$$⊢\phi \to \exists x\in ℂ\left|F\left(x\right)\right|<\left|F\left(0\right)\right|$$