oddvds

Description: The only multiples of A that are equal to the identity are the multiples of the order of A . (Contributed by Mario Carneiro, 14-Jan-2015) (Revised 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	oddvds	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to (O (A) ∥ N \leftrightarrow N \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		simpr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℕ$
6		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \in ℤ$
7		dvdsval3	$⊢ (O (A) \in ℕ \land N \in ℤ) \to (O (A) ∥ N \leftrightarrow N \mod O (A) = 0)$
8	5 6 7	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (O (A) ∥ N \leftrightarrow N \mod O (A) = 0)$
9		simpl2	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to A \in X$
10	1 4 3	mulg0	$⊢ A \in X \to 0 \underset{˙}{\cdot} A = \underset{˙}{0}$
11	9 10	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to 0 \underset{˙}{\cdot} A = \underset{˙}{0}$
12		oveq1	$⊢ N \mod O (A) = 0 \to (N \mod O (A)) \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A$
13	12	eqeq1d	$⊢ N \mod O (A) = 0 \to ((N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow 0 \underset{˙}{\cdot} A = \underset{˙}{0})$
14	11 13	syl5ibrcom	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \mod O (A) = 0 \to (N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0})$
15	6	zred	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \in ℝ$
16	5	nnrpd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℝ^{+}$
17		modlt	$⊢ (N \in ℝ \land O (A) \in ℝ^{+}) \to N \mod O (A) < O (A)$
18	15 16 17	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \mod O (A) < O (A)$
19	6 5	zmodcld	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \mod O (A) \in ℕ_{0}$
20	19	nn0red	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \mod O (A) \in ℝ$
21	5	nnred	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℝ$
22	20 21	ltnled	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \mod O (A) < O (A) \leftrightarrow \neg O (A) \leq N \mod O (A))$
23	18 22	mpbid	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to \neg O (A) \leq N \mod O (A)$
24	1 2 3 4	odlem2	$⊢ (A \in X \land N \mod O (A) \in ℕ \land (N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0}) \to O (A) \in (1 \dots N \mod O (A))$
25		elfzle2	$⊢ O (A) \in (1 \dots N \mod O (A)) \to O (A) \leq N \mod O (A)$
26	24 25	syl	$⊢ (A \in X \land N \mod O (A) \in ℕ \land (N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0}) \to O (A) \leq N \mod O (A)$
27	26	3com23	$⊢ (A \in X \land (N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0} \land N \mod O (A) \in ℕ) \to O (A) \leq N \mod O (A)$
28	27	3expia	$⊢ (A \in X \land (N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0}) \to (N \mod O (A) \in ℕ \to O (A) \leq N \mod O (A))$
29	28	con3d	$⊢ (A \in X \land (N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0}) \to (\neg O (A) \leq N \mod O (A) \to \neg N \mod O (A) \in ℕ)$
30	29	impancom	$⊢ (A \in X \land \neg O (A) \leq N \mod O (A)) \to ((N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0} \to \neg N \mod O (A) \in ℕ)$
31	9 23 30	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to ((N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0} \to \neg N \mod O (A) \in ℕ)$
32		elnn0	$⊢ N \mod O (A) \in ℕ_{0} \leftrightarrow (N \mod O (A) \in ℕ \lor N \mod O (A) = 0)$
33	19 32	sylib	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \mod O (A) \in ℕ \lor N \mod O (A) = 0)$
34	33	ord	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (\neg N \mod O (A) \in ℕ \to N \mod O (A) = 0)$
35	31 34	syld	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to ((N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0} \to N \mod O (A) = 0)$
36	14 35	impbid	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \mod O (A) = 0 \leftrightarrow (N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0})$
37	1 2 3 4	odmod	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (N \mod O (A)) \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$
38	37	eqeq1d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to ((N \mod O (A)) \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
39	8 36 38	3bitrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
40		simpr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to O (A) = 0$
41	40	breq1d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to (O (A) ∥ N \leftrightarrow 0 ∥ N)$
42		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to N \in ℤ$
43		0dvds	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow N = 0)$
44	42 43	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to (0 ∥ N \leftrightarrow N = 0)$
45		simpl2	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to A \in X$
46	45 10	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to 0 \underset{˙}{\cdot} A = \underset{˙}{0}$
47		oveq1	$⊢ N = 0 \to N \underset{˙}{\cdot} A = 0 \underset{˙}{\cdot} A$
48	47	eqeq1d	$⊢ N = 0 \to (N \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow 0 \underset{˙}{\cdot} A = \underset{˙}{0})$
49	46 48	syl5ibrcom	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to (N = 0 \to N \underset{˙}{\cdot} A = \underset{˙}{0})$
50	1 2 3 4	odnncl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to O (A) \in ℕ$
51	50	nnne0d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to O (A) \neq 0$
52	51	expr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \neq 0) \to (N \underset{˙}{\cdot} A = \underset{˙}{0} \to O (A) \neq 0)$
53	52	impancom	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to (N \neq 0 \to O (A) \neq 0)$
54	53	necon4d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \underset{˙}{\cdot} A = \underset{˙}{0}) \to (O (A) = 0 \to N = 0)$
55	54	impancom	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to (N \underset{˙}{\cdot} A = \underset{˙}{0} \to N = 0)$
56	49 55	impbid	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to (N = 0 \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
57	41 44 56	3bitrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) = 0) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
58	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
59	58	3ad2ant2	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (A) \in ℕ_{0}$
60		elnn0	$⊢ O (A) \in ℕ_{0} \leftrightarrow (O (A) \in ℕ \lor O (A) = 0)$
61	59 60	sylib	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to (O (A) \in ℕ \lor O (A) = 0)$
62	39 57 61	mpjaodan	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to (O (A) ∥ N \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$

Metamath Proof Explorer

Theorem oddvds

Proof