Theorem uptoS ≪ | index | src | ≫ 

theorem uptoS (n: nat): $ upto (suc n) = b1 (upto n) $;
StepHypRefExpression
1 addcan1 
upto (suc n) + 1 = b1 (upto n) + 1 <-> upto (suc n) = b1 (upto n)
2 eqtr 
upto (suc n) + 1 = 2 ^ suc n -> 2 ^ suc n = b1 (upto n) + 1 -> upto (suc n) + 1 = b1 (upto n) + 1
3 uptoadd1 
upto (suc n) + 1 = 2 ^ suc n
4 2, 3 ax_mp 
2 ^ suc n = b1 (upto n) + 1 -> upto (suc n) + 1 = b1 (upto n) + 1
5 eqtr 
2 ^ suc n = 2 * 2 ^ n -> 2 * 2 ^ n = b1 (upto n) + 1 -> 2 ^ suc n = b1 (upto n) + 1
6 powS 
2 ^ suc n = 2 * 2 ^ n
7 5, 6 ax_mp 
2 * 2 ^ n = b1 (upto n) + 1 -> 2 ^ suc n = b1 (upto n) + 1
8 eqtr3 
2 * suc (upto n) = 2 * 2 ^ n -> 2 * suc (upto n) = b1 (upto n) + 1 -> 2 * 2 ^ n = b1 (upto n) + 1
9 muleq2 
suc (upto n) = 2 ^ n -> 2 * suc (upto n) = 2 * 2 ^ n
10 sucupto 
suc (upto n) = 2 ^ n
11 9, 10 ax_mp 
2 * suc (upto n) = 2 * 2 ^ n
12 8, 11 ax_mp 
2 * suc (upto n) = b1 (upto n) + 1 -> 2 * 2 ^ n = b1 (upto n) + 1
13 eqtr 
2 * suc (upto n) = 2 * upto n + 2 -> 2 * upto n + 2 = b1 (upto n) + 1 -> 2 * suc (upto n) = b1 (upto n) + 1
14 mulS 
2 * suc (upto n) = 2 * upto n + 2
15 13, 14 ax_mp 
2 * upto n + 2 = b1 (upto n) + 1 -> 2 * suc (upto n) = b1 (upto n) + 1
16 eqtr4 
2 * upto n + 2 = b0 (upto n) + 2 -> b1 (upto n) + 1 = b0 (upto n) + 2 -> 2 * upto n + 2 = b1 (upto n) + 1
17 addeq1 
2 * upto n = b0 (upto n) -> 2 * upto n + 2 = b0 (upto n) + 2
18 b0mul21 
2 * upto n = b0 (upto n)
19 17, 18 ax_mp 
2 * upto n + 2 = b0 (upto n) + 2
20 16, 19 ax_mp 
b1 (upto n) + 1 = b0 (upto n) + 2 -> 2 * upto n + 2 = b1 (upto n) + 1
21 addSass 
suc (b0 (upto n)) + 1 = b0 (upto n) + suc 1
22 21 conv b1, d2 
b1 (upto n) + 1 = b0 (upto n) + 2
23 20, 22 ax_mp 
2 * upto n + 2 = b1 (upto n) + 1
24 15, 23 ax_mp 
2 * suc (upto n) = b1 (upto n) + 1
25 12, 24 ax_mp 
2 * 2 ^ n = b1 (upto n) + 1
26 7, 25 ax_mp 
2 ^ suc n = b1 (upto n) + 1
27 4, 26 ax_mp 
upto (suc n) + 1 = b1 (upto n) + 1
28 1, 27 mpbi 
upto (suc n) = b1 (upto 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)