---

Step * of Lemma opp-side_half-plane-angle-congruence-lemma

∀e:EuclideanPlane. ∀b,p,b',p',a,c,a',c',d:Point.
  ((a leftof bp ∧ c leftof pb)
  ⇒ (a' leftof b'p' ∧ c' leftof p'b')
  ⇒ ((abp ≅a a'b'p' ∧ pbc ≅a p'b'c') ∧ (a-d-c ∧ out(b dp)) ∧ b ≠ d)
  ⇒ (∃a'',c'',d'':Point
       ((ba ≅ b'a'' ∧ (bc ≅ b'c'' ∧ bd ≅ b'd'') ∧ ad ≅ a''d'' ∧ dc ≅ d''c'' ∧ out(b' d''p')) ∧ a''_d''_c'')))
BY
{ (Auto
   THEN (Assert ∃a'',c'':Point. ((out(b' a'a'') ∧ out(b' c'c'')) ∧ ba ≅ b'a'' ∧ bc ≅ b'c'') BY
               ((((gProperProlong ⌜a'⌝⌜b'⌝`A'⌜a'⌝⌜b'⌝⋅ THENA Auto)
                  THEN (gProperProlong ⌜A⌝⌜b'⌝`a\'\''⌜b⌝⌜a⌝⋅ THENA Auto)
                  )
                 THEN (gProperProlong ⌜c'⌝⌜b'⌝`C'⌜a'⌝⌜b'⌝⋅ THENA Auto)
                 THEN (gProperProlong ⌜C⌝⌜b'⌝`c\'\''⌜b⌝⌜c⌝⋅ THENA Auto))
                THEN InstConcl [⌜a''⌝;⌜c''⌝]⋅
                THEN Auto))
   ) }

1
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. A : Point
21. a'-b'-A
22. b'A ≅ a'b'
23. a'' : Point
24. A-b'-a''
25. b'a'' ≅ ba
26. C : Point
27. c'-b'-C
28. b'C ≅ a'b'
29. c'' : Point
30. C-b'-c''
31. b'c'' ≅ bc
⊢ out(b' a'a'')

2
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. A : Point
21. a'-b'-A
22. b'A ≅ a'b'
23. a'' : Point
24. A-b'-a''
25. b'a'' ≅ ba
26. C : Point
27. c'-b'-C
28. b'C ≅ a'b'
29. c'' : Point
30. C-b'-c''
31. b'c'' ≅ bc
32. out(b' a'a'')
⊢ out(b' c'c'')

3
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. ∃a'',c'':Point. ((out(b' a'a'') ∧ out(b' c'c'')) ∧ ba ≅ b'a'' ∧ bc ≅ b'c'')
⊢ ∃a'',c'',d'':Point
   ((ba ≅ b'a'' ∧ (bc ≅ b'c'' ∧ bd ≅ b'd'') ∧ ad ≅ a''d'' ∧ dc ≅ d''c'' ∧ out(b' d''p')) ∧ a''_d''_c'')

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}b,p,b',p',a,c,a',c',d:Point.
    ((a  leftof  bp  \mwedge{}  c  leftof  pb)
    {}\mRightarrow{}  (a'  leftof  b'p'  \mwedge{}  c'  leftof  p'b')
    {}\mRightarrow{}  ((abp  \mcong{}\msuba{}  a'b'p'  \mwedge{}  pbc  \mcong{}\msuba{}  p'b'c')  \mwedge{}  (a-d-c  \mwedge{}  out(b  dp))  \mwedge{}  b  \mneq{}  d)
    {}\mRightarrow{}  (\mexists{}a'',c'',d'':Point
              ((ba  \mcong{}  b'a''  \mwedge{}  (bc  \mcong{}  b'c''  \mwedge{}  bd  \mcong{}  b'd'')  \mwedge{}  ad  \mcong{}  a''d''  \mwedge{}  dc  \mcong{}  d''c''  \mwedge{}  out(b'  d''p'))
              \mwedge{}  a''\_d''\_c'')))


By

---

Latex:
(Auto
  THEN  (Assert  \mexists{}a'',c'':Point.  ((out(b'  a'a'')  \mwedge{}  out(b'  c'c''))  \mwedge{}  ba  \mcong{}  b'a''  \mwedge{}  bc  \mcong{}  b'c'')  BY
                          ((((gProperProlong  \mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`A'\mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}\mcdot{}  THENA  Auto)
                                THEN  (gProperProlong  \mkleeneopen{}A\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`a\mbackslash{}'\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)
                                )
                              THEN  (gProperProlong  \mkleeneopen{}c'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`C'\mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THEN  (gProperProlong  \mkleeneopen{}C\mkleeneclose{}\mkleeneopen{}b'\mkleeneclose{}`c\mbackslash{}'\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto))
                            THEN  InstConcl  [\mkleeneopen{}a''\mkleeneclose{};\mkleeneopen{}c''\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  )

---

Home Index