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 
|- .x. = ( .g ` G )
odid.4 
|- .0. = ( 0g ` G )
Assertion odnncl 
|- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( O ` A ) e. NN )

Proof

Step Hyp Ref Expression
1 odcl.1 
 |-  X = ( Base ` G )
2 odcl.2 
 |-  O = ( od ` G )
3 odid.3 
 |-  .x. = ( .g ` G )
4 odid.4 
 |-  .0. = ( 0g ` G )
5 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> A e. X )
6 simprl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> N =/= 0 )
7 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> N e. ZZ )
8 7 zcnd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> N e. CC )
9 abs00 
 |-  ( N e. CC -> ( ( abs ` N ) = 0 <-> N = 0 ) )
10 9 necon3bbid 
 |-  ( N e. CC -> ( -. ( abs ` N ) = 0 <-> N =/= 0 ) )
11 8 10 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( -. ( abs ` N ) = 0 <-> N =/= 0 ) )
12 6 11 mpbird 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> -. ( abs ` N ) = 0 )
13 nn0abscl 
 |-  ( N e. ZZ -> ( abs ` N ) e. NN0 )
14 7 13 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( abs ` N ) e. NN0 )
15 elnn0 
 |-  ( ( abs ` N ) e. NN0 <-> ( ( abs ` N ) e. NN \/ ( abs ` N ) = 0 ) )
16 14 15 sylib 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( ( abs ` N ) e. NN \/ ( abs ` N ) = 0 ) )
17 16 ord 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( -. ( abs ` N ) e. NN -> ( abs ` N ) = 0 ) )
18 12 17 mt3d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( abs ` N ) e. NN )
19 simprr 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( N .x. A ) = .0. )
20 oveq1 
 |-  ( ( abs ` N ) = N -> ( ( abs ` N ) .x. A ) = ( N .x. A ) )
21 20 eqeq1d 
 |-  ( ( abs ` N ) = N -> ( ( ( abs ` N ) .x. A ) = .0. <-> ( N .x. A ) = .0. ) )
22 19 21 syl5ibrcom 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( ( abs ` N ) = N -> ( ( abs ` N ) .x. A ) = .0. ) )
23 simpl1 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> G e. Grp )
24 eqid 
 |-  ( invg ` G ) = ( invg ` G )
25 1 3 24 mulgneg 
 |-  ( ( G e. Grp /\ N e. ZZ /\ A e. X ) -> ( -u N .x. A ) = ( ( invg ` G ) ` ( N .x. A ) ) )
26 23 7 5 25 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( -u N .x. A ) = ( ( invg ` G ) ` ( N .x. A ) ) )
27 19 fveq2d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( ( invg ` G ) ` ( N .x. A ) ) = ( ( invg ` G ) ` .0. ) )
28 4 24 grpinvid 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
29 23 28 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( ( invg ` G ) ` .0. ) = .0. )
30 26 27 29 3eqtrd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( -u N .x. A ) = .0. )
31 oveq1 
 |-  ( ( abs ` N ) = -u N -> ( ( abs ` N ) .x. A ) = ( -u N .x. A ) )
32 31 eqeq1d 
 |-  ( ( abs ` N ) = -u N -> ( ( ( abs ` N ) .x. A ) = .0. <-> ( -u N .x. A ) = .0. ) )
33 30 32 syl5ibrcom 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( ( abs ` N ) = -u N -> ( ( abs ` N ) .x. A ) = .0. ) )
34 7 zred 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> N e. RR )
35 34 absord 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) )
36 22 33 35 mpjaod 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( ( abs ` N ) .x. A ) = .0. )
37 1 2 3 4 odlem2 
 |-  ( ( A e. X /\ ( abs ` N ) e. NN /\ ( ( abs ` N ) .x. A ) = .0. ) -> ( O ` A ) e. ( 1 ... ( abs ` N ) ) )
38 5 18 36 37 syl3anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( O ` A ) e. ( 1 ... ( abs ` N ) ) )
39 elfznn 
 |-  ( ( O ` A ) e. ( 1 ... ( abs ` N ) ) -> ( O ` A ) e. NN )
40 38 39 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( O ` A ) e. NN )