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

Theorem dchrvmasumlem3 24416
 Description: Lemma for dchrvmasum 24442. (Contributed by Mario Carneiro, 3-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
dchrvmasumlem3
Distinct variable groups:   ,,   ,,,   ,,   ,   ,,   ,,,   ,,,   ,,,   ,,   ,,   ,,,   ,,,
Allowed substitution hints:   ()   ()   ()   (,,)   (,)   ()   ()

Proof of Theorem dchrvmasumlem3
StepHypRef Expression
1 1red 9676 . 2
2 rpvmasum.z . . 3 ℤ/n
3 rpvmasum.l . . 3 RHom
4 rpvmasum.a . . 3
5 rpvmasum.g . . 3 DChr
6 rpvmasum.d . . 3
7 rpvmasum.1 . . 3
8 dchrisum.b . . 3
9 dchrisum.n1 . . 3
10 dchrvmasum.f . . 3
11 dchrvmasum.g . . 3
12 dchrvmasum.c . . 3
13 dchrvmasum.t . . 3
14 dchrvmasum.1 . . 3
15 dchrvmasum.r . . 3
16 dchrvmasum.2 . . 3
172, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16dchrvmasumlem2 24415 . 2
18 fzfid 12224 . . 3
19 simpr 468 . . . . . . . 8
20 elfznn 11854 . . . . . . . . 9
2120nnrpd 11362 . . . . . . . 8
22 rpdivcl 11348 . . . . . . . 8
2319, 21, 22syl2an 485 . . . . . . 7
2410ralrimiva 2809 . . . . . . . 8
2524ad2antrr 740 . . . . . . 7
2611eleq1d 2533 . . . . . . . 8
2726rspcv 3132 . . . . . . 7
2823, 25, 27sylc 61 . . . . . 6
2913ad2antrr 740 . . . . . 6
3028, 29subcld 10005 . . . . 5
3130abscld 13575 . . . 4
3220adantl 473 . . . 4
3331, 32nndivred 10680 . . 3
3418, 33fsumrecl 13877 . 2
358ad2antrr 740 . . . . . 6
36 elfzelz 11826 . . . . . . 7
3736adantl 473 . . . . . 6
385, 2, 6, 3, 35, 37dchrzrhcl 24252 . . . . 5
39 mucl 24147 . . . . . . . . 9
4032, 39syl 17 . . . . . . . 8
4140zred 11063 . . . . . . 7
4241, 32nndivred 10680 . . . . . 6
4342recnd 9687 . . . . 5
4438, 43mulcld 9681 . . . 4
4544, 30mulcld 9681 . . 3
4618, 45fsumcl 13876 . 2
4746abscld 13575 . . . 4
4834recnd 9687 . . . . 5
4948abscld 13575 . . . 4
5045abscld 13575 . . . . . 6
5118, 50fsumrecl 13877 . . . . 5
5218, 45fsumabs 13938 . . . . 5
5344abscld 13575 . . . . . . . 8
5432nnrecred 10677 . . . . . . . 8
5530absge0d 13583 . . . . . . . 8
5638, 43absmuld 13593 . . . . . . . . 9
5738abscld 13575 . . . . . . . . . . 11
58 1red 9676 . . . . . . . . . . 11
5943abscld 13575 . . . . . . . . . . 11
6038absge0d 13583 . . . . . . . . . . 11
6143absge0d 13583 . . . . . . . . . . 11
62 eqid 2471 . . . . . . . . . . . 12
634nnnn0d 10949 . . . . . . . . . . . . . . . 16
642, 62, 3znzrhfo 19195 . . . . . . . . . . . . . . . 16
6563, 64syl 17 . . . . . . . . . . . . . . 15
66 fof 5806 . . . . . . . . . . . . . . 15
6765, 66syl 17 . . . . . . . . . . . . . 14
6867ad2antrr 740 . . . . . . . . . . . . 13
6968, 37ffvelrnd 6038 . . . . . . . . . . . 12
705, 6, 2, 62, 35, 69dchrabs2 24269 . . . . . . . . . . 11
7141recnd 9687 . . . . . . . . . . . . . 14
7232nncnd 10647 . . . . . . . . . . . . . 14
7332nnne0d 10676 . . . . . . . . . . . . . 14
7471, 72, 73absdivd 13594 . . . . . . . . . . . . 13
7532nnrpd 11362 . . . . . . . . . . . . . . . 16
7675rprege0d 11371 . . . . . . . . . . . . . . 15
77 absid 13436 . . . . . . . . . . . . . . 15
7876, 77syl 17 . . . . . . . . . . . . . 14
7978oveq2d 6324 . . . . . . . . . . . . 13
8074, 79eqtrd 2505 . . . . . . . . . . . 12
8171abscld 13575 . . . . . . . . . . . . 13
82 mule1 24154 . . . . . . . . . . . . . 14
8332, 82syl 17 . . . . . . . . . . . . 13
8481, 58, 75, 83lediv1dd 11419 . . . . . . . . . . . 12
8580, 84eqbrtrd 4416 . . . . . . . . . . 11
8657, 58, 59, 54, 60, 61, 70, 85lemul12ad 10571 . . . . . . . . . 10
8754recnd 9687 . . . . . . . . . . 11
8887mulid2d 9679 . . . . . . . . . 10
8986, 88breqtrd 4420 . . . . . . . . 9
9056, 89eqbrtrd 4416 . . . . . . . 8
9153, 54, 31, 55, 90lemul1ad 10568 . . . . . . 7
9244, 30absmuld 13593 . . . . . . 7
9331recnd 9687 . . . . . . . 8
9493, 72, 73divrec2d 10409 . . . . . . 7
9591, 92, 943brtr4d 4426 . . . . . 6
9618, 50, 33, 95fsumle 13936 . . . . 5
9747, 51, 34, 52, 96letrd 9809 . . . 4
9834leabsd 13553 . . . 4
9947, 34, 49, 97, 98letrd 9809 . . 3