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	$⊢ X = {Base}_{G}$
	odmulgid.2	$⊢ O = od (G)$
	odmulgid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	odmulgeq	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (O (N \underset{˙}{\cdot} A) = O (A) \leftrightarrow N \gcd O (A) = 1)$

Proof

Step	Hyp	Ref	Expression
1		odmulgid.1	$⊢ X = {Base}_{G}$
2		odmulgid.2	$⊢ O = od (G)$
3		odmulgid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		eqcom	$⊢ O (N \underset{˙}{\cdot} A) = O (A) \leftrightarrow O (A) = O (N \underset{˙}{\cdot} A)$
5		simpl2	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to A \in X$
6	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
7	5 6	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℕ_{0}$
8	7	nn0cnd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℂ$
9		simpl1	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to G \in Grp$
10		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \in ℤ$
11	1 3	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land A \in X) \to N \underset{˙}{\cdot} A \in X$
12	9 10 5 11	syl3anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \underset{˙}{\cdot} A \in X$
13	1 2	odcl	$⊢ N \underset{˙}{\cdot} A \in X \to O (N \underset{˙}{\cdot} A) \in ℕ_{0}$
14	12 13	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (N \underset{˙}{\cdot} A) \in ℕ_{0}$
15	14	nn0cnd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (N \underset{˙}{\cdot} A) \in ℂ$
16		nnne0	$⊢ O (A) \in ℕ \to O (A) \neq 0$
17	16	adantl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \neq 0$
18	1 2 3	odmulg2	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (N \underset{˙}{\cdot} A) ∥ O (A)$
19	18	adantr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (N \underset{˙}{\cdot} A) ∥ O (A)$
20		breq1	$⊢ O (N \underset{˙}{\cdot} A) = 0 \to (O (N \underset{˙}{\cdot} A) ∥ O (A) \leftrightarrow 0 ∥ O (A))$
21	19 20	syl5ibcom	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (O (N \underset{˙}{\cdot} A) = 0 \to 0 ∥ O (A))$
22	7	nn0zd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) \in ℤ$
23		0dvds	$⊢ O (A) \in ℤ \to (0 ∥ O (A) \leftrightarrow O (A) = 0)$
24	22 23	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (0 ∥ O (A) \leftrightarrow O (A) = 0)$
25	21 24	sylibd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (O (N \underset{˙}{\cdot} A) = 0 \to O (A) = 0)$
26	25	necon3d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (O (A) \neq 0 \to O (N \underset{˙}{\cdot} A) \neq 0)$
27	17 26	mpd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (N \underset{˙}{\cdot} A) \neq 0$
28	8 15 27	diveq1ad	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (\frac{O (A)}{O (N \underset{˙}{\cdot} A)} = 1 \leftrightarrow O (A) = O (N \underset{˙}{\cdot} A))$
29	10 22	gcdcld	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \gcd O (A) \in ℕ_{0}$
30	29	nn0cnd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to N \gcd O (A) \in ℂ$
31	15 30	mulcomd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (N \underset{˙}{\cdot} A) (N \gcd O (A)) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A)$
32	1 2 3	odmulg	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (A) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A)$
33	32	adantr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (A) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A)$
34	31 33	eqtr4d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to O (N \underset{˙}{\cdot} A) (N \gcd O (A)) = O (A)$
35	8 15 30 27	divmuld	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (\frac{O (A)}{O (N \underset{˙}{\cdot} A)} = N \gcd O (A) \leftrightarrow O (N \underset{˙}{\cdot} A) (N \gcd O (A)) = O (A))$
36	34 35	mpbird	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to \frac{O (A)}{O (N \underset{˙}{\cdot} A)} = N \gcd O (A)$
37	36	eqeq1d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (\frac{O (A)}{O (N \underset{˙}{\cdot} A)} = 1 \leftrightarrow N \gcd O (A) = 1)$
38	28 37	bitr3d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (O (A) = O (N \underset{˙}{\cdot} A) \leftrightarrow N \gcd O (A) = 1)$
39	4 38	bitrid	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land O (A) \in ℕ) \to (O (N \underset{˙}{\cdot} A) = O (A) \leftrightarrow N \gcd O (A) = 1)$

Metamath Proof Explorer

Theorem odmulgeq

Proof