This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → 𝐸 ∥ ( ♯ ‘ 𝑋 ) )