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

Theorem dchrvmasumlem3 20648
 Description: Lemma for dchrvmasum 20674. (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 1re 8837 . . 3
21a1i 10 . 2
3 rpvmasum.z . . 3 ℤ/n
4 rpvmasum.l . . 3 RHom
5 rpvmasum.a . . 3
6 rpvmasum.g . . 3 DChr
7 rpvmasum.d . . 3
8 rpvmasum.1 . . 3
9 dchrisum.b . . 3
10 dchrisum.n1 . . 3
11 dchrvmasum.f . . 3
12 dchrvmasum.g . . 3
13 dchrvmasum.c . . 3
14 dchrvmasum.t . . 3
15 dchrvmasum.1 . . 3
16 dchrvmasum.r . . 3
17 dchrvmasum.2 . . 3
183, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17dchrvmasumlem2 20647 . 2
19 fzfid 11035 . . 3
20 simpr 447 . . . . . . . 8
21 elfznn 10819 . . . . . . . . 9
2221nnrpd 10389 . . . . . . . 8
23 rpdivcl 10376 . . . . . . . 8
2420, 22, 23syl2an 463 . . . . . . 7
2511ralrimiva 2626 . . . . . . . 8
2625ad2antrr 706 . . . . . . 7
2712eleq1d 2349 . . . . . . . 8
2827rspcv 2880 . . . . . . 7
2924, 26, 28sylc 56 . . . . . 6
3014ad2antrr 706 . . . . . 6
3129, 30subcld 9157 . . . . 5
3231abscld 11918 . . . 4
3321adantl 452 . . . 4
3432, 33nndivred 9794 . . 3
3519, 34fsumrecl 12207 . 2
369ad2antrr 706 . . . . . 6
37 elfzelz 10798 . . . . . . 7
3837adantl 452 . . . . . 6
396, 3, 7, 4, 36, 38dchrzrhcl 20484 . . . . 5
40 mucl 20379 . . . . . . . . 9
4133, 40syl 15 . . . . . . . 8
4241zred 10117 . . . . . . 7
4342, 33nndivred 9794 . . . . . 6
4443recnd 8861 . . . . 5
4539, 44mulcld 8855 . . . 4
4645, 31mulcld 8855 . . 3
4719, 46fsumcl 12206 . 2
4847abscld 11918 . . . 4
4935recnd 8861 . . . . 5
5049abscld 11918 . . . 4
5146abscld 11918 . . . . . 6
5219, 51fsumrecl 12207 . . . . 5
5319, 46fsumabs 12259 . . . . 5
5445abscld 11918 . . . . . . . 8
5533nnrecred 9791 . . . . . . . 8
5631absge0d 11926 . . . . . . . 8
5739, 44absmuld 11936 . . . . . . . . 9
5839abscld 11918 . . . . . . . . . . 11
591a1i 10 . . . . . . . . . . 11
6044abscld 11918 . . . . . . . . . . 11
6139absge0d 11926 . . . . . . . . . . 11
6244absge0d 11926 . . . . . . . . . . 11
63 eqid 2283 . . . . . . . . . . . 12
645nnnn0d 10018 . . . . . . . . . . . . . . . 16
653, 63, 4znzrhfo 16501 . . . . . . . . . . . . . . . 16
6664, 65syl 15 . . . . . . . . . . . . . . 15
67 fof 5451 . . . . . . . . . . . . . . 15
6866, 67syl 15 . . . . . . . . . . . . . 14
6968ad2antrr 706 . . . . . . . . . . . . 13
70 ffvelrn 5663 . . . . . . . . . . . . 13
7169, 38, 70syl2anc 642 . . . . . . . . . . . 12
726, 7, 3, 63, 36, 71dchrabs2 20501 . . . . . . . . . . 11
7342recnd 8861 . . . . . . . . . . . . . 14
7433nncnd 9762 . . . . . . . . . . . . . 14
7533nnne0d 9790 . . . . . . . . . . . . . 14
7673, 74, 75absdivd 11937 . . . . . . . . . . . . 13
7733nnrpd 10389 . . . . . . . . . . . . . . . 16
7877rprege0d 10397 . . . . . . . . . . . . . . 15
79 absid 11781 . . . . . . . . . . . . . . 15
8078, 79syl 15 . . . . . . . . . . . . . 14
8180oveq2d 5874 . . . . . . . . . . . . 13
8276, 81eqtrd 2315 . . . . . . . . . . . 12
8373abscld 11918 . . . . . . . . . . . . 13
84 mule1 20386 . . . . . . . . . . . . . 14
8533, 84syl 15 . . . . . . . . . . . . 13
8683, 59, 77, 85lediv1dd 10444 . . . . . . . . . . . 12
8782, 86eqbrtrd 4043 . . . . . . . . . . 11
8858, 59, 60, 55, 61, 62, 72, 87lemul12ad 9699 . . . . . . . . . 10
8955recnd 8861 . . . . . . . . . . 11
9089mulid2d 8853 . . . . . . . . . 10
9188, 90breqtrd 4047 . . . . . . . . 9
9257, 91eqbrtrd 4043 . . . . . . . 8
9354, 55, 32, 56, 92lemul1ad 9696 . . . . . . 7
9445, 31absmuld 11936 . . . . . . 7
9532recnd 8861 . . . . . . . 8
9695, 74, 75divrec2d 9540 . . . . . . 7
9793, 94, 963brtr4d 4053 . . . . . 6
9819, 51, 34, 97fsumle 12257 . . . . 5
9948, 52, 35, 53, 98letrd 8973 . . . 4
10035leabsd 11897 . . . 4
10148, 35, 50, 99, 100letrd 8973 . . 3