Step
*
1
of Lemma
qmul-negative
.....assertion..... 
1. a : ℚ@i
2. b : ℚ@i
⊢ a * b < 0 
⇐⇒ 0 < -(a) * b
BY
{ Auto }
1
1. a : ℚ@i
2. b : ℚ@i
3. a * b < 0@i
⊢ 0 < -(a) * b
2
1. a : ℚ@i
2. b : ℚ@i
3. 0 < -(a) * b@i
⊢ a * b < 0
Latex:
Latex:
.....assertion..... 
1.  a  :  \mBbbQ{}@i
2.  b  :  \mBbbQ{}@i
\mvdash{}  a  *  b  <  0  \mLeftarrow{}{}\mRightarrow{}  0  <  -(a)  *  b
By
Latex:
Auto
Home
Index