---

Step * 3 1 1 1 of Lemma equipollent-multiply

.....antecedent..... 
1. a : ℕ
2. b : ℕ
3. a3 : ℕa
4. a4 : ℕb
5. a5 : ℕa
6. a6 : ℕb
7. ((a3 * b) + a4) = ((a5 * b) + a6) ∈ ℕa * b
⊢ Div((a3 * b) + a4;b;a3)
BY
{ (D 0 THEN Auto') }

---

Latex:

---

Latex:
.....antecedent..... 
1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
3.  a3  :  \mBbbN{}a
4.  a4  :  \mBbbN{}b
5.  a5  :  \mBbbN{}a
6.  a6  :  \mBbbN{}b
7.  ((a3  *  b)  +  a4)  =  ((a5  *  b)  +  a6)
\mvdash{}  Div((a3  *  b)  +  a4;b;a3)


By

---

Latex:
(D  0  THEN  Auto')

---

Home Index