Theorem mulinvm ≪ | index | src | ≫

theorem mulinvm (G: wff) (a n: nat):
  $ G -> coprime a n $ >
  $ G -> mod(n): a * invm a n = 1 $;

Step	Hyp	Ref	Expression
1		eqm11	mod(1): a * invm a n = 1
2		gcd01	gcd 0 n = n
3		gcdeq1	a = 0 -> gcd a n = gcd 0 n
4	3	anwr	G /\ a = 0 -> gcd a n = gcd 0 n
5	2, 4	syl6eq	G /\ a = 0 -> gcd a n = n
6		hyp h	G -> coprime a n
7	6	conv coprime	G -> gcd a n = 1
8	7	anwl	G /\ a = 0 -> gcd a n = 1
9	5, 8	eqtr3d	G /\ a = 0 -> n = 1
10	9	eqmeq1d	G /\ a = 0 -> (mod(n): a * invm a n = 1 <-> mod(1): a * invm a n = 1)
11	1, 10	mpbiri	G /\ a = 0 -> mod(n): a * invm a n = 1
12		eqeqm	a * 1 = 1 -> mod(n): a * 1 = 1
13		mul12	a * 1 = a
14		gcd02	gcd a 0 = a
15		gcdeq2	n = 0 -> gcd a n = gcd a 0
16	15	anwr	G /\ ~a = 0 /\ n = 0 -> gcd a n = gcd a 0
17	14, 16	syl6eq	G /\ ~a = 0 /\ n = 0 -> gcd a n = a
18	7	anwll	G /\ ~a = 0 /\ n = 0 -> gcd a n = 1
19	17, 18	eqtr3d	G /\ ~a = 0 /\ n = 0 -> a = 1
20	13, 19	syl5eq	G /\ ~a = 0 /\ n = 0 -> a * 1 = 1
21	12, 20	syl	G /\ ~a = 0 /\ n = 0 -> mod(n): a * 1 = 1
22	21	mulinvmlem	G /\ ~a = 0 /\ n = 0 -> mod(n): a * invm a n = 1
23	6	anwll	G /\ ~a = 0 /\ ~n = 0 -> coprime a n
24		anlr	G /\ ~a = 0 /\ ~n = 0 -> ~a = 0
25	24	conv ne	G /\ ~a = 0 /\ ~n = 0 -> a != 0
26	23, 25	copbezout	G /\ ~a = 0 /\ ~n = 0 -> E. x E. y x * a = y * n + 1
27		anr	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> x * a = y * n + 1
28		mulcom	x * a = a * x
29	28	a1i	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> x * a = a * x
30	27, 29	eqtr3d	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> y * n + 1 = a * x
31		add01	0 + 1 = 1
32	31	a1i	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> 0 + 1 = 1
33	30, 32	eqmeq23d	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> (mod(n): y * n + 1 = 0 + 1 <-> mod(n): a * x = 1)
34		eqm03	mod(n): y * n = 0 <-> n \|\| y * n
35		dvdmul1	n \|\| y * n
36	34, 35	mpbir	mod(n): y * n = 0
37	36	a1i	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> mod(n): y * n = 0
38	37	eqmadd1d	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> mod(n): y * n + 1 = 0 + 1
39	33, 38	mpbid	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> mod(n): a * x = 1
40	39	mulinvmlem	G /\ ~a = 0 /\ ~n = 0 /\ x * a = y * n + 1 -> mod(n): a * invm a n = 1
41	40	eexda	G /\ ~a = 0 /\ ~n = 0 -> E. y x * a = y * n + 1 -> mod(n): a * invm a n = 1
42	41	eexd	G /\ ~a = 0 /\ ~n = 0 -> E. x E. y x * a = y * n + 1 -> mod(n): a * invm a n = 1
43	26, 42	mpd	G /\ ~a = 0 /\ ~n = 0 -> mod(n): a * invm a n = 1
44	22, 43	casesda	G /\ ~a = 0 -> mod(n): a * invm a n = 1
45	11, 44	casesda	G -> mod(n): a * invm a n = 1

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)