Step
*
2
1
1
1
1
2
1
1
of Lemma
rng-pps_wf
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|))
25. c3 : |r|
26. c4 : |r|
27. ¬(c3 = 0 ∈ |r|)
28. ¬(c4 = 0 ∈ |r|)
29. (c3*l) = (c4*(p x q)) ∈ (ℕ3 ⟶ |r|)
30. c1 : |r|
31. c2 : |r|
32. ¬(c1 = 0 ∈ |r|)
33. ¬(c2 = 0 ∈ |r|)
34. (c1*m) = (c2*(p x q)) ∈ (ℕ3 ⟶ |r|)
⊢ ∃c1,c2:|r|. ((¬(c1 = 0 ∈ |r|)) ∧ (¬(c2 = 0 ∈ |r|)) ∧ ((c1*l) = (c2*m) ∈ (ℕ3 ⟶ |r|)))
BY
{ (InstConcl [⌜c2 * c3⌝;⌜c4 * c1⌝]⋅ 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|))
25. c3 : |r|
26. c4 : |r|
27. ¬(c3 = 0 ∈ |r|)
28. ¬(c4 = 0 ∈ |r|)
29. (c3*l) = (c4*(p x q)) ∈ (ℕ3 ⟶ |r|)
30. c1 : |r|
31. c2 : |r|
32. ¬(c1 = 0 ∈ |r|)
33. ¬(c2 = 0 ∈ |r|)
34. (c1*m) = (c2*(p x q)) ∈ (ℕ3 ⟶ |r|)
⊢ ¬((c2 * c3) = 0 ∈ |r|)
2
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|))
25. c3 : |r|
26. c4 : |r|
27. ¬(c3 = 0 ∈ |r|)
28. ¬(c4 = 0 ∈ |r|)
29. (c3*l) = (c4*(p x q)) ∈ (ℕ3 ⟶ |r|)
30. c1 : |r|
31. c2 : |r|
32. ¬(c1 = 0 ∈ |r|)
33. ¬(c2 = 0 ∈ |r|)
34. (c1*m) = (c2*(p x q)) ∈ (ℕ3 ⟶ |r|)
35. ¬((c2 * c3) = 0 ∈ |r|)
⊢ ¬((c4 * c1) = 0 ∈ |r|)
3
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|))
25. c3 : |r|
26. c4 : |r|
27. ¬(c3 = 0 ∈ |r|)
28. ¬(c4 = 0 ∈ |r|)
29. (c3*l) = (c4*(p x q)) ∈ (ℕ3 ⟶ |r|)
30. c1 : |r|
31. c2 : |r|
32. ¬(c1 = 0 ∈ |r|)
33. ¬(c2 = 0 ∈ |r|)
34. (c1*m) = (c2*(p x q)) ∈ (ℕ3 ⟶ |r|)
35. ¬((c2 * c3) = 0 ∈ |r|)
36. ¬((c4 * c1) = 0 ∈ |r|)
⊢ (c2 * c3*l) = (c4 * c1*m) ∈ (ℕ3 ⟶ |r|)
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)
25. c3 : |r|
26. c4 : |r|
27. \mneg{}(c3 = 0)
28. \mneg{}(c4 = 0)
29. (c3*l) = (c4*(p x q))
30. c1 : |r|
31. c2 : |r|
32. \mneg{}(c1 = 0)
33. \mneg{}(c2 = 0)
34. (c1*m) = (c2*(p x q))
\mvdash{} \mexists{}c1,c2:|r|. ((\mneg{}(c1 = 0)) \mwedge{} (\mneg{}(c2 = 0)) \mwedge{} ((c1*l) = (c2*m)))
By
Latex:
(InstConcl [\mkleeneopen{}c2 * c3\mkleeneclose{};\mkleeneopen{}c4 * c1\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index