Theorem powerupto ≪ | index | src | ≫

theorem powerupto (a: nat): $ power (upto a) = upto (2 ^ a) $;

Step	Hyp	Ref	Expression
1		axext	power (upto a) == upto (2 ^ a) -> power (upto a) = upto (2 ^ a)
2		bitr4	(x e. power (upto a) <-> x C_ upto a) -> (x e. upto (2 ^ a) <-> x C_ upto a) -> (x e. power (upto a) <-> x e. upto (2 ^ a))
3		elpower	x e. power (upto a) <-> x C_ upto a
4	2, 3	ax_mp	(x e. upto (2 ^ a) <-> x C_ upto a) -> (x e. power (upto a) <-> x e. upto (2 ^ a))
5		bitr4	(x e. upto (2 ^ a) <-> x < 2 ^ a) -> (x C_ upto a <-> x < 2 ^ a) -> (x e. upto (2 ^ a) <-> x C_ upto a)
6		elupto	x e. upto (2 ^ a) <-> x < 2 ^ a
7	5, 6	ax_mp	(x C_ upto a <-> x < 2 ^ a) -> (x e. upto (2 ^ a) <-> x C_ upto a)
8		lteq2	suc (upto a) = 2 ^ a -> (x < suc (upto a) <-> x < 2 ^ a)
9		sucupto	suc (upto a) = 2 ^ a
10	8, 9	ax_mp	x < suc (upto a) <-> x < 2 ^ a
11		leltsuc	x <= upto a <-> x < suc (upto a)
12		ssle	x C_ upto a -> x <= upto a
13	11, 12	sylib	x C_ upto a -> x < suc (upto a)
14	10, 13	sylib	x C_ upto a -> x < 2 ^ a
15		shreq0	shr x a = 0 <-> x < 2 ^ a
16		elupto	y e. upto a <-> y < a
17		el02	~y - a e. 0
18		anll	shr x a = 0 /\ y e. x /\ ~y < a -> shr x a = 0
19	18	elneq2d	shr x a = 0 /\ y e. x /\ ~y < a -> (y - a e. shr x a <-> y - a e. 0)
20		elshr	y - a e. shr x a <-> y - a + a e. x
21		npcan	a <= y -> y - a + a = y
22		lenlt	a <= y <-> ~y < a
23		anr	shr x a = 0 /\ y e. x /\ ~y < a -> ~y < a
24	22, 23	sylibr	shr x a = 0 /\ y e. x /\ ~y < a -> a <= y
25	21, 24	syl	shr x a = 0 /\ y e. x /\ ~y < a -> y - a + a = y
26	25	eleq1d	shr x a = 0 /\ y e. x /\ ~y < a -> (y - a + a e. x <-> y e. x)
27		anlr	shr x a = 0 /\ y e. x /\ ~y < a -> y e. x
28	26, 27	mpbird	shr x a = 0 /\ y e. x /\ ~y < a -> y - a + a e. x
29	20, 28	sylibr	shr x a = 0 /\ y e. x /\ ~y < a -> y - a e. shr x a
30	19, 29	mpbid	shr x a = 0 /\ y e. x /\ ~y < a -> y - a e. 0
31	30	exp	shr x a = 0 /\ y e. x -> ~y < a -> y - a e. 0
32	31	con1d	shr x a = 0 /\ y e. x -> ~y - a e. 0 -> y < a
33	17, 32	mpi	shr x a = 0 /\ y e. x -> y < a
34	16, 33	sylibr	shr x a = 0 /\ y e. x -> y e. upto a
35	34	exp	shr x a = 0 -> y e. x -> y e. upto a
36	35	iald	shr x a = 0 -> A. y (y e. x -> y e. upto a)
37	36	conv subset	shr x a = 0 -> x C_ upto a
38	15, 37	sylbir	x < 2 ^ a -> x C_ upto a
39	14, 38	ibii	x C_ upto a <-> x < 2 ^ a
40	7, 39	ax_mp	x e. upto (2 ^ a) <-> x C_ upto a
41	4, 40	ax_mp	x e. power (upto a) <-> x e. upto (2 ^ a)
42	41	ax_gen	A. x (x e. power (upto a) <-> x e. upto (2 ^ a))
43	42	conv eqs	power (upto a) == upto (2 ^ a)
44	1, 43	ax_mp	power (upto a) = upto (2 ^ a)

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)