Theorem elb1 ≪ | index | src | ≫ 

theorem elb1 (a b: nat): $ a e. b1 b <-> a = 0 \/ a - 1 e. b $;
StepHypRefExpression
1 el01 
0 e. b1 b <-> odd (b1 b)
2 b1odd 
odd (b1 b)
3 1, 2 mpbir 
0 e. b1 b
4 eleq1 
a = 0 -> (a e. b1 b <-> 0 e. b1 b)
5 3, 4 mpbiri 
a = 0 -> a e. b1 b
6 orl 
a = 0 -> a = 0 \/ a - 1 e. b
7 5, 6 bithd 
a = 0 -> (a e. b1 b <-> a = 0 \/ a - 1 e. b)
8 bior1 
~a = 0 -> (a = 0 \/ a - 1 e. b <-> a - 1 e. b)
9 bitr3 
(a - 1 e. b1 b // 2 <-> a - 1 e. b) -> (a - 1 e. b1 b // 2 <-> suc (a - 1) e. b1 b) -> (a - 1 e. b <-> suc (a - 1) e. b1 b)
10 elneq2 
b1 b // 2 = b -> (a - 1 e. b1 b // 2 <-> a - 1 e. b)
11 b1div2 
b1 b // 2 = b
12 10, 11 ax_mp 
a - 1 e. b1 b // 2 <-> a - 1 e. b
13 9, 12 ax_mp 
(a - 1 e. b1 b // 2 <-> suc (a - 1) e. b1 b) -> (a - 1 e. b <-> suc (a - 1) e. b1 b)
14 eldiv2 
a - 1 e. b1 b // 2 <-> suc (a - 1) e. b1 b
15 13, 14 ax_mp 
a - 1 e. b <-> suc (a - 1) e. b1 b
16 sub1can 
a != 0 -> suc (a - 1) = a
17 16 conv ne 
~a = 0 -> suc (a - 1) = a
18 17 eleq1d 
~a = 0 -> (suc (a - 1) e. b1 b <-> a e. b1 b)
19 15, 18 syl5bb 
~a = 0 -> (a - 1 e. b <-> a e. b1 b)
20 8, 19 bitrd 
~a = 0 -> (a = 0 \/ a - 1 e. b <-> a e. b1 b)
21 20 bicomd 
~a = 0 -> (a e. b1 b <-> a = 0 \/ a - 1 e. b)
22 7, 21 cases 
a e. b1 b <-> a = 0 \/ a - 1 e. 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)