This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ )
9 8 mulridd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ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 ⇝ } , ℝ* , < ) )