---

Step * 3 of Lemma fps-pascal-elim


1. r : CRng
2. x : Atom
3. y : Atom
4. x ≠ y ∈ Atom 
5. ¬(x = y ∈ Atom)
6. ¬(1 = 0 ∈ |r|)
7. ↑(AtomDeq x x)
⊢ (1÷(-(atom(y))+(1-0))) = (1÷(-(atom(y))+1)) ∈ PowerSeries(r)
BY
{ xxxRepeatFor 2 ((EqCD THEN Auto))xxx }

1
.....subterm..... T:t
3:n
1. r : CRng
2. x : Atom
3. y : Atom
4. x ≠ y ∈ Atom 
5. ¬(x = y ∈ Atom)
6. ¬(1 = 0 ∈ |r|)
7. ↑(AtomDeq x x)
⊢ (1-0) = 1 ∈ PowerSeries(r)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  x  :  Atom
3.  y  :  Atom
4.  x  \mneq{}  y  \mmember{}  Atom 
5.  \mneg{}(x  =  y)
6.  \mneg{}(1  =  0)
7.  \muparrow{}(AtomDeq  x  x)
\mvdash{}  (1\mdiv{}(-(atom(y))+(1-0)))  =  (1\mdiv{}(-(atom(y))+1))


By

---

Latex:
xxxRepeatFor  2  ((EqCD  THEN  Auto))xxx

---

Home Index