Theorem revnth ≪ | index | src | ≫ 

theorem revnth (i l: nat):
  $ i < len l -> nth i (rev l) = nth (len l - suc i) l $;
StepHypRefExpression
1 id 
_1 = l -> _1 = l
2 1 leneqd 
_1 = l -> len _1 = len l
3 2 lteq2d 
_1 = l -> (i < len _1 <-> i < len l)
4 1 reveqd 
_1 = l -> rev _1 = rev l
5 4 ntheq2d 
_1 = l -> nth i (rev _1) = nth i (rev l)
6 2 subeq1d 
_1 = l -> len _1 - suc i = len l - suc i
7 6, 1 ntheqd 
_1 = l -> nth (len _1 - suc i) _1 = nth (len l - suc i) l
8 5, 7 eqeqd 
_1 = l -> (nth i (rev _1) = nth (len _1 - suc i) _1 <-> nth i (rev l) = nth (len l - suc i) l)
9 3, 8 imeqd 
_1 = l -> (i < len _1 -> nth i (rev _1) = nth (len _1 - suc i) _1 <-> i < len l -> nth i (rev l) = nth (len l - suc i) l)
10 id 
_1 = 0 -> _1 = 0
11 10 leneqd 
_1 = 0 -> len _1 = len 0
12 11 lteq2d 
_1 = 0 -> (i < len _1 <-> i < len 0)
13 10 reveqd 
_1 = 0 -> rev _1 = rev 0
14 13 ntheq2d 
_1 = 0 -> nth i (rev _1) = nth i (rev 0)
15 11 subeq1d 
_1 = 0 -> len _1 - suc i = len 0 - suc i
16 15, 10 ntheqd 
_1 = 0 -> nth (len _1 - suc i) _1 = nth (len 0 - suc i) 0
17 14, 16 eqeqd 
_1 = 0 -> (nth i (rev _1) = nth (len _1 - suc i) _1 <-> nth i (rev 0) = nth (len 0 - suc i) 0)
18 12, 17 imeqd 
_1 = 0 -> (i < len _1 -> nth i (rev _1) = nth (len _1 - suc i) _1 <-> i < len 0 -> nth i (rev 0) = nth (len 0 - suc i) 0)
19 id 
_1 = a2 -> _1 = a2
20 19 leneqd 
_1 = a2 -> len _1 = len a2
21 20 lteq2d 
_1 = a2 -> (i < len _1 <-> i < len a2)
22 19 reveqd 
_1 = a2 -> rev _1 = rev a2
23 22 ntheq2d 
_1 = a2 -> nth i (rev _1) = nth i (rev a2)
24 20 subeq1d 
_1 = a2 -> len _1 - suc i = len a2 - suc i
25 24, 19 ntheqd 
_1 = a2 -> nth (len _1 - suc i) _1 = nth (len a2 - suc i) a2
26 23, 25 eqeqd 
_1 = a2 -> (nth i (rev _1) = nth (len _1 - suc i) _1 <-> nth i (rev a2) = nth (len a2 - suc i) a2)
27 21, 26 imeqd 
_1 = a2 -> (i < len _1 -> nth i (rev _1) = nth (len _1 - suc i) _1 <-> i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2)
28 id 
_1 = a1 : a2 -> _1 = a1 : a2
29 28 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
30 29 lteq2d 
_1 = a1 : a2 -> (i < len _1 <-> i < len (a1 : a2))
31 28 reveqd 
_1 = a1 : a2 -> rev _1 = rev (a1 : a2)
32 31 ntheq2d 
_1 = a1 : a2 -> nth i (rev _1) = nth i (rev (a1 : a2))
33 29 subeq1d 
_1 = a1 : a2 -> len _1 - suc i = len (a1 : a2) - suc i
34 33, 28 ntheqd 
_1 = a1 : a2 -> nth (len _1 - suc i) _1 = nth (len (a1 : a2) - suc i) (a1 : a2)
35 32, 34 eqeqd 
_1 = a1 : a2 -> (nth i (rev _1) = nth (len _1 - suc i) _1 <-> nth i (rev (a1 : a2)) = nth (len (a1 : a2) - suc i) (a1 : a2))
36 30, 35 imeqd 
_1 = a1 : a2 -> (i < len _1 -> nth i (rev _1) = nth (len _1 - suc i) _1 <-> i < len (a1 : a2) -> nth i (rev (a1 : a2)) = nth (len (a1 : a2) - suc i) (a1 : a2))
37 absurd 
~i < len 0 -> i < len 0 -> nth i (rev 0) = nth (len 0 - suc i) 0
38 lteq2 
len 0 = 0 -> (i < len 0 <-> i < 0)
39 len0 
len 0 = 0
40 38, 39 ax_mp 
i < len 0 <-> i < 0
41 lt02 
~i < 0
42 40, 41 mtbir 
~i < len 0
43 37, 42 ax_mp 
i < len 0 -> nth i (rev 0) = nth (len 0 - suc i) 0
44 bitr4 
(i < len (a1 : a2) <-> i < suc (len a2)) -> (i <= len a2 <-> i < suc (len a2)) -> (i < len (a1 : a2) <-> i <= len a2)
45 lteq2 
len (a1 : a2) = suc (len a2) -> (i < len (a1 : a2) <-> i < suc (len a2))
46 lenS 
len (a1 : a2) = suc (len a2)
47 45, 46 ax_mp 
i < len (a1 : a2) <-> i < suc (len a2)
48 44, 47 ax_mp 
(i <= len a2 <-> i < suc (len a2)) -> (i < len (a1 : a2) <-> i <= len a2)
49 leltsuc 
i <= len a2 <-> i < suc (len a2)
50 48, 49 ax_mp 
i < len (a1 : a2) <-> i <= len a2
51 eqeq 
nth i (rev (a1 : a2)) = nth i (rev a2 |> a1) ->
  nth (len (a1 : a2) - suc i) (a1 : a2) = nth (suc (len a2) - suc i) (a1 : a2) ->
  (nth i (rev (a1 : a2)) = nth (len (a1 : a2) - suc i) (a1 : a2) <-> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2))
52 ntheq2 
rev (a1 : a2) = rev a2 |> a1 -> nth i (rev (a1 : a2)) = nth i (rev a2 |> a1)
53 revS 
rev (a1 : a2) = rev a2 |> a1
54 52, 53 ax_mp 
nth i (rev (a1 : a2)) = nth i (rev a2 |> a1)
55 51, 54 ax_mp 
nth (len (a1 : a2) - suc i) (a1 : a2) = nth (suc (len a2) - suc i) (a1 : a2) ->
  (nth i (rev (a1 : a2)) = nth (len (a1 : a2) - suc i) (a1 : a2) <-> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2))
56 ntheq1 
len (a1 : a2) - suc i = suc (len a2) - suc i -> nth (len (a1 : a2) - suc i) (a1 : a2) = nth (suc (len a2) - suc i) (a1 : a2)
57 subeq1 
len (a1 : a2) = suc (len a2) -> len (a1 : a2) - suc i = suc (len a2) - suc i
58 57, 46 ax_mp 
len (a1 : a2) - suc i = suc (len a2) - suc i
59 56, 58 ax_mp 
nth (len (a1 : a2) - suc i) (a1 : a2) = nth (suc (len a2) - suc i) (a1 : a2)
60 55, 59 ax_mp 
nth i (rev (a1 : a2)) = nth (len (a1 : a2) - suc i) (a1 : a2) <-> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
61 leloe 
i <= len a2 <-> i < len a2 \/ i = len a2
62 eor 
(i < len a2 -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)) ->
  (i = len a2 -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)) ->
  i < len a2 \/ i = len a2 ->
  (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) ->
  nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
63 ax_2 
(i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2 -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)) ->
  (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) ->
  i < len a2 ->
  nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
64 lteq2 
len (rev a2) = len a2 -> (i < len (rev a2) <-> i < len a2)
65 revlen 
len (rev a2) = len a2
66 64, 65 ax_mp 
i < len (rev a2) <-> i < len a2
67 appendnth1 
i < len (rev a2) -> nth i (rev a2 ++ a1 : 0) = nth i (rev a2)
68 67 conv snoc 
i < len (rev a2) -> nth i (rev a2 |> a1) = nth i (rev a2)
69 66, 68 sylbir 
i < len a2 -> nth i (rev a2 |> a1) = nth i (rev a2)
70 69 anwl 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> nth i (rev a2 |> a1) = nth i (rev a2)
71 sucsub 
suc i <= len a2 -> suc (len a2) - suc i = suc (len a2 - suc i)
72 anl 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> i < len a2
73 72 conv lt 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> suc i <= len a2
74 71, 73 syl 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> suc (len a2) - suc i = suc (len a2 - suc i)
75 74 ntheq1d 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> nth (suc (len a2) - suc i) (a1 : a2) = nth (suc (len a2 - suc i)) (a1 : a2)
76 nthS 
nth (suc (len a2 - suc i)) (a1 : a2) = nth (len a2 - suc i) a2
77 anr 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> nth i (rev a2) = nth (len a2 - suc i) a2
78 76, 77 syl6eqr 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> nth i (rev a2) = nth (suc (len a2 - suc i)) (a1 : a2)
79 75, 78 eqtr4d 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> nth (suc (len a2) - suc i) (a1 : a2) = nth i (rev a2)
80 70, 79 eqtr4d 
i < len a2 /\ nth i (rev a2) = nth (len a2 - suc i) a2 -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
81 80 exp 
i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2 -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
82 63, 81 ax_mp 
(i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> i < len a2 -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
83 82 com12 
i < len a2 -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
84 62, 83 ax_mp 
(i = len a2 -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)) ->
  i < len a2 \/ i = len a2 ->
  (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) ->
  nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
85 eqtr3 
nth (len (rev a2) + 0) (rev a2 |> a1) = nth (len a2) (rev a2 |> a1) ->
  nth (len (rev a2) + 0) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2) ->
  nth (len a2) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2)
86 ntheq1 
len (rev a2) + 0 = len a2 -> nth (len (rev a2) + 0) (rev a2 |> a1) = nth (len a2) (rev a2 |> a1)
87 eqtr 
len (rev a2) + 0 = len a2 + 0 -> len a2 + 0 = len a2 -> len (rev a2) + 0 = len a2
88 addeq1 
len (rev a2) = len a2 -> len (rev a2) + 0 = len a2 + 0
89 88, 65 ax_mp 
len (rev a2) + 0 = len a2 + 0
90 87, 89 ax_mp 
len a2 + 0 = len a2 -> len (rev a2) + 0 = len a2
91 add02 
len a2 + 0 = len a2
92 90, 91 ax_mp 
len (rev a2) + 0 = len a2
93 86, 92 ax_mp 
nth (len (rev a2) + 0) (rev a2 |> a1) = nth (len a2) (rev a2 |> a1)
94 85, 93 ax_mp 
nth (len (rev a2) + 0) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2) -> nth (len a2) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2)
95 eqtr4 
nth (len (rev a2) + 0) (rev a2 |> a1) = nth 0 (a1 : 0) ->
  nth (suc (len a2) - suc (len a2)) (a1 : a2) = nth 0 (a1 : 0) ->
  nth (len (rev a2) + 0) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2)
96 appendnth2_ 
nth (len (rev a2) + 0) (rev a2 ++ a1 : 0) = nth 0 (a1 : 0)
97 96 conv snoc 
nth (len (rev a2) + 0) (rev a2 |> a1) = nth 0 (a1 : 0)
98 95, 97 ax_mp 
nth (suc (len a2) - suc (len a2)) (a1 : a2) = nth 0 (a1 : 0) -> nth (len (rev a2) + 0) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2)
99 eqtr 
nth (suc (len a2) - suc (len a2)) (a1 : a2) = nth 0 (a1 : a2) ->
  nth 0 (a1 : a2) = nth 0 (a1 : 0) ->
  nth (suc (len a2) - suc (len a2)) (a1 : a2) = nth 0 (a1 : 0)
100 ntheq1 
suc (len a2) - suc (len a2) = 0 -> nth (suc (len a2) - suc (len a2)) (a1 : a2) = nth 0 (a1 : a2)
101 subid 
suc (len a2) - suc (len a2) = 0
102 100, 101 ax_mp 
nth (suc (len a2) - suc (len a2)) (a1 : a2) = nth 0 (a1 : a2)
103 99, 102 ax_mp 
nth 0 (a1 : a2) = nth 0 (a1 : 0) -> nth (suc (len a2) - suc (len a2)) (a1 : a2) = nth 0 (a1 : 0)
104 eqtr4 
nth 0 (a1 : a2) = suc a1 -> nth 0 (a1 : 0) = suc a1 -> nth 0 (a1 : a2) = nth 0 (a1 : 0)
105 nthZ 
nth 0 (a1 : a2) = suc a1
106 104, 105 ax_mp 
nth 0 (a1 : 0) = suc a1 -> nth 0 (a1 : a2) = nth 0 (a1 : 0)
107 nthZ 
nth 0 (a1 : 0) = suc a1
108 106, 107 ax_mp 
nth 0 (a1 : a2) = nth 0 (a1 : 0)
109 103, 108 ax_mp 
nth (suc (len a2) - suc (len a2)) (a1 : a2) = nth 0 (a1 : 0)
110 98, 109 ax_mp 
nth (len (rev a2) + 0) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2)
111 94, 110 ax_mp 
nth (len a2) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2)
112 id 
i = len a2 -> i = len a2
113 112 ntheq1d 
i = len a2 -> nth i (rev a2 |> a1) = nth (len a2) (rev a2 |> a1)
114 112 suceqd 
i = len a2 -> suc i = suc (len a2)
115 114 subeq2d 
i = len a2 -> suc (len a2) - suc i = suc (len a2) - suc (len a2)
116 115 ntheq1d 
i = len a2 -> nth (suc (len a2) - suc i) (a1 : a2) = nth (suc (len a2) - suc (len a2)) (a1 : a2)
117 113, 116 eqeqd 
i = len a2 -> (nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2) <-> nth (len a2) (rev a2 |> a1) = nth (suc (len a2) - suc (len a2)) (a1 : a2))
118 111, 117 mpbiri 
i = len a2 -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
119 118 a1d 
i = len a2 -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
120 84, 119 ax_mp 
i < len a2 \/ i = len a2 -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
121 61, 120 sylbi 
i <= len a2 -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev a2 |> a1) = nth (suc (len a2) - suc i) (a1 : a2)
122 60, 121 syl6ibr 
i <= len a2 -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev (a1 : a2)) = nth (len (a1 : a2) - suc i) (a1 : a2)
123 50, 122 sylbi 
i < len (a1 : a2) -> (i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> nth i (rev (a1 : a2)) = nth (len (a1 : a2) - suc i) (a1 : a2)
124 123 com12 
(i < len a2 -> nth i (rev a2) = nth (len a2 - suc i) a2) -> i < len (a1 : a2) -> nth i (rev (a1 : a2)) = nth (len (a1 : a2) - suc i) (a1 : a2)
125 9, 18, 27, 36, 43, 124 listind 
i < len l -> nth i (rev l) = nth (len l - suc i) 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)