Metamath Proof Explorer


Theorem dchrmusumlema

Description: Lemma for dchrmusum and dchrisumn0 . Apply dchrisum for the function 1 / y . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses rpvmasum.z Z=/N
rpvmasum.l L=ℤRHomZ
rpvmasum.a φN
rpvmasum.g G=DChrN
rpvmasum.d D=BaseG
rpvmasum.1 1˙=0G
dchrisum.b φXD
dchrisum.n1 φX1˙
dchrisumn0.f F=aXLaa
Assertion dchrmusumlema φtc0+∞seq1+Fty1+∞seq1+Fytcy

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z=/N
2 rpvmasum.l L=ℤRHomZ
3 rpvmasum.a φN
4 rpvmasum.g G=DChrN
5 rpvmasum.d D=BaseG
6 rpvmasum.1 1˙=0G
7 dchrisum.b φXD
8 dchrisum.n1 φX1˙
9 dchrisumn0.f F=aXLaa
10 oveq2 n=x1n=1x
11 1nn 1
12 11 a1i φ1
13 rpreccl n+1n+
14 13 adantl φn+1n+
15 14 rpred φn+1n
16 simp3r φn+x+1nnxnx
17 rpregt0 n+n0<n
18 rpregt0 x+x0<x
19 lerec n0<nx0<xnx1x1n
20 17 18 19 syl2an n+x+nx1x1n
21 20 3ad2ant2 φn+x+1nnxnx1x1n
22 16 21 mpbid φn+x+1nnx1x1n
23 ax-1cn 1
24 divrcnv 1n+1n0
25 23 24 mp1i φn+1n0
26 2fveq3 a=nXLa=XLn
27 oveq2 a=n1a=1n
28 26 27 oveq12d a=nXLa1a=XLn1n
29 28 cbvmptv aXLa1a=nXLn1n
30 1 2 3 4 5 6 7 8 10 12 15 22 25 29 dchrisum φtc0+∞seq1+aXLa1atx1+∞seq1+aXLa1axtc1x
31 7 adantr φnXD
32 nnz nn
33 32 adantl φnn
34 4 1 5 2 31 33 dchrzrhcl φnXLn
35 nncn nn
36 35 adantl φnn
37 nnne0 nn0
38 37 adantl φnn0
39 34 36 38 divrecd φnXLnn=XLn1n
40 39 mpteq2dva φnXLnn=nXLn1n
41 id a=na=n
42 26 41 oveq12d a=nXLaa=XLnn
43 42 cbvmptv aXLaa=nXLnn
44 9 43 eqtri F=nXLnn
45 40 44 29 3eqtr4g φF=aXLa1a
46 45 adantr φc0+∞F=aXLa1a
47 46 seqeq3d φc0+∞seq1+F=seq1+aXLa1a
48 47 breq1d φc0+∞seq1+Ftseq1+aXLa1at
49 2fveq3 y=xseq1+Fy=seq1+Fx
50 49 fvoveq1d y=xseq1+Fyt=seq1+Fxt
51 oveq2 y=xcy=cx
52 50 51 breq12d y=xseq1+Fytcyseq1+Fxtcx
53 52 cbvralvw y1+∞seq1+Fytcyx1+∞seq1+Fxtcx
54 45 seqeq3d φseq1+F=seq1+aXLa1a
55 54 fveq1d φseq1+Fx=seq1+aXLa1ax
56 55 fvoveq1d φseq1+Fxt=seq1+aXLa1axt
57 56 ad2antrr φc0+∞x1+∞seq1+Fxt=seq1+aXLa1axt
58 elrege0 c0+∞c0c
59 58 simplbi c0+∞c
60 59 recnd c0+∞c
61 60 ad2antlr φc0+∞x1+∞c
62 1re 1
63 elicopnf 1x1+∞x1x
64 62 63 ax-mp x1+∞x1x
65 64 simplbi x1+∞x
66 65 adantl φc0+∞x1+∞x
67 66 recnd φc0+∞x1+∞x
68 0red φc0+∞x1+∞0
69 1red φc0+∞x1+∞1
70 0lt1 0<1
71 70 a1i φc0+∞x1+∞0<1
72 64 simprbi x1+∞1x
73 72 adantl φc0+∞x1+∞1x
74 68 69 66 71 73 ltletrd φc0+∞x1+∞0<x
75 74 gt0ne0d φc0+∞x1+∞x0
76 61 67 75 divrecd φc0+∞x1+∞cx=c1x
77 57 76 breq12d φc0+∞x1+∞seq1+Fxtcxseq1+aXLa1axtc1x
78 77 ralbidva φc0+∞x1+∞seq1+Fxtcxx1+∞seq1+aXLa1axtc1x
79 53 78 syl5bb φc0+∞y1+∞seq1+Fytcyx1+∞seq1+aXLa1axtc1x
80 48 79 anbi12d φc0+∞seq1+Fty1+∞seq1+Fytcyseq1+aXLa1atx1+∞seq1+aXLa1axtc1x
81 80 rexbidva φc0+∞seq1+Fty1+∞seq1+Fytcyc0+∞seq1+aXLa1atx1+∞seq1+aXLa1axtc1x
82 81 exbidv φtc0+∞seq1+Fty1+∞seq1+Fytcytc0+∞seq1+aXLa1atx1+∞seq1+aXLa1axtc1x
83 30 82 mpbird φtc0+∞seq1+Fty1+∞seq1+Fytcy