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 ( 𝑂 ‘ 𝐴 ) ) · ( 𝑂 ‘ ( 𝑁 · 𝐴 ) ) ) )