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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odid.4	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	mndodcong	$⊢ ((G \in Mnd \land A \in X) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land O (A) \in ℕ) \to (O (A) ∥ (M - N) \leftrightarrow M \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A)$

Proof

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

Metamath Proof Explorer

Theorem mndodcong

Proof