Step | Hyp | Ref | Expression |
1 |
|
eqtr |
grecaux1 K x k (suc n) = (\\ a1, \ a2, K @ (x - suc a1, a2)) @ (n, recn k (\\ a1, \ a2, K @ (x - suc a1, a2)) n) ->
(\\ a1, \ a2, K @ (x - suc a1, a2)) @ (n, recn k (\\ a1, \ a2, K @ (x - suc a1, a2)) n) = K @ (x - suc n, grecaux1 K x k n) ->
grecaux1 K x k (suc n) = K @ (x - suc n, grecaux1 K x k n) |
2 |
|
recnS |
recn k (\\ a1, \ a2, K @ (x - suc a1, a2)) (suc n) = (\\ a1, \ a2, K @ (x - suc a1, a2)) @ (n, recn k (\\ a1, \ a2, K @ (x - suc a1, a2)) n) |
3 |
2 |
conv grecaux1 |
grecaux1 K x k (suc n) = (\\ a1, \ a2, K @ (x - suc a1, a2)) @ (n, recn k (\\ a1, \ a2, K @ (x - suc a1, a2)) n) |
4 |
1, 3 |
ax_mp |
(\\ a1, \ a2, K @ (x - suc a1, a2)) @ (n, recn k (\\ a1, \ a2, K @ (x - suc a1, a2)) n) = K @ (x - suc n, grecaux1 K x k n) ->
grecaux1 K x k (suc n) = K @ (x - suc n, grecaux1 K x k n) |
5 |
|
anl |
a1 = n /\ a2 = grecaux1 K x k n -> a1 = n |
6 |
5 |
suceqd |
a1 = n /\ a2 = grecaux1 K x k n -> suc a1 = suc n |
7 |
6 |
subeq2d |
a1 = n /\ a2 = grecaux1 K x k n -> x - suc a1 = x - suc n |
8 |
|
anr |
a1 = n /\ a2 = grecaux1 K x k n -> a2 = grecaux1 K x k n |
9 |
7, 8 |
preqd |
a1 = n /\ a2 = grecaux1 K x k n -> x - suc a1, a2 = x - suc n, grecaux1 K x k n |
10 |
9 |
appeq2d |
a1 = n /\ a2 = grecaux1 K x k n -> K @ (x - suc a1, a2) = K @ (x - suc n, grecaux1 K x k n) |
11 |
10 |
applamed |
a1 = n -> (\ a2, K @ (x - suc a1, a2)) @ grecaux1 K x k n = K @ (x - suc n, grecaux1 K x k n) |
12 |
11 |
appslame |
(\\ a1, \ a2, K @ (x - suc a1, a2)) @ (n, grecaux1 K x k n) = K @ (x - suc n, grecaux1 K x k n) |
13 |
12 |
conv grecaux1 |
(\\ a1, \ a2, K @ (x - suc a1, a2)) @ (n, recn k (\\ a1, \ a2, K @ (x - suc a1, a2)) n) = K @ (x - suc n, grecaux1 K x k n) |
14 |
4, 13 |
ax_mp |
grecaux1 K x k (suc n) = K @ (x - suc n, grecaux1 K x k n) |