Theorem mulinvmlem ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		muleq2	x = invm a n -> a * x = a * invm a n
2	1	eqmeq2d	x = invm a n -> (mod(n): a * x = 1 <-> mod(n): a * invm a n = 1)
3	2	elabe	invm a n e. {x \| mod(n): a * x = 1} <-> mod(n): a * invm a n = 1
4		leastel	b e. {x \| mod(n): a * x = 1} -> least {x \| mod(n): a * x = 1} e. {x \| mod(n): a * x = 1}
5	4	conv invm	b e. {x \| mod(n): a * x = 1} -> invm a n e. {x \| mod(n): a * x = 1}
6		muleq2	x = b -> a * x = a * b
7	6	eqmeq2d	x = b -> (mod(n): a * x = 1 <-> mod(n): a * b = 1)
8	7	elabe	b e. {x \| mod(n): a * x = 1} <-> mod(n): a * b = 1
9		hyp h	G -> mod(n): a * b = 1
10	8, 9	sylibr	G -> b e. {x \| mod(n): a * x = 1}
11	5, 10	syl	G -> invm a n e. {x \| mod(n): a * x = 1}
12	3, 11	sylib	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)