Theorem lemul1a ≪ | index | src | ≫ 

theorem lemul1a (a b c: nat): $ a <= b -> a * c <= b * c $;
StepHypRefExpression
1 eqidd 
x = c -> a = a
2 id 
x = c -> x = c
3 1, 2 muleqd 
x = c -> a * x = a * c
4 eqidd 
x = c -> b = b
5 4, 2 muleqd 
x = c -> b * x = b * c
6 3, 5 leeqd 
x = c -> (a * x <= b * x <-> a * c <= b * c)
7 eqidd 
x = 0 -> a = a
8 id 
x = 0 -> x = 0
9 7, 8 muleqd 
x = 0 -> a * x = a * 0
10 eqidd 
x = 0 -> b = b
11 10, 8 muleqd 
x = 0 -> b * x = b * 0
12 9, 11 leeqd 
x = 0 -> (a * x <= b * x <-> a * 0 <= b * 0)
13 eqidd 
x = y -> a = a
14 id 
x = y -> x = y
15 13, 14 muleqd 
x = y -> a * x = a * y
16 eqidd 
x = y -> b = b
17 16, 14 muleqd 
x = y -> b * x = b * y
18 15, 17 leeqd 
x = y -> (a * x <= b * x <-> a * y <= b * y)
19 eqidd 
x = suc y -> a = a
20 id 
x = suc y -> x = suc y
21 19, 20 muleqd 
x = suc y -> a * x = a * suc y
22 eqidd 
x = suc y -> b = b
23 22, 20 muleqd 
x = suc y -> b * x = b * suc y
24 21, 23 leeqd 
x = suc y -> (a * x <= b * x <-> a * suc y <= b * suc y)
25 eqle 
a * 0 = b * 0 -> a * 0 <= b * 0
26 eqtr4 
a * 0 = 0 -> b * 0 = 0 -> a * 0 = b * 0
27 mul0 
a * 0 = 0
28 26, 27 ax_mp 
b * 0 = 0 -> a * 0 = b * 0
29 mul0 
b * 0 = 0
30 28, 29 ax_mp 
a * 0 = b * 0
31 25, 30 ax_mp 
a * 0 <= b * 0
32 31 a1i 
a <= b -> a * 0 <= b * 0
33 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)
34 mulS 
a * suc y = a * y + a
35 33, 34 ax_mp 
b * suc y = b * y + b -> (a * suc y <= b * suc y <-> a * y + a <= b * y + b)
36 mulS 
b * suc y = b * y + b
37 35, 36 ax_mp 
a * suc y <= b * suc y <-> a * y + a <= b * y + b
38 anr 
a <= b /\ a * y <= b * y -> a * y <= b * y
39 anl 
a <= b /\ a * y <= b * y -> a <= b
40 38, 39 leaddd 
a <= b /\ a * y <= b * y -> a * y + a <= b * y + b
41 37, 40 sylibr 
a <= b /\ a * y <= b * y -> a * suc y <= b * suc y
42 6, 12, 18, 24, 32, 41 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)