Theorem dmlistfn ≪ | index | src | ≫ 

theorem dmlistfn (l: nat): $ Dom (listfn l) == upto (len l) $;
StepHypRefExpression
1 id 
_1 = l -> _1 = l
2 1 listfneqd 
_1 = l -> listfn _1 = listfn l
3 2 nseqd 
_1 = l -> listfn _1 == listfn l
4 3 dmeqd 
_1 = l -> Dom (listfn _1) == Dom (listfn l)
5 1 leneqd 
_1 = l -> len _1 = len l
6 5 uptoeqd 
_1 = l -> upto (len _1) = upto (len l)
7 6 nseqd 
_1 = l -> upto (len _1) == upto (len l)
8 4, 7 eqseqd 
_1 = l -> (Dom (listfn _1) == upto (len _1) <-> Dom (listfn l) == upto (len l))
9 id 
_1 = 0 -> _1 = 0
10 9 listfneqd 
_1 = 0 -> listfn _1 = listfn 0
11 10 nseqd 
_1 = 0 -> listfn _1 == listfn 0
12 11 dmeqd 
_1 = 0 -> Dom (listfn _1) == Dom (listfn 0)
13 9 leneqd 
_1 = 0 -> len _1 = len 0
14 13 uptoeqd 
_1 = 0 -> upto (len _1) = upto (len 0)
15 14 nseqd 
_1 = 0 -> upto (len _1) == upto (len 0)
16 12, 15 eqseqd 
_1 = 0 -> (Dom (listfn _1) == upto (len _1) <-> Dom (listfn 0) == upto (len 0))
17 id 
_1 = a2 -> _1 = a2
18 17 listfneqd 
_1 = a2 -> listfn _1 = listfn a2
19 18 nseqd 
_1 = a2 -> listfn _1 == listfn a2
20 19 dmeqd 
_1 = a2 -> Dom (listfn _1) == Dom (listfn a2)
21 17 leneqd 
_1 = a2 -> len _1 = len a2
22 21 uptoeqd 
_1 = a2 -> upto (len _1) = upto (len a2)
23 22 nseqd 
_1 = a2 -> upto (len _1) == upto (len a2)
24 20, 23 eqseqd 
_1 = a2 -> (Dom (listfn _1) == upto (len _1) <-> Dom (listfn a2) == upto (len a2))
25 id 
_1 = a1 : a2 -> _1 = a1 : a2
26 25 listfneqd 
_1 = a1 : a2 -> listfn _1 = listfn (a1 : a2)
27 26 nseqd 
_1 = a1 : a2 -> listfn _1 == listfn (a1 : a2)
28 27 dmeqd 
_1 = a1 : a2 -> Dom (listfn _1) == Dom (listfn (a1 : a2))
29 25 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
30 29 uptoeqd 
_1 = a1 : a2 -> upto (len _1) = upto (len (a1 : a2))
31 30 nseqd 
_1 = a1 : a2 -> upto (len _1) == upto (len (a1 : a2))
32 28, 31 eqseqd 
_1 = a1 : a2 -> (Dom (listfn _1) == upto (len _1) <-> Dom (listfn (a1 : a2)) == upto (len (a1 : a2)))
33 eqstr 
Dom (listfn 0) == Dom 0 -> Dom 0 == upto (len 0) -> Dom (listfn 0) == upto (len 0)
34 dmeq 
listfn 0 == 0 -> Dom (listfn 0) == Dom 0
35 nseq 
listfn 0 = 0 -> listfn 0 == 0
36 listfn0 
listfn 0 = 0
37 35, 36 ax_mp 
listfn 0 == 0
38 34, 37 ax_mp 
Dom (listfn 0) == Dom 0
39 33, 38 ax_mp 
Dom 0 == upto (len 0) -> Dom (listfn 0) == upto (len 0)
40 eqstr4 
Dom 0 == 0 -> upto (len 0) == 0 -> Dom 0 == upto (len 0)
41 dm0 
Dom 0 == 0
42 40, 41 ax_mp 
upto (len 0) == 0 -> Dom 0 == upto (len 0)
43 nseq 
upto (len 0) = 0 -> upto (len 0) == 0
44 eqtr 
upto (len 0) = upto 0 -> upto 0 = 0 -> upto (len 0) = 0
45 uptoeq 
len 0 = 0 -> upto (len 0) = upto 0
46 len0 
len 0 = 0
47 45, 46 ax_mp 
upto (len 0) = upto 0
48 44, 47 ax_mp 
upto 0 = 0 -> upto (len 0) = 0
49 upto0 
upto 0 = 0
50 48, 49 ax_mp 
upto (len 0) = 0
51 43, 50 ax_mp 
upto (len 0) == 0
52 42, 51 ax_mp 
Dom 0 == upto (len 0)
53 39, 52 ax_mp 
Dom (listfn 0) == upto (len 0)
54 dmeq 
listfn (a1 : a2) == \. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1)) ->
  Dom (listfn (a1 : a2)) == Dom (\. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1)))
55 nseq 
listfn (a1 : a2) = \. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1)) ->
  listfn (a1 : a2) == \. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1))
56 listfnS2 
listfn (a1 : a2) = \. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1))
57 55, 56 ax_mp 
listfn (a1 : a2) == \. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1))
58 54, 57 ax_mp 
Dom (listfn (a1 : a2)) == Dom (\. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1)))
59 dmrlam 
Dom (\. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1))) == upto (suc (size (Dom (listfn a2))))
60 uptoeq 
len (a1 : a2) = suc (len a2) -> upto (len (a1 : a2)) = upto (suc (len a2))
61 lenS 
len (a1 : a2) = suc (len a2)
62 60, 61 ax_mp 
upto (len (a1 : a2)) = upto (suc (len a2))
63 sizeupto 
size (upto (len a2)) = len a2
64 sizeeq 
Dom (listfn a2) == upto (len a2) -> size (Dom (listfn a2)) = size (upto (len a2))
65 63, 64 syl6eq 
Dom (listfn a2) == upto (len a2) -> size (Dom (listfn a2)) = len a2
66 65 suceqd 
Dom (listfn a2) == upto (len a2) -> suc (size (Dom (listfn a2))) = suc (len a2)
67 66 uptoeqd 
Dom (listfn a2) == upto (len a2) -> upto (suc (size (Dom (listfn a2)))) = upto (suc (len a2))
68 62, 67 syl6eqr 
Dom (listfn a2) == upto (len a2) -> upto (suc (size (Dom (listfn a2)))) = upto (len (a1 : a2))
69 68 nseqd 
Dom (listfn a2) == upto (len a2) -> upto (suc (size (Dom (listfn a2)))) == upto (len (a1 : a2))
70 59, 69 syl5eqs 
Dom (listfn a2) == upto (len a2) -> Dom (\. i e. upto (suc (size (Dom (listfn a2)))), if (i = 0) a1 (listfn a2 @ (i - 1))) == upto (len (a1 : a2))
71 58, 70 syl5eqs 
Dom (listfn a2) == upto (len a2) -> Dom (listfn (a1 : a2)) == upto (len (a1 : a2))
72 8, 16, 24, 32, 53, 71 listind 
Dom (listfn l) == upto (len l)

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)