Theorem zb0orb0 ≪ | index | src | ≫ 

theorem zb0orb0 (a: nat): $ a = b0 (zabs a) \/ a = -uZ b0 (zabs a) $;
StepHypRefExpression
1 oreq 
(0 <=Z a <-> a = b0 (zabs a)) -> (a <=Z 0 <-> a = -uZ b0 (zabs a)) -> (0 <=Z a \/ a <=Z 0 <-> a = b0 (zabs a) \/ a = -uZ b0 (zabs a))
2 bitr2 
(a = b0 (zabs a) <-> b0 (zabs a) = a) -> (b0 (zabs a) = a <-> 0 <=Z a) -> (0 <=Z a <-> a = b0 (zabs a))
3 eqcomb 
a = b0 (zabs a) <-> b0 (zabs a) = a
4 2, 3 ax_mp 
(b0 (zabs a) = a <-> 0 <=Z a) -> (0 <=Z a <-> a = b0 (zabs a))
5 b0zabs 
b0 (zabs a) = a <-> 0 <=Z a
6 4, 5 ax_mp 
0 <=Z a <-> a = b0 (zabs a)
7 1, 6 ax_mp 
(a <=Z 0 <-> a = -uZ b0 (zabs a)) -> (0 <=Z a \/ a <=Z 0 <-> a = b0 (zabs a) \/ a = -uZ b0 (zabs a))
8 bitr3 
(0 <=Z -uZ a <-> a <=Z 0) -> (0 <=Z -uZ a <-> a = -uZ b0 (zabs a)) -> (a <=Z 0 <-> a = -uZ b0 (zabs a))
9 zle0neg 
0 <=Z -uZ a <-> a <=Z 0
10 8, 9 ax_mp 
(0 <=Z -uZ a <-> a = -uZ b0 (zabs a)) -> (a <=Z 0 <-> a = -uZ b0 (zabs a))
11 bitr3 
(b0 (zabs (-uZ a)) = -uZ a <-> 0 <=Z -uZ a) -> (b0 (zabs (-uZ a)) = -uZ a <-> a = -uZ b0 (zabs a)) -> (0 <=Z -uZ a <-> a = -uZ b0 (zabs a))
12 b0zabs 
b0 (zabs (-uZ a)) = -uZ a <-> 0 <=Z -uZ a
13 11, 12 ax_mp 
(b0 (zabs (-uZ a)) = -uZ a <-> a = -uZ b0 (zabs a)) -> (0 <=Z -uZ a <-> a = -uZ b0 (zabs a))
14 bitr 
(b0 (zabs (-uZ a)) = -uZ a <-> b0 (zabs a) = -uZ a) -> (b0 (zabs a) = -uZ a <-> a = -uZ b0 (zabs a)) -> (b0 (zabs (-uZ a)) = -uZ a <-> a = -uZ b0 (zabs a))
15 eqeq1 
b0 (zabs (-uZ a)) = b0 (zabs a) -> (b0 (zabs (-uZ a)) = -uZ a <-> b0 (zabs a) = -uZ a)
16 b0eq 
zabs (-uZ a) = zabs a -> b0 (zabs (-uZ a)) = b0 (zabs a)
17 zabsneg 
zabs (-uZ a) = zabs a
18 16, 17 ax_mp 
b0 (zabs (-uZ a)) = b0 (zabs a)
19 15, 18 ax_mp 
b0 (zabs (-uZ a)) = -uZ a <-> b0 (zabs a) = -uZ a
20 14, 19 ax_mp 
(b0 (zabs a) = -uZ a <-> a = -uZ b0 (zabs a)) -> (b0 (zabs (-uZ a)) = -uZ a <-> a = -uZ b0 (zabs a))
21 eqznegcom 
b0 (zabs a) = -uZ a <-> a = -uZ b0 (zabs a)
22 20, 21 ax_mp 
b0 (zabs (-uZ a)) = -uZ a <-> a = -uZ b0 (zabs a)
23 13, 22 ax_mp 
0 <=Z -uZ a <-> a = -uZ b0 (zabs a)
24 10, 23 ax_mp 
a <=Z 0 <-> a = -uZ b0 (zabs a)
25 7, 24 ax_mp 
0 <=Z a \/ a <=Z 0 <-> a = b0 (zabs a) \/ a = -uZ b0 (zabs a)
26 zleorle 
0 <=Z a \/ a <=Z 0
27 25, 26 mpbi 
a = b0 (zabs a) \/ a = -uZ b0 (zabs 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)