---

Step * 3 1 1 of Lemma equipollent-multiply

.....assertion..... 
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
⊢ a3 = a5 ∈ ℤ
BY
{ ((InstLemma `div_unique` [⌜(a3 * b) + a4⌝; ⌜b⌝; ⌜a3⌝; ⌜a5⌝])⋅ THEN Auto') }

1
.....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)

2
.....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;a5)

---

Latex:

---

Latex:
.....assertion..... 
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{}  a3  =  a5


By

---

Latex:
((InstLemma  `div\_unique`  [\mkleeneopen{}(a3  *  b)  +  a4\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{};  \mkleeneopen{}a3\mkleeneclose{};  \mkleeneopen{}a5\mkleeneclose{}])\mcdot{}  THEN  Auto')

---

Home Index