Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrvmasumlem2 Unicode version

Theorem dchrvmasumlem2 20647
 Description: Lemma for dchrvmasum 20674. (Contributed by Mario Carneiro, 4-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z ℤ/n
rpvmasum.l RHom
rpvmasum.a
rpvmasum.g DChr
rpvmasum.d
rpvmasum.1
dchrisum.b
dchrisum.n1
dchrvmasum.f
dchrvmasum.g
dchrvmasum.c
dchrvmasum.t
dchrvmasum.1
dchrvmasum.r
dchrvmasum.2
Assertion
Ref Expression
dchrvmasumlem2
Distinct variable groups:   ,,   ,,,   ,,   ,   ,,   ,,,   ,,,   ,,,   ,,   ,,   ,,,   ,,,
Allowed substitution hints:   ()   ()   ()   (,,)   (,)   ()   ()

Proof of Theorem dchrvmasumlem2
StepHypRef Expression
1 1re 8837 . . 3
21a1i 10 . 2
3 dchrvmasum.c . . . . . . 7
4 elrege0 10746 . . . . . . 7
53, 4sylib 188 . . . . . 6
65simpld 445 . . . . 5
76adantr 451 . . . 4
8 fzfid 11035 . . . . 5
9 simpr 447 . . . . . . . 8
10 elfznn 10819 . . . . . . . . 9
1110nnrpd 10389 . . . . . . . 8
12 rpdivcl 10376 . . . . . . . 8
139, 11, 12syl2an 463 . . . . . . 7
14 relogcl 19932 . . . . . . 7
1513, 14syl 15 . . . . . 6
169adantr 451 . . . . . 6
1715, 16rerpdivcld 10417 . . . . 5
188, 17fsumrecl 12207 . . . 4
197, 18remulcld 8863 . . 3
20 dchrvmasum.r . . . . 5
21 3nn 9878 . . . . . . 7
22 nnrp 10363 . . . . . . 7
23 relogcl 19932 . . . . . . 7
2421, 22, 23mp2b 9 . . . . . 6
2524, 1readdcli 8850 . . . . 5
26 remulcl 8822 . . . . 5
2720, 25, 26sylancl 643 . . . 4
29 rpssre 10364 . . . . 5
306recnd 8861 . . . . 5
31 o1const 12093 . . . . 5
3229, 30, 31sylancr 644 . . . 4
33 logfacrlim2 20465 . . . . 5
34 rlimo1 12090 . . . . 5
3533, 34mp1i 11 . . . 4
367, 18, 32, 35o1mul2 12098 . . 3
3727recnd 8861 . . . 4
38 o1const 12093 . . . 4
3929, 37, 38sylancr 644 . . 3
4019, 28, 36, 39o1add2 12097 . 2
42 dchrvmasum.f . . . . . . . . . 10
4342ralrimiva 2626 . . . . . . . . 9
4443ad2antrr 706 . . . . . . . 8
45 dchrvmasum.g . . . . . . . . . 10
4645eleq1d 2349 . . . . . . . . 9
4746rspcv 2880 . . . . . . . 8
4813, 44, 47sylc 56 . . . . . . 7
49 dchrvmasum.t . . . . . . . 8
5049ad2antrr 706 . . . . . . 7
5148, 50subcld 9157 . . . . . 6
5251abscld 11918 . . . . 5
5310adantl 452 . . . . 5
5452, 53nndivred 9794 . . . 4
558, 54fsumrecl 12207 . . 3
5655recnd 8861 . 2
5753nnrpd 10389 . . . . . . . 8
5851absge0d 11926 . . . . . . . 8
5952, 57, 58divge0d 10426 . . . . . . 7
608, 54, 59fsumge0 12253 . . . . . 6
6155, 60absidd 11905 . . . . 5
6261, 55eqeltrd 2357 . . . 4
6341recnd 8861 . . . . 5
6463abscld 11918 . . . 4
65 3re 9817 . . . . . . . 8
6665a1i 10 . . . . . . 7
67 1lt3 9888 . . . . . . . 8
681, 65, 67ltleii 8941 . . . . . . 7
6966, 68jctir 524 . . . . . 6
7020adantr 451 . . . . . . 7
71 rexr 8877 . . . . . . . . . . 11
721, 71ax-mp 8 . . . . . . . . . 10
73 rexr 8877 . . . . . . . . . . 11
7465, 73ax-mp 8 . . . . . . . . . 10
75 lbico1 10706 . . . . . . . . . 10
7672, 74, 67, 75mp3an 1277 . . . . . . . . 9
77 0re 8838 . . . . . . . . . . . 12
7877a1i 10 . . . . . . . . . . 11
79 elico2 10714 . . . . . . . . . . . . . . 15
801, 74, 79mp2an 653 . . . . . . . . . . . . . 14
8180simp1bi 970 . . . . . . . . . . . . 13
8277a1i 10 . . . . . . . . . . . . . 14
831a1i 10 . . . . . . . . . . . . . 14
84 0lt1 9296 . . . . . . . . . . . . . . 15
8584a1i 10 . . . . . . . . . . . . . 14
8680simp2bi 971 . . . . . . . . . . . . . 14
8782, 83, 81, 85, 86ltletrd 8976 . . . . . . . . . . . . 13
8881, 87elrpd 10388 . . . . . . . . . . . 12
8949adantr 451 . . . . . . . . . . . . . 14
9042, 89subcld 9157 . . . . . . . . . . . . 13
9190abscld 11918 . . . . . . . . . . . 12
9288, 91sylan2 460 . . . . . . . . . . 11
9320adantr 451 . . . . . . . . . . 11
9490absge0d 11926 . . . . . . . . . . . 12
9588, 94sylan2 460 . . . . . . . . . . 11
96 dchrvmasum.2 . . . . . . . . . . . 12
9796r19.21bi 2641 . . . . . . . . . . 11
9878, 92, 93, 95, 97letrd 8973 . . . . . . . . . 10
9998ralrimiva 2626 . . . . . . . . 9
100 biidd 228 . . . . . . . . . 10
101100rspcv 2880 . . . . . . . . 9
10276, 99, 101mpsyl 59 . . . . . . . 8
103102adantr 451 . . . . . . 7
10470, 103jca 518 . . . . . 6
10552recnd 8861 . . . . . 6
1066ad2antrr 706 . . . . . . 7
107106, 17remulcld 8863 . . . . . 6
1085ad2antrr 706 . . . . . . 7
109 log1 19939 . . . . . . . . 9
11053nncnd 9762 . . . . . . . . . . . . 13
111110mulid2d 8853 . . . . . . . . . . . 12
112 rpre 10360 . . . . . . . . . . . . . . 15
113112adantl 452 . . . . . . . . . . . . . 14
114 fznnfl 10966 . . . . . . . . . . . . . 14
115113, 114syl 15 . . . . . . . . . . . . 13
116115simplbda 607 . . . . . . . . . . . 12
117111, 116eqbrtrd 4043 . . . . . . . . . . 11
1181a1i 10 . . . . . . . . . . . 12
119112ad2antlr 707 . . . . . . . . . . . 12
120118, 119, 57lemuldivd 10435 . . . . . . . . . . 11
121117, 120mpbid 201 . . . . . . . . . 10
122 1rp 10358 . . . . . . . . . . . 12
123122a1i 10 . . . . . . . . . . 11
124123, 13logled 19978 . . . . . . . . . 10
125121, 124mpbid 201 . . . . . . . . 9
126109, 125syl5eqbrr 4057 . . . . . . . 8
127 rpregt0 10367 . . . . . . . . 9
128127ad2antlr 707 . . . . . . . 8
129 divge0 9625 . . . . . . . 8
13015, 126, 128, 129syl21anc 1181 . . . . . . 7
131 mulge0 9291 . . . . . . 7
132108, 17, 130, 131syl12anc 1180 . . . . . 6
133 absidm 11807 . . . . . . . . 9
13451, 133syl 15 . . . . . . . 8
135134adantr 451 . . . . . . 7
136 nndivre 9781 . . . . . . . . . . . 12
137113, 10, 136syl2an 463 . . . . . . . . . . 11
138137adantr 451 . . . . . . . . . 10
139 simpr 447 . . . . . . . . . 10
140 elicopnf 10739 . . . . . . . . . . 11
14165, 140ax-mp 8 . . . . . . . . . 10
142138, 139, 141sylanbrc 645 . . . . . . . . 9
143 dchrvmasum.1 . . . . . . . . . . 11
144143ralrimiva 2626 . . . . . . . . . 10
145144ad3antrrr 710 . . . . . . . . 9
14645oveq1d 5873 . . . . . . . . . . . 12
147146fveq2d 5529 . . . . . . . . . . 11
148 fveq2 5525 . . . . . . . . . . . . 13
149 id 19 . . . . . . . . . . . . 13
150148, 149oveq12d 5876 . . . . . . . . . . . 12
151150oveq2d 5874 . . . . . . . . . . 11
152147, 151breq12d 4036 . . . . . . . . . 10
153152rspcv 2880 . . . . . . . . 9
154142, 145, 153sylc 56 . . . . . . . 8
15515recnd 8861 . . . . . . . . . . . . 13
156 rpcnne0 10371 . . . . . . . . . . . . . 14
157156ad2antlr 707 . . . . . . . . . . . . 13
158 rpcnne0 10371 . . . . . . . . . . . . . 14
15957, 158syl 15 . . . . . . . . . . . . 13
160 divdiv2 9472 . . . . . . . . . . . . 13
161155, 157, 159, 160syl3anc 1182 . . . . . . . . . . . 12
162 div23 9443 . . . . . . . . . . . . 13
163155, 110, 157, 162syl3anc 1182 . . . . . . . . . . . 12
164161, 163eqtrd 2315 . . . . . . . . . . 11
165164oveq2d 5874 . . . . . . . . . 10
16630ad2antrr 706 . . . . . . . . . . 11
16717recnd 8861 . . . . . . . . . . 11
168166, 167, 110mulassd 8858 . . . . . . . . . 10
169165, 168eqtr4d 2318 . . . . . . . . 9
170169adantr 451 . . . . . . . 8
171154, 170breqtrd 4047 . . . . . . 7
172135, 171eqbrtrd 4043 . . . . . 6
173134adantr 451 . . . . . . 7
174137adantr 451 . . . . . . . . 9
175121adantr 451 . . . . . . . . 9
176 simpr 447 . . . . . . . . 9
177 elico2 10714 . . . . . . . . . 10
1781, 74, 177mp2an 653 . . . . . . . . 9
179174, 175, 176, 178syl3anbrc 1136 . . . . . . . 8
18096ad3antrrr 710 . . . . . . . 8
181147breq1d 4033 . . . . . . . . 9
182181rspcv 2880 . . . . . . . 8
183179, 180, 182sylc 56 . . . . . . 7
184173, 183eqbrtrd 4043 . . . . . 6
1859, 69, 104, 105, 107, 132, 172, 184fsumharmonic 20305 . . . . 5
18630adantr 451 . . . . . . 7
1878, 186, 167fsummulc2 12246 . . . . . 6
188187oveq1d 5873 . . . . 5
189185, 188breqtrrd 4049 . . . 4
19041leabsd 11897 . . . 4
19162, 41, 64, 189, 190letrd 8973 . . 3