Proof of Nuprl Lemma : Prop22-symmetric-point-construction-lemma

Step * 1 1 of Lemma Prop22-symmetric-point-construction-lemma

1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1'' ∧ bc1'' ≅ bc1
32. c2'' : Point
33. b_a_c2'' ∧ ac2'' ≅ ac2
⊢ ∃c1,c1',c1'',c2,c2',c2'':Point
   ((ac1 ≅ ac ∧ out(a bc1))
   ∧ (bc2 ≅ bc ∧ out(b ac2))
   ∧ (b-a-c1' ∧ ac1' ≅ ac1)
   ∧ (a-b-c2' ∧ bc2' ≅ bc2)
   ∧ (a_b_c1'' ∧ bc1'' ≅ bc1)
   ∧ (b_a_c2'' ∧ ac2'' ≅ ac2)
   ∧ (a-c1-c2' ∧ b-c2-c1')
   ∧ (c1'-a-c1 ∧ c2'-b-c2)
   ∧ (c1'-c2-c2' ∧ c2'-c1-c1')
   ∧ c1'-c2-c1
   ∧ c2'-c1-c2)
BY
{ ((InstConcl [⌜c1⌝;⌜c1'⌝;⌜c1''⌝;⌜c2⌝;⌜c2'⌝;⌜c2''⌝]⋅ THENA Auto) THEN GenRepD) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ out(a bc1)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ out(b ac2)

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ a_b_c1''

4
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ bc1'' ≅ bc1

5
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ b_a_c2''

6
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ ac2'' ≅ ac2

7
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ a-c1-c2'

8
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ b-c2-c1'

9
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ c1'-a-c1

10
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ c2'-b-c2

11
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ c1'-c2-c2'

12
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ c2'-c1-c1'

13
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ c1'-c2-c1

14
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. |bc| < |ba| + |ac|
7. |ac| < |ba| + |bc|
8. |ba| < |ac| + |bc|
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. x : Point
13. b-a-x
14. ax ≅ OX
15. y : Point
16. a-b-y
17. by ≅ OX
18. c1 : Point
19. x-a-c1
20. ac1 ≅ ac
21. c2 : Point
22. y-b-c2
23. bc2 ≅ bc
24. c1' : Point
25. b-a-c1'
26. ac1' ≅ ac1
27. c2' : Point
28. a-b-c2'
29. bc2' ≅ bc2
30. c1'' : Point
31. a_b_c1''
32. bc1'' ≅ bc1
33. c2'' : Point
34. b_a_c2''
35. ac2'' ≅ ac2
⊢ c2'-c1-c2

Latex:

Latex:
1. e : EuclideanPlane 2. a : Point 3. b : Point 4. c : Point 5. a \# bc 6. |bc| < |ba| + |ac| 7. |ac| < |ba| + |bc| 8. |ba| < |ac| + |bc| 9. a \mneq{} b 10. b \mneq{} c 11. c \mneq{} a 12. x : Point 13. b-a-x 14. ax \mcong{} OX 15. y : Point 16. a-b-y 17. by \mcong{} OX 18. c1 : Point 19. x-a-c1 20. ac1 \mcong{} ac 21. c2 : Point 22. y-b-c2 23. bc2 \mcong{} bc 24. c1' : Point 25. b-a-c1' 26. ac1' \mcong{} ac1 27. c2' : Point 28. a-b-c2' 29. bc2' \mcong{} bc2 30. c1'' : Point 31. a\_b\_c1'' \mwedge{} bc1'' \mcong{} bc1 32. c2'' : Point 33. b\_a\_c2'' \mwedge{} ac2'' \mcong{} ac2 \mvdash{} \mexists{}c1,c1',c1'',c2,c2',c2'':Point ((ac1 \mcong{} ac \mwedge{} out(a bc1)) \mwedge{} (bc2 \mcong{} bc \mwedge{} out(b ac2)) \mwedge{} (b-a-c1' \mwedge{} ac1' \mcong{} ac1) \mwedge{} (a-b-c2' \mwedge{} bc2' \mcong{} bc2) \mwedge{} (a\_b\_c1'' \mwedge{} bc1'' \mcong{} bc1) \mwedge{} (b\_a\_c2'' \mwedge{} ac2'' \mcong{} ac2) \mwedge{} (a-c1-c2' \mwedge{} b-c2-c1') \mwedge{} (c1'-a-c1 \mwedge{} c2'-b-c2) \mwedge{} (c1'-c2-c2' \mwedge{} c2'-c1-c1') \mwedge{} c1'-c2-c1 \mwedge{} c2'-c1-c2) By Latex: ((InstConcl [\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{};\mkleeneopen{}c1''\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}c2'\mkleeneclose{};\mkleeneopen{}c2''\mkleeneclose{}]\mcdot{} THENA Auto) THEN GenRepD) Home Index