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

Theorem cygznlem1 16839
 Description: Lemma for cygzn 16843. (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
cygzn.b
cygzn.n
cygzn.y ℤ/n
cygzn.m .g
cygzn.l RHom
cygzn.e
cygzn.g CycGrp
cygzn.x
Assertion
Ref Expression
cygznlem1
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   ()

Proof of Theorem cygznlem1
StepHypRef Expression
1 cygzn.n . . . . 5
2 hashcl 11631 . . . . . . 7
32adantl 453 . . . . . 6
4 0nn0 10228 . . . . . . 7
54a1i 11 . . . . . 6
63, 5ifclda 3758 . . . . 5
71, 6syl5eqel 2519 . . . 4
9 simprl 733 . . 3
10 simprr 734 . . 3
11 cygzn.y . . . 4 ℤ/n
12 cygzn.l . . . 4 RHom
1311, 12zndvds 16822 . . 3
148, 9, 10, 13syl3anc 1184 . 2
15 cygzn.g . . . . . . 7 CycGrp
16 cyggrp 15491 . . . . . . 7 CycGrp
1715, 16syl 16 . . . . . 6
18 cygzn.x . . . . . 6
19 cygzn.b . . . . . . 7
20 cygzn.m . . . . . . 7 .g
21 cygzn.e . . . . . . 7
22 eqid 2435 . . . . . . 7
2319, 20, 21, 22cyggenod2 15487 . . . . . 6
2417, 18, 23syl2anc 643 . . . . 5
2524, 1syl6eqr 2485 . . . 4