Theorem append02 | index | src |

theorem append02 (a: nat): $ a ++ 0 = a $;
StepHypRefExpression
1 id
_1 = a -> _1 = a
2 eqidd
_1 = a -> 0 = 0
3 1, 2 appendeqd
_1 = a -> _1 ++ 0 = a ++ 0
4 3, 1 eqeqd
_1 = a -> (_1 ++ 0 = _1 <-> a ++ 0 = a)
5 id
_1 = 0 -> _1 = 0
6 eqidd
_1 = 0 -> 0 = 0
7 5, 6 appendeqd
_1 = 0 -> _1 ++ 0 = 0 ++ 0
8 7, 5 eqeqd
_1 = 0 -> (_1 ++ 0 = _1 <-> 0 ++ 0 = 0)
9 id
_1 = a2 -> _1 = a2
10 eqidd
_1 = a2 -> 0 = 0
11 9, 10 appendeqd
_1 = a2 -> _1 ++ 0 = a2 ++ 0
12 11, 9 eqeqd
_1 = a2 -> (_1 ++ 0 = _1 <-> a2 ++ 0 = a2)
13 id
_1 = a1 : a2 -> _1 = a1 : a2
14 eqidd
_1 = a1 : a2 -> 0 = 0
15 13, 14 appendeqd
_1 = a1 : a2 -> _1 ++ 0 = a1 : a2 ++ 0
16 15, 13 eqeqd
_1 = a1 : a2 -> (_1 ++ 0 = _1 <-> a1 : a2 ++ 0 = a1 : a2)
17 append0
0 ++ 0 = 0
18 appendS
a1 : a2 ++ 0 = a1 : (a2 ++ 0)
19 conseq2
a2 ++ 0 = a2 -> a1 : (a2 ++ 0) = a1 : a2
20 18, 19 syl5eq
a2 ++ 0 = a2 -> a1 : a2 ++ 0 = a1 : a2
21 4, 8, 12, 16, 17, 20 listind
a ++ 0 = 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)