1. a : ℤ@i 2. b : ℤ@i 3. 0 < a * b 4. ¬0 < a 5. ¬0 < b ⊢ (0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0)
BY { (OrRight THEN Auto) }
1 1. a : ℤ@i 2. b : ℤ@i 3. 0 < a * b 4. ¬0 < a 5. ¬0 < b ⊢ a < 0
2 1. a : ℤ@i 2. b : ℤ@i 3. 0 < a * b 4. ¬0 < a 5. ¬0 < b 6. a < 0 ⊢ b < 0
Latex:
Latex:
1. a : \mBbbZ{}@i
2. b : \mBbbZ{}@i
3. 0 < a * b
4. \mneg{}0 < a
5. \mneg{}0 < b
\mvdash{} (0 < a \mwedge{} 0 < b) \mvee{} (a < 0 \mwedge{} b < 0)