Theorem shlss ≪ | index | src | ≫

theorem shlss (a b n: nat): $ a C_ b <-> shl a n C_ shl b n $;

Step	Hyp	Ref	Expression
1		elshl	x e. shl a n <-> n <= x /\ x - n e. a
2		elshl	x e. shl b n <-> n <= x /\ x - n e. b
3		ssel	a C_ b -> x - n e. a -> x - n e. b
4	3	anim2d	a C_ b -> n <= x /\ x - n e. a -> n <= x /\ x - n e. b
5	2, 4	syl6ibr	a C_ b -> n <= x /\ x - n e. a -> x e. shl b n
6	1, 5	syl5bi	a C_ b -> x e. shl a n -> x e. shl b n
7	6	iald	a C_ b -> A. x (x e. shl a n -> x e. shl b n)
8	7	conv subset	a C_ b -> shl a n C_ shl b n
9		sseq	shr (shl a n) n == a -> shr (shl b n) n == b -> (shr (shl a n) n C_ shr (shl b n) n <-> a C_ b)
10		nseq	shr (shl a n) n = a -> shr (shl a n) n == a
11		shrshlid	shr (shl a n) n = a
12	10, 11	ax_mp	shr (shl a n) n == a
13	9, 12	ax_mp	shr (shl b n) n == b -> (shr (shl a n) n C_ shr (shl b n) n <-> a C_ b)
14		nseq	shr (shl b n) n = b -> shr (shl b n) n == b
15		shrshlid	shr (shl b n) n = b
16	14, 15	ax_mp	shr (shl b n) n == b
17	13, 16	ax_mp	shr (shl a n) n C_ shr (shl b n) n <-> a C_ b
18		shrss	shl a n C_ shl b n -> shr (shl a n) n C_ shr (shl b n) n
19	17, 18	sylib	shl a n C_ shl b n -> a C_ b
20	8, 19	ibii	a C_ b <-> shl a n C_ shl b n

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)