Metamath Proof Explorer

Theorem 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 
|- .+ = ( +g ` G )
Assertion odadd 
|- ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( O ` ( A .+ 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 simpl1 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> G e. Abel )
5 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
6 4 5 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> G e. Grp )
7 simpl2 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> A e. X )
8 simpl3 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> B e. X )
9 2 3 grpcl 
 |-  ( ( G e. Grp /\ A e. X /\ B e. X ) -> ( A .+ B ) e. X )
10 6 7 8 9 syl3anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( A .+ B ) e. X )
11 2 1 odcl 
 |-  ( ( A .+ B ) e. X -> ( O ` ( A .+ B ) ) e. NN0 )
12 10 11 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( O ` ( A .+ B ) ) e. NN0 )
13 2 1 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
14 7 13 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( O ` A ) e. NN0 )
15 2 1 odcl 
 |-  ( B e. X -> ( O ` B ) e. NN0 )
16 8 15 syl 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( O ` B ) e. NN0 )
17 14 16 nn0mulcld 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` A ) x. ( O ` B ) ) e. NN0 )
18 simpr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` A ) gcd ( O ` B ) ) = 1 )
19 18 oveq2d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) = ( ( O ` ( A .+ B ) ) x. 1 ) )
20 12 nn0cnd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( O ` ( A .+ B ) ) e. CC )
21 20 mulridd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` ( A .+ B ) ) x. 1 ) = ( O ` ( A .+ B ) ) )
22 19 21 eqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) = ( O ` ( A .+ B ) ) )
23 1 2 3 odadd1 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` A ) x. ( O ` B ) ) )
24 23 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` ( A .+ B ) ) x. ( ( O ` A ) gcd ( O ` B ) ) ) || ( ( O ` A ) x. ( O ` B ) ) )
25 22 24 eqbrtrrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( O ` ( A .+ B ) ) || ( ( O ` A ) x. ( O ` B ) ) )
26 1 2 3 odadd2 
 |-  ( ( G e. Abel /\ A e. X /\ B e. X ) -> ( ( O ` A ) x. ( O ` B ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) )
27 26 adantr 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` A ) x. ( O ` B ) ) || ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) )
28 18 oveq1d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) = ( 1 ^ 2 ) )
29 sq1 
 |-  ( 1 ^ 2 ) = 1
30 28 29 eqtrdi 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) = 1 )
31 30 oveq2d 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) = ( ( O ` ( A .+ B ) ) x. 1 ) )
32 31 21 eqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` ( A .+ B ) ) x. ( ( ( O ` A ) gcd ( O ` B ) ) ^ 2 ) ) = ( O ` ( A .+ B ) ) )
33 27 32 breqtrd 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( ( O ` A ) x. ( O ` B ) ) || ( O ` ( A .+ B ) ) )
34 dvdseq 
 |-  ( ( ( ( O ` ( A .+ B ) ) e. NN0 /\ ( ( O ` A ) x. ( O ` B ) ) e. NN0 ) /\ ( ( O ` ( A .+ B ) ) || ( ( O ` A ) x. ( O ` B ) ) /\ ( ( O ` A ) x. ( O ` B ) ) || ( O ` ( A .+ B ) ) ) ) -> ( O ` ( A .+ B ) ) = ( ( O ` A ) x. ( O ` B ) ) )
35 12 17 25 33 34 syl22anc 
 |-  ( ( ( G e. Abel /\ A e. X /\ B e. X ) /\ ( ( O ` A ) gcd ( O ` B ) ) = 1 ) -> ( O ` ( A .+ B ) ) = ( ( O ` A ) x. ( O ` B ) ) )