Theorem gexdvds2

Description: An integer divides the group exponent iff it divides all the group orders. In other words, the group exponent is the LCM of the orders of all the elements. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gexod.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	gexod.2	⊢ 𝐸 = ( gEx ‘ 𝐺 )
	gexod.3	⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion	gexdvds2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) → ( 𝐸 ∥ 𝑁 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		gexod.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		gexod.2	⊢ 𝐸 = ( gEx ‘ 𝐺 )
3		gexod.3	⊢ 𝑂 = ( od ‘ 𝐺 )
4		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
5		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6	1 2 4 5	gexdvds	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) → ( 𝐸 ∥ 𝑁 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
7	1 3 4 5	oddvds	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
8	7	3expa	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
9	8	an32s	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
10	9	ralbidva	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑁 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) )
11	6 10	bitr4d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ) → ( 𝐸 ∥ 𝑁 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) )