Theorem b0zabs ≪ | index | src | ≫ 

theorem b0zabs (a: nat): $ b0 (zabs a) = a <-> 0 <=Z a $;
StepHypRefExpression
1 bitr 
(b0 (zabs a) = a <-> a = b0 (zabs a)) -> (a = b0 (zabs a) <-> 0 <=Z a) -> (b0 (zabs a) = a <-> 0 <=Z a)
2 eqcomb 
b0 (zabs a) = a <-> a = b0 (zabs a)
3 1, 2 ax_mp 
(a = b0 (zabs a) <-> 0 <=Z a) -> (b0 (zabs a) = a <-> 0 <=Z a)
4 zle0b0 
0 <=Z b0 (zabs a)
5 zleeq2 
a = b0 (zabs a) -> (0 <=Z a <-> 0 <=Z b0 (zabs a))
6 4, 5 mpbiri 
a = b0 (zabs a) -> 0 <=Z a
7 zle02eq 
0 <=Z a <-> a = b0 (a // 2)
8 id 
a = b0 (a // 2) -> a = b0 (a // 2)
9 zabsb0 
zabs (b0 (a // 2)) = a // 2
10 zabseq 
a = b0 (a // 2) -> zabs a = zabs (b0 (a // 2))
11 9, 10 syl6eq 
a = b0 (a // 2) -> zabs a = a // 2
12 11 b0eqd 
a = b0 (a // 2) -> b0 (zabs a) = b0 (a // 2)
13 8, 12 eqtr4d 
a = b0 (a // 2) -> a = b0 (zabs a)
14 7, 13 sylbi 
0 <=Z a -> a = b0 (zabs a)
15 6, 14 ibii 
a = b0 (zabs a) <-> 0 <=Z a
16 3, 15 ax_mp 
b0 (zabs a) = a <-> 0 <=Z 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)