Theorem sreclem2 ≪ | index | src | ≫ 

theorem sreclem2 (f n: nat) {x: nat} (a b: nat x):
  $ f = \. x e. upto n, a -> b < n -> f @ b = N[b / x] a $;
StepHypRefExpression
1 applams 
(\ x, a) @ b = N[b / x] a
2 eqlower2 
finite ((\ x, a) |` upto n) -> (f == (\ x, a) |` upto n <-> f = lower ((\ x, a) |` upto n))
3 finlam 
finite (upto n) -> finite ((\ x, a) |` upto n)
4 finns 
finite (upto n)
5 3, 4 ax_mp 
finite ((\ x, a) |` upto n)
6 2, 5 ax_mp 
f == (\ x, a) |` upto n <-> f = lower ((\ x, a) |` upto n)
7 anl 
f = \. x e. upto n, a /\ b < n -> f = \. x e. upto n, a
8 7 conv rlam 
f = \. x e. upto n, a /\ b < n -> f = lower ((\ x, a) |` upto n)
9 6, 8 sylibr 
f = \. x e. upto n, a /\ b < n -> f == (\ x, a) |` upto n
10 9 appeq1d 
f = \. x e. upto n, a /\ b < n -> f @ b = ((\ x, a) |` upto n) @ b
11 resapp 
b e. upto n -> ((\ x, a) |` upto n) @ b = (\ x, a) @ b
12 elupto 
b e. upto n <-> b < n
13 anr 
f = \. x e. upto n, a /\ b < n -> b < n
14 12, 13 sylibr 
f = \. x e. upto n, a /\ b < n -> b e. upto n
15 11, 14 syl 
f = \. x e. upto n, a /\ b < n -> ((\ x, a) |` upto n) @ b = (\ x, a) @ b
16 10, 15 eqtrd 
f = \. x e. upto n, a /\ b < n -> f @ b = (\ x, a) @ b
17 1, 16 syl6eq 
f = \. x e. upto n, a /\ b < n -> f @ b = N[b / x] a
18 17 exp 
f = \. x e. upto n, a -> b < n -> f @ b = N[b / x] a

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)