Metamath Proof Explorer


Theorem dchrisum0lema

Description: Lemma for dchrisum0 . Apply dchrisum for the function 1 / sqrt y . (Contributed by Mario Carneiro, 10-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
Assertion dchrisum0lema φ t c 0 +∞ seq 1 + F t y 1 +∞ seq 1 + F y t c y

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 7 ssrab3 W D 1 ˙
11 10 8 sselid φ X D 1 ˙
12 11 eldifad φ X D
13 eldifsni X D 1 ˙ X 1 ˙
14 11 13 syl φ X 1 ˙
15 fveq2 n = x n = x
16 15 oveq2d n = x 1 n = 1 x
17 1nn 1
18 17 a1i φ 1
19 rpsqrtcl n + n +
20 19 adantl φ n + n +
21 20 rprecred φ n + 1 n
22 simp3r φ n + x + 1 n n x n x
23 simp2l φ n + x + 1 n n x n +
24 23 rprege0d φ n + x + 1 n n x n 0 n
25 simp2r φ n + x + 1 n n x x +
26 25 rprege0d φ n + x + 1 n n x x 0 x
27 sqrtle n 0 n x 0 x n x n x
28 24 26 27 syl2anc φ n + x + 1 n n x n x n x
29 22 28 mpbid φ n + x + 1 n n x n x
30 23 rpsqrtcld φ n + x + 1 n n x n +
31 25 rpsqrtcld φ n + x + 1 n n x x +
32 30 31 lerecd φ n + x + 1 n n x n x 1 x 1 n
33 29 32 mpbid φ n + x + 1 n n x 1 x 1 n
34 sqrtlim n + 1 n 0
35 34 a1i φ n + 1 n 0
36 2fveq3 a = n X L a = X L n
37 fveq2 a = n a = n
38 37 oveq2d a = n 1 a = 1 n
39 36 38 oveq12d a = n X L a 1 a = X L n 1 n
40 39 cbvmptv a X L a 1 a = n X L n 1 n
41 1 2 3 4 5 6 12 14 16 18 21 33 35 40 dchrisum φ t c 0 +∞ seq 1 + a X L a 1 a t x 1 +∞ seq 1 + a X L a 1 a x t c 1 x
42 12 adantr φ n X D
43 nnz n n
44 43 adantl φ n n
45 4 1 5 2 42 44 dchrzrhcl φ n X L n
46 simpr φ n n
47 46 nnrpd φ n n +
48 47 rpsqrtcld φ n n +
49 48 rpcnd φ n n
50 48 rpne0d φ n n 0
51 45 49 50 divrecd φ n X L n n = X L n 1 n
52 51 mpteq2dva φ n X L n n = n X L n 1 n
53 36 37 oveq12d a = n X L a a = X L n n
54 53 cbvmptv a X L a a = n X L n n
55 9 54 eqtri F = n X L n n
56 52 55 40 3eqtr4g φ F = a X L a 1 a
57 56 seqeq3d φ seq 1 + F = seq 1 + a X L a 1 a
58 57 breq1d φ seq 1 + F t seq 1 + a X L a 1 a t
59 58 adantr φ c 0 +∞ seq 1 + F t seq 1 + a X L a 1 a t
60 2fveq3 y = x seq 1 + F y = seq 1 + F x
61 60 fvoveq1d y = x seq 1 + F y t = seq 1 + F x t
62 fveq2 y = x y = x
63 62 oveq2d y = x c y = c x
64 61 63 breq12d y = x seq 1 + F y t c y seq 1 + F x t c x
65 64 cbvralvw y 1 +∞ seq 1 + F y t c y x 1 +∞ seq 1 + F x t c x
66 56 ad2antrr φ c 0 +∞ x 1 +∞ F = a X L a 1 a
67 66 seqeq3d φ c 0 +∞ x 1 +∞ seq 1 + F = seq 1 + a X L a 1 a
68 67 fveq1d φ c 0 +∞ x 1 +∞ seq 1 + F x = seq 1 + a X L a 1 a x
69 68 fvoveq1d φ c 0 +∞ x 1 +∞ seq 1 + F x t = seq 1 + a X L a 1 a x t
70 elrege0 c 0 +∞ c 0 c
71 70 simplbi c 0 +∞ c
72 71 ad2antlr φ c 0 +∞ x 1 +∞ c
73 72 recnd φ c 0 +∞ x 1 +∞ c
74 1re 1
75 elicopnf 1 x 1 +∞ x 1 x
76 74 75 ax-mp x 1 +∞ x 1 x
77 76 simplbi x 1 +∞ x
78 77 adantl φ c 0 +∞ x 1 +∞ x
79 0red φ c 0 +∞ x 1 +∞ 0
80 1red φ c 0 +∞ x 1 +∞ 1
81 0lt1 0 < 1
82 81 a1i φ c 0 +∞ x 1 +∞ 0 < 1
83 76 simprbi x 1 +∞ 1 x
84 83 adantl φ c 0 +∞ x 1 +∞ 1 x
85 79 80 78 82 84 ltletrd φ c 0 +∞ x 1 +∞ 0 < x
86 78 85 elrpd φ c 0 +∞ x 1 +∞ x +
87 86 rpsqrtcld φ c 0 +∞ x 1 +∞ x +
88 87 rpcnd φ c 0 +∞ x 1 +∞ x
89 87 rpne0d φ c 0 +∞ x 1 +∞ x 0
90 73 88 89 divrecd φ c 0 +∞ x 1 +∞ c x = c 1 x
91 69 90 breq12d φ c 0 +∞ x 1 +∞ seq 1 + F x t c x seq 1 + a X L a 1 a x t c 1 x
92 91 ralbidva φ c 0 +∞ x 1 +∞ seq 1 + F x t c x x 1 +∞ seq 1 + a X L a 1 a x t c 1 x
93 65 92 syl5bb φ c 0 +∞ y 1 +∞ seq 1 + F y t c y x 1 +∞ seq 1 + a X L a 1 a x t c 1 x
94 59 93 anbi12d φ c 0 +∞ seq 1 + F t y 1 +∞ seq 1 + F y t c y seq 1 + a X L a 1 a t x 1 +∞ seq 1 + a X L a 1 a x t c 1 x
95 94 rexbidva φ c 0 +∞ seq 1 + F t y 1 +∞ seq 1 + F y t c y c 0 +∞ seq 1 + a X L a 1 a t x 1 +∞ seq 1 + a X L a 1 a x t c 1 x
96 95 exbidv φ t c 0 +∞ seq 1 + F t y 1 +∞ seq 1 + F y t c y t c 0 +∞ seq 1 + a X L a 1 a t x 1 +∞ seq 1 + a X L a 1 a x t c 1 x
97 41 96 mpbird φ t c 0 +∞ seq 1 + F t y 1 +∞ seq 1 + F y t c y