odadd1

Description: The order of a product in an abelian group divides the LCM of the orders of the factors. (Contributed by Mario Carneiro, 20-Oct-2015)

	Ref	Expression
Hypotheses	odadd1.1	$⊢ O = od (G)$
	odadd1.2	$⊢ X = {Base}_{G}$
	odadd1.3	$⊢ \underset{˙}{+} = +_{G}$
Assertion	odadd1	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ O (A) O (B)$

Proof

Step	Hyp	Ref	Expression
1		odadd1.1	$⊢ O = od (G)$
2		odadd1.2	$⊢ X = {Base}_{G}$
3		odadd1.3	$⊢ \underset{˙}{+} = +_{G}$
4		ablgrp	$⊢ G \in Abel \to G \in Grp$
5	2 3	grpcl	$⊢ (G \in Grp \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
6	4 5	syl3an1	$⊢ (G \in Abel \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
7	2 1	odcl	$⊢ A \underset{˙}{+} B \in X \to O (A \underset{˙}{+} B) \in ℕ_{0}$
8	6 7	syl	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A \underset{˙}{+} B) \in ℕ_{0}$
9	8	nn0zd	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A \underset{˙}{+} B) \in ℤ$
10	2 1	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
11	10	3ad2ant2	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) \in ℕ_{0}$
12	11	nn0zd	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) \in ℤ$
13	2 1	odcl	$⊢ B \in X \to O (B) \in ℕ_{0}$
14	13	3ad2ant3	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (B) \in ℕ_{0}$
15	14	nn0zd	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (B) \in ℤ$
16	12 15	gcdcld	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) \gcd O (B) \in ℕ_{0}$
17	16	nn0zd	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) \gcd O (B) \in ℤ$
18	9 17	zmulcld	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) \in ℤ$
19	18	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) \in ℤ$
20		dvds0	$⊢ O (A \underset{˙}{+} B) (O (A) \gcd O (B)) \in ℤ \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ 0$
21	19 20	syl	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ 0$
22		gcdeq0	$⊢ (O (A) \in ℤ \land O (B) \in ℤ) \to (O (A) \gcd O (B) = 0 \leftrightarrow (O (A) = 0 \land O (B) = 0))$
23	12 15 22	syl2anc	$⊢ (G \in Abel \land A \in X \land B \in X) \to (O (A) \gcd O (B) = 0 \leftrightarrow (O (A) = 0 \land O (B) = 0))$
24	23	biimpa	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to (O (A) = 0 \land O (B) = 0)$
25		oveq12	$⊢ (O (A) = 0 \land O (B) = 0) \to O (A) O (B) = 0 \cdot 0$
26		0cn	$⊢ 0 \in ℂ$
27	26	mul01i	$⊢ 0 \cdot 0 = 0$
28	25 27	eqtrdi	$⊢ (O (A) = 0 \land O (B) = 0) \to O (A) O (B) = 0$
29	24 28	syl	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A) O (B) = 0$
30	21 29	breqtrrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ O (A) O (B)$
31		simpl1	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to G \in Abel$
32	17	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) \gcd O (B) \in ℤ$
33	12	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) \in ℤ$
34	15	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) \in ℤ$
35		gcddvds	$⊢ (O (A) \in ℤ \land O (B) \in ℤ) \to ((O (A) \gcd O (B)) ∥ O (A) \land (O (A) \gcd O (B)) ∥ O (B))$
36	33 34 35	syl2anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to ((O (A) \gcd O (B)) ∥ O (A) \land (O (A) \gcd O (B)) ∥ O (B))$
37	36	simpld	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (A) \gcd O (B)) ∥ O (A)$
38	32 33 34 37	dvdsmultr1d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (A) \gcd O (B)) ∥ O (A) O (B)$
39		simpr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) \gcd O (B) \neq 0$
40	33 34	zmulcld	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) O (B) \in ℤ$
41		dvdsval2	$⊢ (O (A) \gcd O (B) \in ℤ \land O (A) \gcd O (B) \neq 0 \land O (A) O (B) \in ℤ) \to ((O (A) \gcd O (B)) ∥ O (A) O (B) \leftrightarrow \frac{O (A) O (B)}{O (A) \gcd O (B)} \in ℤ)$
42	32 39 40 41	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to ((O (A) \gcd O (B)) ∥ O (A) O (B) \leftrightarrow \frac{O (A) O (B)}{O (A) \gcd O (B)} \in ℤ)$
43	38 42	mpbid	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to \frac{O (A) O (B)}{O (A) \gcd O (B)} \in ℤ$
44		simpl2	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to A \in X$
45		simpl3	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to B \in X$
46		eqid	$⊢ \cdot_{G} = \cdot_{G}$
47	2 46 3	mulgdi	$⊢ (G \in Abel \land (\frac{O (A) O (B)}{O (A) \gcd O (B)} \in ℤ \land A \in X \land B \in X)) \to (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} (A \underset{˙}{+} B) = ((\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} A) \underset{˙}{+} ((\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} B)$
48	31 43 44 45 47	syl13anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} (A \underset{˙}{+} B) = ((\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} A) \underset{˙}{+} ((\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} B)$
49	36	simprd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (A) \gcd O (B)) ∥ O (B)$
50		dvdsval2	$⊢ (O (A) \gcd O (B) \in ℤ \land O (A) \gcd O (B) \neq 0 \land O (B) \in ℤ) \to ((O (A) \gcd O (B)) ∥ O (B) \leftrightarrow \frac{O (B)}{O (A) \gcd O (B)} \in ℤ)$
51	32 39 34 50	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to ((O (A) \gcd O (B)) ∥ O (B) \leftrightarrow \frac{O (B)}{O (A) \gcd O (B)} \in ℤ)$
52	49 51	mpbid	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to \frac{O (B)}{O (A) \gcd O (B)} \in ℤ$
53		dvdsmul1	$⊢ (O (A) \in ℤ \land \frac{O (B)}{O (A) \gcd O (B)} \in ℤ) \to O (A) ∥ O (A) (\frac{O (B)}{O (A) \gcd O (B)})$
54	33 52 53	syl2anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) ∥ O (A) (\frac{O (B)}{O (A) \gcd O (B)})$
55	33	zcnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) \in ℂ$
56	34	zcnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) \in ℂ$
57	32	zcnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) \gcd O (B) \in ℂ$
58	55 56 57 39	divassd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to \frac{O (A) O (B)}{O (A) \gcd O (B)} = O (A) (\frac{O (B)}{O (A) \gcd O (B)})$
59	54 58	breqtrrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)})$
60	31 4	syl	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to G \in Grp$
61		eqid	$⊢ 0_{G} = 0_{G}$
62	2 1 46 61	oddvds	$⊢ (G \in Grp \land A \in X \land \frac{O (A) O (B)}{O (A) \gcd O (B)} \in ℤ) \to (O (A) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \leftrightarrow (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} A = 0_{G})$
63	60 44 43 62	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (A) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \leftrightarrow (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} A = 0_{G})$
64	59 63	mpbid	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} A = 0_{G}$
65		dvdsval2	$⊢ (O (A) \gcd O (B) \in ℤ \land O (A) \gcd O (B) \neq 0 \land O (A) \in ℤ) \to ((O (A) \gcd O (B)) ∥ O (A) \leftrightarrow \frac{O (A)}{O (A) \gcd O (B)} \in ℤ)$
66	32 39 33 65	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to ((O (A) \gcd O (B)) ∥ O (A) \leftrightarrow \frac{O (A)}{O (A) \gcd O (B)} \in ℤ)$
67	37 66	mpbid	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to \frac{O (A)}{O (A) \gcd O (B)} \in ℤ$
68		dvdsmul1	$⊢ (O (B) \in ℤ \land \frac{O (A)}{O (A) \gcd O (B)} \in ℤ) \to O (B) ∥ O (B) (\frac{O (A)}{O (A) \gcd O (B)})$
69	34 67 68	syl2anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) ∥ O (B) (\frac{O (A)}{O (A) \gcd O (B)})$
70	55 56	mulcomd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) O (B) = O (B) O (A)$
71	70	oveq1d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to \frac{O (A) O (B)}{O (A) \gcd O (B)} = \frac{O (B) O (A)}{O (A) \gcd O (B)}$
72	56 55 57 39	divassd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to \frac{O (B) O (A)}{O (A) \gcd O (B)} = O (B) (\frac{O (A)}{O (A) \gcd O (B)})$
73	71 72	eqtrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to \frac{O (A) O (B)}{O (A) \gcd O (B)} = O (B) (\frac{O (A)}{O (A) \gcd O (B)})$
74	69 73	breqtrrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)})$
75	2 1 46 61	oddvds	$⊢ (G \in Grp \land B \in X \land \frac{O (A) O (B)}{O (A) \gcd O (B)} \in ℤ) \to (O (B) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \leftrightarrow (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} B = 0_{G})$
76	60 45 43 75	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (B) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \leftrightarrow (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} B = 0_{G})$
77	74 76	mpbid	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} B = 0_{G}$
78	64 77	oveq12d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to ((\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} A) \underset{˙}{+} ((\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} B) = 0_{G} \underset{˙}{+} 0_{G}$
79	2 61	grpidcl	$⊢ G \in Grp \to 0_{G} \in X$
80	2 3 61	grplid	$⊢ (G \in Grp \land 0_{G} \in X) \to 0_{G} \underset{˙}{+} 0_{G} = 0_{G}$
81	60 79 80	syl2anc2	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to 0_{G} \underset{˙}{+} 0_{G} = 0_{G}$
82	48 78 81	3eqtrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} (A \underset{˙}{+} B) = 0_{G}$
83	6	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to A \underset{˙}{+} B \in X$
84	2 1 46 61	oddvds	$⊢ (G \in Grp \land A \underset{˙}{+} B \in X \land \frac{O (A) O (B)}{O (A) \gcd O (B)} \in ℤ) \to (O (A \underset{˙}{+} B) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \leftrightarrow (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} (A \underset{˙}{+} B) = 0_{G})$
85	60 83 43 84	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (A \underset{˙}{+} B) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \leftrightarrow (\frac{O (A) O (B)}{O (A) \gcd O (B)}) \cdot_{G} (A \underset{˙}{+} B) = 0_{G})$
86	82 85	mpbird	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A \underset{˙}{+} B) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)})$
87	9	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A \underset{˙}{+} B) \in ℤ$
88		dvdsmulcr	$⊢ (O (A \underset{˙}{+} B) \in ℤ \land \frac{O (A) O (B)}{O (A) \gcd O (B)} \in ℤ \land (O (A) \gcd O (B) \in ℤ \land O (A) \gcd O (B) \neq 0)) \to (O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) \leftrightarrow O (A \underset{˙}{+} B) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}))$
89	87 43 32 39 88	syl112anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) \leftrightarrow O (A \underset{˙}{+} B) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}))$
90	86 89	mpbird	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ (\frac{O (A) O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B))$
91	40	zcnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) O (B) \in ℂ$
92	91 57 39	divcan1d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (\frac{O (A) O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) = O (A) O (B)$
93	90 92	breqtrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ O (A) O (B)$
94	30 93	pm2.61dane	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ O (A) O (B)$

Metamath Proof Explorer

Theorem odadd1

Proof