Theorem ltmul1 ≪ | index | src | ≫

theorem ltmul1 (a b c: nat): $ 0 < c -> (a < b <-> a * c < b * c) $;

Step	Hyp	Ref	Expression
1		id	_1 = c -> _1 = c
2	1	lteq2d	_1 = c -> (0 < _1 <-> 0 < c)
3	1	muleq2d	_1 = c -> a * _1 = a * c
4	1	muleq2d	_1 = c -> b * _1 = b * c
5	3, 4	lteqd	_1 = c -> (a * _1 < b * _1 <-> a * c < b * c)
6	2, 5	imeqd	_1 = c -> (0 < _1 -> a * _1 < b * _1 <-> 0 < c -> a * c < b * c)
7		id	_1 = 0 -> _1 = 0
8	7	lteq2d	_1 = 0 -> (0 < _1 <-> 0 < 0)
9	7	muleq2d	_1 = 0 -> a * _1 = a * 0
10	7	muleq2d	_1 = 0 -> b * _1 = b * 0
11	9, 10	lteqd	_1 = 0 -> (a * _1 < b * _1 <-> a * 0 < b * 0)
12	8, 11	imeqd	_1 = 0 -> (0 < _1 -> a * _1 < b * _1 <-> 0 < 0 -> a * 0 < b * 0)
13		id	_1 = a1 -> _1 = a1
14	13	lteq2d	_1 = a1 -> (0 < _1 <-> 0 < a1)
15	13	muleq2d	_1 = a1 -> a * _1 = a * a1
16	13	muleq2d	_1 = a1 -> b * _1 = b * a1
17	15, 16	lteqd	_1 = a1 -> (a * _1 < b * _1 <-> a * a1 < b * a1)
18	14, 17	imeqd	_1 = a1 -> (0 < _1 -> a * _1 < b * _1 <-> 0 < a1 -> a * a1 < b * a1)
19		id	_1 = suc a1 -> _1 = suc a1
20	19	lteq2d	_1 = suc a1 -> (0 < _1 <-> 0 < suc a1)
21	19	muleq2d	_1 = suc a1 -> a * _1 = a * suc a1
22	19	muleq2d	_1 = suc a1 -> b * _1 = b * suc a1
23	21, 22	lteqd	_1 = suc a1 -> (a * _1 < b * _1 <-> a * suc a1 < b * suc a1)
24	20, 23	imeqd	_1 = suc a1 -> (0 < _1 -> a * _1 < b * _1 <-> 0 < suc a1 -> a * suc a1 < b * suc a1)
25		absurd	~0 < 0 -> 0 < 0 -> a * 0 < b * 0
26		lt02	~0 < 0
27	25, 26	ax_mp	0 < 0 -> a * 0 < b * 0
28	27	a1i	a < b -> 0 < 0 -> a * 0 < b * 0
29		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)
30		mulS	a * suc a1 = a * a1 + a
31	29, 30	ax_mp	b * suc a1 = b * a1 + b -> (a * suc a1 < b * suc a1 <-> a * a1 + a < b * a1 + b)
32		mulS	b * suc a1 = b * a1 + b
33	31, 32	ax_mp	a * suc a1 < b * suc a1 <-> a * a1 + a < b * a1 + b
34		bi1	(a < b <-> a * a1 + a < a * a1 + b) -> a < b -> a * a1 + a < a * a1 + b
35		ltadd2	a < b <-> a * a1 + a < a * a1 + b
36	34, 35	ax_mp	a < b -> a * a1 + a < a * a1 + b
37		leadd1	a * a1 <= b * a1 <-> a * a1 + b <= b * a1 + b
38		lemul1a	a <= b -> a * a1 <= b * a1
39		ltle	a < b -> a <= b
40	38, 39	syl	a < b -> a * a1 <= b * a1
41	37, 40	sylib	a < b -> a * a1 + b <= b * a1 + b
42	36, 41	ltletrd	a < b -> a * a1 + a < b * a1 + b
43	33, 42	sylibr	a < b -> a * suc a1 < b * suc a1
44	43	anwl	a < b /\ (0 < a1 -> a * a1 < b * a1) -> a * suc a1 < b * suc a1
45	44	a1d	a < b /\ (0 < a1 -> a * a1 < b * a1) -> 0 < suc a1 -> a * suc a1 < b * suc a1
46	6, 12, 18, 24, 28, 45	indd	a < b -> 0 < c -> a * c < b * c
47	46	com12	0 < c -> a < b -> a * c < b * c
48		ltnle	a * c < b * c <-> ~b * c <= a * c
49		ltnle	a < b <-> ~b <= a
50	48, 49	imeqi	a * c < b * c -> a < b <-> ~b * c <= a * c -> ~b <= a
51		con3	(b <= a -> b * c <= a * c) -> ~b * c <= a * c -> ~b <= a
52		lemul1a	b <= a -> b * c <= a * c
53	51, 52	ax_mp	~b * c <= a * c -> ~b <= a
54	50, 53	mpbir	a * c < b * c -> a < b
55	54	a1i	0 < c -> a * c < b * c -> a < b
56	47, 55	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)