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 mulridd ⊢ ( ( ( 𝐺 ∈ 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 ) → ( 𝑂 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝑂 ‘ 𝐴 ) · ( 𝑂 ‘ 𝐵 ) ) )