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

Theorem mulgz 16289
 Description: A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
Hypotheses
Ref Expression
mulgnn0z.b
mulgnn0z.t .g
mulgnn0z.o
Assertion
Ref Expression
mulgz

Proof of Theorem mulgz
StepHypRef Expression
1 grpmnd 16188 . . . 4
3 mulgnn0z.b . . . 4
4 mulgnn0z.t . . . 4 .g
5 mulgnn0z.o . . . 4
63, 4, 5mulgnn0z 16288 . . 3
72, 6sylan 471 . 2
8 simpll 753 . . . 4
9 nn0z 10908 . . . . 5
109adantl 466 . . . 4
113, 5grpidcl 16204 . . . . 5
1211ad2antrr 725 . . . 4
13 eqid 2457 . . . . 5
143, 4, 13mulgneg 16286 . . . 4
158, 10, 12, 14syl3anc 1228 . . 3
16 zcn 10890 . . . . . 6
1716ad2antlr 726 . . . . 5
1817negnegd 9941 . . . 4
1918oveq1d 6311 . . 3
203, 4, 5mulgnn0z 16288 . . . . . 6
212, 20sylan 471 . . . . 5
2221fveq2d 5876 . . . 4
235, 13grpinvid 16227 . . . . 5
2423ad2antrr 725 . . . 4
2522, 24eqtrd 2498 . . 3
2615, 19, 253eqtr3d 2506 . 2
27 elznn0 10900 . . . 4
2827simprbi 464 . . 3