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

Metamath Proof Explorer

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 ∧ 𝑁 ∈ ℤ ) → ( 𝐸 ∥ 𝑁 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∥ 𝑁 ) )