Proof of Nuprl Lemma : cong-angle-out-exists

Step * 1 3 of Lemma cong-angle-out-exists

1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅_a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A ∧ yA ≅ ba'
28. C : Point
29. r2-y-C ∧ yC ≅ bc'
30. a'c' ≅ AC
⊢ ∃x',z',p':Point

   (((x'-p'-z' ∧ Cong3(a'bc',x'yz')) ∧ out(y xx') ∧ out(y zz')) ∧ (x'p' ≅ a'p ∧ p'z' ≅ pc') ∧ bp ≅ yp' ∧ x'yp' ≅_a a'bp)

{ (((InstLemma `geo-congruent-between-exists` [⌜g⌝;⌜a'⌝;⌜p⌝;⌜c'⌝;⌜A⌝;⌜C⌝]⋅ THENA (Auto THEN D 18 THEN Auto))

    THEN ExRepD
    )
   THEN InstConcl [⌜A⌝;⌜C⌝;⌜b'⌝]⋅
   THEN Auto) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅_a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. a'c' ≅ AC
33. b' : Point
34. A_b'_C
35. a'p ≅ Ab'
36. pc' ≅ b'C
⊢ A-b'-C

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅_a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. a'c' ≅ AC
33. b' : Point
34. A_b'_C
35. a'p ≅ Ab'
36. pc' ≅ b'C
37. A-b'-C
⊢ Cong3(a'bc',AyC)

3
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅_a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. a'c' ≅ AC
33. b' : Point
34. A_b'_C
35. a'p ≅ Ab'
36. pc' ≅ b'C
37. A-b'-C
38. Cong3(a'bc',AyC)
⊢ out(y xA)

4
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅_a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. a'c' ≅ AC
33. b' : Point
34. A_b'_C
35. a'p ≅ Ab'
36. pc' ≅ b'C
37. A-b'-C
38. Cong3(a'bc',AyC)
39. out(y xA)
⊢ out(y zC)

5
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅_a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. a'c' ≅ AC
33. b' : Point
34. A_b'_C
35. a'p ≅ Ab'
36. pc' ≅ b'C
37. A-b'-C
38. Cong3(a'bc',AyC)
39. out(y xA)
40. out(y zC)
41. Ab' ≅ a'p
42. b'C ≅ pc'
⊢ bp ≅ yb'

6
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅_a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. a'c' ≅ AC
33. b' : Point
34. A_b'_C
35. a'p ≅ Ab'
36. pc' ≅ b'C
37. A-b'-C
38. Cong3(a'bc',AyC)
39. out(y xA)
40. out(y zC)
41. Ab' ≅ a'p
42. b'C ≅ pc'
43. bp ≅ yb'
⊢ Ayb' ≅_a a'bp

Latex:

Latex:
1. g : EuclideanPlane 2. a : Point 3. b : Point 4. c : Point 5. x : Point 6. y : Point 7. z : Point 8. a' : Point 9. c' : Point 10. p : Point 11. abc \mcong{}\msuba{} xyz 12. a \mneq{} b 13. c \mneq{} b 14. p \mneq{} b 15. x \mneq{} y 16. z \mneq{} y 17. out(b aa') 18. out(b cc') 19. a'-p-c' 20. r1 : Point 21. x-y-r1 22. yr1 \mcong{} OX 23. r2 : Point 24. z-y-r2 25. yr2 \mcong{} OX 26. A : Point 27. r1-y-A \mwedge{} yA \mcong{} ba' 28. C : Point 29. r2-y-C \mwedge{} yC \mcong{} bc' 30. a'c' \mcong{} AC \mvdash{} \mexists{}x',z',p':Point (((x'-p'-z' \mwedge{} Cong3(a'bc',x'yz')) \mwedge{} out(y xx') \mwedge{} out(y zz')) \mwedge{} (x'p' \mcong{} a'p \mwedge{} p'z' \mcong{} pc') \mwedge{} bp \mcong{} yp' \mwedge{} x'yp' \mcong{}\msuba{} a'bp) By Latex: (((InstLemma `geo-congruent-between-exists` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{} THENA (Auto THEN D 18 THEN Auto) ) THEN ExRepD ) THEN InstConcl [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{} THEN Auto) Home Index