This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odmulg

Description: Relationship between the order of an element and that of a multiple. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
Assertion odmulg ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
4 1 3 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
5 4 3com23 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
6 1 2 odcl ⊢ ( ( 𝑁 · 𝐴 ) ∈ 𝑋 → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℕ0 )
7 5 6 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℕ0 )
8 7 nn0cnd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℂ )
9 8 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℂ )
10 9 mul02d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 ) → ( 0 · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) = 0 )
11 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 )
12 11 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) = ( 0 · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )
13 simp3 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
14 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
15 14 3ad2ant2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
16 15 nn0zd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
17 gcdeq0 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 ↔ ( 𝑁 = 0 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ) )
18 13 16 17 syl2anc ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 ↔ ( 𝑁 = 0 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) ) )
19 18 simplbda ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 ) → ( 𝑂 ‘ 𝐴 ) = 0 )
20 10 12 19 3eqtr4rd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 0 ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )
21 simpll3 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
22 16 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
23 gcddvds ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑁 ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) ) )
24 21 22 23 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑁 ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) ) )
25 24 simprd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) )
26 13 16 gcdcld ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
27 26 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℕ0 )
28 27 nn0zd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℤ )
29 28 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℤ )
30 nn0z ⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
31 30 adantl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑥 ∈ ℤ )
32 dvdstr ⊢ ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) ∧ ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 ) )
33 29 22 31 32 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ ( 𝑂 ‘ 𝐴 ) ∧ ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 ) )
34 25 33 mpand ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 ) )
35 7 nn0zd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℤ )
36 35 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℤ )
37 muldvds1 ⊢ ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℤ ∧ ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 ) )
38 29 36 31 37 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 ) )
39 dvdszrcl ⊢ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) )
40 divides ⊢ ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 ↔ ∃ 𝑦 ∈ ℤ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = 𝑥 ) )
41 39 40 syl ⊢ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 ↔ ∃ 𝑦 ∈ ℤ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = 𝑥 ) )
42 41 ibi ⊢ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 → ∃ 𝑦 ∈ ℤ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = 𝑥 )
43 35 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℤ )
44 simprr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
45 28 adantrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℤ )
46 simprl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 )
47 dvdscmulr ⊢ ( ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℤ ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ) → ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝑦 ) ↔ ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝑦 ) )
48 43 44 45 46 47 syl112anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝑦 ) ↔ ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝑦 ) )
49 1 2 3 odmulgid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝑦 ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · 𝑁 ) ) )
50 49 adantrl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∥ 𝑦 ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · 𝑁 ) ) )
51 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
52 dvdsmulgcd ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · 𝑁 ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ) )
53 44 51 52 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · 𝑁 ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ) )
54 48 50 53 3bitrrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝑦 ) ) )
55 45 zcnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∈ ℂ )
56 44 zcnd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℂ )
57 55 56 mulcomd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝑦 ) = ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) )
58 57 breq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝑦 ) ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ) )
59 54 58 bitrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ) )
60 59 anassrs ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑦 ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ) )
61 breq2 ⊢ ( ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = 𝑥 → ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ↔ ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ) )
62 breq2 ⊢ ( ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = 𝑥 → ( ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) )
63 61 62 bibi12d ⊢ ( ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = 𝑥 → ( ( ( 𝑂 ‘ 𝐴 ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) ) ↔ ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) ) )
64 60 63 syl5ibcom ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = 𝑥 → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) ) )
65 64 rexlimdva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( ∃ 𝑦 ∈ ℤ ( 𝑦 · ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ) = 𝑥 → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) ) )
66 42 65 syl5 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) ) )
67 66 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ∥ 𝑥 → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) ) )
68 34 38 67 pm5.21ndd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) )
69 68 ralrimiva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ∀ 𝑥 ∈ ℕ0 ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) )
70 15 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
71 7 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ∈ ℕ0 )
72 27 71 nn0mulcld ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∈ ℕ0 )
73 dvdsext ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 ∧ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∈ ℕ0 ) → ( ( 𝑂 ‘ 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) ) )
74 70 72 73 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( ( 𝑂 ‘ 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ↔ ∀ 𝑥 ∈ ℕ0 ( ( 𝑂 ‘ 𝐴 ) ∥ 𝑥 ↔ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) ∥ 𝑥 ) ) )
75 69 74 mpbird ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) ≠ 0 ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )
76 20 75 pm2.61dane ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )