Theorem repeatT ≪ | index | src | ≫ 

theorem repeatT (A: set) (a n: nat): $ a e. A -> repeat a n e. List A $;
StepHypRefExpression
1 eqidd 
_1 = n -> a = a
2 id 
_1 = n -> _1 = n
3 1, 2 repeateqd 
_1 = n -> repeat a _1 = repeat a n
4 eqsidd 
_1 = n -> List A == List A
5 3, 4 eleqd 
_1 = n -> (repeat a _1 e. List A <-> repeat a n e. List A)
6 eqidd 
_1 = 0 -> a = a
7 id 
_1 = 0 -> _1 = 0
8 6, 7 repeateqd 
_1 = 0 -> repeat a _1 = repeat a 0
9 eqsidd 
_1 = 0 -> List A == List A
10 8, 9 eleqd 
_1 = 0 -> (repeat a _1 e. List A <-> repeat a 0 e. List A)
11 eqidd 
_1 = a1 -> a = a
12 id 
_1 = a1 -> _1 = a1
13 11, 12 repeateqd 
_1 = a1 -> repeat a _1 = repeat a a1
14 eqsidd 
_1 = a1 -> List A == List A
15 13, 14 eleqd 
_1 = a1 -> (repeat a _1 e. List A <-> repeat a a1 e. List A)
16 eqidd 
_1 = suc a1 -> a = a
17 id 
_1 = suc a1 -> _1 = suc a1
18 16, 17 repeateqd 
_1 = suc a1 -> repeat a _1 = repeat a (suc a1)
19 eqsidd 
_1 = suc a1 -> List A == List A
20 18, 19 eleqd 
_1 = suc a1 -> (repeat a _1 e. List A <-> repeat a (suc a1) e. List A)
21 eleq1 
repeat a 0 = 0 -> (repeat a 0 e. List A <-> 0 e. List A)
22 repeat0 
repeat a 0 = 0
23 21, 22 ax_mp 
repeat a 0 e. List A <-> 0 e. List A
24 elList0 
0 e. List A
25 23, 24 mpbir 
repeat a 0 e. List A
26 25 a1i 
a e. A -> repeat a 0 e. List A
27 bi2 
(repeat a (suc a1) e. List A <-> a e. A /\ repeat a a1 e. List A) -> a e. A /\ repeat a a1 e. List A -> repeat a (suc a1) e. List A
28 bitr 
(repeat a (suc a1) e. List A <-> a : repeat a a1 e. List A) ->
  (a : repeat a a1 e. List A <-> a e. A /\ repeat a a1 e. List A) ->
  (repeat a (suc a1) e. List A <-> a e. A /\ repeat a a1 e. List A)
29 eleq1 
repeat a (suc a1) = a : repeat a a1 -> (repeat a (suc a1) e. List A <-> a : repeat a a1 e. List A)
30 repeatS 
repeat a (suc a1) = a : repeat a a1
31 29, 30 ax_mp 
repeat a (suc a1) e. List A <-> a : repeat a a1 e. List A
32 28, 31 ax_mp 
(a : repeat a a1 e. List A <-> a e. A /\ repeat a a1 e. List A) -> (repeat a (suc a1) e. List A <-> a e. A /\ repeat a a1 e. List A)
33 elListS 
a : repeat a a1 e. List A <-> a e. A /\ repeat a a1 e. List A
34 32, 33 ax_mp 
repeat a (suc a1) e. List A <-> a e. A /\ repeat a a1 e. List A
35 27, 34 ax_mp 
a e. A /\ repeat a a1 e. List A -> repeat a (suc a1) e. List A
36 5, 10, 15, 20, 26, 35 indd 
a e. A -> repeat a n e. List 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)