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. ) )