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 𝑂 = ( od ‘ 𝐺 )
odadd1.2 𝑋 = ( Base ‘ 𝐺 )
odadd1.3 + = ( +g𝐺 )
Assertion odadd ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 odadd1.1 𝑂 = ( od ‘ 𝐺 )
2 odadd1.2 𝑋 = ( Base ‘ 𝐺 )
3 odadd1.3 + = ( +g𝐺 )
4 simpl1 ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → 𝐺 ∈ Abel )
5 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
6 4 5 syl ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → 𝐺 ∈ Grp )
7 simpl2 ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → 𝐴𝑋 )
8 simpl3 ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → 𝐵𝑋 )
9 2 3 grpcl ( ( 𝐺 ∈ Grp ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
10 6 7 8 9 syl3anc ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( 𝐴 + 𝐵 ) ∈ 𝑋 )
11 2 1 odcl ( ( 𝐴 + 𝐵 ) ∈ 𝑋 → ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) ∈ ℕ0 )
12 10 11 syl ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) ∈ ℕ0 )
13 2 1 odcl ( 𝐴𝑋 → ( 𝑂𝐴 ) ∈ ℕ0 )
14 7 13 syl ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( 𝑂𝐴 ) ∈ ℕ0 )
15 2 1 odcl ( 𝐵𝑋 → ( 𝑂𝐵 ) ∈ ℕ0 )
16 8 15 syl ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( 𝑂𝐵 ) ∈ ℕ0 )
17 14 16 nn0mulcld ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) ∈ ℕ0 )
18 simpr ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 )
19 18 oveq2d ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ) = ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · 1 ) )
20 12 nn0cnd ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) ∈ ℂ )
21 20 mulid1d ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · 1 ) = ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) )
22 19 21 eqtrd ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ) = ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) )
23 1 2 3 odadd1 ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ) ∥ ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) )
24 23 adantr ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ) ∥ ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) )
25 22 24 eqbrtrrd ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) ∥ ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) )
26 1 2 3 odadd2 ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) ∥ ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ↑ 2 ) ) )
27 26 adantr ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) ∥ ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ↑ 2 ) ) )
28 18 oveq1d ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
29 sq1 ( 1 ↑ 2 ) = 1
30 28 29 eqtrdi ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ↑ 2 ) = 1 )
31 30 oveq2d ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ↑ 2 ) ) = ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · 1 ) )
32 31 21 eqtrd ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) · ( ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) ↑ 2 ) ) = ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) )
33 27 32 breqtrd ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) ∥ ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) )
34 dvdseq ( ( ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) ∈ ℕ0 ∧ ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) ∈ ℕ0 ) ∧ ( ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) ∥ ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) ∧ ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) ∥ ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) ) ) → ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) )
35 12 17 25 33 34 syl22anc ( ( ( 𝐺 ∈ Abel ∧ 𝐴𝑋𝐵𝑋 ) ∧ ( ( 𝑂𝐴 ) gcd ( 𝑂𝐵 ) ) = 1 ) → ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝑂𝐴 ) · ( 𝑂𝐵 ) ) )