This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oddvds

Description: The only multiples of A that are equal to the identity are the multiples of the order of A . (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Mario Carneiro, 23-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 oddvds 
|- ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )

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 simpr 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. NN )
6 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> N e. ZZ )
7 dvdsval3 
 |-  ( ( ( O ` A ) e. NN /\ N e. ZZ ) -> ( ( O ` A ) || N <-> ( N mod ( O ` A ) ) = 0 ) )
8 5 6 7 syl2anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || N <-> ( N mod ( O ` A ) ) = 0 ) )
9 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> A e. X )
10 1 4 3 mulg0 
 |-  ( A e. X -> ( 0 .x. A ) = .0. )
11 9 10 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( 0 .x. A ) = .0. )
12 oveq1 
 |-  ( ( N mod ( O ` A ) ) = 0 -> ( ( N mod ( O ` A ) ) .x. A ) = ( 0 .x. A ) )
13 12 eqeq1d 
 |-  ( ( N mod ( O ` A ) ) = 0 -> ( ( ( N mod ( O ` A ) ) .x. A ) = .0. <-> ( 0 .x. A ) = .0. ) )
14 11 13 syl5ibrcom 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) = 0 -> ( ( N mod ( O ` A ) ) .x. A ) = .0. ) )
15 6 zred 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> N e. RR )
16 5 nnrpd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. RR+ )
17 modlt 
 |-  ( ( N e. RR /\ ( O ` A ) e. RR+ ) -> ( N mod ( O ` A ) ) < ( O ` A ) )
18 15 16 17 syl2anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( N mod ( O ` A ) ) < ( O ` A ) )
19 6 5 zmodcld 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( N mod ( O ` A ) ) e. NN0 )
20 19 nn0red 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( N mod ( O ` A ) ) e. RR )
21 5 nnred 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. RR )
22 20 21 ltnled 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) < ( O ` A ) <-> -. ( O ` A ) <_ ( N mod ( O ` A ) ) ) )
23 18 22 mpbid 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> -. ( O ` A ) <_ ( N mod ( O ` A ) ) )
24 1 2 3 4 odlem2 
 |-  ( ( A e. X /\ ( N mod ( O ` A ) ) e. NN /\ ( ( N mod ( O ` A ) ) .x. A ) = .0. ) -> ( O ` A ) e. ( 1 ... ( N mod ( O ` A ) ) ) )
25 elfzle2 
 |-  ( ( O ` A ) e. ( 1 ... ( N mod ( O ` A ) ) ) -> ( O ` A ) <_ ( N mod ( O ` A ) ) )
26 24 25 syl 
 |-  ( ( A e. X /\ ( N mod ( O ` A ) ) e. NN /\ ( ( N mod ( O ` A ) ) .x. A ) = .0. ) -> ( O ` A ) <_ ( N mod ( O ` A ) ) )
27 26 3com23 
 |-  ( ( A e. X /\ ( ( N mod ( O ` A ) ) .x. A ) = .0. /\ ( N mod ( O ` A ) ) e. NN ) -> ( O ` A ) <_ ( N mod ( O ` A ) ) )
28 27 3expia 
 |-  ( ( A e. X /\ ( ( N mod ( O ` A ) ) .x. A ) = .0. ) -> ( ( N mod ( O ` A ) ) e. NN -> ( O ` A ) <_ ( N mod ( O ` A ) ) ) )
29 28 con3d 
 |-  ( ( A e. X /\ ( ( N mod ( O ` A ) ) .x. A ) = .0. ) -> ( -. ( O ` A ) <_ ( N mod ( O ` A ) ) -> -. ( N mod ( O ` A ) ) e. NN ) )
30 29 impancom 
 |-  ( ( A e. X /\ -. ( O ` A ) <_ ( N mod ( O ` A ) ) ) -> ( ( ( N mod ( O ` A ) ) .x. A ) = .0. -> -. ( N mod ( O ` A ) ) e. NN ) )
31 9 23 30 syl2anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( ( N mod ( O ` A ) ) .x. A ) = .0. -> -. ( N mod ( O ` A ) ) e. NN ) )
32 elnn0 
 |-  ( ( N mod ( O ` A ) ) e. NN0 <-> ( ( N mod ( O ` A ) ) e. NN \/ ( N mod ( O ` A ) ) = 0 ) )
33 19 32 sylib 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) e. NN \/ ( N mod ( O ` A ) ) = 0 ) )
34 33 ord 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( -. ( N mod ( O ` A ) ) e. NN -> ( N mod ( O ` A ) ) = 0 ) )
35 31 34 syld 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( ( N mod ( O ` A ) ) .x. A ) = .0. -> ( N mod ( O ` A ) ) = 0 ) )
36 14 35 impbid 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) = 0 <-> ( ( N mod ( O ` A ) ) .x. A ) = .0. ) )
37 1 2 3 4 odmod 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) .x. A ) = ( N .x. A ) )
38 37 eqeq1d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( ( N mod ( O ` A ) ) .x. A ) = .0. <-> ( N .x. A ) = .0. ) )
39 8 36 38 3bitrd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
40 simpr 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> ( O ` A ) = 0 )
41 40 breq1d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> ( ( O ` A ) || N <-> 0 || N ) )
42 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> N e. ZZ )
43 0dvds 
 |-  ( N e. ZZ -> ( 0 || N <-> N = 0 ) )
44 42 43 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> ( 0 || N <-> N = 0 ) )
45 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> A e. X )
46 45 10 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> ( 0 .x. A ) = .0. )
47 oveq1 
 |-  ( N = 0 -> ( N .x. A ) = ( 0 .x. A ) )
48 47 eqeq1d 
 |-  ( N = 0 -> ( ( N .x. A ) = .0. <-> ( 0 .x. A ) = .0. ) )
49 46 48 syl5ibrcom 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> ( N = 0 -> ( N .x. A ) = .0. ) )
50 1 2 3 4 odnncl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( O ` A ) e. NN )
51 50 nnne0d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N =/= 0 /\ ( N .x. A ) = .0. ) ) -> ( O ` A ) =/= 0 )
52 51 expr 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ N =/= 0 ) -> ( ( N .x. A ) = .0. -> ( O ` A ) =/= 0 ) )
53 52 impancom 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N .x. A ) = .0. ) -> ( N =/= 0 -> ( O ` A ) =/= 0 ) )
54 53 necon4d 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N .x. A ) = .0. ) -> ( ( O ` A ) = 0 -> N = 0 ) )
55 54 impancom 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> ( ( N .x. A ) = .0. -> N = 0 ) )
56 49 55 impbid 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> ( N = 0 <-> ( N .x. A ) = .0. ) )
57 41 44 56 3bitrd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( O ` A ) = 0 ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
58 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
59 58 3ad2ant2 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( O ` A ) e. NN0 )
60 elnn0 
 |-  ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
61 59 60 sylib 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
62 39 57 61 mpjaodan 
 |-  ( ( G e. Grp /\ A e. X /\ N e. ZZ ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )