Theorem znegzn | index | src |

theorem znegzn (a b: nat): $ -uZ (a -ZN b) = b -ZN a $;
StepHypRefExpression
1 zneqb
zsnd (a -ZN b) -ZN zfst (a -ZN b) = b -ZN a <-> zsnd (a -ZN b) + a = b + zfst (a -ZN b)
2 1 conv zneg
-uZ (a -ZN b) = b -ZN a <-> zsnd (a -ZN b) + a = b + zfst (a -ZN b)
3 eqtr
zsnd (a -ZN b) + a = a + zsnd (a -ZN b) -> a + zsnd (a -ZN b) = b + zfst (a -ZN b) -> zsnd (a -ZN b) + a = b + zfst (a -ZN b)
4 addcom
zsnd (a -ZN b) + a = a + zsnd (a -ZN b)
5 3, 4 ax_mp
a + zsnd (a -ZN b) = b + zfst (a -ZN b) -> zsnd (a -ZN b) + a = b + zfst (a -ZN b)
6 eqtr3
zfst (a -ZN b) + b = a + zsnd (a -ZN b) -> zfst (a -ZN b) + b = b + zfst (a -ZN b) -> a + zsnd (a -ZN b) = b + zfst (a -ZN b)
7 zneqb
zfst (a -ZN b) -ZN zsnd (a -ZN b) = a -ZN b <-> zfst (a -ZN b) + b = a + zsnd (a -ZN b)
8 zfstsnd
zfst (a -ZN b) -ZN zsnd (a -ZN b) = a -ZN b
9 7, 8 mpbi
zfst (a -ZN b) + b = a + zsnd (a -ZN b)
10 6, 9 ax_mp
zfst (a -ZN b) + b = b + zfst (a -ZN b) -> a + zsnd (a -ZN b) = b + zfst (a -ZN b)
11 addcom
zfst (a -ZN b) + b = b + zfst (a -ZN b)
12 10, 11 ax_mp
a + zsnd (a -ZN b) = b + zfst (a -ZN b)
13 5, 12 ax_mp
zsnd (a -ZN b) + a = b + zfst (a -ZN b)
14 2, 13 mpbir
-uZ (a -ZN b) = b -ZN 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)