Theorem uptolem ≪ | index | src | ≫ 

theorem uptolem (a n: nat):
  $ shr (upto n) a = upto (n - a) /\ upto n % 2 ^ a = upto (min n a) $;
StepHypRefExpression
1 subltid 
0 < 2 ^ min n a /\ 0 < 1 -> 2 ^ min n a - 1 < 2 ^ min n a
2 1 conv upto 
0 < 2 ^ min n a /\ 0 < 1 -> upto (min n a) < 2 ^ min n a
3 ian 
0 < 2 ^ min n a -> 0 < 1 -> 0 < 2 ^ min n a /\ 0 < 1
4 powpos 
0 < 2 -> 0 < 2 ^ min n a
5 d0lt2 
0 < 2
6 4, 5 ax_mp 
0 < 2 ^ min n a
7 3, 6 ax_mp 
0 < 1 -> 0 < 2 ^ min n a /\ 0 < 1
8 d0lt1 
0 < 1
9 7, 8 ax_mp 
0 < 2 ^ min n a /\ 0 < 1
10 2, 9 ax_mp 
upto (min n a) < 2 ^ min n a
11 10 a1i 
T. -> upto (min n a) < 2 ^ min n a
12 lepow2a 
2 != 0 -> min n a <= a -> 2 ^ min n a <= 2 ^ a
13 d2ne0 
2 != 0
14 12, 13 ax_mp 
min n a <= a -> 2 ^ min n a <= 2 ^ a
15 minle2 
min n a <= a
16 14, 15 ax_mp 
2 ^ min n a <= 2 ^ a
17 16 a1i 
T. -> 2 ^ min n a <= 2 ^ a
18 11, 17 ltletrd 
T. -> upto (min n a) < 2 ^ a
19 addcan1 
2 ^ a * upto (n - a) + upto (min n a) + 1 = upto n + 1 <-> 2 ^ a * upto (n - a) + upto (min n a) = upto n
20 eqtr 
2 ^ a * upto (n - a) + upto (min n a) + 1 = 2 ^ a * upto (n - a) + (upto (min n a) + 1) ->
  2 ^ a * upto (n - a) + (upto (min n a) + 1) = upto n + 1 ->
  2 ^ a * upto (n - a) + upto (min n a) + 1 = upto n + 1
21 addass 
2 ^ a * upto (n - a) + upto (min n a) + 1 = 2 ^ a * upto (n - a) + (upto (min n a) + 1)
22 20, 21 ax_mp 
2 ^ a * upto (n - a) + (upto (min n a) + 1) = upto n + 1 -> 2 ^ a * upto (n - a) + upto (min n a) + 1 = upto n + 1
23 eqtr4 
2 ^ a * upto (n - a) + (upto (min n a) + 1) = 2 ^ a * upto (n - a) + 2 ^ min n a ->
  upto n + 1 = 2 ^ a * upto (n - a) + 2 ^ min n a ->
  2 ^ a * upto (n - a) + (upto (min n a) + 1) = upto n + 1
24 addeq2 
upto (min n a) + 1 = 2 ^ min n a -> 2 ^ a * upto (n - a) + (upto (min n a) + 1) = 2 ^ a * upto (n - a) + 2 ^ min n a
25 uptoadd1 
upto (min n a) + 1 = 2 ^ min n a
26 24, 25 ax_mp 
2 ^ a * upto (n - a) + (upto (min n a) + 1) = 2 ^ a * upto (n - a) + 2 ^ min n a
27 23, 26 ax_mp 
upto n + 1 = 2 ^ a * upto (n - a) + 2 ^ min n a -> 2 ^ a * upto (n - a) + (upto (min n a) + 1) = upto n + 1
28 eqtr4 
upto n + 1 = 2 ^ n -> 2 ^ a * upto (n - a) + 2 ^ min n a = 2 ^ n -> upto n + 1 = 2 ^ a * upto (n - a) + 2 ^ min n a
29 uptoadd1 
upto n + 1 = 2 ^ n
30 28, 29 ax_mp 
2 ^ a * upto (n - a) + 2 ^ min n a = 2 ^ n -> upto n + 1 = 2 ^ a * upto (n - a) + 2 ^ min n a
31 eqtr3 
2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ a * upto (n - a) + 2 ^ min n a ->
  2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ n ->
  2 ^ a * upto (n - a) + 2 ^ min n a = 2 ^ n
32 addeq 
2 ^ min n a * upto (n - a) = 2 ^ a * upto (n - a) ->
  2 ^ min n a * 1 = 2 ^ min n a ->
  2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ a * upto (n - a) + 2 ^ min n a
33 eqmin2 
a <= n -> min n a = a
34 33 poweq2d 
a <= n -> 2 ^ min n a = 2 ^ a
35 34 muleq1d 
a <= n -> 2 ^ min n a * upto (n - a) = 2 ^ a * upto (n - a)
36 mul0 
2 ^ min n a * 0 = 0
37 muleq2 
upto (n - a) = 0 -> 2 ^ min n a * upto (n - a) = 2 ^ min n a * 0
38 36, 37 syl6eq 
upto (n - a) = 0 -> 2 ^ min n a * upto (n - a) = 0
39 mul0 
2 ^ a * 0 = 0
40 muleq2 
upto (n - a) = 0 -> 2 ^ a * upto (n - a) = 2 ^ a * 0
41 39, 40 syl6eq 
upto (n - a) = 0 -> 2 ^ a * upto (n - a) = 0
42 38, 41 eqtr4d 
upto (n - a) = 0 -> 2 ^ min n a * upto (n - a) = 2 ^ a * upto (n - a)
43 upto0 
upto 0 = 0
44 nlesubeq0 
~a <= n -> n - a = 0
45 44 uptoeqd 
~a <= n -> upto (n - a) = upto 0
46 43, 45 syl6eq 
~a <= n -> upto (n - a) = 0
47 42, 46 syl 
~a <= n -> 2 ^ min n a * upto (n - a) = 2 ^ a * upto (n - a)
48 35, 47 cases 
2 ^ min n a * upto (n - a) = 2 ^ a * upto (n - a)
49 32, 48 ax_mp 
2 ^ min n a * 1 = 2 ^ min n a -> 2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ a * upto (n - a) + 2 ^ min n a
50 mul12 
2 ^ min n a * 1 = 2 ^ min n a
51 49, 50 ax_mp 
2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ a * upto (n - a) + 2 ^ min n a
52 31, 51 ax_mp 
2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ n -> 2 ^ a * upto (n - a) + 2 ^ min n a = 2 ^ n
53 eqtr3 
2 ^ min n a * (upto (n - a) + 1) = 2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 ->
  2 ^ min n a * (upto (n - a) + 1) = 2 ^ n ->
  2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ n
54 muladd 
2 ^ min n a * (upto (n - a) + 1) = 2 ^ min n a * upto (n - a) + 2 ^ min n a * 1
55 53, 54 ax_mp 
2 ^ min n a * (upto (n - a) + 1) = 2 ^ n -> 2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ n
56 eqtr 
2 ^ min n a * (upto (n - a) + 1) = 2 ^ min n a * 2 ^ (n - a) -> 2 ^ min n a * 2 ^ (n - a) = 2 ^ n -> 2 ^ min n a * (upto (n - a) + 1) = 2 ^ n
57 muleq2 
upto (n - a) + 1 = 2 ^ (n - a) -> 2 ^ min n a * (upto (n - a) + 1) = 2 ^ min n a * 2 ^ (n - a)
58 uptoadd1 
upto (n - a) + 1 = 2 ^ (n - a)
59 57, 58 ax_mp 
2 ^ min n a * (upto (n - a) + 1) = 2 ^ min n a * 2 ^ (n - a)
60 56, 59 ax_mp 
2 ^ min n a * 2 ^ (n - a) = 2 ^ n -> 2 ^ min n a * (upto (n - a) + 1) = 2 ^ n
61 eqtr3 
2 ^ (min n a + (n - a)) = 2 ^ min n a * 2 ^ (n - a) -> 2 ^ (min n a + (n - a)) = 2 ^ n -> 2 ^ min n a * 2 ^ (n - a) = 2 ^ n
62 powadd 
2 ^ (min n a + (n - a)) = 2 ^ min n a * 2 ^ (n - a)
63 61, 62 ax_mp 
2 ^ (min n a + (n - a)) = 2 ^ n -> 2 ^ min n a * 2 ^ (n - a) = 2 ^ n
64 poweq2 
min n a + (n - a) = n -> 2 ^ (min n a + (n - a)) = 2 ^ n
65 minaddsub 
min n a + (n - a) = n
66 64, 65 ax_mp 
2 ^ (min n a + (n - a)) = 2 ^ n
67 63, 66 ax_mp 
2 ^ min n a * 2 ^ (n - a) = 2 ^ n
68 60, 67 ax_mp 
2 ^ min n a * (upto (n - a) + 1) = 2 ^ n
69 55, 68 ax_mp 
2 ^ min n a * upto (n - a) + 2 ^ min n a * 1 = 2 ^ n
70 52, 69 ax_mp 
2 ^ a * upto (n - a) + 2 ^ min n a = 2 ^ n
71 30, 70 ax_mp 
upto n + 1 = 2 ^ a * upto (n - a) + 2 ^ min n a
72 27, 71 ax_mp 
2 ^ a * upto (n - a) + (upto (min n a) + 1) = upto n + 1
73 22, 72 ax_mp 
2 ^ a * upto (n - a) + upto (min n a) + 1 = upto n + 1
74 19, 73 mpbi 
2 ^ a * upto (n - a) + upto (min n a) = upto n
75 74 a1i 
T. -> 2 ^ a * upto (n - a) + upto (min n a) = upto n
76 18, 75 eqdivmod 
T. -> upto n // 2 ^ a = upto (n - a) /\ upto n % 2 ^ a = upto (min n a)
77 76 conv shr 
T. -> shr (upto n) a = upto (n - a) /\ upto n % 2 ^ a = upto (min n a)
78 77 trud 
shr (upto n) a = upto (n - a) /\ upto n % 2 ^ a = upto (min n 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)