Metamath Proof Explorer


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