Theorem ltmul1 ≪ | index | src | ≫ 

theorem ltmul1 (a b c: nat): $ 0 < c -> (a < b <-> a * c < b * c) $;
StepHypRefExpression
1 eqidd 
_1 = c -> 0 = 0
2 id 
_1 = c -> _1 = c
3 1, 2 lteqd 
_1 = c -> (0 < _1 <-> 0 < c)
4 eqidd 
_1 = c -> a = a
5 4, 2 muleqd 
_1 = c -> a * _1 = a * c
6 eqidd 
_1 = c -> b = b
7 6, 2 muleqd 
_1 = c -> b * _1 = b * c
8 5, 7 lteqd 
_1 = c -> (a * _1 < b * _1 <-> a * c < b * c)
9 3, 8 imeqd 
_1 = c -> (0 < _1 -> a * _1 < b * _1 <-> 0 < c -> a * c < b * c)
10 eqidd 
_1 = 0 -> 0 = 0
11 id 
_1 = 0 -> _1 = 0
12 10, 11 lteqd 
_1 = 0 -> (0 < _1 <-> 0 < 0)
13 eqidd 
_1 = 0 -> a = a
14 13, 11 muleqd 
_1 = 0 -> a * _1 = a * 0
15 eqidd 
_1 = 0 -> b = b
16 15, 11 muleqd 
_1 = 0 -> b * _1 = b * 0
17 14, 16 lteqd 
_1 = 0 -> (a * _1 < b * _1 <-> a * 0 < b * 0)
18 12, 17 imeqd 
_1 = 0 -> (0 < _1 -> a * _1 < b * _1 <-> 0 < 0 -> a * 0 < b * 0)
19 eqidd 
_1 = a1 -> 0 = 0
20 id 
_1 = a1 -> _1 = a1
21 19, 20 lteqd 
_1 = a1 -> (0 < _1 <-> 0 < a1)
22 eqidd 
_1 = a1 -> a = a
23 22, 20 muleqd 
_1 = a1 -> a * _1 = a * a1
24 eqidd 
_1 = a1 -> b = b
25 24, 20 muleqd 
_1 = a1 -> b * _1 = b * a1
26 23, 25 lteqd 
_1 = a1 -> (a * _1 < b * _1 <-> a * a1 < b * a1)
27 21, 26 imeqd 
_1 = a1 -> (0 < _1 -> a * _1 < b * _1 <-> 0 < a1 -> a * a1 < b * a1)
28 eqidd 
_1 = suc a1 -> 0 = 0
29 id 
_1 = suc a1 -> _1 = suc a1
30 28, 29 lteqd 
_1 = suc a1 -> (0 < _1 <-> 0 < suc a1)
31 eqidd 
_1 = suc a1 -> a = a
32 31, 29 muleqd 
_1 = suc a1 -> a * _1 = a * suc a1
33 eqidd 
_1 = suc a1 -> b = b
34 33, 29 muleqd 
_1 = suc a1 -> b * _1 = b * suc a1
35 32, 34 lteqd 
_1 = suc a1 -> (a * _1 < b * _1 <-> a * suc a1 < b * suc a1)
36 30, 35 imeqd 
_1 = suc a1 -> (0 < _1 -> a * _1 < b * _1 <-> 0 < suc a1 -> a * suc a1 < b * suc a1)
37 absurd 
~0 < 0 -> 0 < 0 -> a * 0 < b * 0
38 lt02 
~0 < 0
39 37, 38 ax_mp 
0 < 0 -> a * 0 < b * 0
40 39 a1i 
a < b -> 0 < 0 -> a * 0 < b * 0
41 lteq 
a * suc a1 = a * a1 + a -> b * suc a1 = b * a1 + b -> (a * suc a1 < b * suc a1 <-> a * a1 + a < b * a1 + b)
42 mulS 
a * suc a1 = a * a1 + a
43 41, 42 ax_mp 
b * suc a1 = b * a1 + b -> (a * suc a1 < b * suc a1 <-> a * a1 + a < b * a1 + b)
44 mulS 
b * suc a1 = b * a1 + b
45 43, 44 ax_mp 
a * suc a1 < b * suc a1 <-> a * a1 + a < b * a1 + b
46 bi1 
(a < b <-> a * a1 + a < a * a1 + b) -> a < b -> a * a1 + a < a * a1 + b
47 ltadd2 
a < b <-> a * a1 + a < a * a1 + b
48 46, 47 ax_mp 
a < b -> a * a1 + a < a * a1 + b
49 leadd1 
a * a1 <= b * a1 <-> a * a1 + b <= b * a1 + b
50 lemul1a 
a <= b -> a * a1 <= b * a1
51 ltle 
a < b -> a <= b
52 50, 51 syl 
a < b -> a * a1 <= b * a1
53 49, 52 sylib 
a < b -> a * a1 + b <= b * a1 + b
54 48, 53 ltletrd 
a < b -> a * a1 + a < b * a1 + b
55 45, 54 sylibr 
a < b -> a * suc a1 < b * suc a1
56 55 anwl 
a < b /\ (0 < a1 -> a * a1 < b * a1) -> a * suc a1 < b * suc a1
57 56 a1d 
a < b /\ (0 < a1 -> a * a1 < b * a1) -> 0 < suc a1 -> a * suc a1 < b * suc a1
58 9, 18, 27, 36, 40, 57 indd 
a < b -> 0 < c -> a * c < b * c
59 58 com12 
0 < c -> a < b -> a * c < b * c
60 ltnle 
a * c < b * c <-> ~b * c <= a * c
61 ltnle 
a < b <-> ~b <= a
62 60, 61 imeqi 
a * c < b * c -> a < b <-> ~b * c <= a * c -> ~b <= a
63 con3 
(b <= a -> b * c <= a * c) -> ~b * c <= a * c -> ~b <= a
64 lemul1a 
b <= a -> b * c <= a * c
65 63, 64 ax_mp 
~b * c <= a * c -> ~b <= a
66 62, 65 mpbir 
a * c < b * c -> a < b
67 66 a1i 
0 < c -> a * c < b * c -> a < b
68 59, 67 ibid 
0 < c -> (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 (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)