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

Theorem dchrvmasumlem3 21195
 Description: Lemma for dchrvmasum 21221. (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 9092 . . 3
21a1i 11 . 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 21194 . 2
19 fzfid 11314 . . 3
20 simpr 449 . . . . . . . 8
21 elfznn 11082 . . . . . . . . 9
2221nnrpd 10649 . . . . . . . 8
23 rpdivcl 10636 . . . . . . . 8
2420, 22, 23syl2an 465 . . . . . . 7
2511ralrimiva 2791 . . . . . . . 8
2625ad2antrr 708 . . . . . . 7
2712eleq1d 2504 . . . . . . . 8
2827rspcv 3050 . . . . . . 7
2924, 26, 28sylc 59 . . . . . 6
3014ad2antrr 708 . . . . . 6
3129, 30subcld 9413 . . . . 5
3231abscld 12240 . . . 4
3321adantl 454 . . . 4
3432, 33nndivred 10050 . . 3
3519, 34fsumrecl 12530 . 2
369ad2antrr 708 . . . . . 6
37 elfzelz 11061 . . . . . . 7
3837adantl 454 . . . . . 6
396, 3, 7, 4, 36, 38dchrzrhcl 21031 . . . . 5
40 mucl 20926 . . . . . . . . 9
4133, 40syl 16 . . . . . . . 8
4241zred 10377 . . . . . . 7
4342, 33nndivred 10050 . . . . . 6
4443recnd 9116 . . . . 5
4539, 44mulcld 9110 . . . 4
4645, 31mulcld 9110 . . 3
4719, 46fsumcl 12529 . 2
4847abscld 12240 . . . 4
4935recnd 9116 . . . . 5
5049abscld 12240 . . . 4
5146abscld 12240 . . . . . 6
5219, 51fsumrecl 12530 . . . . 5
5319, 46fsumabs 12582 . . . . 5
5445abscld 12240 . . . . . . . 8
5533nnrecred 10047 . . . . . . . 8
5631absge0d 12248 . . . . . . . 8
5739, 44absmuld 12258 . . . . . . . . 9
5839abscld 12240 . . . . . . . . . . 11
591a1i 11 . . . . . . . . . . 11
6044abscld 12240 . . . . . . . . . . 11
6139absge0d 12248 . . . . . . . . . . 11
6244absge0d 12248 . . . . . . . . . . 11
63 eqid 2438 . . . . . . . . . . . 12
645nnnn0d 10276 . . . . . . . . . . . . . . . 16
653, 63, 4znzrhfo 16830 . . . . . . . . . . . . . . . 16
6664, 65syl 16 . . . . . . . . . . . . . . 15
67 fof 5655 . . . . . . . . . . . . . . 15
6866, 67syl 16 . . . . . . . . . . . . . 14
6968ad2antrr 708 . . . . . . . . . . . . 13
7069, 38ffvelrnd 5873 . . . . . . . . . . . 12
716, 7, 3, 63, 36, 70dchrabs2 21048 . . . . . . . . . . 11
7242recnd 9116 . . . . . . . . . . . . . 14
7333nncnd 10018 . . . . . . . . . . . . . 14
7433nnne0d 10046 . . . . . . . . . . . . . 14
7572, 73, 74absdivd 12259 . . . . . . . . . . . . 13
7633nnrpd 10649 . . . . . . . . . . . . . . . 16
7776rprege0d 10657 . . . . . . . . . . . . . . 15
78 absid 12103 . . . . . . . . . . . . . . 15
7977, 78syl 16 . . . . . . . . . . . . . 14
8079oveq2d 6099 . . . . . . . . . . . . 13
8175, 80eqtrd 2470 . . . . . . . . . . . 12
8272abscld 12240 . . . . . . . . . . . . 13
83 mule1 20933 . . . . . . . . . . . . . 14
8433, 83syl 16 . . . . . . . . . . . . 13
8582, 59, 76, 84lediv1dd 10704 . . . . . . . . . . . 12
8681, 85eqbrtrd 4234 . . . . . . . . . . 11
8758, 59, 60, 55, 61, 62, 71, 86lemul12ad 9955 . . . . . . . . . 10
8855recnd 9116 . . . . . . . . . . 11
8988mulid2d 9108 . . . . . . . . . 10
9087, 89breqtrd 4238 . . . . . . . . 9
9157, 90eqbrtrd 4234 . . . . . . . 8
9254, 55, 32, 56, 91lemul1ad 9952 . . . . . . 7
9345, 31absmuld 12258 . . . . . . 7
9432recnd 9116 . . . . . . . 8
9594, 73, 74divrec2d 9796 . . . . . . 7
9692, 93, 953brtr4d 4244 . . . . . 6
9719, 51, 34, 96fsumle 12580 . . . . 5
9848, 52, 35, 53, 97letrd 9229 . . . 4
9935leabsd 12219 . . . 4
10048, 35, 50, 98, 99letrd 9229 . . 3