Theorem lemul1a ≪ | index | src | ≫ 

theorem lemul1a (a b c: nat): $ a <= b -> a * c <= b * c $;
StepHypRefExpression
1 id 
x = c -> x = c
2 1 muleq2d 
x = c -> a * x = a * c
3 1 muleq2d 
x = c -> b * x = b * c
4 2, 3 leeqd 
x = c -> (a * x <= b * x <-> a * c <= b * c)
5 id 
x = 0 -> x = 0
6 5 muleq2d 
x = 0 -> a * x = a * 0
7 5 muleq2d 
x = 0 -> b * x = b * 0
8 6, 7 leeqd 
x = 0 -> (a * x <= b * x <-> a * 0 <= b * 0)
9 id 
x = y -> x = y
10 9 muleq2d 
x = y -> a * x = a * y
11 9 muleq2d 
x = y -> b * x = b * y
12 10, 11 leeqd 
x = y -> (a * x <= b * x <-> a * y <= b * y)
13 id 
x = suc y -> x = suc y
14 13 muleq2d 
x = suc y -> a * x = a * suc y
15 13 muleq2d 
x = suc y -> b * x = b * suc y
16 14, 15 leeqd 
x = suc y -> (a * x <= b * x <-> a * suc y <= b * suc y)
17 eqle 
a * 0 = b * 0 -> a * 0 <= b * 0
18 eqtr4 
a * 0 = 0 -> b * 0 = 0 -> a * 0 = b * 0
19 mul0 
a * 0 = 0
20 18, 19 ax_mp 
b * 0 = 0 -> a * 0 = b * 0
21 mul0 
b * 0 = 0
22 20, 21 ax_mp 
a * 0 = b * 0
23 17, 22 ax_mp 
a * 0 <= b * 0
24 23 a1i 
a <= b -> a * 0 <= b * 0
25 leeq 
a * suc y = a * y + a -> b * suc y = b * y + b -> (a * suc y <= b * suc y <-> a * y + a <= b * y + b)
26 mulS 
a * suc y = a * y + a
27 25, 26 ax_mp 
b * suc y = b * y + b -> (a * suc y <= b * suc y <-> a * y + a <= b * y + b)
28 mulS 
b * suc y = b * y + b
29 27, 28 ax_mp 
a * suc y <= b * suc y <-> a * y + a <= b * y + b
30 anr 
a <= b /\ a * y <= b * y -> a * y <= b * y
31 anl 
a <= b /\ a * y <= b * y -> a <= b
32 30, 31 leaddd 
a <= b /\ a * y <= b * y -> a * y + a <= b * y + b
33 29, 32 sylibr 
a <= b /\ a * y <= b * y -> a * suc y <= b * suc y
34 4, 8, 12, 16, 24, 33 indd 
a <= b -> a * c <= b * 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_peano (peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)