Theorem gexdvds3

Description: The exponent of a finite group divides the order (cardinality) of the group. Corollary of Lagrange's theorem for the order of a subgroup. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gexcl2.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	gexcl2.2	⊢ 𝐸 = ( gEx ‘ 𝐺 )
Assertion	gexdvds3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → 𝐸 ∥ ( ♯ ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		gexcl2.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		gexcl2.2	⊢ 𝐸 = ( gEx ‘ 𝐺 )
3		eqid	⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
4	1 3	oddvds2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) )
5	4	3expa	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) ∧ 𝑥 ∈ 𝑋 ) → ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) )
6	5	ralrimiva	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ∀ 𝑥 ∈ 𝑋 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) )
7		hashcl	⊢ ( 𝑋 ∈ Fin → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
8	7	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
9	8	nn0zd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) ∈ ℤ )
10	1 2 3	gexdvds2	⊢ ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝑋 ) ∈ ℤ ) → ( 𝐸 ∥ ( ♯ ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) ) )
11	9 10	syldan	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → ( 𝐸 ∥ ( ♯ ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( ♯ ‘ 𝑋 ) ) )
12	6 11	mpbird	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ) → 𝐸 ∥ ( ♯ ‘ 𝑋 ) )