Theorem appendArray | index | src |

theorem appendArray (A: set) (a b m n: nat):
  $ a e. Array A m -> b e. Array A n -> a ++ b e. Array A (m + n) $;
StepHypRefExpression
1 aneq
(a e. Array A m <-> a e. List A /\ len a = m) ->
  (b e. Array A n <-> b e. List A /\ len b = n) ->
  (a e. Array A m /\ b e. Array A n <-> a e. List A /\ len a = m /\ (b e. List A /\ len b = n))
2 elArray
a e. Array A m <-> a e. List A /\ len a = m
3 1, 2 ax_mp
(b e. Array A n <-> b e. List A /\ len b = n) -> (a e. Array A m /\ b e. Array A n <-> a e. List A /\ len a = m /\ (b e. List A /\ len b = n))
4 elArray
b e. Array A n <-> b e. List A /\ len b = n
5 3, 4 ax_mp
a e. Array A m /\ b e. Array A n <-> a e. List A /\ len a = m /\ (b e. List A /\ len b = n)
6 an4
a e. List A /\ len a = m /\ (b e. List A /\ len b = n) <-> a e. List A /\ b e. List A /\ (len a = m /\ len b = n)
7 elArray
a ++ b e. Array A (m + n) <-> a ++ b e. List A /\ len (a ++ b) = m + n
8 anim
(a e. List A /\ b e. List A -> a ++ b e. List A) ->
  (len a = m /\ len b = n -> len (a ++ b) = m + n) ->
  a e. List A /\ b e. List A /\ (len a = m /\ len b = n) ->
  a ++ b e. List A /\ len (a ++ b) = m + n
9 bi2
(a ++ b e. List A <-> a e. List A /\ b e. List A) -> a e. List A /\ b e. List A -> a ++ b e. List A
10 appendT
a ++ b e. List A <-> a e. List A /\ b e. List A
11 9, 10 ax_mp
a e. List A /\ b e. List A -> a ++ b e. List A
12 8, 11 ax_mp
(len a = m /\ len b = n -> len (a ++ b) = m + n) -> a e. List A /\ b e. List A /\ (len a = m /\ len b = n) -> a ++ b e. List A /\ len (a ++ b) = m + n
13 appendlen
len (a ++ b) = len a + len b
14 addeq
len a = m -> len b = n -> len a + len b = m + n
15 14 imp
len a = m /\ len b = n -> len a + len b = m + n
16 13, 15 syl5eq
len a = m /\ len b = n -> len (a ++ b) = m + n
17 12, 16 ax_mp
a e. List A /\ b e. List A /\ (len a = m /\ len b = n) -> a ++ b e. List A /\ len (a ++ b) = m + n
18 7, 17 sylibr
a e. List A /\ b e. List A /\ (len a = m /\ len b = n) -> a ++ b e. Array A (m + n)
19 6, 18 sylbi
a e. List A /\ len a = m /\ (b e. List A /\ len b = n) -> a ++ b e. Array A (m + n)
20 5, 19 sylbi
a e. Array A m /\ b e. Array A n -> a ++ b e. Array A (m + n)
21 20 exp
a e. Array A m -> b e. Array A n -> a ++ b e. Array A (m + 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)