---

Step * of Lemma rng-pp-nontrivial-3

∀r:IntegDom{i}. ∀eq:EqDecider(|r|). ∀l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} .
  ∃a,b,c:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
   ((¬¬((a . l) = 0 ∈ |r|))
   ∧ (¬¬((b . l) = 0 ∈ |r|))
   ∧ (¬¬((c . l) = 0 ∈ |r|))
   ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((b . l) = 0 ∈ |r|))))
   ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((b . l) = 0 ∈ |r|)) ∧ (¬((c . l) = 0 ∈ |r|))))
   ∧ (∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((c . l) = 0 ∈ |r|)) ∧ (¬((a . l) = 0 ∈ |r|)))))
BY
{ (Auto
   THEN (InstLemma `deq-implies` [⌜|r|⌝]⋅ THENA Auto)
   THEN (InstLemma `rng-pp-nontrivial-2` [⌜r⌝;⌜l⌝]⋅ THENA Auto)
   THEN RepeatFor 4 (ParallelLast)
   THEN RepeatFor 3 ((((RemoveDoubleNegation THENA Auto) THEN Trivial) ORELSE ParallelLast))
   THEN (ParallelLast
   ORELSE ((InstLemma `cross-product-non-zero-implies-ext` [⌜r⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN ParallelLast THEN Auto)
   )) }

1
1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. ∀x,y:|r|.  Dec(x = y ∈ |r|)
5. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
7. c : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
8. (a . l) = 0 ∈ |r|
9. (b . l) = 0 ∈ |r|
10. (c . l) = 0 ∈ |r|
11. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
12. ¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|))
13. ¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((b . l) = 0 ∈ |r|)) ∧ (¬((c . l) = 0 ∈ |r|)))

2
1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. ∀x,y:|r|.  Dec(x = y ∈ |r|)
5. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
7. c : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
8. (a . l) = 0 ∈ |r|
9. (b . l) = 0 ∈ |r|
10. (c . l) = 0 ∈ |r|
11. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
12. ¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|))
13. ¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((c . l) = 0 ∈ |r|)) ∧ (¬((a . l) = 0 ∈ |r|)))

---

Latex:

---

Latex:
\mforall{}r:IntegDom\{i\}.  \mforall{}eq:EqDecider(|r|).  \mforall{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .
    \mexists{}a,b,c:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
      ((\mneg{}\mneg{}((a  .  l)  =  0))
      \mwedge{}  (\mneg{}\mneg{}((b  .  l)  =  0))
      \mwedge{}  (\mneg{}\mneg{}((c  .  l)  =  0))
      \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  l)  =  0))  \mwedge{}  (\mneg{}((b  .  l)  =  0))))
      \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((b  .  l)  =  0))  \mwedge{}  (\mneg{}((c  .  l)  =  0))))
      \mwedge{}  (\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((c  .  l)  =  0))  \mwedge{}  (\mneg{}((a  .  l)  =  0)))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `deq-implies`  [\mkleeneopen{}|r|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rng-pp-nontrivial-2`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  4  (ParallelLast)
  THEN  RepeatFor  3  ((((RemoveDoubleNegation  THENA  Auto)  THEN  Trivial)  ORELSE  ParallelLast))
  THEN  (ParallelLast
  ORELSE  ((InstLemma  `cross-product-non-zero-implies-ext`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  ParallelLast
                  THEN  Auto)
  ))

---

Home Index