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 ) ) )