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 ` G )
Assertion	odadd1	\|- ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) \|\| ( ( O ` A ) x. ( O ` B ) ) )

Proof

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

Metamath Proof Explorer

Theorem odadd1

Proof