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	⊢ 𝐴 = ( coeff ‘ 𝐹 )
	ftalem.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
	ftalem.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	ftalem.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	ftalem4.5	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ≠ 0 )
	ftalem4.6	⊢ 𝐾 = inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < )
	ftalem4.7	⊢ 𝑇 = ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( 1 / 𝐾 ) )
	ftalem4.8	⊢ 𝑈 = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) )
	ftalem4.9	⊢ 𝑋 = if ( 1 ≤ 𝑈 , 1 , 𝑈 )
Assertion	ftalem4	⊢ ( 𝜑 → ( ( 𝐾 ∈ ℕ ∧ ( 𝐴 ‘ 𝐾 ) ≠ 0 ) ∧ ( 𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ) ) )

Proof

Step	Hyp	Ref	Expression
1		ftalem.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		ftalem.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
3		ftalem.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4		ftalem.4	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		ftalem4.5	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ≠ 0 )
6		ftalem4.6	⊢ 𝐾 = inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < )
7		ftalem4.7	⊢ 𝑇 = ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( 1 / 𝐾 ) )
8		ftalem4.8	⊢ 𝑈 = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) )
9		ftalem4.9	⊢ 𝑋 = if ( 1 ≤ 𝑈 , 1 , 𝑈 )
10		ssrab2	⊢ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ℕ
11		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
12	10 11	sseqtri	⊢ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 1 )
13		fveq2	⊢ ( 𝑛 = 𝑁 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑁 ) )
14	13	neeq1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝐴 ‘ 𝑛 ) ≠ 0 ↔ ( 𝐴 ‘ 𝑁 ) ≠ 0 ) )
15	4	nnne0d	⊢ ( 𝜑 → 𝑁 ≠ 0 )
16	2 1	dgreq0	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
17	3 16	syl	⊢ ( 𝜑 → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
18		fveq2	⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) )
19		dgr0	⊢ ( deg ‘ 0𝑝 ) = 0
20	18 19	eqtrdi	⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = 0 )
21	2 20	eqtrid	⊢ ( 𝐹 = 0𝑝 → 𝑁 = 0 )
22	17 21	syl6bir	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑁 ) = 0 → 𝑁 = 0 ) )
23	22	necon3d	⊢ ( 𝜑 → ( 𝑁 ≠ 0 → ( 𝐴 ‘ 𝑁 ) ≠ 0 ) )
24	15 23	mpd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ≠ 0 )
25	14 4 24	elrabd	⊢ ( 𝜑 → 𝑁 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
26	25	ne0d	⊢ ( 𝜑 → { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ≠ ∅ )
27		infssuzcl	⊢ ( ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
28	12 26 27	sylancr	⊢ ( 𝜑 → inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
29	6 28	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } )
30		fveq2	⊢ ( 𝑛 = 𝐾 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝐾 ) )
31	30	neeq1d	⊢ ( 𝑛 = 𝐾 → ( ( 𝐴 ‘ 𝑛 ) ≠ 0 ↔ ( 𝐴 ‘ 𝐾 ) ≠ 0 ) )
32	31	elrab	⊢ ( 𝐾 ∈ { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } ↔ ( 𝐾 ∈ ℕ ∧ ( 𝐴 ‘ 𝐾 ) ≠ 0 ) )
33	29 32	sylib	⊢ ( 𝜑 → ( 𝐾 ∈ ℕ ∧ ( 𝐴 ‘ 𝐾 ) ≠ 0 ) )
34		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
35	3 34	syl	⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ )
36		0cn	⊢ 0 ∈ ℂ
37		ffvelcdm	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ 0 ∈ ℂ ) → ( 𝐹 ‘ 0 ) ∈ ℂ )
38	35 36 37	sylancl	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ ℂ )
39	1	coef3	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
40	3 39	syl	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
41	33	simpld	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
42	41	nnnn0d	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
43	40 42	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ∈ ℂ )
44	33	simprd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐾 ) ≠ 0 )
45	38 43 44	divcld	⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ∈ ℂ )
46	45	negcld	⊢ ( 𝜑 → - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ∈ ℂ )
47	41	nnrecred	⊢ ( 𝜑 → ( 1 / 𝐾 ) ∈ ℝ )
48	47	recnd	⊢ ( 𝜑 → ( 1 / 𝐾 ) ∈ ℂ )
49	46 48	cxpcld	⊢ ( 𝜑 → ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ 𝐾 ) ) ↑𝑐 ( 1 / 𝐾 ) ) ∈ ℂ )
50	7 49	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
51	38 5	absrpcld	⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 0 ) ) ∈ ℝ+ )
52		fzfid	⊢ ( 𝜑 → ( ( 𝐾 + 1 ) ... 𝑁 ) ∈ Fin )
53		peano2nn0	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
54	42 53	syl	⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ0 )
55		elfzuz	⊢ ( 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
56		eluznn0	⊢ ( ( ( 𝐾 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
57	54 55 56	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
58	40	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
59	57 58	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
60		expcl	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑇 ↑ 𝑘 ) ∈ ℂ )
61	50 57 60	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( 𝑇 ↑ 𝑘 ) ∈ ℂ )
62	59 61	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ∈ ℂ )
63	62	abscld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) ∈ ℝ )
64	52 63	fsumrecl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) ∈ ℝ )
65	62	absge0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ) → 0 ≤ ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) )
66	52 63 65	fsumge0	⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) )
67	64 66	ge0p1rpd	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ∈ ℝ+ )
68	51 67	rpdivcld	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑘 ∈ ( ( 𝐾 + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑇 ↑ 𝑘 ) ) ) + 1 ) ) ∈ ℝ+ )
69	8 68	eqeltrid	⊢ ( 𝜑 → 𝑈 ∈ ℝ+ )
70		1rp	⊢ 1 ∈ ℝ+
71		ifcl	⊢ ( ( 1 ∈ ℝ+ ∧ 𝑈 ∈ ℝ+ ) → if ( 1 ≤ 𝑈 , 1 , 𝑈 ) ∈ ℝ+ )
72	70 69 71	sylancr	⊢ ( 𝜑 → if ( 1 ≤ 𝑈 , 1 , 𝑈 ) ∈ ℝ+ )
73	9 72	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
74	50 69 73	3jca	⊢ ( 𝜑 → ( 𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ) )
75	33 74	jca	⊢ ( 𝜑 → ( ( 𝐾 ∈ ℕ ∧ ( 𝐴 ‘ 𝐾 ) ≠ 0 ) ∧ ( 𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ) ) )