---

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


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

1
.....subterm..... T:t
1:n
1. k : ℕ+
2. b1 : ℕ
3. b2 : ℕk
⊢ (((k * b1) + b2) ÷ k) = b1 ∈ ℕ

2
.....subterm..... T:t
2:n
1. k : ℕ+
2. b1 : ℕ
3. b2 : ℕk
⊢ ((k * b1) + b2 rem k) = b2 ∈ ℕk

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  b1  :  \mBbbN{}
3.  b2  :  \mBbbN{}k
\mvdash{}  <((k  *  b1)  +  b2)  \mdiv{}  k,  (k  *  b1)  +  b2  rem  k>  =  <b1,  b2>


By

---

Latex:
EqCD

---

Home Index