Metamath Proof Explorer


Theorem oddvdsi

Description: Any group element is annihilated by any multiple of its order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Revised by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses odcl.1 X = Base G
odcl.2 O = od G
odid.3 · ˙ = G
odid.4 0 ˙ = 0 G
Assertion oddvdsi G Grp A X O A N N · ˙ A = 0 ˙

Proof

Step Hyp Ref Expression
1 odcl.1 X = Base G
2 odcl.2 O = od G
3 odid.3 · ˙ = G
4 odid.4 0 ˙ = 0 G
5 simp3 G Grp A X O A N O A N
6 dvdszrcl O A N O A N
7 6 simprd O A N N
8 1 2 3 4 oddvds G Grp A X N O A N N · ˙ A = 0 ˙
9 7 8 syl3an3 G Grp A X O A N O A N N · ˙ A = 0 ˙
10 5 9 mpbid G Grp A X O A N N · ˙ A = 0 ˙