| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
appeq2 |
suc n - 1 = n -> listfn l @ (suc n - 1) = listfn l @ n |
| 2 |
|
sucsub1 |
suc n - 1 = n |
| 3 |
1, 2 |
ax_mp |
listfn l @ (suc n - 1) = listfn l @ n |
| 4 |
|
ifneg |
~suc n = 0 -> if (suc n = 0) a (listfn l @ (suc n - 1)) = listfn l @ (suc n - 1) |
| 5 |
|
peano1 |
suc n != 0 |
| 6 |
5 |
conv ne |
~suc n = 0 |
| 7 |
4, 6 |
ax_mp |
if (suc n = 0) a (listfn l @ (suc n - 1)) = listfn l @ (suc n - 1) |
| 8 |
|
ltsuc |
n < len l <-> suc n < suc (len l) |
| 9 |
|
listfnSval |
suc n < suc (len l) -> listfn (a : l) @ suc n = if (suc n = 0) a (listfn l @ (suc n - 1)) |
| 10 |
8, 9 |
sylbi |
n < len l -> listfn (a : l) @ suc n = if (suc n = 0) a (listfn l @ (suc n - 1)) |
| 11 |
7, 10 |
syl6eq |
n < len l -> listfn (a : l) @ suc n = listfn l @ (suc n - 1) |
| 12 |
3, 11 |
syl6eq |
n < len l -> listfn (a : l) @ suc n = listfn l @ n |
| 13 |
|
noteq |
(suc n e. Dom (listfn (a : l)) <-> n < len l) -> (~suc n e. Dom (listfn (a : l)) <-> ~n < len l) |
| 14 |
|
bitr |
(suc n e. Dom (listfn (a : l)) <-> suc n e. upto (len (a : l))) -> (suc n e. upto (len (a : l)) <-> n < len l) -> (suc n e. Dom (listfn (a : l)) <-> n < len l) |
| 15 |
|
eleq2 |
Dom (listfn (a : l)) == upto (len (a : l)) -> (suc n e. Dom (listfn (a : l)) <-> suc n e. upto (len (a : l))) |
| 16 |
|
dmlistfn |
Dom (listfn (a : l)) == upto (len (a : l)) |
| 17 |
15, 16 |
ax_mp |
suc n e. Dom (listfn (a : l)) <-> suc n e. upto (len (a : l)) |
| 18 |
14, 17 |
ax_mp |
(suc n e. upto (len (a : l)) <-> n < len l) -> (suc n e. Dom (listfn (a : l)) <-> n < len l) |
| 19 |
|
bitr |
(suc n e. upto (len (a : l)) <-> suc n < len (a : l)) -> (suc n < len (a : l) <-> n < len l) -> (suc n e. upto (len (a : l)) <-> n < len l) |
| 20 |
|
elupto |
suc n e. upto (len (a : l)) <-> suc n < len (a : l) |
| 21 |
19, 20 |
ax_mp |
(suc n < len (a : l) <-> n < len l) -> (suc n e. upto (len (a : l)) <-> n < len l) |
| 22 |
|
bitr4 |
(suc n < len (a : l) <-> suc n < suc (len l)) -> (n < len l <-> suc n < suc (len l)) -> (suc n < len (a : l) <-> n < len l) |
| 23 |
|
lteq2 |
len (a : l) = suc (len l) -> (suc n < len (a : l) <-> suc n < suc (len l)) |
| 24 |
|
lenS |
len (a : l) = suc (len l) |
| 25 |
23, 24 |
ax_mp |
suc n < len (a : l) <-> suc n < suc (len l) |
| 26 |
22, 25 |
ax_mp |
(n < len l <-> suc n < suc (len l)) -> (suc n < len (a : l) <-> n < len l) |
| 27 |
26, 8 |
ax_mp |
suc n < len (a : l) <-> n < len l |
| 28 |
21, 27 |
ax_mp |
suc n e. upto (len (a : l)) <-> n < len l |
| 29 |
18, 28 |
ax_mp |
suc n e. Dom (listfn (a : l)) <-> n < len l |
| 30 |
13, 29 |
ax_mp |
~suc n e. Dom (listfn (a : l)) <-> ~n < len l |
| 31 |
|
ndmapp |
~suc n e. Dom (listfn (a : l)) -> listfn (a : l) @ suc n = 0 |
| 32 |
30, 31 |
sylbir |
~n < len l -> listfn (a : l) @ suc n = 0 |
| 33 |
|
noteq |
(n e. Dom (listfn l) <-> n < len l) -> (~n e. Dom (listfn l) <-> ~n < len l) |
| 34 |
|
bitr |
(n e. Dom (listfn l) <-> n e. upto (len l)) -> (n e. upto (len l) <-> n < len l) -> (n e. Dom (listfn l) <-> n < len l) |
| 35 |
|
eleq2 |
Dom (listfn l) == upto (len l) -> (n e. Dom (listfn l) <-> n e. upto (len l)) |
| 36 |
|
dmlistfn |
Dom (listfn l) == upto (len l) |
| 37 |
35, 36 |
ax_mp |
n e. Dom (listfn l) <-> n e. upto (len l) |
| 38 |
34, 37 |
ax_mp |
(n e. upto (len l) <-> n < len l) -> (n e. Dom (listfn l) <-> n < len l) |
| 39 |
|
elupto |
n e. upto (len l) <-> n < len l |
| 40 |
38, 39 |
ax_mp |
n e. Dom (listfn l) <-> n < len l |
| 41 |
33, 40 |
ax_mp |
~n e. Dom (listfn l) <-> ~n < len l |
| 42 |
|
ndmapp |
~n e. Dom (listfn l) -> listfn l @ n = 0 |
| 43 |
41, 42 |
sylbir |
~n < len l -> listfn l @ n = 0 |
| 44 |
32, 43 |
eqtr4d |
~n < len l -> listfn (a : l) @ suc n = listfn l @ n |
| 45 |
12, 44 |
cases |
listfn (a : l) @ suc n = listfn l @ n |