Metamath Proof Explorer

Theorem abelthlem3

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

Ref Expression
Hypotheses abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
Assertion abelthlem3 ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ∈ dom ⇝ )

Proof

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