Theorem zfstznsub | index | src |

theorem zfstznsub (m n: nat): $ zfst (m -ZN n) = m - n $;
StepHypRefExpression
1 zfstb1
zfst (b1 (n - suc m)) = 0
2 znsubneg
m < n -> m -ZN n = b1 (n - suc m)
3 2 zfsteqd
m < n -> zfst (m -ZN n) = zfst (b1 (n - suc m))
4 1, 3 syl6eq
m < n -> zfst (m -ZN n) = 0
5 ltsubeq0
m < n -> m - n = 0
6 4, 5 eqtr4d
m < n -> zfst (m -ZN n) = m - n
7 zfstb0
zfst (b0 (m - n)) = m - n
8 ifneg
~m < n -> if (m < n) (b1 (n - suc m)) (b0 (m - n)) = b0 (m - n)
9 8 conv znsub
~m < n -> m -ZN n = b0 (m - n)
10 9 zfsteqd
~m < n -> zfst (m -ZN n) = zfst (b0 (m - n))
11 7, 10 syl6eq
~m < n -> zfst (m -ZN n) = m - n
12 6, 11 cases
zfst (m -ZN n) = m - n

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)