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

Metamath Proof Explorer

Theorem mndodcongi

Description: If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. For monoids, the reverse implication is false for elements with infinite order. For example, the powers of 2 mod 1 0 are 1,2,4,8,6,2,4,8,6,... so that the identity 1 never repeats, which is infinite order by our definition, yet other numbers like 6 appear many times in the sequence. (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 mndodcongi 
|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )

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 1 2 3 4 mndodcong 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || ( M - N ) <-> ( M .x. A ) = ( N .x. A ) ) )
6 5 biimpd 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )
7 6 3expia 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) ) )
8 7 3impa 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) ) )
9 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
10 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
11 zsubcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
12 9 10 11 syl2an 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M - N ) e. ZZ )
13 12 3ad2ant3 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M - N ) e. ZZ )
14 0dvds 
 |-  ( ( M - N ) e. ZZ -> ( 0 || ( M - N ) <-> ( M - N ) = 0 ) )
15 13 14 syl 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( 0 || ( M - N ) <-> ( M - N ) = 0 ) )
16 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
17 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
18 subeq0 
 |-  ( ( M e. CC /\ N e. CC ) -> ( ( M - N ) = 0 <-> M = N ) )
19 16 17 18 syl2an 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M - N ) = 0 <-> M = N ) )
20 19 3ad2ant3 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M - N ) = 0 <-> M = N ) )
21 oveq1 
 |-  ( M = N -> ( M .x. A ) = ( N .x. A ) )
22 20 21 biimtrdi 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M - N ) = 0 -> ( M .x. A ) = ( N .x. A ) ) )
23 15 22 sylbid 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( 0 || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )
24 breq1 
 |-  ( ( O ` A ) = 0 -> ( ( O ` A ) || ( M - N ) <-> 0 || ( M - N ) ) )
25 24 imbi1d 
 |-  ( ( O ` A ) = 0 -> ( ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) <-> ( 0 || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) ) )
26 23 25 syl5ibrcom 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) = 0 -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) ) )
27 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
28 27 3ad2ant2 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( O ` A ) e. NN0 )
29 elnn0 
 |-  ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
30 28 29 sylib 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
31 8 26 30 mpjaod 
 |-  ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )