gexcl3

Description: If the order of every group element is bounded by N , the group has finite exponent. (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	gexcl3	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to E \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		gexod.1	$⊢ X = {Base}_{G}$
2		gexod.2	$⊢ E = gEx (G)$
3		gexod.3	$⊢ O = od (G)$
4		simpl	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to G \in Grp$
5	1	grpbn0	$⊢ G \in Grp \to X \neq \emptyset$
6		r19.2z	$⊢ (X \neq \emptyset \land \forall x \in X O (x) \in (1 \dots N)) \to \exists x \in X O (x) \in (1 \dots N)$
7	5 6	sylan	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to \exists x \in X O (x) \in (1 \dots N)$
8		elfzuz2	$⊢ O (x) \in (1 \dots N) \to N \in ℤ_{\geq 1}$
9		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
10	8 9	eleqtrrdi	$⊢ O (x) \in (1 \dots N) \to N \in ℕ$
11	10	rexlimivw	$⊢ \exists x \in X O (x) \in (1 \dots N) \to N \in ℕ$
12	7 11	syl	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to N \in ℕ$
13	12	nnnn0d	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to N \in ℕ_{0}$
14	13	faccld	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to N! \in ℕ$
15		elfzuzb	$⊢ O (x) \in (1 \dots N) \leftrightarrow (O (x) \in ℤ_{\geq 1} \land N \in ℤ_{\geq O (x)})$
16		elnnuz	$⊢ O (x) \in ℕ \leftrightarrow O (x) \in ℤ_{\geq 1}$
17		dvdsfac	$⊢ (O (x) \in ℕ \land N \in ℤ_{\geq O (x)}) \to O (x) ∥ N!$
18	16 17	sylanbr	$⊢ (O (x) \in ℤ_{\geq 1} \land N \in ℤ_{\geq O (x)}) \to O (x) ∥ N!$
19	15 18	sylbi	$⊢ O (x) \in (1 \dots N) \to O (x) ∥ N!$
20	19	adantl	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to O (x) ∥ N!$
21		simpll	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to G \in Grp$
22		simplr	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to x \in X$
23	10	adantl	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to N \in ℕ$
24	23	nnnn0d	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to N \in ℕ_{0}$
25	24	faccld	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to N! \in ℕ$
26	25	nnzd	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to N! \in ℤ$
27		eqid	$⊢ \cdot_{G} = \cdot_{G}$
28		eqid	$⊢ 0_{G} = 0_{G}$
29	1 3 27 28	oddvds	$⊢ (G \in Grp \land x \in X \land N! \in ℤ) \to (O (x) ∥ N! \leftrightarrow N! \cdot_{G} x = 0_{G})$
30	21 22 26 29	syl3anc	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to (O (x) ∥ N! \leftrightarrow N! \cdot_{G} x = 0_{G})$
31	20 30	mpbid	$⊢ ((G \in Grp \land x \in X) \land O (x) \in (1 \dots N)) \to N! \cdot_{G} x = 0_{G}$
32	31	ex	$⊢ (G \in Grp \land x \in X) \to (O (x) \in (1 \dots N) \to N! \cdot_{G} x = 0_{G})$
33	32	ralimdva	$⊢ G \in Grp \to (\forall x \in X O (x) \in (1 \dots N) \to \forall x \in X N! \cdot_{G} x = 0_{G})$
34	33	imp	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to \forall x \in X N! \cdot_{G} x = 0_{G}$
35	1 2 27 28	gexlem2	$⊢ (G \in Grp \land N! \in ℕ \land \forall x \in X N! \cdot_{G} x = 0_{G}) \to E \in (1 \dots N!)$
36	4 14 34 35	syl3anc	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to E \in (1 \dots N!)$
37		elfznn	$⊢ E \in (1 \dots N!) \to E \in ℕ$
38	36 37	syl	$⊢ (G \in Grp \land \forall x \in X O (x) \in (1 \dots N)) \to E \in ℕ$

Metamath Proof Explorer

Theorem gexcl3

Proof