Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odcl2.2	⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion	odcl2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		odcl2.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odcl2.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3	1 2	odcl	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
4	3	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
5		elnn0	⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
6	4 5	sylib	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∨ ( 𝑂 ‘ 𝐴 ) = 0 ) )
7	6	ord	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ¬ ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) = 0 ) )
8		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
9		eqid	⊢ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) )
10	1 2 8 9	odinf	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ¬ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin )
11	1 2 8 9	odf1	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 ↔ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1→ 𝑋 ) )
12	11	biimp3a	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1→ 𝑋 )
13		f1f	⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ –1-1→ 𝑋 → ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ ⟶ 𝑋 )
14		frn	⊢ ( ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) : ℤ ⟶ 𝑋 → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ⊆ 𝑋 )
15		ssfi	⊢ ( ( 𝑋 ∈ Fin ∧ ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ⊆ 𝑋 ) → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin )
16	15	expcom	⊢ ( ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ⊆ 𝑋 → ( 𝑋 ∈ Fin → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin ) )
17	12 13 14 16	4syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( 𝑋 ∈ Fin → ran ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝐺 ) 𝐴 ) ) ∈ Fin ) )
18	10 17	mtod	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ¬ 𝑋 ∈ Fin )
19	18	3expia	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝐴 ) = 0 → ¬ 𝑋 ∈ Fin ) )
20	7 19	syld	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ¬ ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ¬ 𝑋 ∈ Fin ) )
21	20	con4d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑋 ∈ Fin → ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) )
22	21	3impia	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑋 ∈ Fin ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )
23	22	3com23	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ )