Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mndodcongi Structured version   Unicode version

Theorem mndodcongi 15182
 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 mod 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.)
Hypotheses
Ref Expression
odcl.1
odcl.2
odid.3 .g
odid.4
Assertion
Ref Expression
mndodcongi

Proof of Theorem mndodcongi
StepHypRef Expression
1 odcl.1 . . . . . 6
2 odcl.2 . . . . . 6
3 odid.3 . . . . . 6 .g
4 odid.4 . . . . . 6
51, 2, 3, 4mndodcong 15181 . . . . 5
65biimpd 200 . . . 4
763expia 1156 . . 3
873impa 1149 . 2
9 nn0z 10305 . . . . . . 7
10 nn0z 10305 . . . . . . 7
11 zsubcl 10320 . . . . . . 7
129, 10, 11syl2an 465 . . . . . 6
13123ad2ant3 981 . . . . 5
14 0dvds 12871 . . . . 5
1513, 14syl 16 . . . 4
16 nn0cn 10232 . . . . . . 7
17 nn0cn 10232 . . . . . . 7
18 subeq0 9328 . . . . . . 7
1916, 17, 18syl2an 465 . . . . . 6
20193ad2ant3 981 . . . . 5
21 oveq1 6089 . . . . 5
2220, 21syl6bi 221 . . . 4
2315, 22sylbid 208 . . 3
24 breq1 4216 . . . 4
2524imbi1d 310 . . 3
2623, 25syl5ibrcom 215 . 2
271, 2odcl 15175 . . . 4