odmulg

Description: Relationship between the order of an element and that of a multiple. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	odmulgid.1	$⊢ X = {Base}_{G}$
	odmulgid.2	$⊢ O = od (G)$
	odmulgid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	odmulg	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (A) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A)$

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	1 3	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land A \in X) \to N \underset{˙}{\cdot} A \in X$
5	4	3com23	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to N \underset{˙}{\cdot} A \in X$
6	1 2	odcl	$⊢ N \underset{˙}{\cdot} A \in X \to O (N \underset{˙}{\cdot} A) \in ℕ_{0}$
7	5 6	syl	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (N \underset{˙}{\cdot} A) \in ℕ_{0}$
8	7	nn0cnd	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (N \underset{˙}{\cdot} A) \in ℂ$
9	8	adantr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 0) \to O (N \underset{˙}{\cdot} A) \in ℂ$
10	9	mul02d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 0) \to 0 \cdot O (N \underset{˙}{\cdot} A) = 0$
11		simpr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 0) \to N \gcd O (A) = 0$
12	11	oveq1d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 0) \to (N \gcd O (A)) O (N \underset{˙}{\cdot} A) = 0 \cdot O (N \underset{˙}{\cdot} A)$
13		simp3	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to N \in ℤ$
14	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
15	14	3ad2ant2	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (A) \in ℕ_{0}$
16	15	nn0zd	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (A) \in ℤ$
17		gcdeq0	$⊢ (N \in ℤ \land O (A) \in ℤ) \to (N \gcd O (A) = 0 \leftrightarrow (N = 0 \land O (A) = 0))$
18	13 16 17	syl2anc	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to (N \gcd O (A) = 0 \leftrightarrow (N = 0 \land O (A) = 0))$
19	18	simplbda	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 0) \to O (A) = 0$
20	10 12 19	3eqtr4rd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 0) \to O (A) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A)$
21		simpll3	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to N \in ℤ$
22	16	ad2antrr	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to O (A) \in ℤ$
23		gcddvds	$⊢ (N \in ℤ \land O (A) \in ℤ) \to ((N \gcd O (A)) ∥ N \land (N \gcd O (A)) ∥ O (A))$
24	21 22 23	syl2anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to ((N \gcd O (A)) ∥ N \land (N \gcd O (A)) ∥ O (A))$
25	24	simprd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to (N \gcd O (A)) ∥ O (A)$
26	13 16	gcdcld	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to N \gcd O (A) \in ℕ_{0}$
27	26	adantr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to N \gcd O (A) \in ℕ_{0}$
28	27	nn0zd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to N \gcd O (A) \in ℤ$
29	28	adantr	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to N \gcd O (A) \in ℤ$
30		nn0z	$⊢ x \in ℕ_{0} \to x \in ℤ$
31	30	adantl	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to x \in ℤ$
32		dvdstr	$⊢ (N \gcd O (A) \in ℤ \land O (A) \in ℤ \land x \in ℤ) \to (((N \gcd O (A)) ∥ O (A) \land O (A) ∥ x) \to (N \gcd O (A)) ∥ x)$
33	29 22 31 32	syl3anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to (((N \gcd O (A)) ∥ O (A) \land O (A) ∥ x) \to (N \gcd O (A)) ∥ x)$
34	25 33	mpand	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to (O (A) ∥ x \to (N \gcd O (A)) ∥ x)$
35	7	nn0zd	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (N \underset{˙}{\cdot} A) \in ℤ$
36	35	ad2antrr	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to O (N \underset{˙}{\cdot} A) \in ℤ$
37		muldvds1	$⊢ (N \gcd O (A) \in ℤ \land O (N \underset{˙}{\cdot} A) \in ℤ \land x \in ℤ) \to ((N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x \to (N \gcd O (A)) ∥ x)$
38	29 36 31 37	syl3anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to ((N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x \to (N \gcd O (A)) ∥ x)$
39		dvdszrcl	$⊢ (N \gcd O (A)) ∥ x \to (N \gcd O (A) \in ℤ \land x \in ℤ)$
40		divides	$⊢ (N \gcd O (A) \in ℤ \land x \in ℤ) \to ((N \gcd O (A)) ∥ x \leftrightarrow \exists y \in ℤ y (N \gcd O (A)) = x)$
41	39 40	syl	$⊢ (N \gcd O (A)) ∥ x \to ((N \gcd O (A)) ∥ x \leftrightarrow \exists y \in ℤ y (N \gcd O (A)) = x)$
42	41	ibi	$⊢ (N \gcd O (A)) ∥ x \to \exists y \in ℤ y (N \gcd O (A)) = x$
43	35	adantr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to O (N \underset{˙}{\cdot} A) \in ℤ$
44		simprr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to y \in ℤ$
45	28	adantrr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to N \gcd O (A) \in ℤ$
46		simprl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to N \gcd O (A) \neq 0$
47		dvdscmulr	$⊢ (O (N \underset{˙}{\cdot} A) \in ℤ \land y \in ℤ \land (N \gcd O (A) \in ℤ \land N \gcd O (A) \neq 0)) \to ((N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ (N \gcd O (A)) y \leftrightarrow O (N \underset{˙}{\cdot} A) ∥ y)$
48	43 44 45 46 47	syl112anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to ((N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ (N \gcd O (A)) y \leftrightarrow O (N \underset{˙}{\cdot} A) ∥ y)$
49	1 2 3	odmulgid	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land y \in ℤ) \to (O (N \underset{˙}{\cdot} A) ∥ y \leftrightarrow O (A) ∥ y \cdot N)$
50	49	adantrl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to (O (N \underset{˙}{\cdot} A) ∥ y \leftrightarrow O (A) ∥ y \cdot N)$
51		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to N \in ℤ$
52		dvdsmulgcd	$⊢ (y \in ℤ \land N \in ℤ) \to (O (A) ∥ y \cdot N \leftrightarrow O (A) ∥ y (N \gcd O (A)))$
53	44 51 52	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to (O (A) ∥ y \cdot N \leftrightarrow O (A) ∥ y (N \gcd O (A)))$
54	48 50 53	3bitrrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to (O (A) ∥ y (N \gcd O (A)) \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ (N \gcd O (A)) y)$
55	45	zcnd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to N \gcd O (A) \in ℂ$
56	44	zcnd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to y \in ℂ$
57	55 56	mulcomd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to (N \gcd O (A)) y = y (N \gcd O (A))$
58	57	breq2d	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to ((N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ (N \gcd O (A)) y \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ y (N \gcd O (A)))$
59	54 58	bitrd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land (N \gcd O (A) \neq 0 \land y \in ℤ)) \to (O (A) ∥ y (N \gcd O (A)) \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ y (N \gcd O (A)))$
60	59	anassrs	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land y \in ℤ) \to (O (A) ∥ y (N \gcd O (A)) \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ y (N \gcd O (A)))$
61		breq2	$⊢ y (N \gcd O (A)) = x \to (O (A) ∥ y (N \gcd O (A)) \leftrightarrow O (A) ∥ x)$
62		breq2	$⊢ y (N \gcd O (A)) = x \to ((N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ y (N \gcd O (A)) \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x)$
63	61 62	bibi12d	$⊢ y (N \gcd O (A)) = x \to ((O (A) ∥ y (N \gcd O (A)) \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ y (N \gcd O (A))) \leftrightarrow (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x))$
64	60 63	syl5ibcom	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land y \in ℤ) \to (y (N \gcd O (A)) = x \to (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x))$
65	64	rexlimdva	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to (\exists y \in ℤ y (N \gcd O (A)) = x \to (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x))$
66	42 65	syl5	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to ((N \gcd O (A)) ∥ x \to (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x))$
67	66	adantr	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to ((N \gcd O (A)) ∥ x \to (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x))$
68	34 38 67	pm5.21ndd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \land x \in ℕ_{0}) \to (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x)$
69	68	ralrimiva	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to \forall x \in ℕ_{0} (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x)$
70	15	adantr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to O (A) \in ℕ_{0}$
71	7	adantr	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to O (N \underset{˙}{\cdot} A) \in ℕ_{0}$
72	27 71	nn0mulcld	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to (N \gcd O (A)) O (N \underset{˙}{\cdot} A) \in ℕ_{0}$
73		dvdsext	$⊢ (O (A) \in ℕ_{0} \land (N \gcd O (A)) O (N \underset{˙}{\cdot} A) \in ℕ_{0}) \to (O (A) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A) \leftrightarrow \forall x \in ℕ_{0} (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x))$
74	70 72 73	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to (O (A) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A) \leftrightarrow \forall x \in ℕ_{0} (O (A) ∥ x \leftrightarrow (N \gcd O (A)) O (N \underset{˙}{\cdot} A) ∥ x))$
75	69 74	mpbird	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) \neq 0) \to O (A) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A)$
76	20 75	pm2.61dane	$⊢ (G \in Grp \land A \in X \land N \in ℤ) \to O (A) = (N \gcd O (A)) O (N \underset{˙}{\cdot} A)$

Metamath Proof Explorer

Theorem odmulg

Proof