Theorem zmodn02 | index | src |

theorem zmodn02 (a n: nat):
  $ n != 0 -> a %Z n = (zfst a + n - zsnd a % n) % n $;
StepHypRefExpression
1 zabsb0
zabs (b0 (zfst a + n - zsnd a % n)) = zfst a + n - zsnd a % n
2 znsubpos
zsnd a % n <= zfst a + n -> zfst a + n -ZN zsnd a % n = b0 (zfst a + n - zsnd a % n)
3 ltle
zsnd a % n < n -> zsnd a % n <= n
4 modlt
n != 0 -> zsnd a % n < n
5 3, 4 syl
n != 0 -> zsnd a % n <= n
6 leaddid2
n <= zfst a + n
7 6 a1i
n != 0 -> n <= zfst a + n
8 5, 7 letrd
n != 0 -> zsnd a % n <= zfst a + n
9 2, 8 syl
n != 0 -> zfst a + n -ZN zsnd a % n = b0 (zfst a + n - zsnd a % n)
10 9 zabseqd
n != 0 -> zabs (zfst a + n -ZN zsnd a % n) = zabs (b0 (zfst a + n - zsnd a % n))
11 1, 10 syl6eq
n != 0 -> zabs (zfst a + n -ZN zsnd a % n) = zfst a + n - zsnd a % n
12 11 modeq1d
n != 0 -> zabs (zfst a + n -ZN zsnd a % n) % n = (zfst a + n - zsnd a % n) % n
13 12 conv zmod
n != 0 -> a %Z n = (zfst a + n - zsnd a % n) % 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)