---

Step * 2 of Lemma equipollent-nat-prod-nsub


1. k : ℕ+
2. b : ℕ × ℕk
⊢ ∃a:ℕ. (<a ÷ k, a rem k> = b ∈ (ℕ × ℕk))
BY
{ (D (-1) THEN With ⌜(k * b1) + b2⌝ (D 0)⋅ THEN Auto THEN Try ((BLemma `rem_bounds_1` ⋅ THEN Auto))) }

1
1. k : ℕ+
2. b1 : ℕ
3. b2 : ℕk
⊢ <((k * b1) + b2) ÷ k, (k * b1) + b2 rem k> = <b1, b2> ∈ (ℕ × ℕk)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  b  :  \mBbbN{}  \mtimes{}  \mBbbN{}k
\mvdash{}  \mexists{}a:\mBbbN{}.  (<a  \mdiv{}  k,  a  rem  k>  =  b)


By

---

Latex:
(D  (-1)  THEN  With  \mkleeneopen{}(k  *  b1)  +  b2\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Try  ((BLemma  `rem\_bounds\_1`  \mcdot{}  THEN  Auto)))

---

Home Index