---

Step * 2 of Lemma rng-pp-nontrivial-1


1. r : IntegDom{i}@i'
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)@i
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
4. i : {i:ℕ3| ¬((l i) = 0 ∈ |r|)} 
5. ∀i,j:ℕ3.
     ((¬((l i) = 0 ∈ |r|))
     ⇒ (¬(i = j ∈ ℤ))
     ⇒ (λx.if (x =z j) then l i
            if (x =z i) then -r (l j)
            else 0
            fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))
⊢ ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . (∃b:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))}  [(((a . l) = 0 ∈ |r|) ∧ ((b . l)\000C = 0 ∈ |r|) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))))])
BY
{ ((D -2 THEN IntSegCases (-3)) THEN Eliminate ⌜i⌝⋅ THEN ThinVar  `i') }

1
1. r : IntegDom{i}@i'
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)@i
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
4. [%2] : ¬((l 0) = 0 ∈ |r|)
5. ∀i,j:ℕ3.
     ((¬((l i) = 0 ∈ |r|))
     ⇒ (¬(i = j ∈ ℤ))
     ⇒ (λx.if (x =z j) then l i
            if (x =z i) then -r (l j)
            else 0
            fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))
⊢ ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . (∃b:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))}  [(((a . l) = 0 ∈ |r|) ∧ ((b . l)\000C = 0 ∈ |r|) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))))])

2
1. r : IntegDom{i}@i'
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)@i
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
4. [%2] : ¬((l 1) = 0 ∈ |r|)
5. ∀i,j:ℕ3.
     ((¬((l i) = 0 ∈ |r|))
     ⇒ (¬(i = j ∈ ℤ))
     ⇒ (λx.if (x =z j) then l i
            if (x =z i) then -r (l j)
            else 0
            fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))
⊢ ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . (∃b:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))}  [(((a . l) = 0 ∈ |r|) ∧ ((b . l)\000C = 0 ∈ |r|) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))))])

3
1. r : IntegDom{i}@i'
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)@i
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
4. [%2] : ¬((l 2) = 0 ∈ |r|)
5. ∀i,j:ℕ3.
     ((¬((l i) = 0 ∈ |r|))
     ⇒ (¬(i = j ∈ ℤ))
     ⇒ (λx.if (x =z j) then l i
            if (x =z i) then -r (l j)
            else 0
            fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))
⊢ ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . (∃b:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))}  [(((a . l) = 0 ∈ |r|) ∧ ((b . l)\000C = 0 ∈ |r|) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))))])

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  \mforall{}x,y:|r|.    Dec(x  =  y)@i
3.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
4.  i  :  \{i:\mBbbN{}3|  \mneg{}((l  i)  =  0)\} 
5.  \mforall{}i,j:\mBbbN{}3.
          ((\mneg{}((l  i)  =  0))
          {}\mRightarrow{}  (\mneg{}(i  =  j))
          {}\mRightarrow{}  (\mlambda{}x.if  (x  =\msubz{}  j)  then  l  i
                        if  (x  =\msubz{}  i)  then  -r  (l  j)
                        else  0
                        fi    \mmember{}  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  (\mneg{}(p  =  0))  \mwedge{}  ((p  .  l)  =  0)\}  ))
\mvdash{}  \mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  (\mexists{}b:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}    [(((a  .  l)  =  0)  \mwedge{}  ((b  .  l)  =  0)  \mwedge{}  (\mneg{}((a  \000Cx  b)  =  0)))])


By

---

Latex:
((D  -2  THEN  IntSegCases  (-3))  THEN  Eliminate  \mkleeneopen{}i\mkleeneclose{}\mcdot{}  THEN  ThinVar    `i')

---

Home Index