---

Step * 1 2 1 of Lemma posint_div_dec


1. a : ℕ+
2. b : ℕ+
3. ¬((b rem a) = 0 ∈ ℤ)
4. ∃c:ℕ+. (b = (a * c) ∈ ℕ+)
⊢ False
BY
{ TACTIC:(D -2 THEN D -1 THEN HypSubst' (-1) 0) }

1
1. a : ℕ+
2. b : ℕ+
3. c : ℕ+
4. b = (a * c) ∈ ℕ+
⊢ (a * c rem a) = 0 ∈ ℤ

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}\msupplus{}
2.  b  :  \mBbbN{}\msupplus{}
3.  \mneg{}((b  rem  a)  =  0)
4.  \mexists{}c:\mBbbN{}\msupplus{}.  (b  =  (a  *  c))
\mvdash{}  False


By

---

Latex:
TACTIC:(D  -2  THEN  D  -1  THEN  HypSubst'  (-1)  0)

---

Home Index