Theorem srecauxapp ≪ | index | src | ≫ 

theorem srecauxapp (S: set) (a n: nat): $ a < n -> srecaux S n @ a = srec S a $;
StepHypRefExpression
1 id 
x = n -> x = n
2 1 lteq2d 
x = n -> (a < x <-> a < n)
3 1 srecauxeq2d 
x = n -> srecaux S x = srecaux S n
4 3 nseqd 
x = n -> srecaux S x == srecaux S n
5 4 appeq1d 
x = n -> srecaux S x @ a = srecaux S n @ a
6 5 eqeq1d 
x = n -> (srecaux S x @ a = srec S a <-> srecaux S n @ a = srec S a)
7 2, 6 imeqd 
x = n -> (a < x -> srecaux S x @ a = srec S a <-> a < n -> srecaux S n @ a = srec S a)
8 id 
x = 0 -> x = 0
9 8 lteq2d 
x = 0 -> (a < x <-> a < 0)
10 8 srecauxeq2d 
x = 0 -> srecaux S x = srecaux S 0
11 10 nseqd 
x = 0 -> srecaux S x == srecaux S 0
12 11 appeq1d 
x = 0 -> srecaux S x @ a = srecaux S 0 @ a
13 12 eqeq1d 
x = 0 -> (srecaux S x @ a = srec S a <-> srecaux S 0 @ a = srec S a)
14 9, 13 imeqd 
x = 0 -> (a < x -> srecaux S x @ a = srec S a <-> a < 0 -> srecaux S 0 @ a = srec S a)
15 id 
x = y -> x = y
16 15 lteq2d 
x = y -> (a < x <-> a < y)
17 15 srecauxeq2d 
x = y -> srecaux S x = srecaux S y
18 17 nseqd 
x = y -> srecaux S x == srecaux S y
19 18 appeq1d 
x = y -> srecaux S x @ a = srecaux S y @ a
20 19 eqeq1d 
x = y -> (srecaux S x @ a = srec S a <-> srecaux S y @ a = srec S a)
21 16, 20 imeqd 
x = y -> (a < x -> srecaux S x @ a = srec S a <-> a < y -> srecaux S y @ a = srec S a)
22 id 
x = suc y -> x = suc y
23 22 lteq2d 
x = suc y -> (a < x <-> a < suc y)
24 22 srecauxeq2d 
x = suc y -> srecaux S x = srecaux S (suc y)
25 24 nseqd 
x = suc y -> srecaux S x == srecaux S (suc y)
26 25 appeq1d 
x = suc y -> srecaux S x @ a = srecaux S (suc y) @ a
27 26 eqeq1d 
x = suc y -> (srecaux S x @ a = srec S a <-> srecaux S (suc y) @ a = srec S a)
28 23, 27 imeqd 
x = suc y -> (a < x -> srecaux S x @ a = srec S a <-> a < suc y -> srecaux S (suc y) @ a = srec S a)
29 absurd 
~a < 0 -> a < 0 -> srecaux S 0 @ a = srec S a
30 lt02 
~a < 0
31 29, 30 ax_mp 
a < 0 -> srecaux S 0 @ a = srec S a
32 leltsuc 
a <= y <-> a < suc y
33 leloe 
a <= y <-> a < y \/ a = y
34 appeq1 
srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y) -> srecaux S (suc y) @ a = write (srecaux S y) y (S @ srecaux S y) @ a
35 srecauxS 
srecaux S (suc y) == write (srecaux S y) y (S @ srecaux S y)
36 34, 35 ax_mp 
srecaux S (suc y) @ a = write (srecaux S y) y (S @ srecaux S y) @ a
37 writeNe 
a != y -> write (srecaux S y) y (S @ srecaux S y) @ a = srecaux S y @ a
38 ltne 
a < y -> a != y
39 37, 38 syl 
a < y -> write (srecaux S y) y (S @ srecaux S y) @ a = srecaux S y @ a
40 36, 39 syl5eq 
a < y -> srecaux S (suc y) @ a = srecaux S y @ a
41 40 eqeq1d 
a < y -> (srecaux S (suc y) @ a = srec S a <-> srecaux S y @ a = srec S a)
42 41 bi2d 
a < y -> srecaux S y @ a = srec S a -> srecaux S (suc y) @ a = srec S a
43 42 a2i 
(a < y -> srecaux S y @ a = srec S a) -> a < y -> srecaux S (suc y) @ a = srec S a
44 eqcom 
a = y -> y = a
45 44 suceqd 
a = y -> suc y = suc a
46 45 srecauxeq2d 
a = y -> srecaux S (suc y) = srecaux S (suc a)
47 46 appneq1d 
a = y -> srecaux S (suc y) @ a = srecaux S (suc a) @ a
48 47 conv srec 
a = y -> srecaux S (suc y) @ a = srec S a
49 48 a1i 
(a < y -> srecaux S y @ a = srec S a) -> a = y -> srecaux S (suc y) @ a = srec S a
50 43, 49 eord 
(a < y -> srecaux S y @ a = srec S a) -> a < y \/ a = y -> srecaux S (suc y) @ a = srec S a
51 33, 50 syl5bi 
(a < y -> srecaux S y @ a = srec S a) -> a <= y -> srecaux S (suc y) @ a = srec S a
52 32, 51 syl5bir 
(a < y -> srecaux S y @ a = srec S a) -> a < suc y -> srecaux S (suc y) @ a = srec S a
53 7, 14, 21, 28, 31, 52 ind 
a < n -> srecaux S n @ a = srec S 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)