odadd2

Description: The order of a product in an abelian group is divisible by the LCM of the orders of the factors divided by the GCD. (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	odadd2	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) O (B) ∥ O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2}$

Proof

Step	Hyp	Ref	Expression
1		odadd1.1	$⊢ O = od (G)$
2		odadd1.2	$⊢ X = {Base}_{G}$
3		odadd1.3	$⊢ \underset{˙}{+} = +_{G}$
4	2 1	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
5	4	3ad2ant2	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) \in ℕ_{0}$
6	5	nn0zd	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) \in ℤ$
7	2 1	odcl	$⊢ B \in X \to O (B) \in ℕ_{0}$
8	7	3ad2ant3	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (B) \in ℕ_{0}$
9	8	nn0zd	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (B) \in ℤ$
10	6 9	zmulcld	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) O (B) \in ℤ$
11	10	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A) O (B) \in ℤ$
12		dvds0	$⊢ O (A) O (B) \in ℤ \to O (A) O (B) ∥ 0$
13	11 12	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$
14		simpr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A) \gcd O (B) = 0$
15	14	sq0id	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to {(O (A) \gcd O (B))}^{2} = 0$
16	15	oveq2d	$⊢ ((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))}^{2} = O (A \underset{˙}{+} B) \cdot 0$
17		ablgrp	$⊢ G \in Abel \to G \in Grp$
18	2 3	grpcl	$⊢ (G \in Grp \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
19	17 18	syl3an1	$⊢ (G \in Abel \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
20	2 1	odcl	$⊢ A \underset{˙}{+} B \in X \to O (A \underset{˙}{+} B) \in ℕ_{0}$
21	19 20	syl	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A \underset{˙}{+} B) \in ℕ_{0}$
22	21	nn0zd	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A \underset{˙}{+} B) \in ℤ$
23	22	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A \underset{˙}{+} B) \in ℤ$
24	23	zcnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A \underset{˙}{+} B) \in ℂ$
25	24	mul01d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A \underset{˙}{+} B) \cdot 0 = 0$
26	16 25	eqtrd	$⊢ ((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))}^{2} = 0$
27	13 26	breqtrrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 0) \to O (A) O (B) ∥ O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2}$
28	6	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) \in ℤ$
29	9	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) \in ℤ$
30	28 29	gcdcld	$⊢ ((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 ℕ_{0}$
31	30	nn0cnd	$⊢ ((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 ℂ$
32	31	sqvald	$⊢ ((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))}^{2} = (O (A) \gcd O (B)) (O (A) \gcd O (B))$
33	32	oveq2d	$⊢ ((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)}) (\frac{O (B)}{O (A) \gcd O (B)}) {(O (A) \gcd O (B))}^{2} = (\frac{O (A)}{O (A) \gcd O (B)}) (\frac{O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) (O (A) \gcd O (B))$
34		gcddvds	$⊢ (O (A) \in ℤ \land O (B) \in ℤ) \to ((O (A) \gcd O (B)) ∥ O (A) \land (O (A) \gcd O (B)) ∥ O (B))$
35	28 29 34	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))$
36	35	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)$
37	30	nn0zd	$⊢ ((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 ℤ$
38		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$
39		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 ℤ)$
40	37 38 28 39	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 ℤ)$
41	36 40	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 ℤ$
42	41	zcnd	$⊢ ((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 ℂ$
43	35	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)$
44		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 ℤ)$
45	37 38 29 44	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 ℤ)$
46	43 45	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 ℤ$
47	46	zcnd	$⊢ ((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 ℂ$
48	42 31 47 31	mul4d	$⊢ ((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)}) (O (A) \gcd O (B)) (\frac{O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) = (\frac{O (A)}{O (A) \gcd O (B)}) (\frac{O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) (O (A) \gcd O (B))$
49	28	zcnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) \in ℂ$
50	49 31 38	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 (A) \gcd O (B)}) (O (A) \gcd O (B)) = O (A)$
51	29	zcnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) \in ℂ$
52	51 31 38	divcan1d	$⊢ ((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)}) (O (A) \gcd O (B)) = O (B)$
53	50 52	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 (A) \gcd O (B)}) (O (A) \gcd O (B)) (\frac{O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) = O (A) O (B)$
54	33 48 53	3eqtr2d	$⊢ ((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)}) (\frac{O (B)}{O (A) \gcd O (B)}) {(O (A) \gcd O (B))}^{2} = O (A) O (B)$
55	22	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 ℤ$
56		dvdsmul2	$⊢ (O (A \underset{˙}{+} B) \in ℤ \land O (A) \in ℤ) \to O (A) ∥ O (A \underset{˙}{+} B) O (A)$
57	55 28 56	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 \underset{˙}{+} B) O (A)$
58		simpl1	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to G \in Abel$
59	55 29	zmulcld	$⊢ ((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 (B) \in ℤ$
60		simpl2	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to A \in X$
61		simpl3	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to B \in X$
62		eqid	$⊢ \cdot_{G} = \cdot_{G}$
63	2 62 3	mulgdi	$⊢ (G \in Abel \land (O (A \underset{˙}{+} B) O (B) \in ℤ \land A \in X \land B \in X)) \to O (A \underset{˙}{+} B) O (B) \cdot_{G} (A \underset{˙}{+} B) = (O (A \underset{˙}{+} B) O (B) \cdot_{G} A) \underset{˙}{+} (O (A \underset{˙}{+} B) O (B) \cdot_{G} B)$
64	58 59 60 61 63	syl13anc	$⊢ ((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 (B) \cdot_{G} (A \underset{˙}{+} B) = (O (A \underset{˙}{+} B) O (B) \cdot_{G} A) \underset{˙}{+} (O (A \underset{˙}{+} B) O (B) \cdot_{G} B)$
65		dvdsmul2	$⊢ (O (A \underset{˙}{+} B) \in ℤ \land O (B) \in ℤ) \to O (B) ∥ O (A \underset{˙}{+} B) O (B)$
66	55 29 65	syl2anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) ∥ O (A \underset{˙}{+} B) O (B)$
67	58 17	syl	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to G \in Grp$
68		eqid	$⊢ 0_{G} = 0_{G}$
69	2 1 62 68	oddvds	$⊢ (G \in Grp \land B \in X \land O (A \underset{˙}{+} B) O (B) \in ℤ) \to (O (B) ∥ O (A \underset{˙}{+} B) O (B) \leftrightarrow O (A \underset{˙}{+} B) O (B) \cdot_{G} B = 0_{G})$
70	67 61 59 69	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (B) ∥ O (A \underset{˙}{+} B) O (B) \leftrightarrow O (A \underset{˙}{+} B) O (B) \cdot_{G} B = 0_{G})$
71	66 70	mpbid	$⊢ ((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 (B) \cdot_{G} B = 0_{G}$
72	71	oveq2d	$⊢ ((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 (B) \cdot_{G} A) \underset{˙}{+} (O (A \underset{˙}{+} B) O (B) \cdot_{G} B) = (O (A \underset{˙}{+} B) O (B) \cdot_{G} A) \underset{˙}{+} 0_{G}$
73	64 72	eqtrd	$⊢ ((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 (B) \cdot_{G} (A \underset{˙}{+} B) = (O (A \underset{˙}{+} B) O (B) \cdot_{G} A) \underset{˙}{+} 0_{G}$
74		dvdsmul1	$⊢ (O (A \underset{˙}{+} B) \in ℤ \land O (B) \in ℤ) \to O (A \underset{˙}{+} B) ∥ O (A \underset{˙}{+} B) O (B)$
75	55 29 74	syl2anc	$⊢ ((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 \underset{˙}{+} B) O (B)$
76	19	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$
77	2 1 62 68	oddvds	$⊢ (G \in Grp \land A \underset{˙}{+} B \in X \land O (A \underset{˙}{+} B) O (B) \in ℤ) \to (O (A \underset{˙}{+} B) ∥ O (A \underset{˙}{+} B) O (B) \leftrightarrow O (A \underset{˙}{+} B) O (B) \cdot_{G} (A \underset{˙}{+} B) = 0_{G})$
78	67 76 59 77	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) ∥ O (A \underset{˙}{+} B) O (B) \leftrightarrow O (A \underset{˙}{+} B) O (B) \cdot_{G} (A \underset{˙}{+} B) = 0_{G})$
79	75 78	mpbid	$⊢ ((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 (B) \cdot_{G} (A \underset{˙}{+} B) = 0_{G}$
80	2 62	mulgcl	$⊢ (G \in Grp \land O (A \underset{˙}{+} B) O (B) \in ℤ \land A \in X) \to O (A \underset{˙}{+} B) O (B) \cdot_{G} A \in X$
81	67 59 60 80	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) O (B) \cdot_{G} A \in X$
82	2 3 68	grprid	$⊢ (G \in Grp \land O (A \underset{˙}{+} B) O (B) \cdot_{G} A \in X) \to (O (A \underset{˙}{+} B) O (B) \cdot_{G} A) \underset{˙}{+} 0_{G} = O (A \underset{˙}{+} B) O (B) \cdot_{G} A$
83	67 81 82	syl2anc	$⊢ ((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 (B) \cdot_{G} A) \underset{˙}{+} 0_{G} = O (A \underset{˙}{+} B) O (B) \cdot_{G} A$
84	73 79 83	3eqtr3rd	$⊢ ((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 (B) \cdot_{G} A = 0_{G}$
85	2 1 62 68	oddvds	$⊢ (G \in Grp \land A \in X \land O (A \underset{˙}{+} B) O (B) \in ℤ) \to (O (A) ∥ O (A \underset{˙}{+} B) O (B) \leftrightarrow O (A \underset{˙}{+} B) O (B) \cdot_{G} A = 0_{G})$
86	67 60 59 85	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (A) ∥ O (A \underset{˙}{+} B) O (B) \leftrightarrow O (A \underset{˙}{+} B) O (B) \cdot_{G} A = 0_{G})$
87	84 86	mpbird	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) ∥ O (A \underset{˙}{+} B) O (B)$
88	55 28	zmulcld	$⊢ ((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) \in ℤ$
89		dvdsgcd	$⊢ (O (A) \in ℤ \land O (A \underset{˙}{+} B) O (A) \in ℤ \land O (A \underset{˙}{+} B) O (B) \in ℤ) \to ((O (A) ∥ O (A \underset{˙}{+} B) O (A) \land O (A) ∥ O (A \underset{˙}{+} B) O (B)) \to O (A) ∥ (O (A \underset{˙}{+} B) O (A) \gcd O (A \underset{˙}{+} B) O (B)))$
90	28 88 59 89	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to ((O (A) ∥ O (A \underset{˙}{+} B) O (A) \land O (A) ∥ O (A \underset{˙}{+} B) O (B)) \to O (A) ∥ (O (A \underset{˙}{+} B) O (A) \gcd O (A \underset{˙}{+} B) O (B)))$
91	57 87 90	mp2and	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) ∥ (O (A \underset{˙}{+} B) O (A) \gcd O (A \underset{˙}{+} B) O (B))$
92	21	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 ℕ_{0}$
93		mulgcd	$⊢ (O (A \underset{˙}{+} B) \in ℕ_{0} \land O (A) \in ℤ \land O (B) \in ℤ) \to O (A \underset{˙}{+} B) O (A) \gcd O (A \underset{˙}{+} B) O (B) = O (A \underset{˙}{+} B) (O (A) \gcd O (B))$
94	92 28 29 93	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) O (A) \gcd O (A \underset{˙}{+} B) O (B) = O (A \underset{˙}{+} B) (O (A) \gcd O (B))$
95	91 94	breqtrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (A) ∥ O (A \underset{˙}{+} B) (O (A) \gcd O (B))$
96	50 95	eqbrtrd	$⊢ ((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)}) (O (A) \gcd O (B)) ∥ O (A \underset{˙}{+} B) (O (A) \gcd O (B))$
97		dvdsmulcr	$⊢ (\frac{O (A)}{O (A) \gcd O (B)} \in ℤ \land O (A \underset{˙}{+} B) \in ℤ \land (O (A) \gcd O (B) \in ℤ \land O (A) \gcd O (B) \neq 0)) \to ((\frac{O (A)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) ∥ O (A \underset{˙}{+} B) (O (A) \gcd O (B)) \leftrightarrow (\frac{O (A)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B))$
98	41 55 37 38 97	syl112anc	$⊢ ((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)}) (O (A) \gcd O (B)) ∥ O (A \underset{˙}{+} B) (O (A) \gcd O (B)) \leftrightarrow (\frac{O (A)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B))$
99	96 98	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)}) ∥ O (A \underset{˙}{+} B)$
100	2 62 3	mulgdi	$⊢ (G \in Abel \land (O (A \underset{˙}{+} B) O (A) \in ℤ \land A \in X \land B \in X)) \to O (A \underset{˙}{+} B) O (A) \cdot_{G} (A \underset{˙}{+} B) = (O (A \underset{˙}{+} B) O (A) \cdot_{G} A) \underset{˙}{+} (O (A \underset{˙}{+} B) O (A) \cdot_{G} B)$
101	58 88 60 61 100	syl13anc	$⊢ ((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) \cdot_{G} (A \underset{˙}{+} B) = (O (A \underset{˙}{+} B) O (A) \cdot_{G} A) \underset{˙}{+} (O (A \underset{˙}{+} B) O (A) \cdot_{G} B)$
102	2 1 62 68	oddvds	$⊢ (G \in Grp \land A \in X \land O (A \underset{˙}{+} B) O (A) \in ℤ) \to (O (A) ∥ O (A \underset{˙}{+} B) O (A) \leftrightarrow O (A \underset{˙}{+} B) O (A) \cdot_{G} A = 0_{G})$
103	67 60 88 102	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (A) ∥ O (A \underset{˙}{+} B) O (A) \leftrightarrow O (A \underset{˙}{+} B) O (A) \cdot_{G} A = 0_{G})$
104	57 103	mpbid	$⊢ ((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) \cdot_{G} A = 0_{G}$
105	104	oveq1d	$⊢ ((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) \cdot_{G} A) \underset{˙}{+} (O (A \underset{˙}{+} B) O (A) \cdot_{G} B) = 0_{G} \underset{˙}{+} (O (A \underset{˙}{+} B) O (A) \cdot_{G} B)$
106	101 105	eqtrd	$⊢ ((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) \cdot_{G} (A \underset{˙}{+} B) = 0_{G} \underset{˙}{+} (O (A \underset{˙}{+} B) O (A) \cdot_{G} B)$
107		dvdsmul1	$⊢ (O (A \underset{˙}{+} B) \in ℤ \land O (A) \in ℤ) \to O (A \underset{˙}{+} B) ∥ O (A \underset{˙}{+} B) O (A)$
108	55 28 107	syl2anc	$⊢ ((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 \underset{˙}{+} B) O (A)$
109	2 1 62 68	oddvds	$⊢ (G \in Grp \land A \underset{˙}{+} B \in X \land O (A \underset{˙}{+} B) O (A) \in ℤ) \to (O (A \underset{˙}{+} B) ∥ O (A \underset{˙}{+} B) O (A) \leftrightarrow O (A \underset{˙}{+} B) O (A) \cdot_{G} (A \underset{˙}{+} B) = 0_{G})$
110	67 76 88 109	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) ∥ O (A \underset{˙}{+} B) O (A) \leftrightarrow O (A \underset{˙}{+} B) O (A) \cdot_{G} (A \underset{˙}{+} B) = 0_{G})$
111	108 110	mpbid	$⊢ ((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) \cdot_{G} (A \underset{˙}{+} B) = 0_{G}$
112	2 62	mulgcl	$⊢ (G \in Grp \land O (A \underset{˙}{+} B) O (A) \in ℤ \land B \in X) \to O (A \underset{˙}{+} B) O (A) \cdot_{G} B \in X$
113	67 88 61 112	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) O (A) \cdot_{G} B \in X$
114	2 3 68	grplid	$⊢ (G \in Grp \land O (A \underset{˙}{+} B) O (A) \cdot_{G} B \in X) \to 0_{G} \underset{˙}{+} (O (A \underset{˙}{+} B) O (A) \cdot_{G} B) = O (A \underset{˙}{+} B) O (A) \cdot_{G} B$
115	67 113 114	syl2anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to 0_{G} \underset{˙}{+} (O (A \underset{˙}{+} B) O (A) \cdot_{G} B) = O (A \underset{˙}{+} B) O (A) \cdot_{G} B$
116	106 111 115	3eqtr3rd	$⊢ ((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) \cdot_{G} B = 0_{G}$
117	2 1 62 68	oddvds	$⊢ (G \in Grp \land B \in X \land O (A \underset{˙}{+} B) O (A) \in ℤ) \to (O (B) ∥ O (A \underset{˙}{+} B) O (A) \leftrightarrow O (A \underset{˙}{+} B) O (A) \cdot_{G} B = 0_{G})$
118	67 61 88 117	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to (O (B) ∥ O (A \underset{˙}{+} B) O (A) \leftrightarrow O (A \underset{˙}{+} B) O (A) \cdot_{G} B = 0_{G})$
119	116 118	mpbird	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) ∥ O (A \underset{˙}{+} B) O (A)$
120		dvdsgcd	$⊢ (O (B) \in ℤ \land O (A \underset{˙}{+} B) O (A) \in ℤ \land O (A \underset{˙}{+} B) O (B) \in ℤ) \to ((O (B) ∥ O (A \underset{˙}{+} B) O (A) \land O (B) ∥ O (A \underset{˙}{+} B) O (B)) \to O (B) ∥ (O (A \underset{˙}{+} B) O (A) \gcd O (A \underset{˙}{+} B) O (B)))$
121	29 88 59 120	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to ((O (B) ∥ O (A \underset{˙}{+} B) O (A) \land O (B) ∥ O (A \underset{˙}{+} B) O (B)) \to O (B) ∥ (O (A \underset{˙}{+} B) O (A) \gcd O (A \underset{˙}{+} B) O (B)))$
122	119 66 121	mp2and	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) ∥ (O (A \underset{˙}{+} B) O (A) \gcd O (A \underset{˙}{+} B) O (B))$
123	122 94	breqtrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to O (B) ∥ O (A \underset{˙}{+} B) (O (A) \gcd O (B))$
124	52 123	eqbrtrd	$⊢ ((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)}) (O (A) \gcd O (B)) ∥ O (A \underset{˙}{+} B) (O (A) \gcd O (B))$
125		dvdsmulcr	$⊢ (\frac{O (B)}{O (A) \gcd O (B)} \in ℤ \land O (A \underset{˙}{+} B) \in ℤ \land (O (A) \gcd O (B) \in ℤ \land O (A) \gcd O (B) \neq 0)) \to ((\frac{O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) ∥ O (A \underset{˙}{+} B) (O (A) \gcd O (B)) \leftrightarrow (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B))$
126	46 55 37 38 125	syl112anc	$⊢ ((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)}) (O (A) \gcd O (B)) ∥ O (A \underset{˙}{+} B) (O (A) \gcd O (B)) \leftrightarrow (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B))$
127	124 126	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)}) ∥ O (A \underset{˙}{+} B)$
128	41 46	gcdcld	$⊢ ((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)}) \gcd (\frac{O (B)}{O (A) \gcd O (B)}) \in ℕ_{0}$
129	128	nn0cnd	$⊢ ((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)}) \gcd (\frac{O (B)}{O (A) \gcd O (B)}) \in ℂ$
130		1cnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to 1 \in ℂ$
131	31	mulid2d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) \neq 0) \to 1 (O (A) \gcd O (B)) = O (A) \gcd O (B)$
132	50 52	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 (A) \gcd O (B)}) (O (A) \gcd O (B)) \gcd (\frac{O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) = O (A) \gcd O (B)$
133		mulgcdr	$⊢ (\frac{O (A)}{O (A) \gcd O (B)} \in ℤ \land \frac{O (B)}{O (A) \gcd O (B)} \in ℤ \land O (A) \gcd O (B) \in ℕ_{0}) \to (\frac{O (A)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) \gcd (\frac{O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) = ((\frac{O (A)}{O (A) \gcd O (B)}) \gcd (\frac{O (B)}{O (A) \gcd O (B)})) (O (A) \gcd O (B))$
134	41 46 30 133	syl3anc	$⊢ ((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)}) (O (A) \gcd O (B)) \gcd (\frac{O (B)}{O (A) \gcd O (B)}) (O (A) \gcd O (B)) = ((\frac{O (A)}{O (A) \gcd O (B)}) \gcd (\frac{O (B)}{O (A) \gcd O (B)})) (O (A) \gcd O (B))$
135	131 132 134	3eqtr2rd	$⊢ ((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)}) \gcd (\frac{O (B)}{O (A) \gcd O (B)})) (O (A) \gcd O (B)) = 1 (O (A) \gcd O (B))$
136	129 130 31 38 135	mulcan2ad	$⊢ ((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)}) \gcd (\frac{O (B)}{O (A) \gcd O (B)}) = 1$
137		coprmdvds2	$⊢ ((\frac{O (A)}{O (A) \gcd O (B)} \in ℤ \land \frac{O (B)}{O (A) \gcd O (B)} \in ℤ \land O (A \underset{˙}{+} B) \in ℤ) \land (\frac{O (A)}{O (A) \gcd O (B)}) \gcd (\frac{O (B)}{O (A) \gcd O (B)}) = 1) \to (((\frac{O (A)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B) \land (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B)) \to (\frac{O (A)}{O (A) \gcd O (B)}) (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B))$
138	41 46 55 136 137	syl31anc	$⊢ ((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)}) ∥ O (A \underset{˙}{+} B) \land (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B)) \to (\frac{O (A)}{O (A) \gcd O (B)}) (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B))$
139	99 127 138	mp2and	$⊢ ((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)}) (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B)$
140	41 46	zmulcld	$⊢ ((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)}) (\frac{O (B)}{O (A) \gcd O (B)}) \in ℤ$
141		zsqcl	$⊢ O (A) \gcd O (B) \in ℤ \to {(O (A) \gcd O (B))}^{2} \in ℤ$
142	37 141	syl	$⊢ ((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))}^{2} \in ℤ$
143		dvdsmulc	$⊢ ((\frac{O (A)}{O (A) \gcd O (B)}) (\frac{O (B)}{O (A) \gcd O (B)}) \in ℤ \land O (A \underset{˙}{+} B) \in ℤ \land {(O (A) \gcd O (B))}^{2} \in ℤ) \to ((\frac{O (A)}{O (A) \gcd O (B)}) (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B) \to (\frac{O (A)}{O (A) \gcd O (B)}) (\frac{O (B)}{O (A) \gcd O (B)}) {(O (A) \gcd O (B))}^{2} ∥ O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2})$
144	140 55 142 143	syl3anc	$⊢ ((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)}) (\frac{O (B)}{O (A) \gcd O (B)}) ∥ O (A \underset{˙}{+} B) \to (\frac{O (A)}{O (A) \gcd O (B)}) (\frac{O (B)}{O (A) \gcd O (B)}) {(O (A) \gcd O (B))}^{2} ∥ O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2})$
145	139 144	mpd	$⊢ ((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)}) (\frac{O (B)}{O (A) \gcd O (B)}) {(O (A) \gcd O (B))}^{2} ∥ O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2}$
146	54 145	eqbrtrrd	$⊢ ((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 (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2}$
147	27 146	pm2.61dane	$⊢ (G \in Abel \land A \in X \land B \in X) \to O (A) O (B) ∥ O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2}$

Metamath Proof Explorer

Theorem odadd2

Proof