Theorem ltmuld ≪ | index | src | ≫

theorem ltmuld (G: wff) (a b c d: nat):
  $ G -> a < b $ >
  $ G -> c < d $ >
  $ G -> a * c < b * d $;

Step	Hyp	Ref	Expression
1		lemul1a	a <= b -> a * c <= b * c
2		ltle	a < b -> a <= b
3		hyp h1	G -> a < b
4	2, 3	syl	G -> a <= b
5	1, 4	syl	G -> a * c <= b * c
6		ltmul2	0 < b -> (c < d <-> b * c < b * d)
7		lelttr	0 <= a -> a < b -> 0 < b
8		le01	0 <= a
9	7, 8	ax_mp	a < b -> 0 < b
10	9, 3	syl	G -> 0 < b
11	6, 10	syl	G -> (c < d <-> b * c < b * d)
12		hyp h2	G -> c < d
13	11, 12	mpbid	G -> b * c < b * d
14	5, 13	lelttrd	G -> a * c < b * d

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)