Metamath Proof Explorer


Theorem dchrvmasumiflem2

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 5-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˙
dchrvmasumif.f F=aXLaa
dchrvmasumif.c φC0+∞
dchrvmasumif.s φseq1+FS
dchrvmasumif.1 φy1+∞seq1+FySCy
dchrvmasumif.g K=aXLalogaa
dchrvmasumif.e φE0+∞
dchrvmasumif.t φseq1+KT
dchrvmasumif.2 φy3+∞seq1+KyTElogyy
Assertion dchrvmasumiflem2 φx+n=1xXLnΛnn+ifS=0logx0𝑂1

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 dchrvmasumif.f F=aXLaa
10 dchrvmasumif.c φC0+∞
11 dchrvmasumif.s φseq1+FS
12 dchrvmasumif.1 φy1+∞seq1+FySCy
13 dchrvmasumif.g K=aXLalogaa
14 dchrvmasumif.e φE0+∞
15 dchrvmasumif.t φseq1+KT
16 dchrvmasumif.2 φy3+∞seq1+KyTElogyy
17 1red φ1
18 fzfid φx+1xFin
19 7 ad2antrr φx+d1xXD
20 elfzelz d1xd
21 20 adantl φx+d1xd
22 4 1 5 2 19 21 dchrzrhcl φx+d1xXLd
23 elfznn d1xd
24 23 adantl φx+d1xd
25 mucl dμd
26 24 25 syl φx+d1xμd
27 26 zred φx+d1xμd
28 27 24 nndivred φx+d1xμdd
29 28 recnd φx+d1xμdd
30 22 29 mulcld φx+d1xXLdμdd
31 18 30 fsumcl φx+d=1xXLdμdd
32 climcl seq1+FSS
33 11 32 syl φS
34 33 adantr φx+S
35 31 34 mulcld φx+d=1xXLdμddS
36 0cnd φS=00
37 df-ne S0¬S=0
38 climcl seq1+KTT
39 15 38 syl φT
40 39 adantr φS0T
41 33 adantr φS0S
42 simpr φS0S0
43 40 41 42 divcld φS0TS
44 37 43 sylan2br φ¬S=0TS
45 36 44 ifclda φifS=00TS
46 45 adantr φx+ifS=00TS
47 1 2 3 4 5 6 7 8 9 10 11 12 dchrmusum2 φx+d=1xXLdμddS𝑂1
48 rpssre +
49 o1const +ifS=00TSx+ifS=00TS𝑂1
50 48 45 49 sylancr φx+ifS=00TS𝑂1
51 35 46 47 50 o1mul2 φx+d=1xXLdμddSifS=00TS𝑂1
52 fzfid φx+d1x1xdFin
53 19 adantr φx+d1xk1xdXD
54 elfzelz k1xdk
55 54 adantl φx+d1xk1xdk
56 4 1 5 2 53 55 dchrzrhcl φx+d1xk1xdXLk
57 simpr φx+x+
58 23 nnrpd d1xd+
59 rpdivcl x+d+xd+
60 57 58 59 syl2an φx+d1xxd+
61 elfznn k1xdk
62 61 nnrpd k1xdk+
63 ifcl xd+k+ifS=0xdk+
64 60 62 63 syl2an φx+d1xk1xdifS=0xdk+
65 64 relogcld φx+d1xk1xdlogifS=0xdk
66 61 adantl φx+d1xk1xdk
67 65 66 nndivred φx+d1xk1xdlogifS=0xdkk
68 67 recnd φx+d1xk1xdlogifS=0xdkk
69 56 68 mulcld φx+d1xk1xdXLklogifS=0xdkk
70 52 69 fsumcl φx+d1xk=1xdXLklogifS=0xdkk
71 30 70 mulcld φx+d1xXLdμddk=1xdXLklogifS=0xdkk
72 18 71 fsumcl φx+d=1xXLdμddk=1xdXLklogifS=0xdkk
73 35 46 mulcld φx+d=1xXLdμddSifS=00TS
74 0cn 0
75 39 ad2antrr φx+d1xT
76 ifcl 0TifS=00T
77 74 75 76 sylancr φx+d1xifS=00T
78 30 70 77 subdid φx+d1xXLdμddk=1xdXLklogifS=0xdkkifS=00T=XLdμddk=1xdXLklogifS=0xdkkXLdμddifS=00T
79 78 sumeq2dv φx+d=1xXLdμddk=1xdXLklogifS=0xdkkifS=00T=d=1xXLdμddk=1xdXLklogifS=0xdkkXLdμddifS=00T
80 30 77 mulcld φx+d1xXLdμddifS=00T
81 18 71 80 fsumsub φx+d=1xXLdμddk=1xdXLklogifS=0xdkkXLdμddifS=00T=d=1xXLdμddk=1xdXLklogifS=0xdkkd=1xXLdμddifS=00T
82 31 34 46 mulassd φx+d=1xXLdμddSifS=00TS=d=1xXLdμddSifS=00TS
83 ovif2 SifS=00TS=ifS=0S0STS
84 33 mul01d φS0=0
85 84 ifeq1d φifS=0S0STS=ifS=00STS
86 40 41 42 divcan2d φS0STS=T
87 37 86 sylan2br φ¬S=0STS=T
88 87 ifeq2da φifS=00STS=ifS=00T
89 85 88 eqtrd φifS=0S0STS=ifS=00T
90 83 89 eqtrid φSifS=00TS=ifS=00T
91 90 adantr φx+SifS=00TS=ifS=00T
92 91 oveq2d φx+d=1xXLdμddSifS=00TS=d=1xXLdμddifS=00T
93 74 39 76 sylancr φifS=00T
94 93 adantr φx+ifS=00T
95 18 94 30 fsummulc1 φx+d=1xXLdμddifS=00T=d=1xXLdμddifS=00T
96 82 92 95 3eqtrrd φx+d=1xXLdμddifS=00T=d=1xXLdμddSifS=00TS
97 96 oveq2d φx+d=1xXLdμddk=1xdXLklogifS=0xdkkd=1xXLdμddifS=00T=d=1xXLdμddk=1xdXLklogifS=0xdkkd=1xXLdμddSifS=00TS
98 79 81 97 3eqtrd φx+d=1xXLdμddk=1xdXLklogifS=0xdkkifS=00T=d=1xXLdμddk=1xdXLklogifS=0xdkkd=1xXLdμddSifS=00TS
99 98 mpteq2dva φx+d=1xXLdμddk=1xdXLklogifS=0xdkkifS=00T=x+d=1xXLdμddk=1xdXLklogifS=0xdkkd=1xXLdμddSifS=00TS
100 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 dchrvmasumiflem1 φx+d=1xXLdμddk=1xdXLklogifS=0xdkkifS=00T𝑂1
101 99 100 eqeltrrd φx+d=1xXLdμddk=1xdXLklogifS=0xdkkd=1xXLdμddSifS=00TS𝑂1
102 72 73 101 o1dif φx+d=1xXLdμddk=1xdXLklogifS=0xdkk𝑂1x+d=1xXLdμddSifS=00TS𝑂1
103 51 102 mpbird φx+d=1xXLdμddk=1xdXLklogifS=0xdkk𝑂1
104 7 ad2antrr φx+n1xXD
105 elfzelz n1xn
106 105 adantl φx+n1xn
107 4 1 5 2 104 106 dchrzrhcl φx+n1xXLn
108 elfznn n1xn
109 108 adantl φx+n1xn
110 vmacl nΛn
111 nndivre ΛnnΛnn
112 110 111 mpancom nΛnn
113 109 112 syl φx+n1xΛnn
114 113 recnd φx+n1xΛnn
115 107 114 mulcld φx+n1xXLnΛnn
116 18 115 fsumcl φx+n=1xXLnΛnn
117 relogcl x+logx
118 117 adantl φx+logx
119 118 recnd φx+logx
120 ifcl logx0ifS=0logx0
121 119 74 120 sylancl φx+ifS=0logx0
122 116 121 addcld φx+n=1xXLnΛnn+ifS=0logx0
123 122 abscld φx+n=1xXLnΛnn+ifS=0logx0
124 123 adantrr φx+1xn=1xXLnΛnn+ifS=0logx0
125 3 adantr φx+1xN
126 7 adantr φx+1xXD
127 8 adantr φx+1xX1˙
128 simprl φx+1xx+
129 simprr φx+1x1x
130 1 2 125 4 5 6 126 127 128 129 dchrvmasum2if φx+1xn=1xXLnΛnn+ifS=0logx0=d=1xXLdμddk=1xdXLklogifS=0xdkk
131 130 fveq2d φx+1xn=1xXLnΛnn+ifS=0logx0=d=1xXLdμddk=1xdXLklogifS=0xdkk
132 124 131 eqled φx+1xn=1xXLnΛnn+ifS=0logx0d=1xXLdμddk=1xdXLklogifS=0xdkk
133 17 103 72 122 132 o1le φx+n=1xXLnΛnn+ifS=0logx0𝑂1