Theorem appendeq0 | index | src |

theorem appendeq0 (a b: nat): $ a ++ b = 0 <-> a = 0 /\ b = 0 $;
StepHypRefExpression
1 bitr3
(len (a ++ b) = 0 <-> a ++ b = 0) -> (len (a ++ b) = 0 <-> a = 0 /\ b = 0) -> (a ++ b = 0 <-> a = 0 /\ b = 0)
2 leneq0
len (a ++ b) = 0 <-> a ++ b = 0
3 1, 2 ax_mp
(len (a ++ b) = 0 <-> a = 0 /\ b = 0) -> (a ++ b = 0 <-> a = 0 /\ b = 0)
4 bitr
(len (a ++ b) = 0 <-> len a + len b = 0) -> (len a + len b = 0 <-> a = 0 /\ b = 0) -> (len (a ++ b) = 0 <-> a = 0 /\ b = 0)
5 eqeq1
len (a ++ b) = len a + len b -> (len (a ++ b) = 0 <-> len a + len b = 0)
6 appendlen
len (a ++ b) = len a + len b
7 5, 6 ax_mp
len (a ++ b) = 0 <-> len a + len b = 0
8 4, 7 ax_mp
(len a + len b = 0 <-> a = 0 /\ b = 0) -> (len (a ++ b) = 0 <-> a = 0 /\ b = 0)
9 bitr
(len a + len b = 0 <-> len a = 0 /\ len b = 0) -> (len a = 0 /\ len b = 0 <-> a = 0 /\ b = 0) -> (len a + len b = 0 <-> a = 0 /\ b = 0)
10 addeq0
len a + len b = 0 <-> len a = 0 /\ len b = 0
11 9, 10 ax_mp
(len a = 0 /\ len b = 0 <-> a = 0 /\ b = 0) -> (len a + len b = 0 <-> a = 0 /\ b = 0)
12 aneq
(len a = 0 <-> a = 0) -> (len b = 0 <-> b = 0) -> (len a = 0 /\ len b = 0 <-> a = 0 /\ b = 0)
13 leneq0
len a = 0 <-> a = 0
14 12, 13 ax_mp
(len b = 0 <-> b = 0) -> (len a = 0 /\ len b = 0 <-> a = 0 /\ b = 0)
15 leneq0
len b = 0 <-> b = 0
16 14, 15 ax_mp
len a = 0 /\ len b = 0 <-> a = 0 /\ b = 0
17 11, 16 ax_mp
len a + len b = 0 <-> a = 0 /\ b = 0
18 8, 17 ax_mp
len (a ++ b) = 0 <-> a = 0 /\ b = 0
19 3, 18 ax_mp
a ++ b = 0 <-> a = 0 /\ b = 0

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)