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	bitrid	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) = ( 𝑂 ‘ 𝐴 ) ↔ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) )