Theorem abelthlem1

Description: Lemma for abelth . (Contributed by Mario Carneiro, 1-Apr-2015)

	Ref	Expression
Hypotheses	abelth.1	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
	abelth.2	⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
Assertion	abelthlem1	⊢ ( 𝜑 → 1 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		abelth.1	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
2		abelth.2	⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3		abs1	⊢ ( abs ‘ 1 ) = 1
4		eqid	⊢ ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) )
5		eqid	⊢ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
6		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
7	1	feqmptd	⊢ ( 𝜑 → 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ‘ 𝑛 ) ) )
8	1	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
9	8	mulid1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · 1 ) = ( 𝐴 ‘ 𝑛 ) )
10	9	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · 1 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ‘ 𝑛 ) ) )
11	7 10	eqtr4d	⊢ ( 𝜑 → 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · 1 ) ) )
12		ax-1cn	⊢ 1 ∈ ℂ
13		oveq1	⊢ ( 𝑧 = 1 → ( 𝑧 ↑ 𝑛 ) = ( 1 ↑ 𝑛 ) )
14		nn0z	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
15		1exp	⊢ ( 𝑛 ∈ ℤ → ( 1 ↑ 𝑛 ) = 1 )
16	14 15	syl	⊢ ( 𝑛 ∈ ℕ0 → ( 1 ↑ 𝑛 ) = 1 )
17	13 16	sylan9eq	⊢ ( ( 𝑧 = 1 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑛 ) = 1 )
18	17	oveq2d	⊢ ( ( 𝑧 = 1 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑛 ) · 1 ) )
19	18	mpteq2dva	⊢ ( 𝑧 = 1 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · 1 ) ) )
20		nn0ex	⊢ ℕ0 ∈ V
21	20	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · 1 ) ) ∈ V
22	19 4 21	fvmpt	⊢ ( 1 ∈ ℂ → ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · 1 ) ) )
23	12 22	ax-mp	⊢ ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 1 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · 1 ) )
24	11 23	eqtr4di	⊢ ( 𝜑 → 𝐴 = ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 1 ) )
25	24	seqeq3d	⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) = seq 0 ( + , ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 1 ) ) )
26	25 2	eqeltrrd	⊢ ( 𝜑 → seq 0 ( + , ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 1 ) ) ∈ dom ⇝ )
27	4 1 5 6 26	radcnvle	⊢ ( 𝜑 → ( abs ‘ 1 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
28	3 27	eqbrtrrid	⊢ ( 𝜑 → 1 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑧 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑧 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )