Metamath Proof Explorer

Theorem odbezout

Description: If N is coprime to the order of A , there is a modular inverse x to cancel multiplication by N . (Contributed by Mario Carneiro, 27-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 odmulgid.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odmulgid.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odmulgid.3 ⊢ · = ( .g ‘ 𝐺 )
4 simpl3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) → 𝑁 ∈ ℤ )
5 simpl2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) → 𝐴 ∈ 𝑋 )
6 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
7 5 6 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
8 7 nn0zd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
9 bezout ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑂 ‘ 𝐴 ) ∈ ℤ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) )
10 4 8 9 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) )
11 oveq1 ⊢ ( ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) = ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) → ( ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) · 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
12 11 eqcoms ⊢ ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) → ( ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) · 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) )
13 simpll1 ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐺 ∈ Grp )
14 4 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
15 simprl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
16 14 15 zmulcld ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑁 · 𝑥 ) ∈ ℤ )
17 5 adantr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∈ 𝑋 )
18 17 6 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
19 18 nn0zd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
20 simprr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
21 19 20 zmulcld ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ∈ ℤ )
22 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
23 1 3 22 mulgdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑁 · 𝑥 ) ∈ ℤ ∧ ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) · 𝐴 ) = ( ( ( 𝑁 · 𝑥 ) · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) · 𝐴 ) ) )
24 13 16 21 17 23 syl13anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) · 𝐴 ) = ( ( ( 𝑁 · 𝑥 ) · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) · 𝐴 ) ) )
25 14 zcnd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑁 ∈ ℂ )
26 15 zcnd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℂ )
27 25 26 mulcomd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑁 · 𝑥 ) = ( 𝑥 · 𝑁 ) )
28 27 oveq1d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑁 · 𝑥 ) · 𝐴 ) = ( ( 𝑥 · 𝑁 ) · 𝐴 ) )
29 1 3 mulgass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑥 · 𝑁 ) · 𝐴 ) = ( 𝑥 · ( 𝑁 · 𝐴 ) ) )
30 13 15 14 17 29 syl13anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · 𝑁 ) · 𝐴 ) = ( 𝑥 · ( 𝑁 · 𝐴 ) ) )
31 28 30 eqtrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑁 · 𝑥 ) · 𝐴 ) = ( 𝑥 · ( 𝑁 · 𝐴 ) ) )
32 dvdsmul1 ⊢ ( ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) )
33 19 20 32 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) )
34 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
35 1 2 3 34 oddvds ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ∈ ℤ ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ↔ ( ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) ) )
36 13 17 21 35 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝐴 ) ∥ ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ↔ ( ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) ) )
37 33 36 mpbid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) )
38 31 37 oveq12d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑁 · 𝑥 ) · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) · 𝐴 ) ) = ( ( 𝑥 · ( 𝑁 · 𝐴 ) ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
39 1 3 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
40 13 14 17 39 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑁 · 𝐴 ) ∈ 𝑋 )
41 1 3 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ∧ ( 𝑁 · 𝐴 ) ∈ 𝑋 ) → ( 𝑥 · ( 𝑁 · 𝐴 ) ) ∈ 𝑋 )
42 13 15 40 41 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · ( 𝑁 · 𝐴 ) ) ∈ 𝑋 )
43 1 22 34 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 · ( 𝑁 · 𝐴 ) ) ∈ 𝑋 ) → ( ( 𝑥 · ( 𝑁 · 𝐴 ) ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 𝑥 · ( 𝑁 · 𝐴 ) ) )
44 13 42 43 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · ( 𝑁 · 𝐴 ) ) ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = ( 𝑥 · ( 𝑁 · 𝐴 ) ) )
45 38 44 eqtrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑁 · 𝑥 ) · 𝐴 ) ( +g ‘ 𝐺 ) ( ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) · 𝐴 ) ) = ( 𝑥 · ( 𝑁 · 𝐴 ) ) )
46 24 45 eqtrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) · 𝐴 ) = ( 𝑥 · ( 𝑁 · 𝐴 ) ) )
47 simplr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 )
48 47 oveq1d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = ( 1 · 𝐴 ) )
49 1 3 mulg1 ⊢ ( 𝐴 ∈ 𝑋 → ( 1 · 𝐴 ) = 𝐴 )
50 17 49 syl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 1 · 𝐴 ) = 𝐴 )
51 48 50 eqtrd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) = 𝐴 )
52 46 51 eqeq12d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) · 𝐴 ) = ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) · 𝐴 ) ↔ ( 𝑥 · ( 𝑁 · 𝐴 ) ) = 𝐴 ) )
53 12 52 imbitrid ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) → ( 𝑥 · ( 𝑁 · 𝐴 ) ) = 𝐴 ) )
54 53 anassrs ⊢ ( ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) → ( ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) → ( 𝑥 · ( 𝑁 · 𝐴 ) ) = 𝐴 ) )
55 54 rexlimdva ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( ∃ 𝑦 ∈ ℤ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) → ( 𝑥 · ( 𝑁 · 𝐴 ) ) = 𝐴 ) )
56 55 reximdva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = ( ( 𝑁 · 𝑥 ) + ( ( 𝑂 ‘ 𝐴 ) · 𝑦 ) ) → ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑁 · 𝐴 ) ) = 𝐴 ) )
57 10 56 mpd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 gcd ( 𝑂 ‘ 𝐴 ) ) = 1 ) → ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑁 · 𝐴 ) ) = 𝐴 )