Metamath Proof Explorer


Theorem abelthlem8

Description: Lemma for abelth . (Contributed by Mario Carneiro, 2-Apr-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
abelth.6 F = x S n 0 A n x n
abelth.7 φ seq 0 + A 0
Assertion abelthlem8 φ R + w + y S 1 y < w F 1 F y < R

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 abelth.6 F = x S n 0 A n x n
7 abelth.7 φ seq 0 + A 0
8 nn0uz 0 = 0
9 0zd φ R + 0
10 id R + R +
11 3 4 ge0p1rpd φ M + 1 +
12 rpdivcl R + M + 1 + R M + 1 +
13 10 11 12 syl2anr φ R + R M + 1 +
14 eqidd φ R + k 0 seq 0 + A k = seq 0 + A k
15 7 adantr φ R + seq 0 + A 0
16 8 9 13 14 15 climi0 φ R + j 0 k j seq 0 + A k < R M + 1
17 13 adantr φ R + j 0 k j seq 0 + A k < R M + 1 R M + 1 +
18 fzfid φ 0 j 1 Fin
19 0zd φ 0
20 1 ffvelrnda φ w 0 A w
21 8 19 20 serf φ seq 0 + A : 0
22 elfznn0 i 0 j 1 i 0
23 ffvelrn seq 0 + A : 0 i 0 seq 0 + A i
24 21 22 23 syl2an φ i 0 j 1 seq 0 + A i
25 24 abscld φ i 0 j 1 seq 0 + A i
26 18 25 fsumrecl φ i = 0 j 1 seq 0 + A i
27 26 ad2antrr φ R + j 0 k j seq 0 + A k < R M + 1 i = 0 j 1 seq 0 + A i
28 24 absge0d φ i 0 j 1 0 seq 0 + A i
29 18 25 28 fsumge0 φ 0 i = 0 j 1 seq 0 + A i
30 29 ad2antrr φ R + j 0 k j seq 0 + A k < R M + 1 0 i = 0 j 1 seq 0 + A i
31 27 30 ge0p1rpd φ R + j 0 k j seq 0 + A k < R M + 1 i = 0 j 1 seq 0 + A i + 1 +
32 17 31 rpdivcld φ R + j 0 k j seq 0 + A k < R M + 1 R M + 1 i = 0 j 1 seq 0 + A i + 1 +
33 1 2 3 4 5 abelthlem2 φ 1 S S 1 0 ball abs 1
34 33 simpld φ 1 S
35 oveq1 x = 1 x n = 1 n
36 nn0z n 0 n
37 1exp n 1 n = 1
38 36 37 syl n 0 1 n = 1
39 35 38 sylan9eq x = 1 n 0 x n = 1
40 39 oveq2d x = 1 n 0 A n x n = A n 1
41 40 sumeq2dv x = 1 n 0 A n x n = n 0 A n 1
42 sumex n 0 A n 1 V
43 41 6 42 fvmpt 1 S F 1 = n 0 A n 1
44 34 43 syl φ F 1 = n 0 A n 1
45 1 ffvelrnda φ n 0 A n
46 45 mulid1d φ n 0 A n 1 = A n
47 46 eqcomd φ n 0 A n = A n 1
48 46 45 eqeltrd φ n 0 A n 1
49 8 19 47 48 7 isumclim φ n 0 A n 1 = 0
50 44 49 eqtrd φ F 1 = 0
51 50 adantr φ y S F 1 = 0
52 51 oveq1d φ y S F 1 F y = 0 F y
53 df-neg F y = 0 F y
54 52 53 eqtr4di φ y S F 1 F y = F y
55 54 fveq2d φ y S F 1 F y = F y
56 1 2 3 4 5 6 abelthlem4 φ F : S
57 56 ffvelrnda φ y S F y
58 57 absnegd φ y S F y = F y
59 55 58 eqtrd φ y S F 1 F y = F y
60 59 adantlr φ R + y S F 1 F y = F y
61 60 ad2ant2r φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 F 1 F y = F y
62 fveq2 y = 1 F y = F 1
63 62 50 sylan9eqr φ y = 1 F y = 0
64 63 abs00bd φ y = 1 F y = 0
65 64 ad5ant15 φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y = 1 F y = 0
66 simpllr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 R +
67 66 rpgt0d φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 0 < R
68 67 adantr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y = 1 0 < R
69 65 68 eqbrtrd φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y = 1 F y < R
70 1 ad3antrrr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 A : 0
71 2 ad3antrrr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 seq 0 + A dom
72 3 ad3antrrr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 M
73 4 ad3antrrr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 0 M
74 7 ad3antrrr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 seq 0 + A 0
75 simprll φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 y S
76 simprr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 y 1
77 eldifsn y S 1 y S y 1
78 75 76 77 sylanbrc φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 y S 1
79 13 ad2antrr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 R M + 1 +
80 simplrl φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 j 0
81 simplrr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 k j seq 0 + A k < R M + 1
82 2fveq3 k = m seq 0 + A k = seq 0 + A m
83 82 breq1d k = m seq 0 + A k < R M + 1 seq 0 + A m < R M + 1
84 83 cbvralvw k j seq 0 + A k < R M + 1 m j seq 0 + A m < R M + 1
85 81 84 sylib φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 m j seq 0 + A m < R M + 1
86 simprlr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1
87 2fveq3 i = n seq 0 + A i = seq 0 + A n
88 87 cbvsumv i = 0 j 1 seq 0 + A i = n = 0 j 1 seq 0 + A n
89 88 oveq1i i = 0 j 1 seq 0 + A i + 1 = n = 0 j 1 seq 0 + A n + 1
90 89 oveq2i R M + 1 i = 0 j 1 seq 0 + A i + 1 = R M + 1 n = 0 j 1 seq 0 + A n + 1
91 86 90 breqtrdi φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 1 y < R M + 1 n = 0 j 1 seq 0 + A n + 1
92 70 71 72 73 5 6 74 78 79 80 85 91 abelthlem7 φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 F y < M + 1 R M + 1
93 rpcn R + R
94 93 adantl φ R + R
95 11 adantr φ R + M + 1 +
96 95 rpcnd φ R + M + 1
97 95 rpne0d φ R + M + 1 0
98 94 96 97 divcan2d φ R + M + 1 R M + 1 = R
99 98 ad2antrr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 M + 1 R M + 1 = R
100 92 99 breqtrd φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 F y < R
101 100 anassrs φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 y 1 F y < R
102 69 101 pm2.61dane φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 F y < R
103 61 102 eqbrtrd φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 F 1 F y < R
104 103 expr φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 F 1 F y < R
105 104 ralrimiva φ R + j 0 k j seq 0 + A k < R M + 1 y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 F 1 F y < R
106 breq2 w = R M + 1 i = 0 j 1 seq 0 + A i + 1 1 y < w 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1
107 106 rspceaimv R M + 1 i = 0 j 1 seq 0 + A i + 1 + y S 1 y < R M + 1 i = 0 j 1 seq 0 + A i + 1 F 1 F y < R w + y S 1 y < w F 1 F y < R
108 32 105 107 syl2anc φ R + j 0 k j seq 0 + A k < R M + 1 w + y S 1 y < w F 1 F y < R
109 16 108 rexlimddv φ R + w + y S 1 y < w F 1 F y < R