---

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


1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. (a . l) = 0 ∈ |r|
7. (b . l) = 0 ∈ |r|
8. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ (a + b) ∈ {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
BY
{ (MemTypeCD THEN Auto THEN ParallelLast) }

1
1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. (a . l) = 0 ∈ |r|
7. (b . l) = 0 ∈ |r|
8. (a + b) = 0 ∈ (ℕ3 ⟶ |r|)
⊢ (a x b) = 0 ∈ (ℕ3 ⟶ |r|)

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}
2.  \mforall{}x,y:|r|.    Dec(x  =  y)
3.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
4.  a  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
5.  b  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
6.  (a  .  l)  =  0
7.  (b  .  l)  =  0
8.  \mneg{}((a  x  b)  =  0)
\mvdash{}  (a  +  b)  \mmember{}  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 


By

---

Latex:
(MemTypeCD  THEN  Auto  THEN  ParallelLast)

---

Home Index