Theorem lediv1 ≪ | index | src | ≫

theorem lediv1 (a b c: nat): $ a <= b -> a // c <= b // c $;

Step	Hyp	Ref	Expression
1		le01	0 <= b // c
2		div0	a // 0 = 0
3		diveq2	c = 0 -> a // c = a // 0
4	3	anwr	a <= b /\ c = 0 -> a // c = a // 0
5	2, 4	syl6eq	a <= b /\ c = 0 -> a // c = 0
6	5	leeq1d	a <= b /\ c = 0 -> (a // c <= b // c <-> 0 <= b // c)
7	1, 6	mpbiri	a <= b /\ c = 0 -> a // c <= b // c
8		modlt	c != 0 -> a % c < c
9	8	conv ne	~c = 0 -> a % c < c
10	9	anwr	a <= b /\ ~c = 0 -> a % c < c
11		modlt	c != 0 -> b % c < c
12	11	conv ne	~c = 0 -> b % c < c
13	12	anwr	a <= b /\ ~c = 0 -> b % c < c
14		leeq	c * (a // c) + a % c = a -> c * (b // c) + b % c = b -> (c * (a // c) + a % c <= c * (b // c) + b % c <-> a <= b)
15		divmod	c * (a // c) + a % c = a
16	14, 15	ax_mp	c * (b // c) + b % c = b -> (c * (a // c) + a % c <= c * (b // c) + b % c <-> a <= b)
17		divmod	c * (b // c) + b % c = b
18	16, 17	ax_mp	c * (a // c) + a % c <= c * (b // c) + b % c <-> a <= b
19		anl	a <= b /\ ~c = 0 -> a <= b
20	18, 19	sylibr	a <= b /\ ~c = 0 -> c * (a // c) + a % c <= c * (b // c) + b % c
21	10, 13, 20	divlem1	a <= b /\ ~c = 0 -> a // c <= b // c
22	7, 21	casesda	a <= b -> a // c <= b // c

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)