odnncl

Description: If a nonzero multiple of an element is zero, the element has positive order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Revised by Mario Carneiro, 22-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	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 ℕ$

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		simpl2	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to A \in X$
6		simprl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to N \neq 0$
7		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to N \in ℤ$
8	7	zcnd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to N \in ℂ$
9		abs00	$⊢ N \in ℂ \to (\|N\| = 0 \leftrightarrow N = 0)$
10	9	necon3bbid	$⊢ N \in ℂ \to (\neg \|N\| = 0 \leftrightarrow N \neq 0)$
11	8 10	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to (\neg \|N\| = 0 \leftrightarrow N \neq 0)$
12	6 11	mpbird	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to \neg \|N\| = 0$
13		nn0abscl	$⊢ N \in ℤ \to \|N\| \in ℕ_{0}$
14	7 13	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to \|N\| \in ℕ_{0}$
15		elnn0	$⊢ \|N\| \in ℕ_{0} \leftrightarrow (\|N\| \in ℕ \lor \|N\| = 0)$
16	14 15	sylib	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to (\|N\| \in ℕ \lor \|N\| = 0)$
17	16	ord	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to (\neg \|N\| \in ℕ \to \|N\| = 0)$
18	12 17	mt3d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to \|N\| \in ℕ$
19		simprr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to N \underset{˙}{\cdot} A = \underset{˙}{0}$
20		oveq1	$⊢ \|N\| = N \to \|N\| \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$
21	20	eqeq1d	$⊢ \|N\| = N \to (\|N\| \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
22	19 21	syl5ibrcom	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to (\|N\| = N \to \|N\| \underset{˙}{\cdot} A = \underset{˙}{0})$
23		simpl1	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to G \in Grp$
24		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
25	1 3 24	mulgneg	$⊢ (G \in Grp \land N \in ℤ \land A \in X) \to -N \underset{˙}{\cdot} A = {inv}_{g} (G) (N \underset{˙}{\cdot} A)$
26	23 7 5 25	syl3anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to -N \underset{˙}{\cdot} A = {inv}_{g} (G) (N \underset{˙}{\cdot} A)$
27	19	fveq2d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to {inv}_{g} (G) (N \underset{˙}{\cdot} A) = {inv}_{g} (G) (\underset{˙}{0})$
28	4 24	grpinvid	$⊢ G \in Grp \to {inv}_{g} (G) (\underset{˙}{0}) = \underset{˙}{0}$
29	23 28	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to {inv}_{g} (G) (\underset{˙}{0}) = \underset{˙}{0}$
30	26 27 29	3eqtrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to -N \underset{˙}{\cdot} A = \underset{˙}{0}$
31		oveq1	$⊢ \|N\| = - N \to \|N\| \underset{˙}{\cdot} A = -N \underset{˙}{\cdot} A$
32	31	eqeq1d	$⊢ \|N\| = - N \to (\|N\| \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow -N \underset{˙}{\cdot} A = \underset{˙}{0})$
33	30 32	syl5ibrcom	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to (\|N\| = - N \to \|N\| \underset{˙}{\cdot} A = \underset{˙}{0})$
34	7	zred	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to N \in ℝ$
35	34	absord	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to (\|N\| = N \lor \|N\| = - N)$
36	22 33 35	mpjaod	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \neq 0 \land N \underset{˙}{\cdot} A = \underset{˙}{0})) \to \|N\| \underset{˙}{\cdot} A = \underset{˙}{0}$
37	1 2 3 4	odlem2	$⊢ (A \in X \land \|N\| \in ℕ \land \|N\| \underset{˙}{\cdot} A = \underset{˙}{0}) \to O (A) \in (1 \dots \|N\|)$
38	5 18 36 37	syl3anc	$⊢ ((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 (1 \dots \|N\|)$
39		elfznn	$⊢ O (A) \in (1 \dots \|N\|) \to O (A) \in ℕ$
40	38 39	syl	$⊢ ((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 ℕ$

Metamath Proof Explorer

Theorem odnncl

Proof