Theorem insdiv2 ≪ | index | src | ≫ 

theorem insdiv2 (a b: nat): $ suc a ; b // 2 = a ; (b // 2) $;
StepHypRefExpression
1 eor 
(b = b0 (b // 2) -> suc a ; b // 2 = a ; (b // 2)) ->
  (b = b1 (b // 2) -> suc a ; b // 2 = a ; (b // 2)) ->
  b = b0 (b // 2) \/ b = b1 (b // 2) ->
  suc a ; b // 2 = a ; (b // 2)
2 b0div2 
b0 (a ; (b // 2)) // 2 = a ; (b // 2)
3 b0ins 
b0 (a ; (b // 2)) = suc a ; b0 (b // 2)
4 inseq2 
b = b0 (b // 2) -> suc a ; b = suc a ; b0 (b // 2)
5 3, 4 syl6eqr 
b = b0 (b // 2) -> suc a ; b = b0 (a ; (b // 2))
6 5 diveq1d 
b = b0 (b // 2) -> suc a ; b // 2 = b0 (a ; (b // 2)) // 2
7 2, 6 syl6eq 
b = b0 (b // 2) -> suc a ; b // 2 = a ; (b // 2)
8 1, 7 ax_mp 
(b = b1 (b // 2) -> suc a ; b // 2 = a ; (b // 2)) -> b = b0 (b // 2) \/ b = b1 (b // 2) -> suc a ; b // 2 = a ; (b // 2)
9 b1div2 
b1 (a ; (b // 2)) // 2 = a ; (b // 2)
10 b1ins 
b1 (a ; (b // 2)) = 0 ; b0 (a ; (b // 2))
11 inseq2 
b0 (a ; (b // 2)) = suc a ; b0 (b // 2) -> 0 ; b0 (a ; (b // 2)) = 0 ; suc a ; b0 (b // 2)
12 11, 3 ax_mp 
0 ; b0 (a ; (b // 2)) = 0 ; suc a ; b0 (b // 2)
13 inscom 
suc a ; 0 ; b0 (b // 2) = 0 ; suc a ; b0 (b // 2)
14 b1ins 
b1 (b // 2) = 0 ; b0 (b // 2)
15 id 
b = b1 (b // 2) -> b = b1 (b // 2)
16 14, 15 syl6eq 
b = b1 (b // 2) -> b = 0 ; b0 (b // 2)
17 16 inseq2d 
b = b1 (b // 2) -> suc a ; b = suc a ; 0 ; b0 (b // 2)
18 13, 17 syl6eq 
b = b1 (b // 2) -> suc a ; b = 0 ; suc a ; b0 (b // 2)
19 12, 18 syl6eqr 
b = b1 (b // 2) -> suc a ; b = 0 ; b0 (a ; (b // 2))
20 10, 19 syl6eqr 
b = b1 (b // 2) -> suc a ; b = b1 (a ; (b // 2))
21 20 diveq1d 
b = b1 (b // 2) -> suc a ; b // 2 = b1 (a ; (b // 2)) // 2
22 9, 21 syl6eq 
b = b1 (b // 2) -> suc a ; b // 2 = a ; (b // 2)
23 8, 22 ax_mp 
b = b0 (b // 2) \/ b = b1 (b // 2) -> suc a ; b // 2 = a ; (b // 2)
24 b0orb1 
b = b0 (b // 2) \/ b = b1 (b // 2)
25 23, 24 ax_mp 
suc a ; b // 2 = a ; (b // 2)

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)