Metamath Proof Explorer

Theorem ftalem6

Description: Lemma for fta : Discharge the auxiliary variables in ftalem5 . (Contributed by Mario Carneiro, 20-Sep-2014) (Proof shortened by AV, 28-Sep-2020)

Ref Expression
Hypotheses ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
ftalem6.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ≠ 0 )
Assertion ftalem6 ( 𝜑 → ∃ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) )

Proof

Step Hyp Ref Expression
1 ftalem.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 ftalem.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 ftalem.3 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4 ftalem.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5 ftalem6.5 ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ≠ 0 )
6 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑛 ) )
7 6 neeq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 ↔ ( 𝐴 ‘ 𝑛 ) ≠ 0 ) )
8 7 cbvrabv ⊢ { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } = { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 }
9 8 infeq1i ⊢ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝐴 ‘ 𝑛 ) ≠ 0 } , ℝ , < )
10 eqid ⊢ ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) = ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) )
11 fveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝐴 ‘ 𝑟 ) = ( 𝐴 ‘ 𝑠 ) )
12 oveq2 ⊢ ( 𝑟 = 𝑠 → ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) = ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑠 ) )
13 11 12 oveq12d ⊢ ( 𝑟 = 𝑠 → ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) = ( ( 𝐴 ‘ 𝑠 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑠 ) ) )
14 13 fveq2d ⊢ ( 𝑟 = 𝑠 → ( abs ‘ ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) ) = ( abs ‘ ( ( 𝐴 ‘ 𝑠 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑠 ) ) ) )
15 14 cbvsumv ⊢ Σ 𝑟 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) ) = Σ 𝑠 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑠 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑠 ) ) )
16 15 oveq1i ⊢ ( Σ 𝑟 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) ) + 1 ) = ( Σ 𝑠 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑠 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑠 ) ) ) + 1 )
17 16 oveq2i ⊢ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑟 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) ) + 1 ) ) = ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑠 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑠 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑠 ) ) ) + 1 ) )
18 eqid ⊢ if ( 1 ≤ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑟 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) ) + 1 ) ) , 1 , ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑟 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) ) + 1 ) ) ) = if ( 1 ≤ ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑟 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) ) + 1 ) ) , 1 , ( ( abs ‘ ( 𝐹 ‘ 0 ) ) / ( Σ 𝑟 ∈ ( ( inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) + 1 ) ... 𝑁 ) ( abs ‘ ( ( 𝐴 ‘ 𝑟 ) · ( ( - ( ( 𝐹 ‘ 0 ) / ( 𝐴 ‘ inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑𝑐 ( 1 / inf ( { 𝑘 ∈ ℕ ∣ ( 𝐴 ‘ 𝑘 ) ≠ 0 } , ℝ , < ) ) ) ↑ 𝑟 ) ) ) + 1 ) ) )
19 1 2 3 4 5 9 10 17 18 ftalem5 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℂ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) < ( abs ‘ ( 𝐹 ‘ 0 ) ) )