gexnnod

Description: Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gexod.1	$⊢ X = {Base}_{G}$
	gexod.2	$⊢ E = gEx (G)$
	gexod.3	$⊢ O = od (G)$
Assertion	gexnnod	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to O (A) \in ℕ$

Step	Hyp	Ref	Expression
1		gexod.1	$⊢ X = {Base}_{G}$
2		gexod.2	$⊢ E = gEx (G)$
3		gexod.3	$⊢ O = od (G)$
4		nnne0	$⊢ E \in ℕ \to E \neq 0$
5	4	3ad2ant2	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to E \neq 0$
6		nnz	$⊢ E \in ℕ \to E \in ℤ$
7	6	3ad2ant2	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to E \in ℤ$
8		0dvds	$⊢ E \in ℤ \to (0 ∥ E \leftrightarrow E = 0)$
9	7 8	syl	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to (0 ∥ E \leftrightarrow E = 0)$
10	9	necon3bbid	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to (\neg 0 ∥ E \leftrightarrow E \neq 0)$
11	5 10	mpbird	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to \neg 0 ∥ E$
12	1 2 3	gexod	$⊢ (G \in Grp \land A \in X) \to O (A) ∥ E$
13	12	3adant2	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to O (A) ∥ E$
14		breq1	$⊢ O (A) = 0 \to (O (A) ∥ E \leftrightarrow 0 ∥ E)$
15	13 14	syl5ibcom	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to (O (A) = 0 \to 0 ∥ E)$
16	11 15	mtod	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to \neg O (A) = 0$
17	1 3	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
18	17	3ad2ant3	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to O (A) \in ℕ_{0}$
19		elnn0	$⊢ O (A) \in ℕ_{0} \leftrightarrow (O (A) \in ℕ \lor O (A) = 0)$
20	18 19	sylib	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to (O (A) \in ℕ \lor O (A) = 0)$
21	20	ord	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to (\neg O (A) \in ℕ \to O (A) = 0)$
22	16 21	mt3d	$⊢ (G \in Grp \land E \in ℕ \land A \in X) \to O (A) \in ℕ$

Metamath Proof Explorer