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

Theorem mul2lt0rlt0 9558
 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.1 . . . . . 6
2 mul2lt0.2 . . . . . 6
31, 2remulcld 7808 . . . . 5
43adantr 274 . . . 4
5 0red 7779 . . . 4
62adantr 274 . . . . 5
7 simpr 109 . . . . 5
86, 7negelrpd 9488 . . . 4
9 mul2lt0.3 . . . . 5
109adantr 274 . . . 4
114, 5, 8, 10ltdiv1dd 9553 . . 3
121recnd 7806 . . . . . . 7
1312adantr 274 . . . . . 6
142recnd 7806 . . . . . . 7
1514adantr 274 . . . . . 6
1613, 15mulcld 7798 . . . . 5
176, 7lt0ap0d 8423 . . . . 5 #
1816, 15, 17divneg2apd 8576 . . . 4
1913, 15, 17divcanap4d 8568 . . . . 5
2019negeqd 7969 . . . 4
2118, 20eqtr3d 2174 . . 3
2215negcld 8072 . . . 4
2315, 17negap0d 8405 . . . 4 #
2422, 23div0apd 8559 . . 3
2511, 21, 243brtr3d 3959 . 2