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 X = Base G
odmulgid.2 O = od G
odmulgid.3 · ˙ = G
Assertion odbezout G Grp A X N N gcd O A = 1 x x · ˙ N · ˙ A = A

Proof

Step Hyp Ref Expression
1 odmulgid.1 X = Base G
2 odmulgid.2 O = od G
3 odmulgid.3 · ˙ = G
4 simpl3 G Grp A X N N gcd O A = 1 N
5 simpl2 G Grp A X N N gcd O A = 1 A X
6 1 2 odcl A X O A 0
7 5 6 syl G Grp A X N N gcd O A = 1 O A 0
8 7 nn0zd G Grp A X N N gcd O A = 1 O A
9 bezout N O A x y N gcd O A = N x + O A y
10 4 8 9 syl2anc G Grp A X N N gcd O A = 1 x y N gcd O A = N x + O A y
11 oveq1 N x + O A y = N gcd O A N x + O A y · ˙ A = N gcd O A · ˙ A
12 11 eqcoms N gcd O A = N x + O A y N x + O A y · ˙ A = N gcd O A · ˙ A
13 simpll1 G Grp A X N N gcd O A = 1 x y G Grp
14 4 adantr G Grp A X N N gcd O A = 1 x y N
15 simprl G Grp A X N N gcd O A = 1 x y x
16 14 15 zmulcld G Grp A X N N gcd O A = 1 x y N x
17 5 adantr G Grp A X N N gcd O A = 1 x y A X
18 17 6 syl G Grp A X N N gcd O A = 1 x y O A 0
19 18 nn0zd G Grp A X N N gcd O A = 1 x y O A
20 simprr G Grp A X N N gcd O A = 1 x y y
21 19 20 zmulcld G Grp A X N N gcd O A = 1 x y O A y
22 eqid + G = + G
23 1 3 22 mulgdir G Grp N x O A y A X N x + O A y · ˙ A = N x · ˙ A + G O A y · ˙ A
24 13 16 21 17 23 syl13anc G Grp A X N N gcd O A = 1 x y N x + O A y · ˙ A = N x · ˙ A + G O A y · ˙ A
25 14 zcnd G Grp A X N N gcd O A = 1 x y N
26 15 zcnd G Grp A X N N gcd O A = 1 x y x
27 25 26 mulcomd G Grp A X N N gcd O A = 1 x y N x = x N
28 27 oveq1d G Grp A X N N gcd O A = 1 x y N x · ˙ A = x N · ˙ A
29 1 3 mulgass G Grp x N A X x N · ˙ A = x · ˙ N · ˙ A
30 13 15 14 17 29 syl13anc G Grp A X N N gcd O A = 1 x y x N · ˙ A = x · ˙ N · ˙ A
31 28 30 eqtrd G Grp A X N N gcd O A = 1 x y N x · ˙ A = x · ˙ N · ˙ A
32 dvdsmul1 O A y O A O A y
33 19 20 32 syl2anc G Grp A X N N gcd O A = 1 x y O A O A y
34 eqid 0 G = 0 G
35 1 2 3 34 oddvds G Grp A X O A y O A O A y O A y · ˙ A = 0 G
36 13 17 21 35 syl3anc G Grp A X N N gcd O A = 1 x y O A O A y O A y · ˙ A = 0 G
37 33 36 mpbid G Grp A X N N gcd O A = 1 x y O A y · ˙ A = 0 G
38 31 37 oveq12d G Grp A X N N gcd O A = 1 x y N x · ˙ A + G O A y · ˙ A = x · ˙ N · ˙ A + G 0 G
39 1 3 mulgcl G Grp N A X N · ˙ A X
40 13 14 17 39 syl3anc G Grp A X N N gcd O A = 1 x y N · ˙ A X
41 1 3 mulgcl G Grp x N · ˙ A X x · ˙ N · ˙ A X
42 13 15 40 41 syl3anc G Grp A X N N gcd O A = 1 x y x · ˙ N · ˙ A X
43 1 22 34 grprid G Grp x · ˙ N · ˙ A X x · ˙ N · ˙ A + G 0 G = x · ˙ N · ˙ A
44 13 42 43 syl2anc G Grp A X N N gcd O A = 1 x y x · ˙ N · ˙ A + G 0 G = x · ˙ N · ˙ A
45 38 44 eqtrd G Grp A X N N gcd O A = 1 x y N x · ˙ A + G O A y · ˙ A = x · ˙ N · ˙ A
46 24 45 eqtrd G Grp A X N N gcd O A = 1 x y N x + O A y · ˙ A = x · ˙ N · ˙ A
47 simplr G Grp A X N N gcd O A = 1 x y N gcd O A = 1
48 47 oveq1d G Grp A X N N gcd O A = 1 x y N gcd O A · ˙ A = 1 · ˙ A
49 1 3 mulg1 A X 1 · ˙ A = A
50 17 49 syl G Grp A X N N gcd O A = 1 x y 1 · ˙ A = A
51 48 50 eqtrd G Grp A X N N gcd O A = 1 x y N gcd O A · ˙ A = A
52 46 51 eqeq12d G Grp A X N N gcd O A = 1 x y N x + O A y · ˙ A = N gcd O A · ˙ A x · ˙ N · ˙ A = A
53 12 52 syl5ib G Grp A X N N gcd O A = 1 x y N gcd O A = N x + O A y x · ˙ N · ˙ A = A
54 53 anassrs G Grp A X N N gcd O A = 1 x y N gcd O A = N x + O A y x · ˙ N · ˙ A = A
55 54 rexlimdva G Grp A X N N gcd O A = 1 x y N gcd O A = N x + O A y x · ˙ N · ˙ A = A
56 55 reximdva G Grp A X N N gcd O A = 1 x y N gcd O A = N x + O A y x x · ˙ N · ˙ A = A
57 10 56 mpd G Grp A X N N gcd O A = 1 x x · ˙ N · ˙ A = A