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 eqtrid ⊢ ( 𝐹 = 0𝑝 → 𝑁 = 0 )
22 17 21 biimtrrdi ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑁 ) = 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 ) ∧ ( 𝑇 ∈ ℂ ∧ 𝑈 ∈ ℝ+ ∧ 𝑋 ∈ ℝ+ ) ) )