Step * 2 1 1 1 of Lemma rng-pps_wf


1. IntegDom{i}@i'
2. eq EqDecider(|r|)
3. : ℕ3 ⟶ |r|@i
4. ¬(m 0 ∈ (ℕ3 ⟶ |r|))
5. : ℕ3 ⟶ |r|@i
6. ¬(l 0 ∈ (ℕ3 ⟶ |r|))
7. : ℕ3 ⟶ |r|@i
8. ¬(p 0 ∈ (ℕ3 ⟶ |r|))
9. : ℕ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. : ℕ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 q) 0 ∈ (ℕ3 ⟶ |r|))
⊢ False
BY
(Assert ¬((l m) 0 ∈ (ℕ3 ⟶ |r|)) BY
         ((D THENA Auto)
          THEN (RWO "cross-product-equal-0-iff" (-1) THENA Auto)
          THEN SplitOrHyps
          THEN Auto
          THEN (InstHyp [⌜a⌝(-1)⋅ THENA Auto)
          THEN (RWO "scalar-product-comm" (-1) THENA Auto)
          THEN -1
          THEN -2
          THEN Auto)) }

1
1. IntegDom{i}@i'
2. eq EqDecider(|r|)
3. : ℕ3 ⟶ |r|@i
4. ¬(m 0 ∈ (ℕ3 ⟶ |r|))
5. : ℕ3 ⟶ |r|@i
6. ¬(l 0 ∈ (ℕ3 ⟶ |r|))
7. : ℕ3 ⟶ |r|@i
8. ¬(p 0 ∈ (ℕ3 ⟶ |r|))
9. : ℕ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. : ℕ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 q) 0 ∈ (ℕ3 ⟶ |r|))
25. ¬((l m) 0 ∈ (ℕ3 ⟶ |r|))
⊢ False


Latex:


Latex:

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


By


Latex:
(Assert  \mneg{}((l  x  m)  =  0)  BY
              ((D  0  THENA  Auto)
                THEN  (RWO  "cross-product-equal-0-iff"  (-1)  THENA  Auto)
                THEN  SplitOrHyps
                THEN  Auto
                THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  (RWO  "scalar-product-comm"  (-1)  THENA  Auto)
                THEN  D  -1
                THEN  D  -2
                THEN  Auto))




Home Index