Theorem b0ins ≪ | index | src | ≫ 

theorem b0ins (a b: nat): $ b0 (a ; b) = suc a ; b0 b $;
StepHypRefExpression
1 axext 
b0 (a ; b) == suc a ; b0 b -> b0 (a ; b) = suc a ; b0 b
2 elb0 
x e. b0 (a ; b) <-> 0 < x /\ x - 1 e. a ; b
3 bitr 
(x e. suc a ; b0 b <-> x = suc a \/ x e. b0 b) ->
  (x = suc a \/ x e. b0 b <-> x = suc a \/ 0 < x /\ x - 1 e. b) ->
  (x e. suc a ; b0 b <-> x = suc a \/ 0 < x /\ x - 1 e. b)
4 elins 
x e. suc a ; b0 b <-> x = suc a \/ x e. b0 b
5 3, 4 ax_mp 
(x = suc a \/ x e. b0 b <-> x = suc a \/ 0 < x /\ x - 1 e. b) -> (x e. suc a ; b0 b <-> x = suc a \/ 0 < x /\ x - 1 e. b)
6 oreq2 
(x e. b0 b <-> 0 < x /\ x - 1 e. b) -> (x = suc a \/ x e. b0 b <-> x = suc a \/ 0 < x /\ x - 1 e. b)
7 elb0 
x e. b0 b <-> 0 < x /\ x - 1 e. b
8 6, 7 ax_mp 
x = suc a \/ x e. b0 b <-> x = suc a \/ 0 < x /\ x - 1 e. b
9 5, 8 ax_mp 
x e. suc a ; b0 b <-> x = suc a \/ 0 < x /\ x - 1 e. b
10 anl 
0 < x /\ x - 1 e. a ; b -> 0 < x
11 eor 
(x = suc a -> 0 < x) -> (0 < x /\ x - 1 e. b -> 0 < x) -> x = suc a \/ 0 < x /\ x - 1 e. b -> 0 < x
12 lt01S 
0 < suc a
13 lteq2 
x = suc a -> (0 < x <-> 0 < suc a)
14 12, 13 mpbiri 
x = suc a -> 0 < x
15 11, 14 ax_mp 
(0 < x /\ x - 1 e. b -> 0 < x) -> x = suc a \/ 0 < x /\ x - 1 e. b -> 0 < x
16 anl 
0 < x /\ x - 1 e. b -> 0 < x
17 15, 16 ax_mp 
x = suc a \/ 0 < x /\ x - 1 e. b -> 0 < x
18 bian1 
0 < x -> (0 < x /\ x - 1 e. a ; b <-> x - 1 e. a ; b)
19 elins 
x - 1 e. a ; b <-> x - 1 = a \/ x - 1 e. b
20 peano2 
suc (x - 1) = suc a <-> x - 1 = a
21 lt01 
0 < x <-> x != 0
22 sub1can 
x != 0 -> suc (x - 1) = x
23 21, 22 sylbi 
0 < x -> suc (x - 1) = x
24 23 eqeq1d 
0 < x -> (suc (x - 1) = suc a <-> x = suc a)
25 20, 24 syl5bbr 
0 < x -> (x - 1 = a <-> x = suc a)
26 bian1 
0 < x -> (0 < x /\ x - 1 e. b <-> x - 1 e. b)
27 26 bicomd 
0 < x -> (x - 1 e. b <-> 0 < x /\ x - 1 e. b)
28 25, 27 oreqd 
0 < x -> (x - 1 = a \/ x - 1 e. b <-> x = suc a \/ 0 < x /\ x - 1 e. b)
29 19, 28 syl5bb 
0 < x -> (x - 1 e. a ; b <-> x = suc a \/ 0 < x /\ x - 1 e. b)
30 18, 29 bitrd 
0 < x -> (0 < x /\ x - 1 e. a ; b <-> x = suc a \/ 0 < x /\ x - 1 e. b)
31 10, 17, 30 rbid 
0 < x /\ x - 1 e. a ; b <-> x = suc a \/ 0 < x /\ x - 1 e. b
32 2, 9, 31 bitr4gi 
x e. b0 (a ; b) <-> x e. suc a ; b0 b
33 32 ax_gen 
A. x (x e. b0 (a ; b) <-> x e. suc a ; b0 b)
34 33 conv eqs 
b0 (a ; b) == suc a ; b0 b
35 1, 34 ax_mp 
b0 (a ; b) = suc a ; b0 b

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)