Theorem mulmod1 ≪ | index | src | ≫

theorem mulmod1 (a b: nat): $ b * a % b = 0 $;

Step	Hyp	Ref	Expression
1		modeq2	b = 0 -> b * a % b = b * a % 0
2		mod0	b * a % 0 = b * a
3		mul01	0 * a = 0
4		muleq1	b = 0 -> b * a = 0 * a
5	3, 4	syl6eq	b = 0 -> b * a = 0
6	2, 5	syl5eq	b = 0 -> b * a % 0 = 0
7	1, 6	eqtrd	b = 0 -> b * a % b = 0
8		bi2	(0 < b <-> ~b = 0) -> ~b = 0 -> 0 < b
9		lt01	0 < b <-> b != 0
10	9	conv ne	0 < b <-> ~b = 0
11	8, 10	ax_mp	~b = 0 -> 0 < b
12		add0	b * a + 0 = b * a
13	12	a1i	~b = 0 -> b * a + 0 = b * a
14	11, 13	eqdivmod	~b = 0 -> b * a // b = a /\ b * a % b = 0
15	14	anrd	~b = 0 -> b * a % b = 0
16	7, 15	cases	b * a % b = 0

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)