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 syl5ib ( ( ( ( 𝐺 ∈ 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 ) → ∃ 𝑥 ∈ ℤ ( 𝑥 · ( 𝑁 · 𝐴 ) ) = 𝐴 )