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