Metamath Proof Explorer

Theorem oddvdsnn0

Description: The only multiples of A that are equal to the identity are the multiples of the order of A . (Contributed 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 oddvdsnn0 
|- ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( 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 0nn0 
 |-  0 e. NN0
6 1 2 3 4 mndodcong 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( N e. NN0 /\ 0 e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) )
7 6 3expia 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( N e. NN0 /\ 0 e. NN0 ) ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) ) )
8 5 7 mpanr2 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ N e. NN0 ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) ) )
9 8 3impa 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) ) )
10 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
11 10 3ad2ant3 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> N e. CC )
12 11 subid1d 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( N - 0 ) = N )
13 12 breq2d 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) || ( N - 0 ) <-> ( O ` A ) || N ) )
14 1 4 3 mulg0 
 |-  ( A e. X -> ( 0 .x. A ) = .0. )
15 14 3ad2ant2 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( 0 .x. A ) = .0. )
16 15 eqeq2d 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( N .x. A ) = ( 0 .x. A ) <-> ( N .x. A ) = .0. ) )
17 13 16 bibi12d 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( ( O ` A ) || ( N - 0 ) <-> ( N .x. A ) = ( 0 .x. A ) ) <-> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) ) )
18 9 17 sylibd 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) ) )
19 simpr 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( O ` A ) = 0 )
20 19 breq1d 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( ( O ` A ) || N <-> 0 || N ) )
21 simpl3 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> N e. NN0 )
22 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
23 0dvds 
 |-  ( N e. ZZ -> ( 0 || N <-> N = 0 ) )
24 21 22 23 3syl 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( 0 || N <-> N = 0 ) )
25 15 adantr 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( 0 .x. A ) = .0. )
26 oveq1 
 |-  ( N = 0 -> ( N .x. A ) = ( 0 .x. A ) )
27 26 eqeq1d 
 |-  ( N = 0 -> ( ( N .x. A ) = .0. <-> ( 0 .x. A ) = .0. ) )
28 25 27 syl5ibrcom 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( N = 0 -> ( N .x. A ) = .0. ) )
29 1 2 3 4 odlem2 
 |-  ( ( A e. X /\ N e. NN /\ ( N .x. A ) = .0. ) -> ( O ` A ) e. ( 1 ... N ) )
30 29 3com23 
 |-  ( ( A e. X /\ ( N .x. A ) = .0. /\ N e. NN ) -> ( O ` A ) e. ( 1 ... N ) )
31 elfznn 
 |-  ( ( O ` A ) e. ( 1 ... N ) -> ( O ` A ) e. NN )
32 nnne0 
 |-  ( ( O ` A ) e. NN -> ( O ` A ) =/= 0 )
33 30 31 32 3syl 
 |-  ( ( A e. X /\ ( N .x. A ) = .0. /\ N e. NN ) -> ( O ` A ) =/= 0 )
34 33 3expia 
 |-  ( ( A e. X /\ ( N .x. A ) = .0. ) -> ( N e. NN -> ( O ` A ) =/= 0 ) )
35 34 3ad2antl2 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( N e. NN -> ( O ` A ) =/= 0 ) )
36 35 necon2bd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( ( O ` A ) = 0 -> -. N e. NN ) )
37 simpl3 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> N e. NN0 )
38 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
39 37 38 sylib 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( N e. NN \/ N = 0 ) )
40 39 ord 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( -. N e. NN -> N = 0 ) )
41 36 40 syld 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( N .x. A ) = .0. ) -> ( ( O ` A ) = 0 -> N = 0 ) )
42 41 impancom 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( ( N .x. A ) = .0. -> N = 0 ) )
43 28 42 impbid 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( N = 0 <-> ( N .x. A ) = .0. ) )
44 20 24 43 3bitrd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) = 0 ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )
45 44 ex 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) = 0 -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) ) )
46 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
47 46 3ad2ant2 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( O ` A ) e. NN0 )
48 elnn0 
 |-  ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
49 47 48 sylib 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
50 18 45 49 mpjaod 
 |-  ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) -> ( ( O ` A ) || N <-> ( N .x. A ) = .0. ) )