Theorem listfnSval | index | src |

theorem listfnSval (a l n: nat):
  $ n < suc (len l) -> listfn (a : l) @ n = if (n = 0) a (listfn l @ (n - 1)) $;
StepHypRefExpression
1 appneq1
listfn (a : l) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1)) ->
  listfn (a : l) @ n = (\. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))) @ n
2 listfnS
listfn (a : l) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))
3 1, 2 ax_mp
listfn (a : l) @ n = (\. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))) @ n
4 elupto
n e. upto (suc (len l)) <-> n < suc (len l)
5 eqeq1
i = n -> (i = 0 <-> n = 0)
6 eqidd
i = n -> a = a
7 subeq1
i = n -> i - 1 = n - 1
8 7 appeq2d
i = n -> listfn l @ (i - 1) = listfn l @ (n - 1)
9 5, 6, 8 ifeqd
i = n -> if (i = 0) a (listfn l @ (i - 1)) = if (n = 0) a (listfn l @ (n - 1))
10 9 apprlame
n e. upto (suc (len l)) -> (\. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))) @ n = if (n = 0) a (listfn l @ (n - 1))
11 4, 10 sylbir
n < suc (len l) -> (\. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))) @ n = if (n = 0) a (listfn l @ (n - 1))
12 3, 11 syl5eq
n < suc (len l) -> listfn (a : l) @ n = if (n = 0) a (listfn l @ (n - 1))

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)