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

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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odid.3 ⊢ · = ( .g ‘ 𝐺 )
odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion mndodcong ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 oveq1 ⊢ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) → ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
6 simp2l ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑀 ∈ ℕ0 )
7 6 nn0zd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑀 ∈ ℤ )
8 simp3 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
9 7 8 zmodcld ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
10 9 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
11 10 nn0red ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℝ )
12 simp2r ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℕ0 )
13 12 nn0zd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℤ )
14 13 8 zmodcld ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
15 14 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
16 15 nn0red ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ∈ ℝ )
17 simp1l ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐺 ∈ Mnd )
18 17 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → 𝐺 ∈ Mnd )
19 simp1r ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ 𝑋 )
20 19 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → 𝐴 ∈ 𝑋 )
21 8 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
22 6 nn0red ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑀 ∈ ℝ )
23 8 nnrpd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ )
24 modlt ⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) )
25 22 23 24 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) )
26 25 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) )
27 12 nn0red ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℝ )
28 modlt ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℝ+ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) )
29 27 23 28 syl2anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) )
30 29 adantr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) < ( 𝑂 ‘ 𝐴 ) )
31 simpr ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
32 1 2 3 4 18 20 21 10 15 26 30 31 mndodconglem ⊢ ( ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) ∧ ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) ≤ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) )
33 31 eqcomd ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
34 1 2 3 4 18 20 21 15 10 30 26 33 mndodconglem ⊢ ( ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) ∧ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ≤ ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) ) → ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) )
35 34 eqcomd ⊢ ( ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) ∧ ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ≤ ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) )
36 11 16 32 35 lecasei ⊢ ( ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) ∧ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) )
37 36 ex ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) → ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ) )
38 5 37 impbid2 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ↔ ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ) )
39 moddvds ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ) )
40 8 7 13 39 syl3anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) = ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ) )
41 1 2 3 4 odmodnn0 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑀 · 𝐴 ) )
42 17 19 6 8 41 syl31anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑀 · 𝐴 ) )
43 1 2 3 4 odmodnn0 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )
44 17 19 12 8 43 syl31anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )
45 42 44 eqeq12d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑀 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( ( 𝑁 mod ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) )
46 38 40 45 3bitr3d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) )