Theorem modmodid | index | src |

theorem modmodid (a n: nat): $ a % n % n = a % n $;
StepHypRefExpression
1 mod0
a % 0 = a
2 modeq2
n = 0 -> a % n = a % 0
3 1, 2 syl6eq
n = 0 -> a % n = a
4 eqidd
n = 0 -> n = n
5 3, 4 modeqd
n = 0 -> a % n % n = a % n
6 modlteq
a % n < n -> a % n % n = a % n
7 modlt
n != 0 -> a % n < n
8 7 conv ne
~n = 0 -> a % n < n
9 6, 8 syl
~n = 0 -> a % n % n = a % n
10 5, 9 cases
a % n % n = a % 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)