Theorem elupto ≪ | index | src | ≫

pub theorem elupto (k n: nat): $ k e. upto n <-> k < n $;

Step	Hyp	Ref	Expression
1		bitr	(k e. upto n <-> odd (shr (upto n) k)) -> (odd (shr (upto n) k) <-> k < n) -> (k e. upto n <-> k < n)
2		elnel	k e. upto n <-> odd (shr (upto n) k)
3	1, 2	ax_mp	(odd (shr (upto n) k) <-> k < n) -> (k e. upto n <-> k < n)
4		bitr	(odd (shr (upto n) k) <-> odd (upto (n - k))) -> (odd (upto (n - k)) <-> k < n) -> (odd (shr (upto n) k) <-> k < n)
5		oddeq	shr (upto n) k = upto (n - k) -> (odd (shr (upto n) k) <-> odd (upto (n - k)))
6		shrupto	shr (upto n) k = upto (n - k)
7	5, 6	ax_mp	odd (shr (upto n) k) <-> odd (upto (n - k))
8	4, 7	ax_mp	(odd (upto (n - k)) <-> k < n) -> (odd (shr (upto n) k) <-> k < n)
9		bitr4	(odd (upto (n - k)) <-> ~n - k = 0) -> (k < n <-> ~n - k = 0) -> (odd (upto (n - k)) <-> k < n)
10		odd0	~odd 0
11	10	a1i	odd (upto (n - k)) -> ~odd 0
12		upto0	upto 0 = 0
13		uptoeq	n - k = 0 -> upto (n - k) = upto 0
14	12, 13	syl6eq	n - k = 0 -> upto (n - k) = 0
15	14	oddeqd	n - k = 0 -> (odd (upto (n - k)) <-> odd 0)
16	15	bi1d	n - k = 0 -> odd (upto (n - k)) -> odd 0
17	16	com12	odd (upto (n - k)) -> n - k = 0 -> odd 0
18	11, 17	mtd	odd (upto (n - k)) -> ~n - k = 0
19		b1odd	odd (b1 (upto (n - k - 1)))
20		uptoS	upto (suc (n - k - 1)) = b1 (upto (n - k - 1))
21		sub1can	n - k != 0 -> suc (n - k - 1) = n - k
22	21	conv ne	~n - k = 0 -> suc (n - k - 1) = n - k
23	22	uptoeqd	~n - k = 0 -> upto (suc (n - k - 1)) = upto (n - k)
24	20, 23	syl5eqr	~n - k = 0 -> b1 (upto (n - k - 1)) = upto (n - k)
25	24	oddeqd	~n - k = 0 -> (odd (b1 (upto (n - k - 1))) <-> odd (upto (n - k)))
26	19, 25	mpbii	~n - k = 0 -> odd (upto (n - k))
27	18, 26	ibii	odd (upto (n - k)) <-> ~n - k = 0
28	9, 27	ax_mp	(k < n <-> ~n - k = 0) -> (odd (upto (n - k)) <-> k < n)
29		bitr	(k < n <-> 0 < n - k) -> (0 < n - k <-> ~n - k = 0) -> (k < n <-> ~n - k = 0)
30		subpos	k < n <-> 0 < n - k
31	29, 30	ax_mp	(0 < n - k <-> ~n - k = 0) -> (k < n <-> ~n - k = 0)
32		lt01	0 < n - k <-> n - k != 0
33	32	conv ne	0 < n - k <-> ~n - k = 0
34	31, 33	ax_mp	k < n <-> ~n - k = 0
35	28, 34	ax_mp	odd (upto (n - k)) <-> k < n
36	8, 35	ax_mp	odd (shr (upto n) k) <-> k < n
37	3, 36	ax_mp	k e. upto n <-> k < 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)