odeq

Description: The oddvds property uniquely defines the group order. (Contributed by Stefan O'Rear, 6-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	odeq	$⊢ (G \in Grp \land A \in X \land N \in ℕ_{0}) \to (N = O (A) \leftrightarrow \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$

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		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
6	1 2 3 4	oddvds	$⊢ (G \in Grp \land A \in X \land y \in ℤ) \to (O (A) ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})$
7	5 6	syl3an3	$⊢ (G \in Grp \land A \in X \land y \in ℕ_{0}) \to (O (A) ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})$
8	7	3expa	$⊢ ((G \in Grp \land A \in X) \land y \in ℕ_{0}) \to (O (A) ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})$
9	8	ralrimiva	$⊢ (G \in Grp \land A \in X) \to \forall y \in ℕ_{0} (O (A) ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})$
10		breq1	$⊢ N = O (A) \to (N ∥ y \leftrightarrow O (A) ∥ y)$
11	10	bibi1d	$⊢ N = O (A) \to ((N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}) \leftrightarrow (O (A) ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$
12	11	ralbidv	$⊢ N = O (A) \to (\forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}) \leftrightarrow \forall y \in ℕ_{0} (O (A) ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$
13	9 12	syl5ibrcom	$⊢ (G \in Grp \land A \in X) \to (N = O (A) \to \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$
14	13	3adant3	$⊢ (G \in Grp \land A \in X \land N \in ℕ_{0}) \to (N = O (A) \to \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$
15		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to N \in ℕ_{0}$
16		simpl2	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to A \in X$
17	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
18	16 17	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to O (A) \in ℕ_{0}$
19	1 2 3 4	odid	$⊢ A \in X \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
20	16 19	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to O (A) \underset{˙}{\cdot} A = \underset{˙}{0}$
21	17	3ad2ant2	$⊢ (G \in Grp \land A \in X \land N \in ℕ_{0}) \to O (A) \in ℕ_{0}$
22		breq2	$⊢ y = O (A) \to (N ∥ y \leftrightarrow N ∥ O (A))$
23		oveq1	$⊢ y = O (A) \to y \underset{˙}{\cdot} A = O (A) \underset{˙}{\cdot} A$
24	23	eqeq1d	$⊢ y = O (A) \to (y \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow O (A) \underset{˙}{\cdot} A = \underset{˙}{0})$
25	22 24	bibi12d	$⊢ y = O (A) \to ((N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}) \leftrightarrow (N ∥ O (A) \leftrightarrow O (A) \underset{˙}{\cdot} A = \underset{˙}{0}))$
26	25	rspcva	$⊢ (O (A) \in ℕ_{0} \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to (N ∥ O (A) \leftrightarrow O (A) \underset{˙}{\cdot} A = \underset{˙}{0})$
27	21 26	sylan	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to (N ∥ O (A) \leftrightarrow O (A) \underset{˙}{\cdot} A = \underset{˙}{0})$
28	20 27	mpbird	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to N ∥ O (A)$
29		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
30		iddvds	$⊢ N \in ℤ \to N ∥ N$
31	15 29 30	3syl	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to N ∥ N$
32		breq2	$⊢ y = N \to (N ∥ y \leftrightarrow N ∥ N)$
33		oveq1	$⊢ y = N \to y \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$
34	33	eqeq1d	$⊢ y = N \to (y \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
35	32 34	bibi12d	$⊢ y = N \to ((N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}) \leftrightarrow (N ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0}))$
36	35	rspcva	$⊢ (N \in ℕ_{0} \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to (N ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
37	36	3ad2antl3	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to (N ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
38	31 37	mpbid	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to N \underset{˙}{\cdot} A = \underset{˙}{0}$
39	1 2 3 4	oddvds	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
40	29 39	syl3an3	$⊢ (G \in Grp \land A \in X \land N \in ℕ_{0}) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
41	40	adantr	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
42	38 41	mpbird	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to O (A) ∥ N$
43		dvdseq	$⊢ ((N \in ℕ_{0} \land O (A) \in ℕ_{0}) \land (N ∥ O (A) \land O (A) ∥ N)) \to N = O (A)$
44	15 18 28 42 43	syl22anc	$⊢ ((G \in Grp \land A \in X \land N \in ℕ_{0}) \land \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0})) \to N = O (A)$
45	44	ex	$⊢ (G \in Grp \land A \in X \land N \in ℕ_{0}) \to (\forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}) \to N = O (A))$
46	14 45	impbid	$⊢ (G \in Grp \land A \in X \land N \in ℕ_{0}) \to (N = O (A) \leftrightarrow \forall y \in ℕ_{0} (N ∥ y \leftrightarrow y \underset{˙}{\cdot} A = \underset{˙}{0}))$

Metamath Proof Explorer

Theorem odeq

Proof