Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mul2lt0rlt0 Structured version   Unicode version

Theorem mul2lt0rlt0 27388
 Description: If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
Hypotheses
Ref Expression
mul2lt0.1
mul2lt0.2
mul2lt0.3
Assertion
Ref Expression
mul2lt0rlt0

Proof of Theorem mul2lt0rlt0
StepHypRef Expression
1 mul2lt0.3 . . . . 5
21adantr 465 . . . 4
3 mul2lt0.1 . . . . . . 7
4 mul2lt0.2 . . . . . . 7
53, 4remulcld 9636 . . . . . 6
65adantr 465 . . . . 5
7 0re 9608 . . . . . 6
87a1i 11 . . . . 5
9 negelrp 27387 . . . . . . 7
104, 9syl 16 . . . . . 6
1110biimpar 485 . . . . 5
126, 8, 11ltdiv1d 11309 . . . 4
132, 12mpbid 210 . . 3
143recnd 9634 . . . . . . . 8
1514adantr 465 . . . . . . 7
164recnd 9634 . . . . . . . 8
1716adantr 465 . . . . . . 7
1815, 17mulcld 9628 . . . . . 6
194adantr 465 . . . . . . 7
20 simpr 461 . . . . . . 7
2119, 20ltned 9732 . . . . . 6
2218, 17, 21divneg2d 10346 . . . . 5
2315, 17, 21divcan4d 10338 . . . . . 6
2423negeqd 9826 . . . . 5
2522, 24eqtr3d 2510 . . . 4
2617negcld 9929 . . . . 5
2717, 21negne0d 9940 . . . . 5
28 div0 10247 . . . . 5
2926, 27, 28syl2anc 661 . . . 4
3025, 29breq12d 4466 . . 3
3113, 30mpbid 210 . 2