mndodconglem

	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}$
	mndodconglem.1	$⊢ φ \to G \in Mnd$
	mndodconglem.2	$⊢ φ \to A \in X$
	mndodconglem.3	$⊢ φ \to O (A) \in ℕ$
	mndodconglem.4	$⊢ φ \to M \in ℕ_{0}$
	mndodconglem.5	$⊢ φ \to N \in ℕ_{0}$
	mndodconglem.6	$⊢ φ \to M < O (A)$
	mndodconglem.7	$⊢ φ \to N < O (A)$
	mndodconglem.8	$⊢ φ \to M \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$
Assertion	mndodconglem	$⊢ (φ \land M \leq N) \to M = N$

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		mndodconglem.1	$⊢ φ \to G \in Mnd$
6		mndodconglem.2	$⊢ φ \to A \in X$
7		mndodconglem.3	$⊢ φ \to O (A) \in ℕ$
8		mndodconglem.4	$⊢ φ \to M \in ℕ_{0}$
9		mndodconglem.5	$⊢ φ \to N \in ℕ_{0}$
10		mndodconglem.6	$⊢ φ \to M < O (A)$
11		mndodconglem.7	$⊢ φ \to N < O (A)$
12		mndodconglem.8	$⊢ φ \to M \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$
13	7	nnred	$⊢ φ \to O (A) \in ℝ$
14	13	recnd	$⊢ φ \to O (A) \in ℂ$
15	8	nn0red	$⊢ φ \to M \in ℝ$
16	15	recnd	$⊢ φ \to M \in ℂ$
17	9	nn0red	$⊢ φ \to N \in ℝ$
18	17	recnd	$⊢ φ \to N \in ℂ$
19	14 16 18	addsubassd	$⊢ φ \to O (A) + M - N = O (A) + M - N$
20	7	nnzd	$⊢ φ \to O (A) \in ℤ$
21	8	nn0zd	$⊢ φ \to M \in ℤ$
22	20 21	zaddcld	$⊢ φ \to O (A) + M \in ℤ$
23	22	zred	$⊢ φ \to O (A) + M \in ℝ$
24		nn0addge1	$⊢ (O (A) \in ℝ \land M \in ℕ_{0}) \to O (A) \leq O (A) + M$
25	13 8 24	syl2anc	$⊢ φ \to O (A) \leq O (A) + M$
26	17 13 23 11 25	ltletrd	$⊢ φ \to N < O (A) + M$
27	9	nn0zd	$⊢ φ \to N \in ℤ$
28		znnsub	$⊢ (N \in ℤ \land O (A) + M \in ℤ) \to (N < O (A) + M \leftrightarrow O (A) + M - N \in ℕ)$
29	27 22 28	syl2anc	$⊢ φ \to (N < O (A) + M \leftrightarrow O (A) + M - N \in ℕ)$
30	26 29	mpbid	$⊢ φ \to O (A) + M - N \in ℕ$
31	19 30	eqeltrrd	$⊢ φ \to O (A) + M - N \in ℕ$
32	14 16 18	addsub12d	$⊢ φ \to O (A) + M - N = M + O (A) - N$
33	32	oveq1d	$⊢ φ \to (O (A) + M - N) \underset{˙}{\cdot} A = (M + O (A) - N) \underset{˙}{\cdot} A$
34	12	oveq1d	$⊢ φ \to (M \underset{˙}{\cdot} A) +_{G} ((O (A) - N) \underset{˙}{\cdot} A) = (N \underset{˙}{\cdot} A) +_{G} ((O (A) - N) \underset{˙}{\cdot} A)$
35		znnsub	$⊢ (N \in ℤ \land O (A) \in ℤ) \to (N < O (A) \leftrightarrow O (A) - N \in ℕ)$
36	27 20 35	syl2anc	$⊢ φ \to (N < O (A) \leftrightarrow O (A) - N \in ℕ)$
37	11 36	mpbid	$⊢ φ \to O (A) - N \in ℕ$
38	37	nnnn0d	$⊢ φ \to O (A) - N \in ℕ_{0}$
39		eqid	$⊢ +_{G} = +_{G}$
40	1 3 39	mulgnn0dir	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land O (A) - N \in ℕ_{0} \land A \in X)) \to (M + O (A) - N) \underset{˙}{\cdot} A = (M \underset{˙}{\cdot} A) +_{G} ((O (A) - N) \underset{˙}{\cdot} A)$
41	5 8 38 6 40	syl13anc	$⊢ φ \to (M + O (A) - N) \underset{˙}{\cdot} A = (M \underset{˙}{\cdot} A) +_{G} ((O (A) - N) \underset{˙}{\cdot} A)$
42	1 3 39	mulgnn0dir	$⊢ (G \in Mnd \land (N \in ℕ_{0} \land O (A) - N \in ℕ_{0} \land A \in X)) \to (N + O (A) - N) \underset{˙}{\cdot} A = (N \underset{˙}{\cdot} A) +_{G} ((O (A) - N) \underset{˙}{\cdot} A)$
43	5 9 38 6 42	syl13anc	$⊢ φ \to (N + O (A) - N) \underset{˙}{\cdot} A = (N \underset{˙}{\cdot} A) +_{G} ((O (A) - N) \underset{˙}{\cdot} A)$
44	34 41 43	3eqtr4d	$⊢ φ \to (M + O (A) - N) \underset{˙}{\cdot} A = (N + O (A) - N) \underset{˙}{\cdot} A$
45	18 14	pncan3d	$⊢ φ \to N + O (A) - N = O (A)$
46	45	oveq1d	$⊢ φ \to (N + O (A) - N) \underset{˙}{\cdot} A = O (A) \underset{˙}{\cdot} A$
47	1 2 3 4	odid	$⊢ A \in X \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
48	6 47	syl	$⊢ φ \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
49	46 48	eqtrd	$⊢ φ \to (N + O (A) - N) \underset{˙}{\cdot} A = \underset{˙}{0}$
50	44 49	eqtrd	$⊢ φ \to (M + O (A) - N) \underset{˙}{\cdot} A = \underset{˙}{0}$
51	33 50	eqtrd	$⊢ φ \to (O (A) + M - N) \underset{˙}{\cdot} A = \underset{˙}{0}$
52	1 2 3 4	odlem2	$⊢ (A \in X \land O (A) + M - N \in ℕ \land (O (A) + M - N) \underset{˙}{\cdot} A = \underset{˙}{0}) \to O (A) \in (1 \dots O (A) + M - N)$
53	6 31 51 52	syl3anc	$⊢ φ \to O (A) \in (1 \dots O (A) + M - N)$
54		elfzle2	$⊢ O (A) \in (1 \dots O (A) + M - N) \to O (A) \leq O (A) + M - N$
55	53 54	syl	$⊢ φ \to O (A) \leq O (A) + M - N$
56	21 27	zsubcld	$⊢ φ \to M - N \in ℤ$
57	56	zred	$⊢ φ \to M - N \in ℝ$
58	13 57	addge01d	$⊢ φ \to (0 \leq M - N \leftrightarrow O (A) \leq O (A) + M - N)$
59	55 58	mpbird	$⊢ φ \to 0 \leq M - N$
60	15 17	subge0d	$⊢ φ \to (0 \leq M - N \leftrightarrow N \leq M)$
61	59 60	mpbid	$⊢ φ \to N \leq M$
62	15 17	letri3d	$⊢ φ \to (M = N \leftrightarrow (M \leq N \land N \leq M))$
63	62	biimprd	$⊢ φ \to ((M \leq N \land N \leq M) \to M = N)$
64	61 63	mpan2d	$⊢ φ \to (M \leq N \to M = N)$
65	64	imp	$⊢ (φ \land M \leq N) \to M = N$

Metamath Proof Explorer

Theorem mndodconglem

Proof