Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltmul12a Unicode version

Theorem ltmul12a 7826
 Description: Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.)
Assertion
Ref Expression
ltmul12a

Proof of Theorem ltmul12a
StepHypRef Expression
1 simplll 485 . . . 4
2 simpllr 486 . . . 4
3 simpll 481 . . . . . 6
4 simprl 483 . . . . . 6
53, 4jca 290 . . . . 5
65ad2ant2l 477 . . . 4
7 ltle 7105 . . . . . . 7
87imp 115 . . . . . 6
98adantrl 447 . . . . 5
109ad2ant2r 478 . . . 4
11 lemul1a 7824 . . . 4
121, 2, 6, 10, 11syl31anc 1138 . . 3
13 simplrl 487 . . . . . . 7
14 simplrr 488 . . . . . . 7
15 simpllr 486 . . . . . . 7
16 0re 7027 . . . . . . . . . 10
17 lelttr 7106 . . . . . . . . . 10
1816, 17mp3an1 1219 . . . . . . . . 9
1918imp 115 . . . . . . . 8
2019adantlr 446 . . . . . . 7
21 ltmul2 7822 . . . . . . 7
2213, 14, 15, 20, 21syl112anc 1139 . . . . . 6
2322biimpa 280 . . . . 5
2423anasss 379 . . . 4