Metamath Proof Explorer

Theorem abelthlem1

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

Ref Expression
Hypotheses abelth.1 ⊢φ→A:ℕ0⟶ℂ
abelth.2 ⊢φ→seq0+A∈dom⁡⇝
Assertion abelthlem1 ⊢φ→1≤supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢φ→A:ℕ0⟶ℂ
2 abelth.2 ⊢φ→seq0+A∈dom⁡⇝
3 abs1 ⊢1=1
4 eqid ⊢z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn=z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn
5 eqid ⊢supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<=supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<
6 1cnd ⊢φ→1∈ℂ
7 1 feqmptd ⊢φ→A=n∈ℕ0⟼A⁡n
8 1 ffvelcdmda ⊢φ∧n∈ℕ0→A⁡n∈ℂ
9 8 mulridd ⊢φ∧n∈ℕ0→A⁡n⋅1=A⁡n
10 9 mpteq2dva ⊢φ→n∈ℕ0⟼A⁡n⋅1=n∈ℕ0⟼A⁡n
11 7 10 eqtr4d ⊢φ→A=n∈ℕ0⟼A⁡n⋅1
12 ax-1cn ⊢1∈ℂ
13 oveq1 ⊢z=1→zn=1n
14 nn0z ⊢n∈ℕ0→n∈ℤ
15 1exp ⊢n∈ℤ→1n=1
16 14 15 syl ⊢n∈ℕ0→1n=1
17 13 16 sylan9eq ⊢z=1∧n∈ℕ0→zn=1
18 17 oveq2d ⊢z=1∧n∈ℕ0→A⁡n⁢zn=A⁡n⋅1
19 18 mpteq2dva ⊢z=1→n∈ℕ0⟼A⁡n⁢zn=n∈ℕ0⟼A⁡n⋅1
20 nn0ex ⊢ℕ0∈V
21 20 mptex ⊢n∈ℕ0⟼A⁡n⋅1∈V
22 19 4 21 fvmpt ⊢1∈ℂ→z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡1=n∈ℕ0⟼A⁡n⋅1
23 12 22 ax-mp ⊢z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡1=n∈ℕ0⟼A⁡n⋅1
24 11 23 eqtr4di ⊢φ→A=z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡1
25 24 seqeq3d ⊢φ→seq0+A=seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡1
26 25 2 eqeltrrd ⊢φ→seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡1∈dom⁡⇝
27 4 1 5 6 26 radcnvle ⊢φ→1≤supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<
28 3 27 eqbrtrrid ⊢φ→1≤supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<