Metamath Proof Explorer

Theorem odmulgeq

Description: A multiple of a point of finite order only has the same order if the multiplier is relatively prime. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
Assertion odmulgeq ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
4 eqcom ⊢ ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑂 ‘ 𝐴 ) = ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) )
5 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ 𝑋 )
6 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
7 5 6 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
8 7 nn0cnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℂ )
9 simpl1 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝐺 ∈ Grp )
10 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → 𝑁 ∈ ℤ )
11 1 3 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
12 9 10 5 11 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
13 1 2 odcl ⊢ ( ( 𝑁 · 𝐴 ) ∈ 𝑋 → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℕ0 )
14 12 13 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℕ0 )
15 14 nn0cnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℂ )
16 nnne0 ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ → ( 𝑂 ‘ 𝐴 ) ≠ 0 )
17 16 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ≠ 0 )
18 1 2 3 odmulg2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) )
19 18 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) )
20 breq1 ⊢ ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) = 0 → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) ↔ 0 ∥ ( 𝑂 ‘ 𝐴 ) ) )
21 19 20 syl5ibcom ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) = 0 → 0 ∥ ( 𝑂 ‘ 𝐴 ) ) )
22 7 nn0zd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
23 0dvds ⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ → ( 0 ∥ ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑂 ‘ 𝐴 ) = 0 ) )
24 22 23 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 0 ∥ ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑂 ‘ 𝐴 ) = 0 ) )
25 21 24 sylibd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) = 0 → ( 𝑂 ‘ 𝐴 ) = 0 ) )
26 25 necon3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) ≠ 0 → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ≠ 0 ) )
27 17 26 mpd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ≠ 0 )
28 8 15 27 diveq1ad ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) / ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) = 1 ↔ ( 𝑂 ‘ 𝐴 ) = ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )
29 10 22 gcdcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
30 29 nn0cnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℂ )
31 15 30 mulcomd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )
32 1 2 3 odmulg ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )
33 32 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )
34 31 33 eqtr4d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = ( 𝑂 ‘ 𝐴 ) )
35 8 15 30 27 divmuld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) / ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) = ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ↔ ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = ( 𝑂 ‘ 𝐴 ) ) )
36 34 35 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) / ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) = ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) )
37 36 eqeq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( ( 𝑂 ‘ 𝐴 ) / ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) = 1 ↔ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) )
38 28 37 bitr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ 𝐴 ) = ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ↔ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) )
39 4 38 syl5bb ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) )