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 sselid φ 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 sselid φ 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