Theorem zmulneg1 | index | src |

theorem zmulneg1 (a b: nat): $ -uZ a *Z b = -uZ (a *Z b) $;
StepHypRefExpression
1 eqtr3
(0 -Z a) *Z b = -uZ a *Z b -> (0 -Z a) *Z b = -uZ (a *Z b) -> -uZ a *Z b = -uZ (a *Z b)
2 zmuleq1
0 -Z a = -uZ a -> (0 -Z a) *Z b = -uZ a *Z b
3 zsub01
0 -Z a = -uZ a
4 2, 3 ax_mp
(0 -Z a) *Z b = -uZ a *Z b
5 1, 4 ax_mp
(0 -Z a) *Z b = -uZ (a *Z b) -> -uZ a *Z b = -uZ (a *Z b)
6 eqtr
(0 -Z a) *Z b = 0 *Z b -Z a *Z b -> 0 *Z b -Z a *Z b = -uZ (a *Z b) -> (0 -Z a) *Z b = -uZ (a *Z b)
7 zsubmul
(0 -Z a) *Z b = 0 *Z b -Z a *Z b
8 6, 7 ax_mp
0 *Z b -Z a *Z b = -uZ (a *Z b) -> (0 -Z a) *Z b = -uZ (a *Z b)
9 eqtr
0 *Z b -Z a *Z b = 0 -Z a *Z b -> 0 -Z a *Z b = -uZ (a *Z b) -> 0 *Z b -Z a *Z b = -uZ (a *Z b)
10 zsubeq1
0 *Z b = 0 -> 0 *Z b -Z a *Z b = 0 -Z a *Z b
11 zmul01
0 *Z b = 0
12 10, 11 ax_mp
0 *Z b -Z a *Z b = 0 -Z a *Z b
13 9, 12 ax_mp
0 -Z a *Z b = -uZ (a *Z b) -> 0 *Z b -Z a *Z b = -uZ (a *Z b)
14 zsub01
0 -Z a *Z b = -uZ (a *Z b)
15 13, 14 ax_mp
0 *Z b -Z a *Z b = -uZ (a *Z b)
16 8, 15 ax_mp
(0 -Z a) *Z b = -uZ (a *Z b)
17 5, 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)