odadd

Description: The order of a product is the product of the orders, if the factors have coprime order. (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	odadd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} 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		simpl1	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to G \in Abel$
5		ablgrp	$⊢ G \in Abel \to G \in Grp$
6	4 5	syl	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to G \in Grp$
7		simpl2	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to A \in X$
8		simpl3	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to B \in X$
9	2 3	grpcl	$⊢ (G \in Grp \land A \in X \land B \in X) \to A \underset{˙}{+} B \in X$
10	6 7 8 9	syl3anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to A \underset{˙}{+} B \in X$
11	2 1	odcl	$⊢ A \underset{˙}{+} B \in X \to O (A \underset{˙}{+} B) \in ℕ_{0}$
12	10 11	syl	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) \in ℕ_{0}$
13	2 1	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
14	7 13	syl	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A) \in ℕ_{0}$
15	2 1	odcl	$⊢ B \in X \to O (B) \in ℕ_{0}$
16	8 15	syl	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (B) \in ℕ_{0}$
17	14 16	nn0mulcld	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A) O (B) \in ℕ_{0}$
18		simpr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A) \gcd O (B) = 1$
19	18	oveq2d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) = O (A \underset{˙}{+} B) \cdot 1$
20	12	nn0cnd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) \in ℂ$
21	20	mulid1d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) \cdot 1 = O (A \underset{˙}{+} B)$
22	19 21	eqtrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) = O (A \underset{˙}{+} B)$
23	1 2 3	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)$
24	23	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) (O (A) \gcd O (B)) ∥ O (A) O (B)$
25	22 24	eqbrtrrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) ∥ O (A) O (B)$
26	1 2 3	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}$
27	26	adantr	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A) O (B) ∥ O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2}$
28	18	oveq1d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to {(O (A) \gcd O (B))}^{2} = 1^{2}$
29		sq1	$⊢ 1^{2} = 1$
30	28 29	eqtrdi	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to {(O (A) \gcd O (B))}^{2} = 1$
31	30	oveq2d	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2} = O (A \underset{˙}{+} B) \cdot 1$
32	31 21	eqtrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) {(O (A) \gcd O (B))}^{2} = O (A \underset{˙}{+} B)$
33	27 32	breqtrd	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A) O (B) ∥ O (A \underset{˙}{+} B)$
34		dvdseq	$⊢ ((O (A \underset{˙}{+} B) \in ℕ_{0} \land O (A) O (B) \in ℕ_{0}) \land (O (A \underset{˙}{+} B) ∥ O (A) O (B) \land O (A) O (B) ∥ O (A \underset{˙}{+} B))) \to O (A \underset{˙}{+} B) = O (A) O (B)$
35	12 17 25 33 34	syl22anc	$⊢ ((G \in Abel \land A \in X \land B \in X) \land O (A) \gcd O (B) = 1) \to O (A \underset{˙}{+} B) = O (A) O (B)$

Metamath Proof Explorer

Theorem odadd

Proof