Theorem znegadd2 ≪ | index | src | ≫ 

theorem znegadd2 (a b: nat): $ -uZ (a +Z b) = -uZ a -Z b $;
StepHypRefExpression
1 eqcom 
-uZ a -Z b = -uZ (a +Z b) -> -uZ (a +Z b) = -uZ a -Z b
2 eqzsub 
-uZ a -Z b = -uZ (a +Z b) <-> -uZ (a +Z b) +Z b = -uZ a
3 eqtr 
-uZ (a +Z b) +Z b = b +Z -uZ (a +Z b) -> b +Z -uZ (a +Z b) = -uZ a -> -uZ (a +Z b) +Z b = -uZ a
4 zaddcom 
-uZ (a +Z b) +Z b = b +Z -uZ (a +Z b)
5 3, 4 ax_mp 
b +Z -uZ (a +Z b) = -uZ a -> -uZ (a +Z b) +Z b = -uZ a
6 eqzsub 
b -Z (a +Z b) = -uZ a <-> -uZ a +Z (a +Z b) = b
7 6 conv zsub 
b +Z -uZ (a +Z b) = -uZ a <-> -uZ a +Z (a +Z b) = b
8 eqtr 
-uZ a +Z (a +Z b) = a +Z b +Z -uZ a -> a +Z b +Z -uZ a = b -> -uZ a +Z (a +Z b) = b
9 zaddcom 
-uZ a +Z (a +Z b) = a +Z b +Z -uZ a
10 8, 9 ax_mp 
a +Z b +Z -uZ a = b -> -uZ a +Z (a +Z b) = b
11 zpncan2 
a +Z b -Z a = b
12 11 conv zsub 
a +Z b +Z -uZ a = b
13 10, 12 ax_mp 
-uZ a +Z (a +Z b) = b
14 7, 13 mpbir 
b +Z -uZ (a +Z b) = -uZ a
15 5, 14 ax_mp 
-uZ (a +Z b) +Z b = -uZ a
16 2, 15 mpbir 
-uZ a -Z b = -uZ (a +Z b)
17 1, 16 ax_mp 
-uZ (a +Z b) = -uZ a -Z 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)