Theorem ftalem4

Description: Lemma for fta : Closure of the auxiliary variables for ftalem5 . (Contributed by Mario Carneiro, 20-Sep-2014) (Revised 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}$$
	ftalem4.5	$$⊢\phi \to F\left(0\right)\ne 0$$
	ftalem4.6	$$⊢K=inf\left(\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\},ℝ,<\right)$$
	ftalem4.7	$$⊢T={\left(-\left(\frac{F\left(0\right)}{A\left(K\right)}\right)\right)}^{\frac{1}{K}}$$
	ftalem4.8	$$⊢U=\frac{\left|F\left(0\right)\right|}{\sum _{k=K+1}^N\left|A\left(k\right)T^k\right|+1}$$
	ftalem4.9	$$⊢X=if\left(1\le U,1,U\right)$$
Assertion	ftalem4	$$⊢\phi \to \left(\left(K\in \mathbb{N}\wedge A\left(K\right)\ne 0\right)\wedge \left(T\in ℂ\wedge U\in {ℝ}^{+}\wedge X\in {ℝ}^{+}\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		ftalem4.5	$$⊢\phi \to F\left(0\right)\ne 0$$
6		ftalem4.6	$$⊢K=inf\left(\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\},ℝ,<\right)$$
7		ftalem4.7	$$⊢T={\left(-\left(\frac{F\left(0\right)}{A\left(K\right)}\right)\right)}^{\frac{1}{K}}$$
8		ftalem4.8	$$⊢U=\frac{\left|F\left(0\right)\right|}{\sum _{k=K+1}^N\left|A\left(k\right)T^k\right|+1}$$
9		ftalem4.9	$$⊢X=if\left(1\le U,1,U\right)$$
10		ssrab2	$$⊢\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}\subseteq \mathbb{N}$$
11		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
12	10 11	sseqtri	$$⊢\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}\subseteq {\mathbb{Z}}_{\ge 1}$$
13		fveq2	$$⊢n=N\to A\left(n\right)=A\left(N\right)$$
14	13	neeq1d	$$⊢n=N\to \left(A\left(n\right)\ne 0\leftrightarrow A\left(N\right)\ne 0\right)$$
15	4	nnne0d	$$⊢\phi \to N\ne 0$$
16	2 1	dgreq0	$$⊢F\in \mathrm{Poly}\left(S\right)\to \left(F=0_{𝑝}\leftrightarrow A\left(N\right)=0\right)$$
17	3 16	syl	$$⊢\phi \to \left(F=0_{𝑝}\leftrightarrow A\left(N\right)=0\right)$$
18		fveq2	$$⊢F=0_{𝑝}\to \mathrm{deg}\left(F\right)=\mathrm{deg}\left(0_{𝑝}\right)$$
19		dgr0	$$⊢\mathrm{deg}\left(0_{𝑝}\right)=0$$
20	18 19	eqtrdi	$$⊢F=0_{𝑝}\to \mathrm{deg}\left(F\right)=0$$
21	2 20	eqtrid	$$⊢F=0_{𝑝}\to N=0$$
22	17 21	biimtrrdi	$$⊢\phi \to \left(A\left(N\right)=0\to N=0\right)$$
23	22	necon3d	$$⊢\phi \to \left(N\ne 0\to A\left(N\right)\ne 0\right)$$
24	15 23	mpd	$$⊢\phi \to A\left(N\right)\ne 0$$
25	14 4 24	elrabd	$$⊢\phi \to N\in \left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}$$
26	25	ne0d	$$⊢\phi \to \left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}\ne \varnothing$$
27		infssuzcl	$$⊢\left(\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}\subseteq {\mathbb{Z}}_{\ge 1}\wedge \left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}\ne \varnothing \right)\to inf\left(\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\},ℝ,<\right)\in \left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}$$
28	12 26 27	sylancr	$$⊢\phi \to inf\left(\left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\},ℝ,<\right)\in \left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}$$
29	6 28	eqeltrid	$$⊢\phi \to K\in \left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}$$
30		fveq2	$$⊢n=K\to A\left(n\right)=A\left(K\right)$$
31	30	neeq1d	$$⊢n=K\to \left(A\left(n\right)\ne 0\leftrightarrow A\left(K\right)\ne 0\right)$$
32	31	elrab	$$⊢K\in \left\{n\in \mathbb{N}|A\left(n\right)\ne 0\right\}\leftrightarrow \left(K\in \mathbb{N}\wedge A\left(K\right)\ne 0\right)$$
33	29 32	sylib	$$⊢\phi \to \left(K\in \mathbb{N}\wedge A\left(K\right)\ne 0\right)$$
34		plyf	$$⊢F\in \mathrm{Poly}\left(S\right)\to F:ℂ⟶ℂ$$
35	3 34	syl	$$⊢\phi \to F:ℂ⟶ℂ$$
36		0cn	$$⊢0\in ℂ$$
37		ffvelcdm	$$⊢\left(F:ℂ⟶ℂ\wedge 0\in ℂ\right)\to F\left(0\right)\in ℂ$$
38	35 36 37	sylancl	$$⊢\phi \to F\left(0\right)\in ℂ$$
39	1	coef3	$$⊢F\in \mathrm{Poly}\left(S\right)\to A:{\mathbb{N}}_0⟶ℂ$$
40	3 39	syl	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
41	33	simpld	$$⊢\phi \to K\in \mathbb{N}$$
42	41	nnnn0d	$$⊢\phi \to K\in {\mathbb{N}}_0$$
43	40 42	ffvelcdmd	$$⊢\phi \to A\left(K\right)\in ℂ$$
44	33	simprd	$$⊢\phi \to A\left(K\right)\ne 0$$
45	38 43 44	divcld	$$⊢\phi \to \frac{F\left(0\right)}{A\left(K\right)}\in ℂ$$
46	45	negcld	$$⊢\phi \to -\frac{F\left(0\right)}{A\left(K\right)}\in ℂ$$
47	41	nnrecred	$$⊢\phi \to \frac{1}{K}\in ℝ$$
48	47	recnd	$$⊢\phi \to \frac{1}{K}\in ℂ$$
49	46 48	cxpcld	$$⊢\phi \to {\left(-\left(\frac{F\left(0\right)}{A\left(K\right)}\right)\right)}^{\frac{1}{K}}\in ℂ$$
50	7 49	eqeltrid	$$⊢\phi \to T\in ℂ$$
51	38 5	absrpcld	$$⊢\phi \to \left|F\left(0\right)\right|\in {ℝ}^{+}$$
52		fzfid	$$⊢\phi \to \left(K+1\dots N\right)\in \mathrm{Fin}$$
53		peano2nn0	$$⊢K\in {\mathbb{N}}_0\to K+1\in {\mathbb{N}}_0$$
54	42 53	syl	$$⊢\phi \to K+1\in {\mathbb{N}}_0$$
55		elfzuz	$$⊢k\in \left(K+1\dots N\right)\to k\in {\mathbb{Z}}_{\ge \left(K+1\right)}$$
56		eluznn0	$$⊢\left(K+1\in {\mathbb{N}}_0\wedge k\in {\mathbb{Z}}_{\ge \left(K+1\right)}\right)\to k\in {\mathbb{N}}_0$$
57	54 55 56	syl2an	$$⊢\left(\phi \wedge k\in \left(K+1\dots N\right)\right)\to k\in {\mathbb{N}}_0$$
58	40	ffvelcdmda	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\left(k\right)\in ℂ$$
59	57 58	syldan	$$⊢\left(\phi \wedge k\in \left(K+1\dots N\right)\right)\to A\left(k\right)\in ℂ$$
60		expcl	$$⊢\left(T\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to T^k\in ℂ$$
61	50 57 60	syl2an2r	$$⊢\left(\phi \wedge k\in \left(K+1\dots N\right)\right)\to T^k\in ℂ$$
62	59 61	mulcld	$$⊢\left(\phi \wedge k\in \left(K+1\dots N\right)\right)\to A\left(k\right)T^k\in ℂ$$
63	62	abscld	$$⊢\left(\phi \wedge k\in \left(K+1\dots N\right)\right)\to \left|A\left(k\right)T^k\right|\in ℝ$$
64	52 63	fsumrecl	$$⊢\phi \to \sum _{k=K+1}^N\left|A\left(k\right)T^k\right|\in ℝ$$
65	62	absge0d	$$⊢\left(\phi \wedge k\in \left(K+1\dots N\right)\right)\to 0\le \left|A\left(k\right)T^k\right|$$
66	52 63 65	fsumge0	$$⊢\phi \to 0\le \sum _{k=K+1}^N\left|A\left(k\right)T^k\right|$$
67	64 66	ge0p1rpd	$$⊢\phi \to \sum _{k=K+1}^N\left|A\left(k\right)T^k\right|+1\in {ℝ}^{+}$$
68	51 67	rpdivcld	$$⊢\phi \to \frac{\left|F\left(0\right)\right|}{\sum _{k=K+1}^N\left|A\left(k\right)T^k\right|+1}\in {ℝ}^{+}$$
69	8 68	eqeltrid	$$⊢\phi \to U\in {ℝ}^{+}$$
70		1rp	$$⊢1\in {ℝ}^{+}$$
71		ifcl	$$⊢\left(1\in {ℝ}^{+}\wedge U\in {ℝ}^{+}\right)\to if\left(1\le U,1,U\right)\in {ℝ}^{+}$$
72	70 69 71	sylancr	$$⊢\phi \to if\left(1\le U,1,U\right)\in {ℝ}^{+}$$
73	9 72	eqeltrid	$$⊢\phi \to X\in {ℝ}^{+}$$
74	50 69 73	3jca	$$⊢\phi \to \left(T\in ℂ\wedge U\in {ℝ}^{+}\wedge X\in {ℝ}^{+}\right)$$
75	33 74	jca	$$⊢\phi \to \left(\left(K\in \mathbb{N}\wedge A\left(K\right)\ne 0\right)\wedge \left(T\in ℂ\wedge U\in {ℝ}^{+}\wedge X\in {ℝ}^{+}\right)\right)$$