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 · ˙ = G
odid.4 0 ˙ = 0 G
Assertion mndodcong G Mnd A X M 0 N 0 O A O A M N M · ˙ A = N · ˙ A

Proof

Step Hyp Ref Expression
1 odcl.1 X = Base G
2 odcl.2 O = od G
3 odid.3 · ˙ = G
4 odid.4 0 ˙ = 0 G
5 oveq1 M mod O A = N mod O A M mod O A · ˙ A = N mod O A · ˙ A
6 simp2l G Mnd A X M 0 N 0 O A M 0
7 6 nn0zd G Mnd A X M 0 N 0 O A M
8 simp3 G Mnd A X M 0 N 0 O A O A
9 7 8 zmodcld G Mnd A X M 0 N 0 O A M mod O A 0
10 9 adantr G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A M mod O A 0
11 10 nn0red G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A M mod O A
12 simp2r G Mnd A X M 0 N 0 O A N 0
13 12 nn0zd G Mnd A X M 0 N 0 O A N
14 13 8 zmodcld G Mnd A X M 0 N 0 O A N mod O A 0
15 14 adantr G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A N mod O A 0
16 15 nn0red G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A N mod O A
17 simp1l G Mnd A X M 0 N 0 O A G Mnd
18 17 adantr G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A G Mnd
19 simp1r G Mnd A X M 0 N 0 O A A X
20 19 adantr G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A A X
21 8 adantr G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A O A
22 6 nn0red G Mnd A X M 0 N 0 O A M
23 8 nnrpd G Mnd A X M 0 N 0 O A O A +
24 modlt M O A + M mod O A < O A
25 22 23 24 syl2anc G Mnd A X M 0 N 0 O A M mod O A < O A
26 25 adantr G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A M mod O A < O A
27 12 nn0red G Mnd A X M 0 N 0 O A N
28 modlt N O A + N mod O A < O A
29 27 23 28 syl2anc G Mnd A X M 0 N 0 O A N mod O A < O A
30 29 adantr G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A N mod O A < O A
31 simpr G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A M mod O A · ˙ A = N mod O A · ˙ A
32 1 2 3 4 18 20 21 10 15 26 30 31 mndodconglem G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A M mod O A N mod O A M mod O A = N mod O A
33 31 eqcomd G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A N mod O A · ˙ A = M mod O A · ˙ A
34 1 2 3 4 18 20 21 15 10 30 26 33 mndodconglem G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A N mod O A M mod O A N mod O A = M mod O A
35 34 eqcomd G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A N mod O A M mod O A M mod O A = N mod O A
36 11 16 32 35 lecasei G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A M mod O A = N mod O A
37 36 ex G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A M mod O A = N mod O A
38 5 37 impbid2 G Mnd A X M 0 N 0 O A M mod O A = N mod O A M mod O A · ˙ A = N mod O A · ˙ A
39 moddvds O A M N M mod O A = N mod O A O A M N
40 8 7 13 39 syl3anc G Mnd A X M 0 N 0 O A M mod O A = N mod O A O A M N
41 1 2 3 4 odmodnn0 G Mnd A X M 0 O A M mod O A · ˙ A = M · ˙ A
42 17 19 6 8 41 syl31anc G Mnd A X M 0 N 0 O A M mod O A · ˙ A = M · ˙ A
43 1 2 3 4 odmodnn0 G Mnd A X N 0 O A N mod O A · ˙ A = N · ˙ A
44 17 19 12 8 43 syl31anc G Mnd A X M 0 N 0 O A N mod O A · ˙ A = N · ˙ A
45 42 44 eqeq12d G Mnd A X M 0 N 0 O A M mod O A · ˙ A = N mod O A · ˙ A M · ˙ A = N · ˙ A
46 38 40 45 3bitr3d G Mnd A X M 0 N 0 O A O A M N M · ˙ A = N · ˙ A