Metamath Proof Explorer


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 syl5eq ( 𝐹 = 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 ffvelrn ( ( 𝐹 : ℂ ⟶ ℂ ∧ 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 ffvelrnd ( 𝜑 → ( 𝐴𝐾 ) ∈ ℂ )
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 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ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 ) ∧ ( 𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+𝑋 ∈ ℝ+ ) ) )