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 ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 · 𝐴 ) = ( 𝑁 · 𝐴 ) ) )