---

Step * 1 2 2 2 2 2 1 of Lemma rmul-is-negative1


1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. N : {4...}
5. (imax(|x 1|;|y 1|) + 4) = N ∈ {4...}
6. ¬x ((2 * N) * n) < -4
7. ¬y ((2 * N) * n) < -4
8. ¬4 < x ((2 * N) * n)
9. ¬4 < y ((2 * N) * n)
10. a : {-4..5-}
11. (x ((2 * N) * n)) = a ∈ {-4..5-}
12. b : {-4..5-}
13. (y ((2 * N) * n)) = b ∈ {-4..5-}
⊢ ((a * b) ÷ 2 * (2 * N) * n ÷ 2 * N) + 4 < 2 * n * 0 ⇒ False
BY
{ (GenConcl ⌜(a * b) = z ∈ {-16..17-}⌝⋅ THENA (All Thin THEN Auto THEN IntSegCases 2 THEN Auto')) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. N : {4...}
5. (imax(|x 1|;|y 1|) + 4) = N ∈ {4...}
6. ¬x ((2 * N) * n) < -4
7. ¬y ((2 * N) * n) < -4
8. ¬4 < x ((2 * N) * n)
9. ¬4 < y ((2 * N) * n)
10. a : {-4..5-}
11. (x ((2 * N) * n)) = a ∈ {-4..5-}
12. b : {-4..5-}
13. (y ((2 * N) * n)) = b ∈ {-4..5-}
14. z : {-16..17-}
15. (a * b) = z ∈ {-16..17-}
⊢ (z ÷ 2 * (2 * N) * n ÷ 2 * N) + 4 < 2 * n * 0 ⇒ False

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
4.  N  :  \{4...\}
5.  (imax(|x  1|;|y  1|)  +  4)  =  N
6.  \mneg{}x  ((2  *  N)  *  n)  <  -4
7.  \mneg{}y  ((2  *  N)  *  n)  <  -4
8.  \mneg{}4  <  x  ((2  *  N)  *  n)
9.  \mneg{}4  <  y  ((2  *  N)  *  n)
10.  a  :  \{-4..5\msupminus{}\}
11.  (x  ((2  *  N)  *  n))  =  a
12.  b  :  \{-4..5\msupminus{}\}
13.  (y  ((2  *  N)  *  n))  =  b
\mvdash{}  ((a  *  b)  \mdiv{}  2  *  (2  *  N)  *  n  \mdiv{}  2  *  N)  +  4  <  2  *  n  *  0  {}\mRightarrow{}  False


By

---

Latex:
(GenConcl  \mkleeneopen{}(a  *  b)  =  z\mkleeneclose{}\mcdot{}  THENA  (All  Thin  THEN  Auto  THEN  IntSegCases  2  THEN  Auto'))

---

Home Index