Metamath Proof Explorer

Theorem abelthlem3

Description: Lemma for abelth . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses abelth.1 ⊢ φ → A : ℕ 0 ⟶ ℂ
abelth.2 ⊢ φ → seq 0 + A ∈ dom ⁡ ⇝
abelth.3 ⊢ φ → M ∈ ℝ
abelth.4 ⊢ φ → 0 ≤ M
abelth.5 ⊢ S = z ∈ ℂ | 1 − z ≤ M ⁢ 1 − z
Assertion abelthlem3 ⊢ φ ∧ X ∈ S → seq 0 + n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ φ → A : ℕ 0 ⟶ ℂ
2 abelth.2 ⊢ φ → seq 0 + A ∈ dom ⁡ ⇝
3 abelth.3 ⊢ φ → M ∈ ℝ
4 abelth.4 ⊢ φ → 0 ≤ M
5 abelth.5 ⊢ S = z ∈ ℂ | 1 − z ≤ M ⁢ 1 − z
6 1 2 3 4 5 abelthlem2 ⊢ φ → 1 ∈ S ∧ S ∖ 1 ⊆ 0 ball ⁡ abs ∘ − 1
7 6 simprd ⊢ φ → S ∖ 1 ⊆ 0 ball ⁡ abs ∘ − 1
8 ssundif ⊢ S ⊆ 1 ∪ 0 ball ⁡ abs ∘ − 1 ↔ S ∖ 1 ⊆ 0 ball ⁡ abs ∘ − 1
9 7 8 sylibr ⊢ φ → S ⊆ 1 ∪ 0 ball ⁡ abs ∘ − 1
10 9 sselda ⊢ φ ∧ X ∈ S → X ∈ 1 ∪ 0 ball ⁡ abs ∘ − 1
11 elun ⊢ X ∈ 1 ∪ 0 ball ⁡ abs ∘ − 1 ↔ X ∈ 1 ∨ X ∈ 0 ball ⁡ abs ∘ − 1
12 10 11 sylib ⊢ φ ∧ X ∈ S → X ∈ 1 ∨ X ∈ 0 ball ⁡ abs ∘ − 1
13 1 feqmptd ⊢ φ → A = n ∈ ℕ 0 ⟼ A ⁡ n
14 1 ffvelrnda ⊢ φ ∧ n ∈ ℕ 0 → A ⁡ n ∈ ℂ
15 14 mulid1d ⊢ φ ∧ n ∈ ℕ 0 → A ⁡ n ⋅ 1 = A ⁡ n
16 15 mpteq2dva ⊢ φ → n ∈ ℕ 0 ⟼ A ⁡ n ⋅ 1 = n ∈ ℕ 0 ⟼ A ⁡ n
17 13 16 eqtr4d ⊢ φ → A = n ∈ ℕ 0 ⟼ A ⁡ n ⋅ 1
18 elsni ⊢ X ∈ 1 → X = 1
19 18 oveq1d ⊢ X ∈ 1 → X n = 1 n
20 nn0z ⊢ n ∈ ℕ 0 → n ∈ ℤ
21 1exp ⊢ n ∈ ℤ → 1 n = 1
22 20 21 syl ⊢ n ∈ ℕ 0 → 1 n = 1
23 19 22 sylan9eq ⊢ X ∈ 1 ∧ n ∈ ℕ 0 → X n = 1
24 23 oveq2d ⊢ X ∈ 1 ∧ n ∈ ℕ 0 → A ⁡ n ⁢ X n = A ⁡ n ⋅ 1
25 24 mpteq2dva ⊢ X ∈ 1 → n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n = n ∈ ℕ 0 ⟼ A ⁡ n ⋅ 1
26 25 eqcomd ⊢ X ∈ 1 → n ∈ ℕ 0 ⟼ A ⁡ n ⋅ 1 = n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n
27 17 26 sylan9eq ⊢ φ ∧ X ∈ 1 → A = n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n
28 27 seqeq3d ⊢ φ ∧ X ∈ 1 → seq 0 + A = seq 0 + n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n
29 2 adantr ⊢ φ ∧ X ∈ 1 → seq 0 + A ∈ dom ⁡ ⇝
30 28 29 eqeltrrd ⊢ φ ∧ X ∈ 1 → seq 0 + n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n ∈ dom ⁡ ⇝
31 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
32 0cn ⊢ 0 ∈ ℂ
33 1xr ⊢ 1 ∈ ℝ *
34 blssm ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ * → 0 ball ⁡ abs ∘ − 1 ⊆ ℂ
35 31 32 33 34 mp3an ⊢ 0 ball ⁡ abs ∘ − 1 ⊆ ℂ
36 simpr ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X ∈ 0 ball ⁡ abs ∘ − 1
37 35 36 sseldi ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X ∈ ℂ
38 oveq1 ⊢ z = X → z n = X n
39 38 oveq2d ⊢ z = X → A ⁡ n ⁢ z n = A ⁡ n ⁢ X n
40 39 mpteq2dv ⊢ z = X → n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n = n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n
41 eqid ⊢ z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n = z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n
42 nn0ex ⊢ ℕ 0 ∈ V
43 42 mptex ⊢ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n ∈ V
44 40 41 43 fvmpt ⊢ X ∈ ℂ → z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ X = n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n
45 37 44 syl ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ X = n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n
46 45 seqeq3d ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ X = seq 0 + n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n
47 1 adantr ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → A : ℕ 0 ⟶ ℂ
48 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 ⁡ ⇝ ℝ * <
49 37 abscld ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X ∈ ℝ
50 49 rexrd ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X ∈ ℝ *
51 1re ⊢ 1 ∈ ℝ
52 rexr ⊢ 1 ∈ ℝ → 1 ∈ ℝ *
53 51 52 mp1i ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → 1 ∈ ℝ *
54 iccssxr ⊢ 0 +∞ ⊆ ℝ *
55 41 47 48 radcnvcl ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * < ∈ 0 +∞
56 54 55 sseldi ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * < ∈ ℝ *
57 eqid ⊢ abs ∘ − = abs ∘ −
58 57 cnmetdval ⊢ X ∈ ℂ ∧ 0 ∈ ℂ → X abs ∘ − 0 = X − 0
59 37 32 58 sylancl ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X abs ∘ − 0 = X − 0
60 37 subid1d ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X − 0 = X
61 60 fveq2d ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X − 0 = X
62 59 61 eqtrd ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X abs ∘ − 0 = X
63 elbl3 ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ 1 ∈ ℝ * ∧ 0 ∈ ℂ ∧ X ∈ ℂ → X ∈ 0 ball ⁡ abs ∘ − 1 ↔ X abs ∘ − 0 < 1
64 31 33 63 mpanl12 ⊢ 0 ∈ ℂ ∧ X ∈ ℂ → X ∈ 0 ball ⁡ abs ∘ − 1 ↔ X abs ∘ − 0 < 1
65 32 37 64 sylancr ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X ∈ 0 ball ⁡ abs ∘ − 1 ↔ X abs ∘ − 0 < 1
66 36 65 mpbid ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X abs ∘ − 0 < 1
67 62 66 eqbrtrrd ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X < 1
68 1 2 abelthlem1 ⊢ φ → 1 ≤ sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * <
69 68 adantr ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → 1 ≤ sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * <
70 50 53 56 67 69 xrltletrd ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → X < sup r ∈ ℝ | seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ r ∈ dom ⁡ ⇝ ℝ * <
71 41 47 48 37 70 radcnvlt2 ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → seq 0 + z ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ z n ⁡ X ∈ dom ⁡ ⇝
72 46 71 eqeltrrd ⊢ φ ∧ X ∈ 0 ball ⁡ abs ∘ − 1 → seq 0 + n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n ∈ dom ⁡ ⇝
73 30 72 jaodan ⊢ φ ∧ X ∈ 1 ∨ X ∈ 0 ball ⁡ abs ∘ − 1 → seq 0 + n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n ∈ dom ⁡ ⇝
74 12 73 syldan ⊢ φ ∧ X ∈ S → seq 0 + n ∈ ℕ 0 ⟼ A ⁡ n ⁢ X n ∈ dom ⁡ ⇝