Metamath Proof Explorer


Theorem dchrisum0lem3

Description: Lemma for dchrisum0 . (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rpvmasum.z Z = /N
rpvmasum.l L = ℤRHom Z
rpvmasum.a φ N
rpvmasum2.g G = DChr N
rpvmasum2.d D = Base G
rpvmasum2.1 1 ˙ = 0 G
rpvmasum2.w W = y D 1 ˙ | m y L m m = 0
dchrisum0.b φ X W
dchrisum0lem1.f F = a X L a a
dchrisum0.c φ C 0 +∞
dchrisum0.s φ seq 1 + F S
dchrisum0.1 φ y 1 +∞ seq 1 + F y S C y
Assertion dchrisum0lem3 φ x + m = 1 x 2 d = 1 x 2 m X L m m d 𝑂1

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z = /N
2 rpvmasum.l L = ℤRHom Z
3 rpvmasum.a φ N
4 rpvmasum2.g G = DChr N
5 rpvmasum2.d D = Base G
6 rpvmasum2.1 1 ˙ = 0 G
7 rpvmasum2.w W = y D 1 ˙ | m y L m m = 0
8 dchrisum0.b φ X W
9 dchrisum0lem1.f F = a X L a a
10 dchrisum0.c φ C 0 +∞
11 dchrisum0.s φ seq 1 + F S
12 dchrisum0.1 φ y 1 +∞ seq 1 + F y S C y
13 1red φ 1
14 sumex m = 1 x d = 1 x 2 m X L m m d V
15 14 a1i φ x + m = 1 x d = 1 x 2 m X L m m d V
16 sumex m = x + 1 x 2 d = 1 x 2 m X L m m d V
17 16 a1i φ x + m = x + 1 x 2 d = 1 x 2 m X L m m d V
18 7 ssrab3 W D 1 ˙
19 difss D 1 ˙ D
20 18 19 sstri W D
21 20 8 sselid φ X D
22 18 8 sselid φ X D 1 ˙
23 eldifsni X D 1 ˙ X 1 ˙
24 22 23 syl φ X 1 ˙
25 eqid a X L a a = a X L a a
26 1 2 3 4 5 6 21 24 25 dchrmusumlema φ t c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y
27 3 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y N
28 8 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y X W
29 10 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y C 0 +∞
30 11 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y seq 1 + F S
31 12 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y y 1 +∞ seq 1 + F y S C y
32 eqid y + d = 1 y 1 d 2 y = y + d = 1 y 1 d 2 y
33 32 divsqrsum y + d = 1 y 1 d 2 y dom
34 32 divsqrsumf y + d = 1 y 1 d 2 y : +
35 ax-resscn
36 fss y + d = 1 y 1 d 2 y : + y + d = 1 y 1 d 2 y : +
37 34 35 36 mp2an y + d = 1 y 1 d 2 y : +
38 37 a1i φ y + d = 1 y 1 d 2 y : +
39 rpsup sup + * < = +∞
40 39 a1i φ sup + * < = +∞
41 38 40 rlimdm φ y + d = 1 y 1 d 2 y dom y + d = 1 y 1 d 2 y y + d = 1 y 1 d 2 y
42 33 41 mpbii φ y + d = 1 y 1 d 2 y y + d = 1 y 1 d 2 y
43 42 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y y + d = 1 y 1 d 2 y y + d = 1 y 1 d 2 y
44 simprl φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y c 0 +∞
45 simprrl φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y seq 1 + a X L a a t
46 simprrr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y y 1 +∞ seq 1 + a X L a a y t c y
47 1 2 27 4 5 6 7 28 9 29 30 31 32 43 25 44 45 46 dchrisum0lem2 φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y x + m = 1 x d = 1 x 2 m X L m m d 𝑂1
48 47 rexlimdvaa φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y x + m = 1 x d = 1 x 2 m X L m m d 𝑂1
49 48 exlimdv φ t c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y x + m = 1 x d = 1 x 2 m X L m m d 𝑂1
50 26 49 mpd φ x + m = 1 x d = 1 x 2 m X L m m d 𝑂1
51 1 2 3 4 5 6 7 8 9 10 11 12 dchrisum0lem1 φ x + m = x + 1 x 2 d = 1 x 2 m X L m m d 𝑂1
52 15 17 50 51 o1add2 φ x + m = 1 x d = 1 x 2 m X L m m d + m = x + 1 x 2 d = 1 x 2 m X L m m d 𝑂1
53 ovexd φ x + m = 1 x d = 1 x 2 m X L m m d + m = x + 1 x 2 d = 1 x 2 m X L m m d V
54 fzfid φ x + 1 x 2 Fin
55 fzfid φ x + m 1 x 2 1 x 2 m Fin
56 21 ad2antrr φ x + m 1 x 2 X D
57 elfzelz m 1 x 2 m
58 57 adantl φ x + m 1 x 2 m
59 4 1 5 2 56 58 dchrzrhcl φ x + m 1 x 2 X L m
60 59 adantr φ x + m 1 x 2 d 1 x 2 m X L m
61 elfznn m 1 x 2 m
62 61 adantl φ x + m 1 x 2 m
63 62 nnrpd φ x + m 1 x 2 m +
64 elfznn d 1 x 2 m d
65 64 nnrpd d 1 x 2 m d +
66 rpmulcl m + d + m d +
67 63 65 66 syl2an φ x + m 1 x 2 d 1 x 2 m m d +
68 67 rpsqrtcld φ x + m 1 x 2 d 1 x 2 m m d +
69 68 rpcnd φ x + m 1 x 2 d 1 x 2 m m d
70 68 rpne0d φ x + m 1 x 2 d 1 x 2 m m d 0
71 60 69 70 divcld φ x + m 1 x 2 d 1 x 2 m X L m m d
72 55 71 fsumcl φ x + m 1 x 2 d = 1 x 2 m X L m m d
73 54 72 fsumcl φ x + m = 1 x 2 d = 1 x 2 m X L m m d
74 73 abscld φ x + m = 1 x 2 d = 1 x 2 m X L m m d
75 74 adantrr φ x + 1 x m = 1 x 2 d = 1 x 2 m X L m m d
76 62 adantr φ x + m 1 x 2 d 1 x 2 m m
77 76 nnrpd φ x + m 1 x 2 d 1 x 2 m m +
78 77 rprege0d φ x + m 1 x 2 d 1 x 2 m m 0 m
79 64 adantl φ x + m 1 x 2 d 1 x 2 m d
80 79 nnrpd φ x + m 1 x 2 d 1 x 2 m d +
81 80 rprege0d φ x + m 1 x 2 d 1 x 2 m d 0 d
82 sqrtmul m 0 m d 0 d m d = m d
83 78 81 82 syl2anc φ x + m 1 x 2 d 1 x 2 m m d = m d
84 83 oveq2d φ x + m 1 x 2 d 1 x 2 m X L m m d = X L m m d
85 77 rpsqrtcld φ x + m 1 x 2 d 1 x 2 m m +
86 85 rpcnne0d φ x + m 1 x 2 d 1 x 2 m m m 0
87 80 rpsqrtcld φ x + m 1 x 2 d 1 x 2 m d +
88 87 rpcnne0d φ x + m 1 x 2 d 1 x 2 m d d 0
89 divdiv1 X L m m m 0 d d 0 X L m m d = X L m m d
90 60 86 88 89 syl3anc φ x + m 1 x 2 d 1 x 2 m X L m m d = X L m m d
91 84 90 eqtr4d φ x + m 1 x 2 d 1 x 2 m X L m m d = X L m m d
92 91 sumeq2dv φ x + m 1 x 2 d = 1 x 2 m X L m m d = d = 1 x 2 m X L m m d
93 92 sumeq2dv φ x + m = 1 x 2 d = 1 x 2 m X L m m d = m = 1 x 2 d = 1 x 2 m X L m m d
94 93 adantrr φ x + 1 x m = 1 x 2 d = 1 x 2 m X L m m d = m = 1 x 2 d = 1 x 2 m X L m m d
95 simpr φ x + x +
96 95 rpred φ x + x
97 reflcl x x
98 96 97 syl φ x + x
99 98 ltp1d φ x + x < x + 1
100 fzdisj x < x + 1 1 x x + 1 x 2 =
101 99 100 syl φ x + 1 x x + 1 x 2 =
102 101 adantrr φ x + 1 x 1 x x + 1 x 2 =
103 95 rprege0d φ x + x 0 x
104 flge0nn0 x 0 x x 0
105 nn0p1nn x 0 x + 1
106 103 104 105 3syl φ x + x + 1
107 nnuz = 1
108 106 107 eleqtrdi φ x + x + 1 1
109 108 adantrr φ x + 1 x x + 1 1
110 96 adantrr φ x + 1 x x
111 2z 2
112 rpexpcl x + 2 x 2 +
113 95 111 112 sylancl φ x + x 2 +
114 113 adantrr φ x + 1 x x 2 +
115 114 rpred φ x + 1 x x 2
116 110 recnd φ x + 1 x x
117 116 mulid1d φ x + 1 x x 1 = x
118 simprr φ x + 1 x 1 x
119 1red φ x + 1 x 1
120 rpregt0 x + x 0 < x
121 120 ad2antrl φ x + 1 x x 0 < x
122 lemul2 1 x x 0 < x 1 x x 1 x x
123 119 110 121 122 syl3anc φ x + 1 x 1 x x 1 x x
124 118 123 mpbid φ x + 1 x x 1 x x
125 117 124 eqbrtrrd φ x + 1 x x x x
126 116 sqvald φ x + 1 x x 2 = x x
127 125 126 breqtrrd φ x + 1 x x x 2
128 flword2 x x 2 x x 2 x 2 x
129 110 115 127 128 syl3anc φ x + 1 x x 2 x
130 fzsplit2 x + 1 1 x 2 x 1 x 2 = 1 x x + 1 x 2
131 109 129 130 syl2anc φ x + 1 x 1 x 2 = 1 x x + 1 x 2
132 fzfid φ x + 1 x 1 x 2 Fin
133 92 72 eqeltrrd φ x + m 1 x 2 d = 1 x 2 m X L m m d
134 133 adantlrr φ x + 1 x m 1 x 2 d = 1 x 2 m X L m m d
135 102 131 132 134 fsumsplit φ x + 1 x m = 1 x 2 d = 1 x 2 m X L m m d = m = 1 x d = 1 x 2 m X L m m d + m = x + 1 x 2 d = 1 x 2 m X L m m d
136 94 135 eqtrd φ x + 1 x m = 1 x 2 d = 1 x 2 m X L m m d = m = 1 x d = 1 x 2 m X L m m d + m = x + 1 x 2 d = 1 x 2 m X L m m d
137 136 fveq2d φ x + 1 x m = 1 x 2 d = 1 x 2 m X L m m d = m = 1 x d = 1 x 2 m X L m m d + m = x + 1 x 2 d = 1 x 2 m X L m m d
138 75 137 eqled φ x + 1 x m = 1 x 2 d = 1 x 2 m X L m m d m = 1 x d = 1 x 2 m X L m m d + m = x + 1 x 2 d = 1 x 2 m X L m m d
139 13 52 53 73 138 o1le φ x + m = 1 x 2 d = 1 x 2 m X L m m d 𝑂1