Theorem shlupto ≪ | index | src | ≫ 

theorem shlupto (a n: nat): $ shl (upto n) a + upto a = upto (n + a) $;
StepHypRefExpression
1 peano2 
suc (shl (upto n) a + upto a) = suc (upto (n + a)) <-> shl (upto n) a + upto a = upto (n + a)
2 eqtr3 
shl (upto n) a + suc (upto a) = suc (shl (upto n) a + upto a) ->
  shl (upto n) a + suc (upto a) = suc (upto (n + a)) ->
  suc (shl (upto n) a + upto a) = suc (upto (n + a))
3 addS2 
shl (upto n) a + suc (upto a) = suc (shl (upto n) a + upto a)
4 2, 3 ax_mp 
shl (upto n) a + suc (upto a) = suc (upto (n + a)) -> suc (shl (upto n) a + upto a) = suc (upto (n + a))
5 eqtr4 
shl (upto n) a + suc (upto a) = shl (upto n) a + 2 ^ a -> suc (upto (n + a)) = shl (upto n) a + 2 ^ a -> shl (upto n) a + suc (upto a) = suc (upto (n + a))
6 addeq2 
suc (upto a) = 2 ^ a -> shl (upto n) a + suc (upto a) = shl (upto n) a + 2 ^ a
7 sucupto 
suc (upto a) = 2 ^ a
8 6, 7 ax_mp 
shl (upto n) a + suc (upto a) = shl (upto n) a + 2 ^ a
9 5, 8 ax_mp 
suc (upto (n + a)) = shl (upto n) a + 2 ^ a -> shl (upto n) a + suc (upto a) = suc (upto (n + a))
10 eqtr4 
suc (upto (n + a)) = 2 ^ (n + a) -> shl (upto n) a + 2 ^ a = 2 ^ (n + a) -> suc (upto (n + a)) = shl (upto n) a + 2 ^ a
11 sucupto 
suc (upto (n + a)) = 2 ^ (n + a)
12 10, 11 ax_mp 
shl (upto n) a + 2 ^ a = 2 ^ (n + a) -> suc (upto (n + a)) = shl (upto n) a + 2 ^ a
13 eqtr3 
suc (upto n) * 2 ^ a = shl (upto n) a + 2 ^ a -> suc (upto n) * 2 ^ a = 2 ^ (n + a) -> shl (upto n) a + 2 ^ a = 2 ^ (n + a)
14 mulS1 
suc (upto n) * 2 ^ a = upto n * 2 ^ a + 2 ^ a
15 14 conv shl 
suc (upto n) * 2 ^ a = shl (upto n) a + 2 ^ a
16 13, 15 ax_mp 
suc (upto n) * 2 ^ a = 2 ^ (n + a) -> shl (upto n) a + 2 ^ a = 2 ^ (n + a)
17 eqtr4 
suc (upto n) * 2 ^ a = 2 ^ n * 2 ^ a -> 2 ^ (n + a) = 2 ^ n * 2 ^ a -> suc (upto n) * 2 ^ a = 2 ^ (n + a)
18 muleq1 
suc (upto n) = 2 ^ n -> suc (upto n) * 2 ^ a = 2 ^ n * 2 ^ a
19 sucupto 
suc (upto n) = 2 ^ n
20 18, 19 ax_mp 
suc (upto n) * 2 ^ a = 2 ^ n * 2 ^ a
21 17, 20 ax_mp 
2 ^ (n + a) = 2 ^ n * 2 ^ a -> suc (upto n) * 2 ^ a = 2 ^ (n + a)
22 powadd 
2 ^ (n + a) = 2 ^ n * 2 ^ a
23 21, 22 ax_mp 
suc (upto n) * 2 ^ a = 2 ^ (n + a)
24 16, 23 ax_mp 
shl (upto n) a + 2 ^ a = 2 ^ (n + a)
25 12, 24 ax_mp 
suc (upto (n + a)) = shl (upto n) a + 2 ^ a
26 9, 25 ax_mp 
shl (upto n) a + suc (upto a) = suc (upto (n + a))
27 4, 26 ax_mp 
suc (shl (upto n) a + upto a) = suc (upto (n + a))
28 1, 27 mpbi 
shl (upto n) a + upto a = upto (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)