Metamath Proof Explorer


Theorem odnncl

Description: If a nonzero multiple of an element is zero, the element has positive order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Revised by Mario Carneiro, 22-Sep-2015)

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

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 simpl2 G Grp A X N N 0 N · ˙ A = 0 ˙ A X
6 simprl G Grp A X N N 0 N · ˙ A = 0 ˙ N 0
7 simpl3 G Grp A X N N 0 N · ˙ A = 0 ˙ N
8 7 zcnd G Grp A X N N 0 N · ˙ A = 0 ˙ N
9 abs00 N N = 0 N = 0
10 9 necon3bbid N ¬ N = 0 N 0
11 8 10 syl G Grp A X N N 0 N · ˙ A = 0 ˙ ¬ N = 0 N 0
12 6 11 mpbird G Grp A X N N 0 N · ˙ A = 0 ˙ ¬ N = 0
13 nn0abscl N N 0
14 7 13 syl G Grp A X N N 0 N · ˙ A = 0 ˙ N 0
15 elnn0 N 0 N N = 0
16 14 15 sylib G Grp A X N N 0 N · ˙ A = 0 ˙ N N = 0
17 16 ord G Grp A X N N 0 N · ˙ A = 0 ˙ ¬ N N = 0
18 12 17 mt3d G Grp A X N N 0 N · ˙ A = 0 ˙ N
19 simprr G Grp A X N N 0 N · ˙ A = 0 ˙ N · ˙ A = 0 ˙
20 oveq1 N = N N · ˙ A = N · ˙ A
21 20 eqeq1d N = N N · ˙ A = 0 ˙ N · ˙ A = 0 ˙
22 19 21 syl5ibrcom G Grp A X N N 0 N · ˙ A = 0 ˙ N = N N · ˙ A = 0 ˙
23 simpl1 G Grp A X N N 0 N · ˙ A = 0 ˙ G Grp
24 eqid inv g G = inv g G
25 1 3 24 mulgneg G Grp N A X -N · ˙ A = inv g G N · ˙ A
26 23 7 5 25 syl3anc G Grp A X N N 0 N · ˙ A = 0 ˙ -N · ˙ A = inv g G N · ˙ A
27 19 fveq2d G Grp A X N N 0 N · ˙ A = 0 ˙ inv g G N · ˙ A = inv g G 0 ˙
28 4 24 grpinvid G Grp inv g G 0 ˙ = 0 ˙
29 23 28 syl G Grp A X N N 0 N · ˙ A = 0 ˙ inv g G 0 ˙ = 0 ˙
30 26 27 29 3eqtrd G Grp A X N N 0 N · ˙ A = 0 ˙ -N · ˙ A = 0 ˙
31 oveq1 N = N N · ˙ A = -N · ˙ A
32 31 eqeq1d N = N N · ˙ A = 0 ˙ -N · ˙ A = 0 ˙
33 30 32 syl5ibrcom G Grp A X N N 0 N · ˙ A = 0 ˙ N = N N · ˙ A = 0 ˙
34 7 zred G Grp A X N N 0 N · ˙ A = 0 ˙ N
35 34 absord G Grp A X N N 0 N · ˙ A = 0 ˙ N = N N = N
36 22 33 35 mpjaod G Grp A X N N 0 N · ˙ A = 0 ˙ N · ˙ A = 0 ˙
37 1 2 3 4 odlem2 A X N N · ˙ A = 0 ˙ O A 1 N
38 5 18 36 37 syl3anc G Grp A X N N 0 N · ˙ A = 0 ˙ O A 1 N
39 elfznn O A 1 N O A
40 38 39 syl G Grp A X N N 0 N · ˙ A = 0 ˙ O A