---

Step * of Lemma equipollent-multiply

∀a,b:ℕ.  ℕa × ℕb ~ ℕa * b
BY
{ (Auto THEN Unfold `equipollent` 0 THEN InstConcl [⌜λp.let x,y = p in (x * b) + y⌝]⋅ THEN Auto') }

1
1. a : ℕ
2. b : ℕ
3. p1 : ℕa
4. p2 : ℤ
5. 0 ≤ p2
6. p2 < b
⊢ (0 - p1 * b) ≤ p2

2
1. a : ℕ
2. b : ℕ
3. p1 : ℕa
4. p2 : ℤ
5. 0 ≤ p2
6. p2 < b
⊢ p2 < (a * b) - p1 * b

3
1. a : ℕ
2. b : ℕ
⊢ Bij(ℕa × ℕb;ℕa * b;λp.let x,y = p 
                        in (x * b) + y)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}.    \mBbbN{}a  \mtimes{}  \mBbbN{}b  \msim{}  \mBbbN{}a  *  b


By

---

Latex:
(Auto  THEN  Unfold  `equipollent`  0  THEN  InstConcl  [\mkleeneopen{}\mlambda{}p.let  x,y  =  p  in  (x  *  b)  +  y\mkleeneclose{}]\mcdot{}  THEN  Auto')

---

Home Index