【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [201-220]

jgex_ag_231 기하 문제 풀이 [201-220]

 

추천글 : 【AlphaGeometry】 jgex_ag_231 문제 재구성 및 풀이 

---

 

201. examples/complete2/unsolved/complete_015_7_Book_00EE_06_E056-33.gex

a b = segment a b; c = on_tline c a a b, on_circle c a b; e = s_angle b a e 60, on_circle e a b; d = s_angle b a d 30, on_circle d a b; f = on_line f a e, on_line f b c; g = on_line g a d, on_line g b c ? cong c f g b

 

○ 번역 

 

선분 AB가 주어져 있습니다. C는 A를 지나고 AB에 수직한 직선 위에 있으며, A를 중심으로 하고 B를 지나는 원 위에 있습니다.  E는 ∠BAE = 60°를 만족하고, A를 중심으로 하고 D를 지나는 원 위에 있습니다. D는 ∠BAD = 30°를 만족하고, A를 중심으로 하고 B를 지나는 원 위에 있습니다. F는 직선 AE와 BC의 교점이며, G는 직선 AD와 BC의 교점입니다. 선분 CF와 선분 GB의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
AC ⟂ AB [00]
AC = AB [01]
∠DAB = 1_PI/3 [02]
∠EAB = 1_PI/6 [03]
F,A,D are collinear [04]
F,C,B are collinear [05]
A,E,G are collinear [06]
C,G,B are collinear [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AC ⟂ AB [00] & ∠DAB = 1_PI/3 [02] (Angle chase)⇒  ∠CAD = 1_PI/6 [08]
002. A,E,G are collinear [06] & F,A,D are collinear [04] & ∠CAD = 1_PI/6 [08] & ∠EAB = 1_PI/6 [03] ⇒  ∠GAB = ∠CAF [09]
003. AC = AB [01] ⇒  ∠CBA = ∠ACB [10]
004. C,G,B are collinear [07] & F,C,B are collinear [05] & ∠CBA = ∠ACB [10] ⇒  ∠GBA = ∠ACF [11]
005. ∠GAB = ∠CAF [09] & ∠GBA = ∠ACF [11] (Similar Triangles)⇒  BA:CA = BG:CF [12]
006. BA:CA = BG:CF [12] & AC = AB [01] ⇒  BG = CF
==========================

 

 

202. examples/complete2/unsolved/complete_005_Other_unsolved_E074-24.gex

a b = segment a b; c = on_tline c a a b; d = foot d a b c; e = midpoint e d a; f = on_line f b e, on_line f a c; g = foot g f b c; h = midpoint h c a; i = on_tline i f a c, on_circle i h a ? cong f i f g

 

○ 번역 

 

선분 AB가 주어져 있습니다. C는 A를 지나고 AB에 수직한 직선 위에 있습니다. D는 A에서 BC로 내린 수선의 발입니다. E는 선분 DA의 중점입니다. F는 직선 BE와 AC의 교점입니다. G는 F에서 BC로 내린 수선의 발입니다. H는 선분 CA의 중점입니다. I는 F를 지나고 AC에 수직한 직선 위에 있으며, H를 중심으로 하고 A를 지나는 원 위에 있습니다. 선분 FI와 선분 FG의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
AC ⟂ AB [00]
AD ⟂ BC [01]
C,D,B are collinear [02]
ED = EA [03]
A,E,D are collinear [04]
A,C,F are collinear [05]
E,F,B are collinear [06]
BC ⟂ GF [07]
C,G,B are collinear [08]
A,H,C are collinear [09]
HC = HA [10]
AC ⟂ IF [11]
HI = HA [12]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. BC ⟂ GF [07] & AD ⟂ BC [01] ⇒  GF ∥ AD [13]
002. C,D,B are collinear [02] & C,G,B are collinear [08] ⇒  C,D,G are collinear [14]
003. C,D,B are collinear [02] & C,G,B are collinear [08] ⇒  B,D,G are collinear [15]
004. FG ∥ AD [13] & A,C,F are collinear [05] & C,D,G are collinear [14] ⇒  AC:AF = CD:GD [16]
005. A,E,D are collinear [04] & FG ∥ AD [13] ⇒  ED ∥ FG [17]
006. ED ∥ FG [17] & E,F,B are collinear [06] & B,D,G are collinear [15] ⇒  EB:EF = DB:GD [18]
007. ED ∥ FG [17] & E,F,B are collinear [06] & B,D,G are collinear [15] ⇒  BE:BF = ED:FG [19]
008. BE:BF = ED:FG [19] & ED = EA [03] ⇒  EB:FB = AE:GF [20]
009. A,H,C are collinear [09] & HC = HA [10] ⇒  H is midpoint of AC [21]
010. A,E,D are collinear [04] & ED = EA [03] ⇒  E is midpoint of AD [22]
011. H is midpoint of AC [21] & E is midpoint of AD [22] ⇒  HE ∥ CD [23]
012. CD ∥ HE [23] & A,H,C are collinear [09] & A,E,D are collinear [04] ⇒  AC:AH = AD:AE [24]
013. CD ∥ HE [23] & A,H,C are collinear [09] & A,E,D are collinear [04] ⇒  AC:AH = CD:HE [25]
014. C,D,B are collinear [02] & BC ⟂ AD [01] ⇒  CD ⟂ DA [26]
015. CD ⟂ DA [26] & H is midpoint of AC [21] ⇒  AH = DH [27]
016. AC:AH = AD:AE [24] & AH = DH [27] ⇒  AC:DH = AD:AE [28]
017. AC:AH = CD:HE [25] & AH = DH [27] ⇒  AC:DH = CD:EH [29]
018. HE ∥ CD [23] & C,D,B are collinear [02] ⇒  EH ∥ BC [30]
019. A,H,C are collinear [09] & A,C,F are collinear [05] ⇒  F,C,H are collinear [31]
020. EH ∥ BC [30] & F,C,H are collinear [31] & E,F,B are collinear [06] ⇒  CF:HF = FB:EF [32]
021. EH ∥ BC [30] & F,C,H are collinear [31] & E,F,B are collinear [06] ⇒  CF:HF = CB:EH [33]
022. C,D,B are collinear [02] & G,C,B are collinear [08] & AD ⟂ BC [01] & AD ∥ FG [13] ⇒  ∠BDA = ∠FGC [34]
023. A,H,C are collinear [09] & AC ⟂ AB [00] ⇒  AH ⟂ AB [35]
024. C,G,B are collinear [08] & A,E,D are collinear [04] & BC ⟂ AD [01] ⇒  CG ⟂ AE [36]
025. AH ⟂ AB [35] & CG ⟂ AE [36] ⇒  ∠HAE = ∠(AB-CG) [37]
026. C,A,F are collinear [05] & C,D,B are collinear [02] & ∠HAE = ∠(AB-CG) [37] & A,H,C are collinear [09] & A,E,D are collinear [04] & C,G,B are collinear [08] & AD ∥ FG [13] ⇒  ∠CFG = ∠ABD [38]
027. ∠BDA = ∠FGC [34] & ∠CFG = ∠ABD [38] (Similar Triangles)⇒  CG:GF = AD:DB [39]
028. A,C,F are collinear [05] & AC ⟂ AB [00] & AC ⟂ IF [11] ⇒  ∠AFI = ∠IFC [40]
029. HI = HA [12] & HC = HA [10] ⇒  H is the circumcenter of \Delta AIC [41]
030. H is the circumcenter of \Delta AIC [41] & AH ⟂ AB [35] ⇒  ∠IAB = ∠ICA [42]
031. C,A,F are collinear [05] & ∠IAB = ∠ICA [42] & AC ⟂ IF [11] & AC ⟂ AB [00] ⇒  ∠AIF = ∠ICF [43]
032. ∠AFI = ∠IFC [40] & ∠AIF = ∠ICF [43] (Similar Triangles)⇒  AF:IF = IF:CF [44]
033. G,C,B are collinear [08] & AC ⟂ AB [00] & AD ⟂ BC [01] & AD ∥ FG [13] ⇒  ∠CGF = ∠BAC [45]
034. C,A,F are collinear [05] & ∠HAE = ∠(AB-CG) [37] & A,H,C are collinear [09] & A,E,D are collinear [04] & C,G,B are collinear [08] & AD ∥ FG [13] ⇒  ∠CFG = ∠ABC [46]
035. ∠CGF = ∠BAC [45] & ∠CFG = ∠ABC [46] (Similar Triangles)⇒  CG:CF = AC:CB [47]
036. ED = EA [03] & AC:AF = CD:GD [16] & EB:EF = DB:GD [18] & EB:FB = AE:GF [20] & AC:DH = AD:AE [28] & AC:DH = CD:EH [29] & CF:HF = FB:EF [32] & CF:HF = CB:EH [33] & CG:GF = AD:DB [39] & AF:IF = IF:CF [44] & CG:CF = AC:CB [47] (Ratio chase)⇒  GF = IF
==========================

 

 

203. examples/complete2/unsolved1/complete_008_7_Book_LLL_L057-3.gex

a b = segment a b; c = on_bline c a b; e = midpoint e a c; d = mirror d c a; f = midpoint f b d ? cong e b f b

 

○ 번역 

 

선분 AB가 주어져 있습니다. C는 AB의 수직이등분선 위에 있습니다. E는 선분 AC의 중점이고, A는 CD의 중점입니다. F는 선분 BD의 중점입니다. 선분 EB와 선분 FB의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
CA = CB [00]
A,D,C are collinear [01]
DA = DC [02]
E,A,C are collinear [03]
AC = AE [04]
FB = FE [05]
E,F,B are collinear [06]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. E,A,C are collinear [03] & AC = AE [04] ⇒  A is midpoint of EC [07]
002. E,F,B are collinear [06] & FB = FE [05] ⇒  F is midpoint of EB [08]
003. A is midpoint of EC [07] & F is midpoint of EB [08] ⇒  AF ∥ CB [09]
004. AF ∥ BC [09] & E,F,B are collinear [06] & E,A,C are collinear [03] ⇒  EB:EF = BC:FA [10]
005. A,D,C are collinear [01] & DA = DC [02] ⇒  D is midpoint of AC [11]
006. D is midpoint of AC [11] & F is midpoint of EB [08] ⇒  DA:AC = FE:EB [12]
007. EB:EF = BC:FA [10] & AC = AE [04] & CA = CB [00] & DA:AC = FE:EB [12] & DA = DC [02] ⇒  CD:CB = AF:AE [13]
008. D,A,C are collinear [01] & E,A,C are collinear [03] & BC ∥ AF [09] ⇒  ∠DCB = ∠EAF [14]
009. CD:CB = AF:AE [13] & ∠DCB = ∠EAF [14] (Similar Triangles)⇒  BC:EA = BD:EF [15]
010. FB = FE [05] & BC:EA = BD:EF [15] & AC = AE [04] & CA = CB [00] ⇒  DB = FB
==========================

 

 

204. examples/complete2/unsolved1/complete_006_7_Book_LLL_L046-17.gex

c a b = risos c a b; d = midpoint d b a; e = on_line e a b; f = foot f e a c; g = foot g e b c ? cong d f d g

 

○ 번역 

 

AB = AC이고 AB와 AC가 수직한 직각삼각형 ABC가 주어져 있습니다. D는 선분 BA의 중점입니다. E는 직선 AB 위에 있고, F는 E에서 AC로 내린 수선의 발이며, G는 E에서 BC로 내린 수선의 발입니다. 선분 DF와 선분 DG의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
AB ⟂ AC [00]
AB = AC [01]
C,D,B are collinear [02]
DC = DB [03]
C,E,B are collinear [04]
A,B,F are collinear [05]
BA ⟂ FE [06]
A,C,G are collinear [07]
CA ⟂ GE [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AB = AC [01] & DC = DB [03] ⇒  BC ⟂ AD [09]
002. AB = AC [01] & DC = DB [03] ⇒  DC:DB = AC:AB [10]
003. C,E,B are collinear [04] & C,D,B are collinear [02] & A,B,F are collinear [05] & AB ⟂ AC [00] & BC ⟂ AD [09] & BA ⟂ FE [06] ⇒  ∠EDA = ∠EFA [11]
004. ∠EDA = ∠EFA [11] ⇒  A,D,E,F are concyclic [12]
005. A,B,F are collinear [05] & A,C,G are collinear [07] & AB ⟂ AC [00] & BA ⟂ FE [06] & CA ⟂ GE [08] ⇒  ∠FEG = ∠FAG [13]
006. ∠FEG = ∠FAG [13] ⇒  A,E,G,F are concyclic [14]
007. A,D,E,F are concyclic [12] & A,E,G,F are concyclic [14] ⇒  D,G,F,A are concyclic [15]
008. DC:DB = AC:AB [10] & C,D,B are collinear [02] ⇒  ∠DAC = ∠BAD [16]
009. A,C,G are collinear [07] & A,B,F are collinear [05] & ∠DAC = ∠BAD [16] ⇒  ∠DAG = ∠FAD [17]
010. D,G,F,A are concyclic [15] & ∠DAG = ∠FAD [17] ⇒  DG = FD
==========================

 

 

205. examples/complete2/unsolved1/complete_008_7_Book_LLL_L057-2.gex

c a b = triangle a b c; d = angle_bisector d b a c; e = foot e c a d; f = intersection_lp f a c e a b ? cong f e f c

 

○ 번역 : 추후 업데이트 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
B C A D E F : Points
∠CBD = ∠DBA [00]
AE ⟂ BD [01]
A,F,B are collinear [02]
EF ∥ BC [03]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. ∠CBD = ∠DBA [00] & AE ⟂ BD [01] (Angle chase)⇒  ∠BAE = ∠(AE-BC) [04]
002. A,F,B are collinear [02] & ∠BAE = ∠(AE-BC) [04] & BC ∥ EF [03] ⇒  ∠FAE = ∠AEF [05]
003. ∠FAE = ∠AEF [05] ⇒  FA = FE
==========================

 

 

206. examples/complete2/unsolved1/complete_008_ex-gao_ex160_e102.gex

a b c = triangle a b c; d = on_line d a c, angle_bisector d c b a; e = on_line e a b, angle_bisector e b c a; f = foot f a c e; g = foot g a b d ? para g f b c 

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 직선 AC 위에 있으며, ∠CBA의 이등분선 위에 있습니다. E는 직선 AB 위에 있으며, ∠BCA의 이등분선 위에 있습니다. F는 A에서 CE로 내린 수선의 발이고, G는 A에서 BD로 내린 수선의 발입니다. 선분 GF와 선분 BC가 서로 평행임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
∠CBD = ∠DBA [00]
∠BCE = ∠ECA [01]
E,C,F are collinear [02]
AF ⟂ CE [03]
B,G,D are collinear [04]
AG ⟂ BD [05]

 * Auxiliary Constructions:
H I : Points
C,H,A are collinear [06]
HC = HA [07]
B,I,A are collinear [08]
IB = IA [09]

 * Proof steps:
001. B,G,D are collinear [04] & AG ⟂ BD [05] ⇒  GA ⟂ BG [10]
002. B,I,A are collinear [08] & IB = IA [09] ⇒  I is midpoint of AB [11]
003. GA ⟂ BG [10] & I is midpoint of AB [11] ⇒  BI = GI [12]
004. BI = GI [12] ⇒  ∠IGB = ∠GBI [13]
005. C,H,A are collinear [06] & HC = HA [07] ⇒  H is midpoint of AC [14]
006. H is midpoint of AC [14] & I is midpoint of AB [11] ⇒  HI ∥ CB [15]
007. B,G,D are collinear [04] & ∠IGB = ∠GBI [13] & B,I,A are collinear [08] & ∠CBD = ∠DBA [00] & BC ∥ HI [15] ⇒  ∠(IH-BG) = ∠IGB [16]
008. ∠(IH-BG) = ∠IGB [16] ⇒  IH ∥ IG [17]
009. HI ∥ GI [17] ⇒  I,G,H are collinear [18]
010. F,E,C are collinear [02] & AF ⟂ CE [03] ⇒  AF ⟂ FC [19]
011. AF ⟂ FC [19] & H is midpoint of AC [14] ⇒  CH = FH [20]
012. CH = FH [20] ⇒  ∠HFC = ∠FCH [21]
013. ∠HFC = ∠FCH [21] & E,C,F are collinear [02] & C,H,A are collinear [06] & ∠BCE = ∠ECA [01] & BC ∥ HI [15] ⇒  ∠(IH-EC) = ∠(FH-EC) [22]
014. ∠(IH-EC) = ∠(FH-EC) [22] ⇒  IH ∥ FH [23]
015. HI ∥ FH [23] ⇒  F,I,H are collinear [24]
016. C,H,A are collinear [06] & B,I,A are collinear [08] ⇒  ∠CAB = ∠HAI [25]
017. B,I,A are collinear [08] & BC ∥ HI [15] ⇒  ∠CBA = ∠HIA [26]
018. ∠CAB = ∠HAI [25] & ∠CBA = ∠HIA [26] (Similar Triangles)⇒  ∠ACB = ∠AHI [27]
019. I,G,H are collinear [18] & F,I,H are collinear [24] & ∠ACB = ∠AHI [27] & C,H,A are collinear [06] ⇒  GF ∥ BC
==========================

 

 

207. examples/complete2/unsolved1/complete_012_7_Book_00EE_11_E075-27f.gex

a b c = triangle a b c; d = foot d c a b; e = on_line e c d; f = on_line f b e, on_line f a c; g = on_line g a e, on_line g b c ? eqangle d f d c d c d g

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 C에서 AB로 내린 수선의 발입니다. E는 직선 CD 위에 있습니다. F는 직선 BE와 AC의 교점입니다. G는 직선 AE와 BC의 교점입니다. ∠FDC = ∠CDG임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용하면 다음과 같은 에러가 발생함 

 

ValueError: cd and cd Cannot be perp.

 

 

208. examples/complete2/unsolved1/complete_006_7_Book_LLL_L091-13.gex

b c d = triangle b c d; e = midpoint e c d; a = eqdistance a d c b, on_pline a b d c; f = midpoint f b a ? perp a b e f

 

○ 번역 

 

삼각형 BCD가 주어져 있습니다. E는 선분 CD의 중점입니다. A는 AD = CB가 성립하며, B를 지나고 DC에 평행한 직선 위에 있습니다. F는 선분 BA의 중점입니다. 선분 AB와 선분 EF가 서로 수직임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
C,B,D are collinear [00]
DB = DC [01]
EA ∥ CB [02]
EC = BA [03]
FA = FE [04]

 * Auxiliary Constructions:
G H : Points
GA = CD [05]
GA ∥ CD [06]
E,C,H are collinear [07]
H,G,D are collinear [08]

 * Proof steps:
001. C,B,D are collinear [00] & GA ∥ CD [06] ⇒  ∠AGD = ∠CDG [09]
002. GA = CD [05] & ∠AGD = ∠CDG [09] (SAS)⇒  DA = GC [10]
003. GA ∥ CD [06] & C,B,D are collinear [00] & AE ∥ BC [02] ⇒  AE ∥ AG [11]
004. AE ∥ AG [11] ⇒  E,A,G are collinear [12]
005. E,A,G are collinear [12] & C,B,D are collinear [00] & AE ∥ BC [02] ⇒  EG ∥ CD [13]
006. EG ∥ CD [13] & E,C,H are collinear [07] & H,G,D are collinear [08] ⇒  EC:GD = EH:GH [14]
007. EG ∥ CD [13] & E,C,H are collinear [07] & H,G,D are collinear [08] ⇒  CE:DG = CH:DH [15]
008. DB = DC [01] & GA = CD [05] ⇒  AG = DB [16]
009. C,B,D are collinear [00] & GA ∥ CD [06] ⇒  ∠AGB = ∠DBG [17]
010. AG = DB [16] & ∠AGB = ∠DBG [17] (SAS)⇒  BA = GD [18]
011. EC:GD = EH:GH [14] & BA = GD [18] & EC = BA [03] ⇒  EH = GH [19]
012. CE:DG = CH:DH [15] & BA = GD [18] & EC = BA [03] ⇒  CH = DH [20]
013. G,H,D are collinear [08] & E,C,H are collinear [07] ⇒  ∠GHC = ∠DHE [21]
014. EH = GH [19] & CH = DH [20] & ∠GHC = ∠DHE [21] (SAS)⇒  CG = DE [22]
015. DA = GC [10] & CG = DE [22] ⇒  DE = DA [23]
016. FA = FE [04] & DE = DA [23] ⇒  AE ⟂ DF
==========================

 

 

209. examples/complete2/unsolved1/complete_010_Other_gao_Y_yL157-1.gex

a b d = triangle a b d; e = midpoint e d a; c = angle_bisector c a b d, on_dia c a b ? para c e b d

 

○ 번역 

 

삼각형 ABD가 주어져 있습니다. E는 선분 DA의 중점입니다. C는 ∠ABD의 이등분선 위에 있으며, AC와 BC가 수직합니다. 선분 CE와 선분 BD가 서로 평행임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E : Points
C,A,D are collinear [00]
DC = DA [01]
AE ⟂ BE [02]
∠EBA = ∠CBE [03]

 * Auxiliary Constructions:
F : Points
B,A,F are collinear [04]
FB = FA [05]

 * Proof steps:
001. C,A,D are collinear [00] & DC = DA [01] ⇒  D is midpoint of AC [06]
002. B,A,F are collinear [04] & FB = FA [05] ⇒  F is midpoint of AB [07]
003. D is midpoint of AC [06] & F is midpoint of AB [07] ⇒  DF ∥ CB [08]
004. C,A,D are collinear [00] & DF ∥ BC [08] ⇒  ∠FDA = ∠BCA [09]
005. B,F,A are collinear [04] & C,A,D are collinear [00] ⇒  ∠FAD = ∠BAC [10]
006. ∠FDA = ∠BCA [09] & ∠FAD = ∠BAC [10] (Similar Triangles)⇒  ∠DFA = ∠CBA [11]
007. AE ⟂ BE [02] & F is midpoint of AB [07] ⇒  BF = EF [12]
008. BF = EF [12] ⇒  ∠FEB = ∠EBF [13]
009. ∠FEB = ∠EBF [13] & B,A,F are collinear [04] & ∠EBA = ∠CBE [03] ⇒  ∠CBE = ∠FEB [14]
010. ∠CBE = ∠FEB [14] ⇒  CB ∥ EF [15]
011. BC ∥ EF [15] & DF ∥ BC [08] ⇒  FD ∥ FE [16]
012. FD ∥ FE [16] ⇒  E,F,D are collinear [17]
013. ∠DFA = ∠CBA [11] & E,F,D are collinear [17] & B,A,F are collinear [04] ⇒  DE ∥ BC
==========================

 

 

210. examples/complete2/unsolved1/complete_008_7_Book_LLL_L055-5.gex

d b a = triangle d b a; c = angle_bisector c d a b, angle_bisector c d b a; e = on_line e b c, on_tline e d b c; f = on_line f a c, on_tline f d a c ? para e f a b

 

○ 번역 

 

삼각형 DBA가 주어져 있습니다. C는 ∠DAB와 ∠DBA의 이등분선 위에 있습니다. E는 직선 BC 위에 있으며, D를 지나고 BC에 수직인 직선 위에 있습니다. F는 직선 AC 위에 있으며, D를 지나고 AC에 수직인 직선 위에 있습니다. 선분 EF와 선분 AB가 서로 평행임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
∠ABD = ∠DBC [00]
∠ACD = ∠DCB [01]
D,E,B are collinear [02]
AE ⟂ BD [03]
D,F,C are collinear [04]
AF ⟂ CD [05]

 * Auxiliary Constructions:
G : Points
BG = BC [06]
DG = DC [07]

 * Proof steps:
001. D,E,B are collinear [02] & D,F,C are collinear [04] & AF ⟂ CD [05] & AE ⟂ BD [03] ⇒  ∠AED = ∠AFD [08]
002. ∠AED = ∠AFD [08] ⇒  A,D,F,E are concyclic [09]
003. A,D,F,E are concyclic [09] ⇒  ∠ADF = ∠AEF [10]
004. BG = BC [06] & DG = DC [07] ⇒  BD ⟂ GC [11]
005. BG = BC [06] & DG = DC [07] (SSS)⇒  ∠GBD = ∠DBC [12]
006. BG = BC [06] & DG = DC [07] (SSS)⇒  ∠(CD-BG) = ∠(BC-DG) [13]
007. D,E,B are collinear [02] & ∠GBD = ∠DBC [12] & ∠ABD = ∠DBC [00] ⇒  ∠(AB-DE) = ∠(GB-DE) [14]
008. ∠(AB-DE) = ∠(GB-DE) [14] ⇒  AB ∥ GB [15]
009. AB ∥ BG [15] ⇒  A,G,B are collinear [16]
010. D,F,C are collinear [04] & ∠ACD = ∠DCB [01] ⇒  ∠(AC-DF) = ∠(DF-CB) [17]
011. D,F,C are collinear [04] & ∠(CD-BG) = ∠(BC-DG) [13] ⇒  ∠(DF-GB) = ∠(CB-DG) [18]
012. ∠(AC-DF) = ∠(DF-CB) [17] & ∠(DF-GB) = ∠(CB-DG) [18] ⇒  ∠(AC-GB) = ∠FDG [19]
013. A,B,G are collinear [16] & ∠(AC-GB) = ∠FDG [19] & D,F,C are collinear [04] & BG ∥ AB [15] ⇒  ∠AGD = ∠ACD [20]
014. ∠AGD = ∠ACD [20] ⇒  A,D,C,G are concyclic [21]
015. A,D,C,G are concyclic [21] ⇒  ∠ADC = ∠AGC [22]
016. BG = BC [06] ⇒  ∠CGB = ∠BCG [23]
017. ∠ADF = ∠AEF [10] & D,F,C are collinear [04] & BD ⟂ GC [11] & AE ⟂ BD [03] & ∠ADC = ∠AGC [22] & A,G,B are collinear [16] & AB ∥ BG [15] & ∠CGB = ∠BCG [23] ⇒  ∠(CB-AE) = ∠FEA [24]
018. ∠(CB-AE) = ∠FEA [24] ⇒  CB ∥ FE
==========================

 

 

211. examples/complete2/unsolved1/complete_013_7_Book_00EE_11_E075-29.gex

a b = segment a b; d = midpoint d b a; f = on_circle f d a; c = intersection_lt c a b f d f; e = midpoint e c a; g = on_tline g b a b, on_circle g e a ? eqangle f c f g g f g c

 

○ 번역 : 추후 업데이트 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
CB = CA [00]
CD = CA [01]
B,E,A are collinear [02]
DE ⟂ CD [03]
∠(DE-AB) = ∠(DE-AB) [04]
F,E,A are collinear [05]
FE = FA [06]
BG ⟂ AB [07]
FG = FA [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. CB = CA [00] & CD = CA [01] ⇒  C is the circumcenter of \Delta DBA [09]
002. C is the circumcenter of \Delta DBA [09] & DE ⟂ CD [03] ⇒  ∠EDA = ∠DBA [10]
003. B,E,A are collinear [02] & ∠DBA = ∠EDA [10] ⇒  ∠DBE = ∠EDA [11]
004. B,E,A are collinear [02] & ∠(DE-AB) = ∠(DE-AB) [04] ⇒  ∠DEB = ∠DEA [12]
005. ∠DBE = ∠EDA [11] & ∠DEB = ∠DEA [12] (Similar Triangles)⇒  BD:DE = DA:EA [13]
006. ∠DBE = ∠EDA [11] & ∠DEB = ∠DEA [12] (Similar Triangles)⇒  BD:BE = DA:DE [14]
007. B,E,A are collinear [02] & BG ⟂ AB [07] ⇒  ∠EBG = ∠GBA [15]
008. F,E,A are collinear [05] & B,E,A are collinear [02] & AB ⟂ BG [07] ⇒  FB ⟂ BG [16]
009. FG = FA [08] & FE = FA [06] ⇒  F is the circumcenter of \Delta EGA [17]
010. F is the circumcenter of \Delta EGA [17] & F,E,A are collinear [05] ⇒  EG ⟂ AG [18]
011. FB ⟂ BG [16] & EG ⟂ AG [18] ⇒  ∠(FB-AG) = ∠BGE [19]
012. FB ⟂ BG [16] & EG ⟂ AG [18] ⇒  ∠(FB-EG) = ∠BGA [20]
013. ∠(FB-AG) = ∠BGE [19] & F,E,A are collinear [05] & B,E,A are collinear [02] ⇒  ∠BAG = ∠BGE [21]
014. ∠EBG = ∠GBA [15] & ∠BAG = ∠BGE [21] (Similar Triangles)⇒  BE:EG = BG:AG [22]
015. ∠EBG = ∠GBA [15] & ∠BAG = ∠BGE [21] (Similar Triangles)⇒  BE:BG = BG:BA [23]
016. EG ⟂ AG [18] & BG ⟂ AB [07] ⇒  ∠ABG = ∠EGA [24]
017. B,E,A are collinear [02] & ∠(FB-EG) = ∠BGA [20] & F,E,A are collinear [05] ⇒  ∠AGB = ∠GEA [25]
018. ∠ABG = ∠EGA [24] & ∠AGB = ∠GEA [25] (Similar Triangles)⇒  BA:AG = AG:EA [26]
019. BD:DE = DA:EA [13] & BD:BE = DA:DE [14] & BE:EG = BG:AG [22] & BE:BG = BG:BA [23] & BA:AG = AG:EA [26] (Ratio chase)⇒  DE = EG [27]
020. DE = EG [27] ⇒  ∠EDG = ∠DGE
==========================

 

 

212. examples/complete2/unsolved1/complete_012_7_Book_00EE_05_E051-14-1.gex

a b c d = quadrangle a b c d; e = midpoint e b a; f = foot f a c d; g = foot g b c d ? cong e f e g

 

○ 번역 

 

사각형 ABCD가 주어져 있습니다. E는 선분 BA의 중점입니다. F는 A에서 CD로 내린 수선의 발이고, G는 B에서 CD로 내린 수선의 발입니다. 선분 EF와 선분 EG의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
E,B,A are collinear [00]
EB = EA [01]
D,F,C are collinear [02]
AF ⟂ CD [03]
D,G,C are collinear [04]
CD ⟂ GB [05]

 * Auxiliary Constructions:
H : Points
H,F,B are collinear [06]
HF = HB [07]

 * Proof steps:
001. D,G,C are collinear [04] & D,F,C are collinear [02] & BG ⟂ CD [05] ⇒  BG ⟂ GF [08]
002. H,F,B are collinear [06] & HF = HB [07] ⇒  H is midpoint of BF [09]
003. BG ⟂ GF [08] & H is midpoint of BF [09] ⇒  FH = GH [10]
004. BG ⟂ GF [08] & H is midpoint of BF [09] ⇒  BH = GH [11]
005. BH = GH [11] ⇒  ∠HBG = ∠BGH [12]
006. E,B,A are collinear [00] & EB = EA [01] ⇒  E is midpoint of BA [13]
007. E is midpoint of BA [13] & H is midpoint of BF [09] ⇒  EH ∥ AF [14]
008. H,F,B are collinear [06] & ∠HBG = ∠BGH [12] & CD ⟂ GB [05] & AF ⟂ CD [03] & AF ∥ EH [14] ⇒  ∠FHE = ∠EHG [15]
009. FH = GH [10] & ∠FHE = ∠EHG [15] (SAS)⇒  EF = EG
==========================

 

 

213. examples/complete2/unsolved1/complete_007_7_Book_LLL_L057-3-1.gex

a b = segment a b; c = on_bline c a b; e = midpoint e a c; f = mirror f b e; d = on_circle d a c, on_line d a c ? cong f b b d

 

○ 번역 

 

선분 AB가 주어져 있습니다. C는 AB의 수직이등분선 위에 있고, E는 선분 AC의 중점입니다. E는 선분 BF의 중점입니다. D는 A를 중심으로 하고 C를 지나는 원 위에 있으며, 직선 AC 위에 있습니다. 선분 FB와 선분 BD의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
CA = CB [00]
∠BAC = ∠CBA [01]
DA = DC [02]
C,A,D are collinear [03]
DB = DE [04]
B,D,E are collinear [05]
AF = AC [06]
F,C,A are collinear [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. C,A,D are collinear [03] & B,D,E are collinear [05] ⇒  ∠ADE = ∠CDB [08]
002. DA = DC [02] & DB = DE [04] & ∠ADE = ∠CDB [08] (SAS)⇒  EA = BC [09]
003. AF = AC [06] & CA = CB [00] & EA = BC [09] ⇒  AE = AF [10]
004. C,A,D are collinear [03] & DA = DC [02] ⇒  D is midpoint of CA [11]
005. B,D,E are collinear [05] & DB = DE [04] ⇒  D is midpoint of BE [12]
006. D is midpoint of CA [11] & D is midpoint of BE [12] ⇒  CB ∥ AE [13]
007. F,C,A are collinear [07] & ∠CBA = ∠BAC [01] & BC ∥ AE [13] ⇒  ∠EAB = ∠BAF [14]
008. AE = AF [10] & ∠EAB = ∠BAF [14] (SAS)⇒  BE = BF
==========================

 

 

214. examples/complete2/unsolved1/complete_001_6_GDD_FULL_61-80_80.gex

a b c = triangle a b c; o = circle o a b c; u = angle_bisector u b a c, on_line u b c; t = on_tline t a a o, on_line t b c ? cong t a t u

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. O는 삼각형 ABC의 외심입니다. U는 ∠BAC의 이등분선 위에 있으며, 직선 BC 위에 있습니다. T는 A를 지나고 AO에 수직한 직선 위에 있으며, 직선 BC 위에 있습니다. 선분 TA와 선분 TU의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
DA = DB [00]
DB = DC [01]
E,C,B are collinear [02]
∠BAE = ∠EAC [03]
F,C,B are collinear [04]
AF ⟂ AD [05]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. DA = DB [00] & DB = DC [01] ⇒  DC = DA [06]
002. DC = DA [06] ⇒  ∠DCA = ∠CAD [07]
003. DB = DC [01] ⇒  ∠DCB = ∠CBD [08]
004. DA = DB [00] ⇒  ∠DAB = ∠ABD [09]
005. ∠BAE = ∠EAC [03] & AF ⟂ AD [05] & ∠DCA = ∠CAD [07] & ∠DCB = ∠CBD [08] & ∠DAB = ∠ABD [09] (Angle chase)⇒  ∠FAE = ∠(AE-BC) [10]
006. F,C,B are collinear [04] & E,C,B are collinear [02] & ∠FAE = ∠(AE-BC) [10] ⇒  ∠FAE = ∠AEF [11]
007. ∠FAE = ∠AEF [11] ⇒  FA = FE
==========================

 

 

215. examples/complete2/unsolved1/complete_008_ex-gao_ex160_e213.gex

a b c = triangle a b c; d = midpoint d a b; e = midpoint e c a; f = on_line f d e, angle_bisector f c b a ? perp a f b f

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 선분 AB의 중점이고, E는 선분 CA의 중점입니다. F는 직선 DE 위에 있으며, ∠CBA의 이등분선 위에 있습니다. 선분 AF와 선분 BF가 서로 수직임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
A,D,B are collinear [00]
DA = DB [01]
A,C,E are collinear [02]
EC = EA [03]
D,E,F are collinear [04]
∠FBC = ∠ABF [05]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. A,D,B are collinear [00] & DA = DB [01] ⇒  D is midpoint of AB [06]
002. A,C,E are collinear [02] & EC = EA [03] ⇒  E is midpoint of AC [07]
003. D is midpoint of AB [06] & E is midpoint of AC [07] ⇒  DE ∥ BC [08]
004. A,D,B are collinear [00] & F,E,D are collinear [04] & ∠ABF = ∠FBC [05] & BC ∥ DE [08] ⇒  ∠DBF = ∠BFD [09]
005. ∠DBF = ∠BFD [09] ⇒  DB = DF [10]
006. DB = DF [10] & DA = DB [01] ⇒  D is the circumcenter of \Delta AFB [11]
007. D is the circumcenter of \Delta AFB [11] & A,D,B are collinear [00] ⇒  AF ⟂ BF
==========================

 

 

216. examples/complete2/unsolved1/complete_011_7_Book_00EE_04_E051-2.gex

a b c = triangle a b c; d = on_line d a b; e = on_pline e d b c, on_line e a c; f = on_line f c d, on_line f b e; g = on_line g a f, on_line g b c ? midp g b c

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 직선 AB 위에 있습니다. E는 D를 지나고 BC에 평행한 직선 위에 있으며, 직선 AC 위에 있습니다. F는 직선 CD와 BE의 교점에 있습니다. G는 직선 AF와 BC의 교점입니다. G가 선분 BC의 중점임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
B,D,A are collinear [00]
ED ∥ BC [01]
E,C,A are collinear [02]
B,E,F are collinear [03]
C,D,F are collinear [04]
B,G,C are collinear [05]
G,F,A are collinear [06]

 * Auxiliary Constructions:
H : Points
AH = AC [07]
H,C,A are collinear [08]

 * Proof steps:
001. DE ∥ BC [01] & E,C,A are collinear [02] & B,D,A are collinear [00] ⇒  EA:CA = ED:BC [09]
002. DE ∥ BC [01] & B,E,F are collinear [03] & C,D,F are collinear [04] ⇒  EF:BF = ED:BC [10]
003. EA:CA = ED:BC [09] & EF:BF = ED:BC [10] & HA = CA [07] ⇒  EF:FB = EA:AH [11]
004. H,C,A are collinear [08] & E,C,A are collinear [02] ⇒  E,A,H are collinear [12]
005. EF:FB = EA:AH [11] & B,E,F are collinear [03] & E,A,H are collinear [12] ⇒  FA ∥ BH [13]
006. G,F,A are collinear [06] & AF ∥ BH [13] ⇒  GA ∥ BH [14]
007. GA ∥ BH [14] & B,G,C are collinear [05] & H,C,A are collinear [08] ⇒  AC:AH = GC:GB [15]
008. B,G,C are collinear [05] & AC:AH = GC:GB [15] & AH = AC [07] ⇒  G is midpoint of BC
==========================

 

 

217. examples/complete2/unsolved1/complete_007_7_Book_LLL_L043-5.gex

a b = segment a b; c = on_circle c a b; d = on_circle d a b; e = on_circle e a b; f = intersection_ll f b c d e; g = intersection_ll g c d b e; h = angle_bisector h d f b; i = angle_bisector i c g b; j = intersection_ll j f h g i ? perp g i f h

 

○ 번역 : 추후 업데이트 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
AC = AB [00]
AD = AB [01]
AE = AB [02]
E,F,D are collinear [03]
C,F,B are collinear [04]
D,G,C are collinear [05]
E,G,B are collinear [06]
∠DFH = ∠HFB [07]
∠CGI = ∠IGB [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. ∠DFH = ∠HFB [07] & E,F,D are collinear [03] & C,F,B are collinear [04] ⇒  ∠(DE-FH) = ∠(FH-BC) [09]
002. ∠CGI = ∠IGB [08] & D,G,C are collinear [05] & E,G,B are collinear [06] ⇒  ∠(CD-GI) = ∠(GI-BE) [10]
003. AC = AB [00] & AE = AB [02] & AD = AB [01] ⇒  C,D,E,B are concyclic [11]
004. C,D,E,B are concyclic [11] ⇒  ∠CDE = ∠CBE [12]
005. ∠(DE-FH) = ∠(FH-BC) [09] & ∠(CD-GI) = ∠(GI-BE) [10] & ∠CDE = ∠CBE [12] (Angle chase)⇒  FH ⟂ GI
==========================

 

 

218. examples/complete2/unsolved1/complete_001_6_GDD_FULL_61-80_71.gex

a b c = triangle a b c; o = circle o a b c; e = on_pline e a b c, on_circle e o a; f = foot f e a b; g = foot g e a c ? para f g a o

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. O는 삼각형 ABC의 외심입니다. E는 A를 지나고 BC에 평행한 직선 위에 있고, O를 중심으로 하고 A를 지나는 원 위에 있습니다. F는 E에서 AB로 내린 수선의 발이고, G는 E에서 AC로 내린 수선의 발입니다. 선분 FG와 선분 AO가 서로 평행임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
DA = DB [00]
DB = DC [01]
DE = DA [02]
EA ∥ BC [03]
EF ⟂ AB [04]
A,F,B are collinear [05]
A,C,G are collinear [06]
EG ⟂ AC [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. DA = DB [00] & DE = DA [02] & DB = DC [01] ⇒  A,C,E,B are concyclic [08]
002. A,C,E,B are concyclic [08] ⇒  ∠AEC = ∠ABC [09]
003. A,C,E,B are concyclic [08] ⇒  ∠ACE = ∠ABE [10]
004. ∠AEC = ∠ABC [09] & AE ∥ BC [03] ⇒  ∠BCE = ∠ABC [11]
005. DA = DB [00] ⇒  ∠DAB = ∠ABD [12]
006. DE = DA [02] ⇒  ∠DAE = ∠AED [13]
007. ∠DAE = ∠AED [13] & AE ∥ BC [03] ⇒  ∠(AD-BC) = ∠(BC-DE) [14]
008. DE = DA [02] & DA = DB [00] ⇒  DB = DE [15]
009. DB = DE [15] ⇒  ∠DBE = ∠BED [16]
010. A,C,G are collinear [06] & A,F,B are collinear [05] & EF ⟂ AB [04] & EG ⟂ AC [07] ⇒  ∠AGE = ∠AFE [17]
011. ∠AGE = ∠AFE [17] ⇒  A,F,E,G are concyclic [18]
012. A,F,E,G are concyclic [18] ⇒  ∠AEF = ∠AGF [19]
013. ∠AEF = ∠AGF [19] & A,C,G are collinear [06] & AE ∥ BC [03] ⇒  ∠(BC-EF) = ∠(AC-FG) [20]
014. EF ⟂ AB [04] & ∠BCE = ∠ABC [11] & ∠ACE = ∠ABE [10] & ∠DAB = ∠ABD [12] & ∠(AD-BC) = ∠(BC-DE) [14] & ∠DBE = ∠BED [16] & ∠(BC-EF) = ∠(AC-FG) [20] (Angle chase)⇒  AD ∥ FG
==========================

 

 

219. examples/complete2/unsolved1/complete_007_7_Book_LLL_L043-5-1.gex

a b = segment a b; c = on_circle c a b; d = on_circle d a b; e = on_circle e a b; f = intersection_ll f b c d e; g = intersection_ll g c d b e; h = angle_bisector h d f b; i = angle_bisector i c g b; j = intersection_ll j f h g i; k = intersection_ll k d e g i; l = intersection_ll l g i b c ? perp g i f h

 

○ 번역 : 추후 업데이트

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
AC = AB [00]
AD = AB [01]
AE = AB [02]
C,B,F are collinear [03]
E,F,D are collinear [04]
E,G,B are collinear [05]
G,C,D are collinear [06]
∠DFH = ∠HFB [07]
∠CGI = ∠IGB [08]

 * Auxiliary Constructions:
J K L : Points
J,H,F are collinear [09]
I,G,J are collinear [10]
E,K,D are collinear [11]
I,G,K are collinear [12]
C,B,L are collinear [13]
I,G,L are collinear [14]

 * Proof steps:
001. C,B,L are collinear [13] & C,B,F are collinear [03] & H,J,F are collinear [09] & E,K,D are collinear [11] & E,F,D are collinear [04] & ∠DFH = ∠HFB [07] ⇒  ∠LFJ = ∠JFK [15]
002. I,G,L are collinear [14] & E,G,B are collinear [05] & G,C,D are collinear [06] & I,G,K are collinear [12] & ∠CGI = ∠IGB [08] ⇒  ∠LGB = ∠DGK [16]
003. AD = AB [01] & AE = AB [02] & AC = AB [00] ⇒  C,E,B,D are concyclic [17]
004. C,E,B,D are concyclic [17] ⇒  ∠CBE = ∠CDE [18]
005. C,B,L are collinear [13] & E,G,B are collinear [05] & G,C,D are collinear [06] & E,K,D are collinear [11] & ∠CBE = ∠CDE [18] ⇒  ∠LBG = ∠GDK [19]
006. ∠LGB = ∠DGK [16] & ∠LBG = ∠GDK [19] (Similar Triangles)⇒  ∠GLB = ∠DKG [20]
007. I,G,L are collinear [14] & I,G,J are collinear [10] & C,B,L are collinear [13] & C,B,F are collinear [03] & E,K,D are collinear [11] & E,F,D are collinear [04] & I,G,K are collinear [12] & ∠GLB = ∠DKG [20] ⇒  ∠JLF = ∠FKJ [21]
008. ∠LFJ = ∠JFK [15] & ∠JLF = ∠FKJ [21] (Similar Triangles)⇒  ∠FJL = ∠KJF [22]
009. ∠FJL = ∠KJF [22] & J,H,F are collinear [09] & I,G,L are collinear [14] & I,G,J are collinear [10] & I,G,K are collinear [12] ⇒  GI ⟂ FH
==========================

 

 

220. examples/complete2/unsolved1/complete_011_7_Book_00EE_04_E051-8.gex

a b c = triangle a b c; d = angle_bisector d a c b, on_line d a b; e = on_pline e d b c, on_line e a c; f = on_pline f e a b, on_line f b c ? cong c e f b

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 ∠ACB의 이등분선 위에 있으며, 직선 AB 위에 있습니다. E는 D를 지나고 BC에 평행한 직선 위에 있고, 직선 AC 위에 있습니다. F는 E를 지나고 AB에 평행한 직선 위에 있고, 직선 BC 위에 있습니다. 선분 CE와 선분 FB의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
A,D,B are collinear [00]
∠ACD = ∠DCB [01]
ED ∥ BC [02]
C,A,E are collinear [03]
C,B,F are collinear [04]
FE ∥ AB [05]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. C,B,F are collinear [04] & A,D,B are collinear [00] & EF ∥ AB [05] & BC ∥ DE [02] ⇒  ∠EFB = ∠BDE [06]
002. C,B,F are collinear [04] & BC ∥ DE [02] ⇒  ∠EBF = ∠BED [07]
003. ∠EFB = ∠BDE [06] & ∠EBF = ∠BED [07] (Similar Triangles)⇒  BF = ED [08]
004. C,A,E are collinear [03] & ∠ACD = ∠DCB [01] & BC ∥ DE [02] ⇒  ∠ECD = ∠CDE [09]
005. ∠ECD = ∠CDE [09] ⇒  EC = ED [10]
006. BF = ED [08] & EC = ED [10] ⇒  CE = FB
==========================

 

입력: 2024.08.07 13:24