---

Step * 2 1 1 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ ∀m,l,p,q:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} .
    ((¬¬((p . l) = 0 ∈ |r|))
    ⇒ (¬¬((q . l) = 0 ∈ |r|))
    ⇒ (¬¬((p . m) = 0 ∈ |r|))
    ⇒ (¬¬((q . m) = 0 ∈ |r|))
    ⇒ (¬((¬¬(∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((p . l) = 0 ∈ |r|)) ∧ (¬((q . l) = 0 ∈ |r|)))))
       ∧ (¬¬(∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((a . m) = 0 ∈ |r|))))))))
BY
{ (Intros
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN ∀h:hyp. (SupposeMore h THENA Auto) 
   THEN ExRepD
   THEN ∀h:hyp. (SupposeMore h THENA Auto) 
   THEN DSetVars
   THEN (InstLemma `deq-implies` [|r|]⋅ THENA Auto)
   THEN (Assert ¬((p x q) = 0 ∈ (ℕ3 ⟶ |r|)) BY
               ((D 0 THENA Auto) THEN (RWO "cross-product-equal-0-iff" (-1) THENA Auto) THEN SplitOrHyps THEN Auto))) }

1
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. m : ℕ3 ⟶ |r|@i
4. ¬(m = 0 ∈ (ℕ3 ⟶ |r|))
5. l : ℕ3 ⟶ |r|@i
6. ¬(l = 0 ∈ (ℕ3 ⟶ |r|))
7. p : ℕ3 ⟶ |r|@i
8. ¬(p = 0 ∈ (ℕ3 ⟶ |r|))
9. q : ℕ3 ⟶ |r|@i
10. ¬(q = 0 ∈ (ℕ3 ⟶ |r|))
11. (p . l) = 0 ∈ |r|
12. (q . l) = 0 ∈ |r|
13. (p . m) = 0 ∈ |r|
14. (q . m) = 0 ∈ |r|
15. l1 : ℕ3 ⟶ |r|@i
16. ¬(l1 = 0 ∈ (ℕ3 ⟶ |r|))
17. (p . l1) = 0 ∈ |r|
18. ¬((q . l1) = 0 ∈ |r|)
19. a : ℕ3 ⟶ |r|@i
20. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
21. (a . l) = 0 ∈ |r|
22. ¬((a . m) = 0 ∈ |r|)
23. ∀x,y:|r|.  Dec(x = y ∈ |r|)
24. ¬((p x q) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ False

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
\mvdash{}  \mforall{}m,l,p,q:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .
        ((\mneg{}\mneg{}((p  .  l)  =  0))
        {}\mRightarrow{}  (\mneg{}\mneg{}((q  .  l)  =  0))
        {}\mRightarrow{}  (\mneg{}\mneg{}((p  .  m)  =  0))
        {}\mRightarrow{}  (\mneg{}\mneg{}((q  .  m)  =  0))
        {}\mRightarrow{}  (\mneg{}((\mneg{}\mneg{}(\mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((p  .  l)  =  0))  \mwedge{}  (\mneg{}((q  .  l)  =  0)))))
              \mwedge{}  (\mneg{}\mneg{}(\mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  l)  =  0))  \mwedge{}  (\mneg{}((a  .  m)  =  0))))))))


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  \mforall{}h:hyp.  (SupposeMore  h  THENA  Auto) 
  THEN  ExRepD
  THEN  \mforall{}h:hyp.  (SupposeMore  h  THENA  Auto) 
  THEN  DSetVars
  THEN  (InstLemma  `deq-implies`  [|r|]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mneg{}((p  x  q)  =  0)  BY
                          ((D  0  THENA  Auto)
                            THEN  (RWO  "cross-product-equal-0-iff"  (-1)  THENA  Auto)
                            THEN  SplitOrHyps
                            THEN  Auto)))

---

Home Index