Theorem uptoS_ins ≪ | index | src | ≫ 

theorem uptoS_ins (a: nat): $ upto (suc a) = a ; upto a $;
StepHypRefExpression
1 axext 
upto (suc a) == a ; upto a -> upto (suc a) = a ; upto a
2 bitr4 
(x e. upto (suc a) <-> x < suc a) -> (x e. a ; upto a <-> x < suc a) -> (x e. upto (suc a) <-> x e. a ; upto a)
3 elupto 
x e. upto (suc a) <-> x < suc a
4 2, 3 ax_mp 
(x e. a ; upto a <-> x < suc a) -> (x e. upto (suc a) <-> x e. a ; upto a)
5 bitr4 
(x e. a ; upto a <-> x = a \/ x e. upto a) -> (x < suc a <-> x = a \/ x e. upto a) -> (x e. a ; upto a <-> x < suc a)
6 elins 
x e. a ; upto a <-> x = a \/ x e. upto a
7 5, 6 ax_mp 
(x < suc a <-> x = a \/ x e. upto a) -> (x e. a ; upto a <-> x < suc a)
8 bitr3 
(x <= a <-> x < suc a) -> (x <= a <-> x = a \/ x e. upto a) -> (x < suc a <-> x = a \/ x e. upto a)
9 leltsuc 
x <= a <-> x < suc a
10 8, 9 ax_mp 
(x <= a <-> x = a \/ x e. upto a) -> (x < suc a <-> x = a \/ x e. upto a)
11 bitr4 
(x <= a <-> x < a \/ x = a) -> (x = a \/ x e. upto a <-> x < a \/ x = a) -> (x <= a <-> x = a \/ x e. upto a)
12 leloe 
x <= a <-> x < a \/ x = a
13 11, 12 ax_mp 
(x = a \/ x e. upto a <-> x < a \/ x = a) -> (x <= a <-> x = a \/ x e. upto a)
14 bitr 
(x = a \/ x e. upto a <-> x e. upto a \/ x = a) -> (x e. upto a \/ x = a <-> x < a \/ x = a) -> (x = a \/ x e. upto a <-> x < a \/ x = a)
15 orcomb 
x = a \/ x e. upto a <-> x e. upto a \/ x = a
16 14, 15 ax_mp 
(x e. upto a \/ x = a <-> x < a \/ x = a) -> (x = a \/ x e. upto a <-> x < a \/ x = a)
17 oreq1 
(x e. upto a <-> x < a) -> (x e. upto a \/ x = a <-> x < a \/ x = a)
18 elupto 
x e. upto a <-> x < a
19 17, 18 ax_mp 
x e. upto a \/ x = a <-> x < a \/ x = a
20 16, 19 ax_mp 
x = a \/ x e. upto a <-> x < a \/ x = a
21 13, 20 ax_mp 
x <= a <-> x = a \/ x e. upto a
22 10, 21 ax_mp 
x < suc a <-> x = a \/ x e. upto a
23 7, 22 ax_mp 
x e. a ; upto a <-> x < suc a
24 4, 23 ax_mp 
x e. upto (suc a) <-> x e. a ; upto a
25 24 ax_gen 
A. x (x e. upto (suc a) <-> x e. a ; upto a)
26 25 conv eqs 
upto (suc a) == a ; upto a
27 1, 26 ax_mp 
upto (suc a) = a ; upto 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)