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 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝐴 β€˜ 𝑛 ) ∈ β„‚ )
15 14 mulridd ⊒ ( ( πœ‘ ∧ 𝑛 ∈ β„•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 sselid ⊒ ( ( πœ‘ ∧ 𝑋 ∈ ( 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 sselid ⊒ ( ( πœ‘ ∧ 𝑋 ∈ ( 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 ⇝ )