Theorem eldiv2 ≪ | index | src | ≫ 

theorem eldiv2 (a b: nat): $ a e. b // 2 <-> suc a e. b $;
StepHypRefExpression
1 bitr3 
(a e. shr b 1 <-> a e. b // 2) -> (a e. shr b 1 <-> suc a e. b) -> (a e. b // 2 <-> suc a e. b)
2 elneq2 
shr b 1 = b // 2 -> (a e. shr b 1 <-> a e. b // 2)
3 shr12 
shr b 1 = b // 2
4 2, 3 ax_mp 
a e. shr b 1 <-> a e. b // 2
5 1, 4 ax_mp 
(a e. shr b 1 <-> suc a e. b) -> (a e. b // 2 <-> suc a e. b)
6 bitr 
(a e. shr b 1 <-> a + 1 e. b) -> (a + 1 e. b <-> suc a e. b) -> (a e. shr b 1 <-> suc a e. b)
7 elshr 
a e. shr b 1 <-> a + 1 e. b
8 6, 7 ax_mp 
(a + 1 e. b <-> suc a e. b) -> (a e. shr b 1 <-> suc a e. b)
9 eleq1 
a + 1 = suc a -> (a + 1 e. b <-> suc a e. b)
10 add12 
a + 1 = suc a
11 9, 10 ax_mp 
a + 1 e. b <-> suc a e. b
12 8, 11 ax_mp 
a e. shr b 1 <-> suc a e. b
13 5, 12 ax_mp 
a e. b // 2 <-> suc a 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)