Theorem uptoss ≪ | index | src | ≫

theorem uptoss (a b: nat): $ upto a C_ upto b <-> a <= b $;

Step	Hyp	Ref	Expression
1		ltirr	~b < b
2		ltnle	b < a <-> ~a <= b
3		elupto	b e. upto a <-> b < a
4		elupto	b e. upto b <-> b < b
5	3, 4	imeqi	b e. upto a -> b e. upto b <-> b < a -> b < b
6		ssel	upto a C_ upto b -> b e. upto a -> b e. upto b
7	5, 6	sylib	upto a C_ upto b -> b < a -> b < b
8	2, 7	syl5bir	upto a C_ upto b -> ~a <= b -> b < b
9	8	con1d	upto a C_ upto b -> ~b < b -> a <= b
10	1, 9	mpi	upto a C_ upto b -> a <= b
11		elupto	x e. upto a <-> x < a
12		elupto	x e. upto b <-> x < b
13	11, 12	imeqi	x e. upto a -> x e. upto b <-> x < a -> x < b
14		ltletr	x < a -> a <= b -> x < b
15	14	com12	a <= b -> x < a -> x < b
16	13, 15	sylibr	a <= b -> x e. upto a -> x e. upto b
17	16	iald	a <= b -> A. x (x e. upto a -> x e. upto b)
18	17	conv subset	a <= b -> upto a C_ upto b
19	10, 18	ibii	upto a C_ upto b <-> a <= b

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)