Metamath Proof Explorer

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}=\mathrm{od}\left({G}\right)$
odadd1.2 ${⊢}{X}={\mathrm{Base}}_{{G}}$

Proof

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