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 ⊢ φ → seq 0 + A ∈ dom ⁡ ⇝
Assertion abelthlem1 ⊢ φ → 1 ≤ sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * <

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ φ → A : ℕ 0 ⟶ ℂ
2 abelth.2 ⊢ φ → seq 0 + A ∈ dom ⁡ ⇝
3 abs1 ⊢ 1 = 1
4 eqid ⊢ z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n = z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n
5 eqid ⊢ sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * < = sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * <
6 1cnd ⊢ φ → 1 ∈ ℂ
7 1 feqmptd ⊢ φ → A = n ∈ ℕ 0 ⟼ A ⁡ n
8 1 ffvelrnda ⊢ φ ∧ n ∈ ℕ 0 → A ⁡ n ∈ ℂ
9 8 mulid1d ⊢ φ ∧ 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 → z n = 1 n
14 nn0z ⊢ n ∈ ℕ 0 → n ∈ ℤ
15 1exp ⊢ n ∈ ℤ → 1 n = 1
16 14 15 syl ⊢ n ∈ ℕ 0 → 1 n = 1
17 13 16 sylan9eq ⊢ z = 1 ∧ n ∈ ℕ 0 → z n = 1
18 17 oveq2d ⊢ z = 1 ∧ n ∈ ℕ 0 → A ⁡ n ⁢ z n = A ⁡ n ⋅ 1
19 18 mpteq2dva ⊢ z = 1 → n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n = 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 ⁢ z n ⁡ 1 = n ∈ ℕ 0 ⟼ A ⁡ n ⋅ 1
23 12 22 ax-mp ⊢ z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ 1 = n ∈ ℕ 0 ⟼ A ⁡ n ⋅ 1
24 11 23 eqtr4di ⊢ φ → A = z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ 1
25 24 seqeq3d ⊢ φ → seq 0 + A = seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ 1
26 25 2 eqeltrrd ⊢ φ → seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ 1 ∈ dom ⁡ ⇝
27 4 1 5 6 26 radcnvle ⊢ φ → 1 ≤ sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * <
28 3 27 eqbrtrrid ⊢ φ → 1 ≤ sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * <