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 = coeff (F)$
	ftalem.2	$⊢ N = \deg (F)$
	ftalem.3	$⊢ φ \to F \in Poly (S)$
	ftalem.4	$⊢ φ \to N \in ℕ$
	ftalem4.5	$⊢ φ \to F (0) \neq 0$
	ftalem4.6	$⊢ K = sup (\{n \in ℕ \| A (n) \neq 0\} ℝ <)$
	ftalem4.7	$⊢ T = {(- (\frac{F (0)}{A (K)}))}^{\frac{1}{K}}$
	ftalem4.8	$⊢ U = \frac{\|F (0)\|}{\sum_{k = K + 1}^{N} \|A (k) T^{k}\| + 1}$
	ftalem4.9	$⊢ X = if (1 \leq U, 1, U)$
Assertion	ftalem4	$⊢ φ \to ((K \in ℕ \land A (K) \neq 0) \land (T \in ℂ \land U \in ℝ^{+} \land X \in ℝ^{+}))$

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

Metamath Proof Explorer

Theorem ftalem4

Proof