odcl2

Description: The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015)

	Ref	Expression
Hypotheses	odcl2.1	$⊢ X = {Base}_{G}$
	odcl2.2	$⊢ O = od (G)$
Assertion	odcl2	$⊢ (G \in Grp \land X \in Fin \land A \in X) \to O (A) \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		odcl2.1	$⊢ X = {Base}_{G}$
2		odcl2.2	$⊢ O = od (G)$
3	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
4	3	adantl	$⊢ (G \in Grp \land A \in X) \to O (A) \in ℕ_{0}$
5		elnn0	$⊢ O (A) \in ℕ_{0} \leftrightarrow (O (A) \in ℕ \lor O (A) = 0)$
6	4 5	sylib	$⊢ (G \in Grp \land A \in X) \to (O (A) \in ℕ \lor O (A) = 0)$
7	6	ord	$⊢ (G \in Grp \land A \in X) \to (\neg O (A) \in ℕ \to O (A) = 0)$
8		eqid	$⊢ \cdot_{G} = \cdot_{G}$
9		eqid	$⊢ (x \in ℤ ⟼ x \cdot_{G} A) = (x \in ℤ ⟼ x \cdot_{G} A)$
10	1 2 8 9	odinf	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \neg ran (x \in ℤ ⟼ x \cdot_{G} A) \in Fin$
11	1 2 8 9	odf1	$⊢ (G \in Grp \land A \in X) \to (O (A) = 0 \leftrightarrow (x \in ℤ ⟼ x \cdot_{G} A) : ℤ \underset{1-1}{⟶} X)$
12	11	biimp3a	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (x \in ℤ ⟼ x \cdot_{G} A) : ℤ \underset{1-1}{⟶} X$
13		f1f	$⊢ (x \in ℤ ⟼ x \cdot_{G} A) : ℤ \underset{1-1}{⟶} X \to (x \in ℤ ⟼ x \cdot_{G} A) : ℤ ⟶ X$
14		frn	$⊢ (x \in ℤ ⟼ x \cdot_{G} A) : ℤ ⟶ X \to ran (x \in ℤ ⟼ x \cdot_{G} A) \subseteq X$
15		ssfi	$⊢ (X \in Fin \land ran (x \in ℤ ⟼ x \cdot_{G} A) \subseteq X) \to ran (x \in ℤ ⟼ x \cdot_{G} A) \in Fin$
16	15	expcom	$⊢ ran (x \in ℤ ⟼ x \cdot_{G} A) \subseteq X \to (X \in Fin \to ran (x \in ℤ ⟼ x \cdot_{G} A) \in Fin)$
17	12 13 14 16	4syl	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (X \in Fin \to ran (x \in ℤ ⟼ x \cdot_{G} A) \in Fin)$
18	10 17	mtod	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to \neg X \in Fin$
19	18	3expia	$⊢ (G \in Grp \land A \in X) \to (O (A) = 0 \to \neg X \in Fin)$
20	7 19	syld	$⊢ (G \in Grp \land A \in X) \to (\neg O (A) \in ℕ \to \neg X \in Fin)$
21	20	con4d	$⊢ (G \in Grp \land A \in X) \to (X \in Fin \to O (A) \in ℕ)$
22	21	3impia	$⊢ (G \in Grp \land A \in X \land X \in Fin) \to O (A) \in ℕ$
23	22	3com23	$⊢ (G \in Grp \land X \in Fin \land A \in X) \to O (A) \in ℕ$

Metamath Proof Explorer

Theorem odcl2

Proof