Theorem mulmoddi ≪ | index | src | ≫ 

theorem mulmoddi (a b c: nat): $ a * (b % c) = a * b % (a * c) $;
StepHypRefExpression
1 muleq1 
a = 0 -> a * (b % c) = 0 * (b % c)
2 mul01 
0 * (b % c) = 0
3 mod0 
0 % 0 = 0
4 mul01 
0 * b = 0
5 muleq1 
a = 0 -> a * b = 0 * b
6 4, 5 syl6eq 
a = 0 -> a * b = 0
7 mul01 
0 * c = 0
8 muleq1 
a = 0 -> a * c = 0 * c
9 7, 8 syl6eq 
a = 0 -> a * c = 0
10 6, 9 modeqd 
a = 0 -> a * b % (a * c) = 0 % 0
11 3, 10 syl6eq 
a = 0 -> a * b % (a * c) = 0
12 2, 11 syl6eqr 
a = 0 -> a * b % (a * c) = 0 * (b % c)
13 1, 12 eqtr4d 
a = 0 -> a * (b % c) = a * b % (a * c)
14 divmoddilem 
a != 0 -> a * b // (a * c) = b // c /\ a * b % (a * c) = a * (b % c)
15 14 conv ne 
~a = 0 -> a * b // (a * c) = b // c /\ a * b % (a * c) = a * (b % c)
16 15 anrd 
~a = 0 -> a * b % (a * c) = a * (b % c)
17 16 eqcomd 
~a = 0 -> a * (b % c) = a * b % (a * c)
18 13, 17 cases 
a * (b % c) = a * b % (a * c)

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)