Metamath Proof Explorer

Theorem mndodcong

Description: If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. (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 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 ) ) )

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 oveq1 
 |-  ( ( M mod ( O ` A ) ) = ( N mod ( O ` A ) ) -> ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) )
6 simp2l 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> M e. NN0 )
7 6 nn0zd 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> M e. ZZ )
8 simp3 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. NN )
9 7 8 zmodcld 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( M mod ( O ` A ) ) e. NN0 )
10 9 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( M mod ( O ` A ) ) e. NN0 )
11 10 nn0red 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( M mod ( O ` A ) ) e. RR )
12 simp2r 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> N e. NN0 )
13 12 nn0zd 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> N e. ZZ )
14 13 8 zmodcld 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( N mod ( O ` A ) ) e. NN0 )
15 14 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( N mod ( O ` A ) ) e. NN0 )
16 15 nn0red 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( N mod ( O ` A ) ) e. RR )
17 simp1l 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> G e. Mnd )
18 17 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> G e. Mnd )
19 simp1r 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> A e. X )
20 19 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> A e. X )
21 8 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( O ` A ) e. NN )
22 6 nn0red 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> M e. RR )
23 8 nnrpd 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. RR+ )
24 modlt 
 |-  ( ( M e. RR /\ ( O ` A ) e. RR+ ) -> ( M mod ( O ` A ) ) < ( O ` A ) )
25 22 23 24 syl2anc 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( M mod ( O ` A ) ) < ( O ` A ) )
26 25 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( M mod ( O ` A ) ) < ( O ` A ) )
27 12 nn0red 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> N e. RR )
28 modlt 
 |-  ( ( N e. RR /\ ( O ` A ) e. RR+ ) -> ( N mod ( O ` A ) ) < ( O ` A ) )
29 27 23 28 syl2anc 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( N mod ( O ` A ) ) < ( O ` A ) )
30 29 adantr 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( N mod ( O ` A ) ) < ( O ` A ) )
31 simpr 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) )
32 1 2 3 4 18 20 21 10 15 26 30 31 mndodconglem 
 |-  ( ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) /\ ( M mod ( O ` A ) ) <_ ( N mod ( O ` A ) ) ) -> ( M mod ( O ` A ) ) = ( N mod ( O ` A ) ) )
33 31 eqcomd 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( ( N mod ( O ` A ) ) .x. A ) = ( ( M mod ( O ` A ) ) .x. A ) )
34 1 2 3 4 18 20 21 15 10 30 26 33 mndodconglem 
 |-  ( ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) /\ ( N mod ( O ` A ) ) <_ ( M mod ( O ` A ) ) ) -> ( N mod ( O ` A ) ) = ( M mod ( O ` A ) ) )
35 34 eqcomd 
 |-  ( ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) /\ ( N mod ( O ` A ) ) <_ ( M mod ( O ` A ) ) ) -> ( M mod ( O ` A ) ) = ( N mod ( O ` A ) ) )
36 11 16 32 35 lecasei 
 |-  ( ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) /\ ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) -> ( M mod ( O ` A ) ) = ( N mod ( O ` A ) ) )
37 36 ex 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) -> ( M mod ( O ` A ) ) = ( N mod ( O ` A ) ) ) )
38 5 37 impbid2 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( M mod ( O ` A ) ) = ( N mod ( O ` A ) ) <-> ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) ) )
39 moddvds 
 |-  ( ( ( O ` A ) e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( M mod ( O ` A ) ) = ( N mod ( O ` A ) ) <-> ( O ` A ) || ( M - N ) ) )
40 8 7 13 39 syl3anc 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( M mod ( O ` A ) ) = ( N mod ( O ` A ) ) <-> ( O ` A ) || ( M - N ) ) )
41 1 2 3 4 odmodnn0 
 |-  ( ( ( G e. Mnd /\ A e. X /\ M e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( M mod ( O ` A ) ) .x. A ) = ( M .x. A ) )
42 17 19 6 8 41 syl31anc 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( M mod ( O ` A ) ) .x. A ) = ( M .x. A ) )
43 1 2 3 4 odmodnn0 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) .x. A ) = ( N .x. A ) )
44 17 19 12 8 43 syl31anc 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) .x. A ) = ( N .x. A ) )
45 42 44 eqeq12d 
 |-  ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( M mod ( O ` A ) ) .x. A ) = ( ( N mod ( O ` A ) ) .x. A ) <-> ( M .x. A ) = ( N .x. A ) ) )
46 38 40 45 3bitr3d 
 |-  ( ( ( 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 ) ) )