【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [181-200]

jgex_ag_231 기하 문제 풀이 [181-200]

 

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

---

 

181. examples/complete2/unsolved2/complete_002_6_GDD_FULL_41-60_42.gex

a b c = triangle a b c; d = incenter d a b c; e = foot e a b c; f = foot f b a d; g = foot g c a d; h = midpoint h c b ? cyclic e f g h

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 삼각형 ABC의 내심입니다. E는 A에서 BC로 내린 수선의 발이고, F는 B에서 AD로 내린 수선의 발입니다. G는 C에서 AD로 내린 수선의 발이고, H는 선분 CB의 중점입니다. 점 E, F, G, H가 한 원 위에 있음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
∠BAD = ∠DAC [00]
E,C,B are collinear [01]
AE ⟂ BC [02]
D,F,A are collinear [03]
BF ⟂ AD [04]
D,G,A are collinear [05]
AD ⟂ GC [06]
B,H,C are collinear [07]
HC = HB [08]

 * Auxiliary Constructions:
I : Points
I,C,A are collinear [09]
IC = IA [10]

 * Proof steps:
001. F,A,D are collinear [03] & E,C,B are collinear [01] & AE ⟂ BC [02] & BF ⟂ AD [04] ⇒  ∠BFA = ∠BEA [11]
002. ∠BFA = ∠BEA [11] ⇒  E,B,F,A are concyclic [12]
003. E,B,F,A are concyclic [12] ⇒  ∠EBA = ∠EFA [13]
004. I,C,A are collinear [09] & IC = IA [10] ⇒  I is midpoint of CA [14]
005. H,C,B are collinear [07] & HC = HB [08] ⇒  H is midpoint of CB [15]
006. I is midpoint of CA [14] & H is midpoint of CB [15] ⇒  IH ∥ AB [16]
007. D,G,A are collinear [05] & CG ⟂ AD [06] ⇒  CG ⟂ GA [17]
008. CG ⟂ GA [17] & I is midpoint of CA [14] ⇒  AI = GI [18]
009. AI = GI [18] ⇒  ∠IAG = ∠AGI [19]
010. D,F,A are collinear [03] & ∠BAD = ∠DAC [00] & ∠IAG = ∠AGI [19] & I,C,A are collinear [09] & D,G,A are collinear [05] ⇒  ∠(IG-DF) = ∠(BA-DF) [20]
011. ∠(IG-DF) = ∠(BA-DF) [20] ⇒  IG ∥ BA [21]
012. HI ∥ AB [16] & GI ∥ AB [21] ⇒  IG ∥ IH [22]
013. IG ∥ IH [22] ⇒  H,I,G are collinear [23]
014. D,G,A are collinear [05] & D,F,A are collinear [03] & B,H,C are collinear [07] & E,C,B are collinear [01] & ∠EBA = ∠EFA [13] & HI ∥ AB [16] & H,I,G are collinear [23] ⇒  ∠EFG = ∠EHG [24]
015. ∠EFG = ∠EHG [24] ⇒  E,F,G,H are concyclic
==========================

 

 

182. examples/complete2/unsolved2/complete_014_7_Book_00EE_08_E061-63f.gex

a b = segment a b; c = midpoint c b a; d = s_angle b a d 30, on_circle d c a; e = lc_tangent e d c, on_line e a b ? cong d a d e

 

○ 번역 : 추후 업데이트 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E : Points
A,B,C are collinear [00]
∠DAB = 1_PI/6 [01]
CD = CA [02]
A,B,E are collinear [03]
DE ⟂ CD [04]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. CD = CA [02] ⇒  ∠CAD = ∠ADC [05]
002. ∠CAD = ∠ADC [05] & A,B,C are collinear [00] ⇒  ∠BAD = ∠ADC [06]
003. ∠DAB = 1_PI/6 [01] & DE ⟂ CD [04] & ∠BAD = ∠ADC [06] (Angle chase)⇒  ∠(AB-DE) = 1_PI/6 [07]
004. A,B,E are collinear [03] & ∠(AB-DE) = 1_PI/6 [07] & ∠DAB = 1_PI/6 [01] ⇒  ∠DAE = ∠AED [08]
005. ∠DAE = ∠AED [08] ⇒  DA = DE
==========================

 

 

183. examples/complete2/unsolved2/complete_007_7_Book_LLL_yL198-1.gex

c d = segment c d; e = midpoint e c d; b = free b; f = midpoint f b c; a = eqdistance a d c b, on_pline a b d c; g = midpoint g a b; h = midpoint h d a ? cong h e e f

 

○ 번역 

 

선분 CD가 주어져 있으며, E는 선분 CD의 중점입니다. B는 자유롭게 선택된 점입니다. F는 선분 BC의 중점입니다. DA = CB가 성립하며, A는 B를 지나고 DC에 평행한 직선 위에 있습니다. G는 선분 AB의 중점이고, H는 선분 DA의 중점입니다. 선분 HE와 선분 EF의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F H : Points
B,A,C are collinear [00]
CA = CB [01]
D,E,A are collinear [02]
ED = EA [03]
FB = AD [04]
FD ∥ BA [05]
B,H,F are collinear [06]
HB = HF [07]

 * Auxiliary Constructions:
G I J : Points
D,G,F are collinear [08]
GF = GD [09]
B,D,I are collinear [10]
ID = IB [11]
I,J,G are collinear [12]
IJ = IG [13]

 * Proof steps:
001. D,E,A are collinear [02] & ED = EA [03] ⇒  E is midpoint of AD [14]
002. B,D,I are collinear [10] & ID = IB [11] ⇒  I is midpoint of BD [15]
003. E is midpoint of AD [14] & I is midpoint of BD [15] ⇒  EI ∥ AB [16]
004. B,A,C are collinear [00] & CA = CB [01] ⇒  C is midpoint of BA [17]
005. C is midpoint of BA [17] & E is midpoint of AD [14] ⇒  CE ∥ BD [18]
006. B,A,C are collinear [00] & B,I,D are collinear [10] & AB ∥ EI [16] & BD ∥ CE [18] ⇒  ∠CBI = ∠IEC [19]
007. B,I,D are collinear [10] & BD ∥ CE [18] ⇒  ∠CIB = ∠ICE [20]
008. ∠CBI = ∠IEC [19] & ∠CIB = ∠ICE [20] (Similar Triangles)⇒  CB = IE [21]
009. B,H,F are collinear [06] & HB = HF [07] ⇒  H is midpoint of BF [22]
010. E is midpoint of AD [14] & H is midpoint of BF [22] ⇒  AD:BF = EA:HB [23]
011. B,A,C are collinear [00] & B,I,D are collinear [10] & BD ∥ CE [18] ⇒  ∠CBI = ∠ACE [24]
012. C is midpoint of BA [17] & I is midpoint of BD [15] ⇒  CI ∥ AD [25]
013. B,I,D are collinear [10] & D,E,A are collinear [02] & CI ∥ AD [25] & BD ∥ CE [18] ⇒  ∠CIB = ∠AEC [26]
014. ∠CBI = ∠ACE [24] & ∠CIB = ∠AEC [26] (Similar Triangles)⇒  CB:AC = CI:AE [27]
015. AD:BF = EA:HB [23] & FB = AD [04] & CB:AC = CI:AE [27] & CA = CB [01] ⇒  IC = BH [28]
016. EA = ED [03] & HB = HF [07] ⇒  EA:ED = HB:HF [29]
017. DF ∥ AB [05] & D,E,A are collinear [02] & B,H,F are collinear [06] & EA:ED = HB:HF [29] ⇒  EH ∥ AB [30]
018. EH ∥ AB [30] & EI ∥ AB [16] ⇒  EI ∥ EH [31]
019. EI ∥ EH [31] ⇒  H,I,E are collinear [32]
020. H is midpoint of BF [22] & I is midpoint of BD [15] ⇒  HI ∥ FD [33]
021. I,J,G are collinear [12] & IJ = IG [13] ⇒  I is midpoint of JG [34]
022. I is midpoint of BD [15] & I is midpoint of JG [34] ⇒  BJ ∥ DG [35]
023. B,I,D are collinear [10] & HI ∥ DF [33] & BJ ∥ DG [35] & D,G,F are collinear [08] ⇒  ∠JBI = ∠HIB [36]
024. D,G,F are collinear [08] & GF = GD [09] ⇒  G is midpoint of DF [37]
025. G is midpoint of DF [37] & I is midpoint of BD [15] ⇒  GI ∥ FB [38]
026. I,G,J are collinear [12] & B,I,D are collinear [10] & B,F,H are collinear [06] & GI ∥ BF [38] ⇒  ∠JIB = ∠HBI [39]
027. ∠JBI = ∠HIB [36] & ∠JIB = ∠HBI [39] (Similar Triangles)⇒  IJ = BH [40]
028. IJ = BH [40] & AD:BF = EA:HB [23] & FB = AD [04] & CB:AC = CI:AE [27] & CA = CB [01] ⇒  IC = IJ [41]
029. IC = IJ [41] ⇒  ∠ICJ = ∠CJI [42]
030. DF ∥ AB [05] & BJ ∥ DG [35] & D,G,F are collinear [08] ⇒  BJ ∥ BA [43]
031. BJ ∥ BA [43] ⇒  B,A,J are collinear [44]
032. B,A,C are collinear [00] & B,F,H are collinear [06] & H,I,E are collinear [32] & ∠ICJ = ∠CJI [42] & B,A,J are collinear [44] & I,J,G are collinear [12] & CI ∥ AD [25] & GI ∥ BF [38] & BJ ∥ AB [43] & BJ ∥ DG [35] & D,G,F are collinear [08] & DF ∥ AB [05] & EH ∥ AB [30] ⇒  ∠CBH = ∠CIE [45]
033. CB = IE [21] & IC = BH [28] & ∠CBH = ∠CIE [45] (SAS)⇒  HC = CE
==========================

 

 

184. examples/complete2/unsolved/complete_015_7_Book_00EE_08_E061-61.gex

a b = segment a b; c = on_circle c a b; d = on_circle d a b; e = lc_tangent e c a, lc_tangent e d a; f = lc_tangent f b a, on_line f c e; h = on_pline h c b f, on_line h b d; g = on_line g d e, on_line g b f; i = on_line i b e, on_line i c h ? cong c i i h

 

○ 번역 : 추후 업데이트 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G I : Points
AC = AB [00]
AD = AB [01]
∠DBC = ∠DBC [02]
CE ⟂ AC [03]
DE ⟂ AD [04]
E,C,F are collinear [05]
BF ⟂ AB [06]
GC ∥ BF [07]
D,B,G are collinear [08]
I,C,G are collinear [09]
E,I,B are collinear [10]

 * Auxiliary Constructions:
J : Points
AJ = AC [11]
A,C,J are collinear [12]

 * Proof steps:
001. G,I,C are collinear [09] & CG ∥ BF [07] ⇒  IC ∥ BF [13]
002. IC ∥ BF [13] & E,I,B are collinear [10] & E,C,F are collinear [05] ⇒  EI:EB = EC:EF [14]
003. IC ∥ BF [13] & E,I,B are collinear [10] & E,C,F are collinear [05] ⇒  EI:EB = IC:FB [15]
004. AJ = AC [11] & AC = AB [00] & AD = AB [01] ⇒  A is the circumcenter of \Delta DJC [16]
005. AJ = AC [11] & AC = AB [00] & AD = AB [01] ⇒  A is the circumcenter of \Delta DJB [17]
006. A is the circumcenter of \Delta DJC [16] & CE ⟂ AC [03] ⇒  ∠ECJ = ∠CDJ [18]
007. A is the circumcenter of \Delta DJC [16] & DE ⟂ AD [04] ⇒  ∠EDJ = ∠DCJ [19]
008. ∠ECJ = ∠CDJ [18] & A,C,J are collinear [12] & ∠EDJ = ∠DCJ [19] ⇒  ∠EDC = ∠DCE [20]
009. ∠EDC = ∠DCE [20] ⇒  EC = ED [21]
010. A,C,J are collinear [12] & ∠ECJ = ∠CDJ [18] ⇒  ∠DJA = ∠DCE [22]
011. DE ⟂ AD [04] & CE ⟂ AC [03] ⇒  ∠DAC = ∠DEC [23]
012. DE ⟂ AD [04] & CE ⟂ AC [03] ⇒  ∠ECA = ∠EDA [24]
013. A,C,J are collinear [12] & ∠DAC = ∠DEC [23] ⇒  ∠DAJ = ∠DEC [25]
014. ∠DJA = ∠DCE [22] & ∠DAJ = ∠DEC [25] (Similar Triangles)⇒  DJ:DA = DC:DE [26]
015. DJ:DA = DC:DE [26] & AJ = AC [11] & AC = AB [00] & AD = AB [01] & EC = ED [21] ⇒  DJ:AJ = DC:EC [27]
016. AD = AB [01] & AC = AB [00] ⇒  A is the circumcenter of \Delta DBC [28]
017. A is the circumcenter of \Delta DBC [28] & BF ⟂ AB [06] ⇒  ∠DBF = ∠DCB [29]
018. D,B,G are collinear [08] & ∠DCB = ∠DBF [29] & BF ∥ CG [07] ⇒  ∠DCB = ∠BGC [30]
019. D,B,G are collinear [08] & ∠DBC = ∠DBC [02] ⇒  ∠DBC = ∠GBC [31]
020. ∠DCB = ∠BGC [30] & ∠DBC = ∠GBC [31] (Similar Triangles)⇒  DC:DB = CG:CB [32]
021. AJ = AC [11] & AC = AB [00] ⇒  A is the circumcenter of \Delta BJC [33]
022. A is the circumcenter of \Delta BJC [33] & A,C,J are collinear [12] ⇒  BJ ⟂ BC [34]
023. BJ ⟂ BC [34] & BF ⟂ AB [06] ⇒  ∠FBA = ∠CBJ [35]
024. A is the circumcenter of \Delta BJC [33] & CE ⟂ AC [03] ⇒  ∠ECJ = ∠CBJ [36]
025. F,C,E are collinear [05] & BF ⟂ AB [06] & CE ⟂ AC [03] ⇒  ∠FCA = ∠FBA [37]
026. ∠FCA = ∠FBA [37] ⇒  A,F,C,B are concyclic [38]
027. A,F,C,B are concyclic [38] ⇒  ∠AFC = ∠ABC [39]
028. A,C,J are collinear [12] & ∠ECJ = ∠CBJ [36] & ∠AFC = ∠ABC [39] & E,C,F are collinear [05] ⇒  ∠FAB = ∠CJB [40]
029. ∠FBA = ∠CBJ [35] & ∠FAB = ∠CJB [40] (Similar Triangles)⇒  FB:AF = CB:CJ [41]
030. G,I,C are collinear [09] & BJ ⟂ BC [34] & BF ⟂ AB [06] & BF ∥ CG [07] ⇒  ∠(AB-IC) = ∠CBJ [42]
031. A is the circumcenter of \Delta DJB [17] & BF ⟂ AB [06] ⇒  ∠FBD = ∠BJD [43]
032. G,I,C are collinear [09] & ∠FBD = ∠BJD [43] & BF ∥ CG [07] ⇒  ∠(IC-DB) = ∠BJD [44]
033. ∠(AB-IC) = ∠CBJ [42] & ∠(IC-DB) = ∠BJD [44] ⇒  ∠ABC = ∠BDJ [45]
034. F,C,E are collinear [05] & ∠ABC = ∠BDJ [45] & ∠AFC = ∠ABC [39] ⇒  ∠AFE = ∠BDJ [46]
035. A is the circumcenter of \Delta DJC [16] & A,C,J are collinear [12] ⇒  DJ ⟂ CD [47]
036. DJ ⟂ CD [47] & DE ⟂ AD [04] ⇒  ∠ADE = ∠CDJ [48]
037. A is the circumcenter of \Delta DJB [17] & DE ⟂ AD [04] ⇒  ∠EDB = ∠DJB [49]
038. ∠ADE = ∠CDJ [48] & ∠EDB = ∠DJB [49] ⇒  ∠ADC = ∠DBJ [50]
039. ∠ECA = ∠EDA [24] ⇒  D,A,E,C are concyclic [51]
040. D,A,E,C are concyclic [51] ⇒  ∠ADC = ∠AEC [52]
041. E,C,F are collinear [05] & ∠ADC = ∠DBJ [50] & ∠ADC = ∠AEC [52] ⇒  ∠AEF = ∠DBJ [53]
042. ∠AFE = ∠BDJ [46] & ∠AEF = ∠DBJ [53] (Similar Triangles)⇒  AF:EF = DJ:DB [54]
043. AD = AB [01] & EI:EB = EC:EF [14] & EI:EB = IC:FB [15] & EC = ED [21] & DJ:AJ = DC:EC [27] & DC:DB = CG:CB [32] & FB:AF = CB:CJ [41] & AF:EF = DJ:DB [54] (Ratio chase)⇒  AB:IC = CJ:CG [55]
044. AB:IC = CJ:CG [55] & AJ = AC [11] & AC = AB [00] ⇒  CJ:CG = CA:CI [56]
045. A,C,J are collinear [12] & I,C,G are collinear [09] & BF ∥ CG [07] ⇒  ∠JCG = ∠ACI [57]
046. CJ:CG = CA:CI [56] & ∠JCG = ∠ACI [57] (Similar Triangles)⇒  ∠CJG = ∠CAI [58]
047. ∠CJG = ∠CAI [58] & A,C,J are collinear [12] ⇒  GJ ∥ AI [59]
048. GJ ∥ AI [59] & A,C,J are collinear [12] & I,C,G are collinear [09] ⇒  AC:AJ = IC:IG [60]
049. AC:AJ = IC:IG [60] & AJ = AC [11] ⇒  IC = IG
==========================

 

 

185. examples/complete2/unsolved/complete_008_ex-gao_ex160_204.gex

a b c = triangle a b c; d = circumcenter d a b c; e = on_circle e d a; f = on_line f a b, on_line f c e; h = on_line h b c, angle_bisector h a f c; g = on_line g a e, on_line g b c; i = on_line i a b, angle_bisector i a g b; j = on_line j f h, on_line j g i; k = on_line k a e, on_line k f h ? perp g i f h

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 삼각형 ABC의 외심입니다. E는 D를 중심으로 하고 A를 지나는 원 위에 있습니다. F는 직선 AB와 CE의 교점입니다. H는 직선 BC 위에 있으며, ∠AFC의 이등분선 위에 있습니다. G는 직선 AE와 BC의 교점에 있습니다. I는 직선 AB 위에 있고, ∠AGB의 이등분선 위에 있습니다. J는 직선 FH와 GI의 교점입니다. K는 직선 AE와 FH의 교점입니다. 선분 GI와 선분 FH가 서로 수직임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
DA = DB [00]
DB = DC [01]
DE = DA [02]
C,E,F are collinear [03]
F,B,A are collinear [04]
C,G,B are collinear [05]
∠AFG = ∠GFC [06]
H,E,A are collinear [07]
C,H,B are collinear [08]
∠AHI = ∠IHB [09]

 * Auxiliary Constructions:
J K : Points
H,I,J are collinear [10]
J,G,F are collinear [11]
K,E,A are collinear [12]
K,G,F are collinear [13]

 * Proof steps:
001. K,E,A are collinear [12] & H,E,A are collinear [07] & H,I,J are collinear [10] & C,H,B are collinear [08] & C,G,B are collinear [05] & ∠AHI = ∠IHB [09] ⇒  ∠KHJ = ∠JHG [14]
002. K,G,F are collinear [13] & C,E,F are collinear [03] & A,B,F are collinear [04] & ∠AFG = ∠GFC [06] ⇒  ∠KFE = ∠BFG [15]
003. DA = DB [00] & DE = DA [02] & DB = DC [01] ⇒  C,E,B,A are concyclic [16]
004. C,E,B,A are concyclic [16] ⇒  ∠AEC = ∠ABC [17]
005. K,E,A are collinear [12] & C,E,F are collinear [03] & A,B,F are collinear [04] & C,G,B are collinear [05] & ∠AEC = ∠ABC [17] ⇒  ∠KEF = ∠FBG [18]
006. ∠KFE = ∠BFG [15] & ∠KEF = ∠FBG [18] (Similar Triangles)⇒  ∠FKE = ∠BGF [19]
007. J,G,F are collinear [11] & C,H,B are collinear [08] & C,G,B are collinear [05] & K,E,A are collinear [12] & H,E,A are collinear [07] & K,G,F are collinear [13] & ∠FKE = ∠BGF [19] ⇒  ∠JGH = ∠HKJ [20]
008. ∠KHJ = ∠JHG [14] & ∠JGH = ∠HKJ [20] (Similar Triangles)⇒  ∠HJG = ∠KJH [21]
009. ∠HJG = ∠KJH [21] & H,I,J are collinear [10] & J,G,F are collinear [11] & K,G,F are collinear [13] ⇒  HI ⟂ FG
==========================

 

 

186. examples/complete2/unsolved/complete_005_Other_unsolved_65.gex

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

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. E는 직선 AB 위에 있습니다. F는 E를 지나고 BC에 평행한 직선 위에 있고, 직선 AC 위에 있습니다. D는 삼각형 ABC의 외심이고, G는 삼각형 AEF의 외심입니다. 점 A, 원 G, 원 D가 한 선 위에 존재함을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

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

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. FA = FB [03] ⇒  ∠FBA = ∠BAF [07]
002. FB = FC [04] ⇒  ∠FBC = ∠BCF [08]
003. FB = FC [04] & FA = FB [03] ⇒  FA = FC [09]
004. FA = FC [09] ⇒  ∠FAC = ∠ACF [10]
005. GA = GD [05] & GD = GE [06] ⇒  GE = GA [11]
006. GE = GA [11] ⇒  ∠GEA = ∠EAG [12]
007. ∠GEA = ∠EAG [12] & E,C,A are collinear [01] ⇒  ∠(EG-AC) = ∠CAG [13]
008. GD = GE [06] ⇒  ∠GED = ∠EDG [14]
009. ∠GED = ∠EDG [14] & DE ∥ BC [02] ⇒  ∠(EG-BC) = ∠(BC-DG) [15]
010. GA = GD [05] ⇒  ∠GAD = ∠ADG [16]
011. ∠GAD = ∠ADG [16] & B,A,D are collinear [00] ⇒  ∠GAB = ∠(AB-DG) [17]
012. ∠FBA = ∠BAF [07] & ∠FBC = ∠BCF [08] & ∠FAC = ∠ACF [10] & ∠(EG-AC) = ∠CAG [13] & ∠(EG-BC) = ∠(BC-DG) [15] & ∠GAB = ∠(AB-DG) [17] (Angle chase)⇒  AF ∥ AG [18]
013. AF ∥ AG [18] ⇒  F,A,G are collinear
==========================

 

 

187. examples/complete2/unsolved/complete_008_ex-gao_ex160_005.gex

a b c = triangle a b c; d = on_line d b c, angle_bisector d b a c; e = on_line e a b; f = on_line f a c, eqdistance f c b e; g = midpoint g f e; h = midpoint h c b ? para g h a d

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 직선 BC 위에 있고, ∠BAC의 이등분선 위에 있습니다. E는 직선 AB 위에 있습니다. F는 직선 AC 위에 있고, FC = BE입니다. G는 선분 FE의 중점이고, H는 선분 CB의 중점입니다. 선분 GH와 선분 AD가 서로 평행임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
∠BAD = ∠DAC [00]
B,A,E are collinear [01]
FC = BE [02]
BE:EF = BE:EF [03]
A,C,F are collinear [04]
G,E,F are collinear [05]
GF = GE [06]
B,H,C are collinear [07]
HC = HB [08]

 * Auxiliary Constructions:
I : Points
B,F,I are collinear [09]
IF = IB [10]

 * Proof steps:
001. B,H,C are collinear [07] & HC = HB [08] ⇒  H is midpoint of BC [11]
002. B,F,I are collinear [09] & IF = IB [10] ⇒  I is midpoint of BF [12]
003. H is midpoint of BC [11] & I is midpoint of BF [12] ⇒  HI ∥ CF [13]
004. CF ∥ HI [13] & B,F,I are collinear [09] & B,H,C are collinear [07] ⇒  BF:BI = FC:IH [14]
005. G,E,F are collinear [05] & GF = GE [06] ⇒  G is midpoint of FE [15]
006. G is midpoint of FE [15] & I is midpoint of BF [12] ⇒  GI ∥ EB [16]
007. GI ∥ EB [16] & B,F,I are collinear [09] & G,E,F are collinear [05] ⇒  FI:FB = IG:BE [17]
008. BF:BI = FC:IH [14] & FC = BE [02] & FI:FB = IG:BE [17] & IF = IB [10] ⇒  GI:BE = HI:BE [18]
009. GI:BE = HI:BE [18] & BE:EF = BE:EF [03] ⇒  GI = HI [19]
010. GI = HI [19] ⇒  ∠IGH = ∠GHI [20]
011. ∠IGH = ∠GHI [20] & GI ∥ EB [16] & B,A,E are collinear [01] & HI ∥ CF [13] & A,C,F are collinear [04] ⇒  ∠(AB-GH) = ∠(GH-AC) [21]
012. ∠BAD = ∠DAC [00] & ∠(AB-GH) = ∠(GH-AC) [21] (Angle chase)⇒  AD ∥ GH
==========================

 

 

188. examples/complete2/unsolved/complete_006_Other_ndgTest_65.gex

a b c = triangle a b c; e = on_line e a b; f = intersection_lp f a c e c b; d = circle d a b c; g = circle g a e f ? coll a g d

 

○ 번역 : 추후 업데이트

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
A,B,D are collinear [00]
A,E,C are collinear [01]
DE ∥ CB [02]
FB = FC [03]
FA = FB [04]
GA = GD [05]
GD = GE [06]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. FB = FC [03] ⇒  ∠FBC = ∠BCF [07]
002. FA = FB [04] ⇒  ∠FBA = ∠BAF [08]
003. FA = FB [04] & FB = FC [03] ⇒  FC = FA [09]
004. FC = FA [09] ⇒  ∠FCA = ∠CAF [10]
005. GA = GD [05] ⇒  ∠GAD = ∠ADG [11]
006. ∠GAD = ∠ADG [11] & A,B,D are collinear [00] ⇒  ∠GAB = ∠(AB-DG) [12]
007. GD = GE [06] & GA = GD [05] ⇒  GA = GE [13]
008. GA = GE [13] ⇒  ∠GAE = ∠AEG [14]
009. ∠GAE = ∠AEG [14] & A,E,C are collinear [01] ⇒  ∠GAC = ∠(AC-EG) [15]
010. GD = GE [06] ⇒  ∠GDE = ∠DEG [16]
011. ∠GDE = ∠DEG [16] & DE ∥ BC [02] ⇒  ∠(DG-BC) = ∠(BC-EG) [17]
012. ∠FBC = ∠BCF [07] & ∠FBA = ∠BAF [08] & ∠FCA = ∠CAF [10] & ∠GAB = ∠(AB-DG) [12] & ∠GAC = ∠(AC-EG) [15] & ∠(DG-BC) = ∠(BC-EG) [17] (Angle chase)⇒  AF ∥ AG [18]
013. AF ∥ AG [18] ⇒  A,G,F are collinear
==========================

 

 

189. examples/complete2/unsolved/complete_005_Other_unsolved_E051-7.gex

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

 

○ 번역 

 

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

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
A,B,D are collinear [00]
∠CBE = ∠EBA [01]
C,B,F are collinear [02]
FE ∥ AB [03]
E,G,F are collinear [04]
∠CBG = ∠GBD [05]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. C,B,F are collinear [02] & E,G,F are collinear [04] & ∠CBG = ∠GBD [05] & A,B,D are collinear [00] & AB ∥ EF [03] ⇒  ∠FBG = ∠BGF [06]
002. ∠FBG = ∠BGF [06] ⇒  FB = FG [07]
003. C,B,F are collinear [02] & ∠CBE = ∠EBA [01] & AB ∥ EF [03] ⇒  ∠FBE = ∠BEF [08]
004. ∠FBE = ∠BEF [08] ⇒  FB = FE [09]
005. FB = FG [07] & FB = FE [09] ⇒  EF = FG
==========================

 

 

190. examples/complete2/unsolved/complete_005_Other_unsolved_E046-10.gex

a b c d = isquare a b c d; e = midpoint e b a; f = on_line f a b; g = on_tline g e d e, angle_bisector g c b f ? cong d e e g

 

○ 번역 

 

정사각형 ABCD가 주어져 있습니다. E는 선분 BA의 중점이고, F는 직선 AB 위에 있습니다. G는 E를 지나고 DE에 수직인 직선 위에 있으며, ∠CBF의 이등분선 위에 있습니다. 선분 DE와 선분 EG의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
AB = BC [00]
AB ⟂ BC [01]
AD ∥ BC [02]
AB ∥ CD [03]
A,E,B are collinear [04]
F,A,B are collinear [05]
EG ⟂ DE [06]
∠CBG = ∠GBF [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. BC ∥ AD [02] & AB ∥ CD [03] ⇒  ∠DAB = ∠BCD [08]
002. AB ∥ CD [03] ⇒  ∠DBA = ∠BDC [09]
003. ∠DAB = ∠BCD [08] & ∠DBA = ∠BDC [09] (Similar Triangles)⇒  BA = DC [10]
004. ∠DAB = ∠BCD [08] & ∠DBA = ∠BDC [09] (Similar Triangles)⇒  DA = BC [11]
005. AB = BC [00] & BA = DC [10] ⇒  CD = CB [12]
006. DA = BC [11] & AB = BC [00] ⇒  AB = AD [13]
007. CD = CB [12] & AB = AD [13] ⇒  BD ⟂ AC [14]
008. BD ⟂ AC [14] & EG ⟂ DE [06] ⇒  ∠(AC-BD) = ∠GED [15]
009. ∠CBG = ∠GBF [07] & F,A,B are collinear [05] ⇒  ∠CBG = ∠GBA [16]
010. AB = BC [00] ⇒  ∠BAC = ∠ACB [17]
011. ∠CBG = ∠GBA [16] & ∠BAC = ∠ACB [17] (Angle chase)⇒  BG ∥ AC [18]
012. ∠(AC-BD) = ∠GED [15] & AC ∥ BG [18] ⇒  ∠GBD = ∠GED [19]
013. ∠GBD = ∠GED [19] ⇒  D,E,G,B are concyclic [20]
014. AB ⟂ BC [01] & BC ∥ AD [02] & AB ∥ CD [03] ⇒  ∠DAB = ∠DCB [21]
015. ∠DAB = ∠DCB [21] ⇒  A,D,C,B are concyclic [22]
016. A,D,C,B are concyclic [22] ⇒  ∠ACD = ∠ABD [23]
017. A,E,B are collinear [04] & ∠ACD = ∠ABD [23] & AB ∥ CD [03] & AC ∥ BG [18] ⇒  ∠EBD = ∠GBE [24]
018. D,E,G,B are concyclic [20] & ∠EBD = ∠GBE [24] ⇒  DE = EG
==========================

 

 

191. examples/complete2/unsolved/ex-gao_ex160_103.gex

c b y = triangle c b y; a = foot a c b y; x = angle_bisector x c b y; d = foot d a b c; e = on_line e b x, on_line e c a; f = foot f e b c; g = on_line g b x, on_line g a d ? cong f g f e

 

○ 번역 

 

삼각형 CBY가 주어져 있습니다. A는 C에서 BY로 내린 수선의 발입니다. X는 ∠CBY의 이등분선 위에 있습니다. D는 A에서 BC로 내린 수선의 발입니다. E는 직선 BX와 CA의 교점입니다. F는 E에서 BC로 내린 수선의 발입니다. G는 직선 BX와 AD의 교점입니다. 선분 FG와 선분 FE의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
C,B,D are collinear [00]
AD ⟂ BC [01]
AB:BD = AB:BD [02]
∠EBA = ∠CBE [03]
DF ⟂ AB [04]
F,A,B are collinear [05]
A,D,G are collinear [06]
E,B,G are collinear [07]
H,A,B are collinear [08]
BA ⟂ HG [09]
E,B,I are collinear [10]
F,D,I are collinear [11]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. H,A,B are collinear [08] & C,B,D are collinear [00] & A,D,G are collinear [06] & AD ⟂ BC [01] & DF ⟂ AB [04] & BA ⟂ HG [09] ⇒  ∠GHB = ∠BDG [12]
002. E,B,G are collinear [07] & H,A,B are collinear [08] & C,B,D are collinear [00] & ∠EBA = ∠CBE [03] ⇒  ∠GBH = ∠DBG [13]
003. ∠GHB = ∠BDG [12] & ∠GBH = ∠DBG [13] (Similar Triangles)⇒  GH = GD [14]
004. ∠GHB = ∠BDG [12] & ∠GBH = ∠DBG [13] (Similar Triangles)⇒  HG:HB = DG:DB [15]
005. ∠GHB = ∠BDG [12] & ∠GBH = ∠DBG [13] (Similar Triangles)⇒  ∠HGB = ∠BGD [16]
006. F,A,B are collinear [05] & E,B,I are collinear [10] & C,B,D are collinear [00] & ∠ABE = ∠EBC [03] ⇒  ∠FBI = ∠IBD [17]
007. ∠FBI = ∠IBD [17] & F,D,I are collinear [11] ⇒  FB:FI = BD:DI [18]
008. F,D,I are collinear [11] & BA ⟂ HG [09] & DF ⟂ AB [04] ⇒  HG ∥ FI [19]
009. H,A,B are collinear [08] & F,A,B are collinear [05] ⇒  B,H,F are collinear [20]
010. E,B,G are collinear [07] & E,B,I are collinear [10] ⇒  B,G,I are collinear [21]
011. HG ∥ FI [19] & B,H,F are collinear [20] & B,G,I are collinear [21] ⇒  HB:HG = FB:FI [22]
012. FB:FI = BD:DI [18] & HB:HG = FB:FI [22] & HB:HG = BD:DG [15] ⇒  BD:DG = BD:DI [23]
013. AB:BD = AB:BD [02] & BD:DG = BD:DI [23] ⇒  DG = DI [24]
014. A,D,G are collinear [06] & E,B,G are collinear [07] & E,B,I are collinear [10] & ∠HGB = ∠BGD [16] ⇒  ∠DGI = ∠IGH [25]
015. GH = GD [14] & ∠DGI = ∠IGH [25] (SAS)⇒  ID = IH [26]
016. GH = GD [14] & DG = DI [24] & ID = IH [26] ⇒  HI = HG
==========================

 

 

192. examples/complete2/unsolved/ex-gao_ex160_104.gex

c a y = triangle c a y; b = foot b c a y; x = angle_bisector x c a y; e = foot e b a c; d = on_line d a x, on_line d c b; f = on_line f a x, on_line f b e; g = on_line g c b, on_pline g f a c ? cong b d c g

 

○ 번역 

 

삼각형 CAY가 주어져 있습니다. B는 C에서 AY로 내린 수선의 발입니다. X는 ∠CAY의 이등분선 위에 있습니다. E는 B에서 AC로 내린 수선의 발입니다. D는 직선 AX와 CB의 교점입니다. F는 직선 AX와 BE의 교점입니다. G는 직선 CB 위에 있으며, F를 지나고 AC와 평행한 직선 위에 있습니다. 선분 BD와 선분 CG의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
D,C,B are collinear [00]
AD ⟂ BC [01]
∠ABE = ∠EBC [02]
A,B,F are collinear [03]
DF ⟂ AB [04]
A,G,D are collinear [05]
G,E,B are collinear [06]
H,E,B are collinear [07]
H,D,F are collinear [08]
HF:BF = HF:BF [09]
HB:GB = HB:GB [10]
IH ∥ BA [11]
I,A,D are collinear [12]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. I,A,D are collinear [12] & A,G,D are collinear [05] ⇒  I,A,G are collinear [13]
002. H,E,B are collinear [07] & G,E,B are collinear [06] ⇒  G,H,B are collinear [14]
003. HI ∥ AB [11] & G,I,A are collinear [13] & G,H,B are collinear [14] ⇒  IG:HG = IA:HB [15]
004. H,E,B are collinear [07] & D,C,B are collinear [00] & G,E,B are collinear [06] & ∠EBC = ∠ABE [02] & AB ∥ HI [11] ⇒  ∠HBD = ∠IHG [16]
005. H,D,F are collinear [08] & A,B,F are collinear [03] & C,B,D are collinear [00] & A,G,D are collinear [05] & AD ⟂ BC [01] & DF ⟂ AB [04] ⇒  ∠HFB = ∠BDG [17]
006. H,E,B are collinear [07] & A,B,F are collinear [03] & D,C,B are collinear [00] & E,G,B are collinear [06] & ∠EBA = ∠CBE [02] ⇒  ∠HBF = ∠DBG [18]
007. ∠HFB = ∠BDG [17] & ∠HBF = ∠DBG [18] (Similar Triangles)⇒  ∠FHB = ∠BGD [19]
008. ∠HFB = ∠BDG [17] & ∠HBF = ∠DBG [18] (Similar Triangles)⇒  GD:HF = DB:BF [20]
009. I,A,D are collinear [12] & I,A,G are collinear [13] & H,E,B are collinear [07] & G,E,B are collinear [06] & H,D,F are collinear [08] & ∠FHB = ∠BGD [19] & A,G,D are collinear [05] ⇒  ∠IGH = ∠BHD [21]
010. ∠HBD = ∠IHG [16] & ∠IGH = ∠BHD [21] (Similar Triangles)⇒  GI:GH = HD:HB [22]
011. D,C,B are collinear [00] & H,E,B are collinear [07] & A,B,F are collinear [03] & ∠CBE = ∠EBA [02] ⇒  ∠DBH = ∠HBF [23]
012. ∠DBH = ∠HBF [23] & H,D,F are collinear [08] ⇒  HD:HF = DB:BF [24]
013. HD:HF = DB:BF [24] & GD:HF = DB:BF [20] ⇒  GD:HF = HD:HF [25]
014. GD:HF = HD:HF [25] & HF:BF = HF:BF [09] ⇒  GD = HD [26]
015. IG:HG = IA:HB [15] & GI:GH = HD:HB [22] & GD = HD [26] ⇒  GD:HB = IA:HB [27]
016. GD:HB = IA:HB [27] & HB:GB = HB:GB [10] ⇒  GD = IA
==========================

 

 

193. examples/complete2/unsolved/complete_005_Other_unsolved_109f.gex

a b d = triangle a b d; e = on_line e a d; c = on_line c a b; f = on_line f b e, on_line f c d; g = circle g d e f; h = circle h a c d; i = circle i b c f; j = circle j b a e ? cyclic i j h g

 

○ 번역 

 

삼각형 ABD가 주어져 있습니다. E는 직선 AD 위에 있고, C는 직선 AB 위에 있습니다. F는 직선 BE와 CD의 교점입니다. G는 삼각형 DEF의 외심이고, H는 삼각형 ACD의 외심이며, I는 삼각형 BCF의 외심이고, J는 삼각형 BAE의 외심입니다. 점 I, J, H, G가 한 원 위에 있음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용했을 때 풀리지 않았음 

 

ValueError: too many values to unpack (expected 2)

 

 

194. examples/complete2/unsolved/complete_005_Other_unsolved_E046-7.gex

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

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 선분 CA의 중점입니다. E는 ∠BAD의 이등분선 위에 있고, 직선 BD 위에 있습니다. F는 B를 지나고 CE와 평행한 직선 위에 있으며, 직선 AC 위에 있습니다. 선분 BA와 선분 CF의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
A,C,D are collinear [00]
DC = DA [01]
ED:AD = ED:AD [02]
E,D,B are collinear [03]
∠BAE = ∠EAD [04]
FB ∥ CE [05]
F,A,C are collinear [06]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. F,A,C are collinear [06] & A,C,D are collinear [00] ⇒  D,C,F are collinear [07]
002. BF ∥ CE [05] & E,D,B are collinear [03] & D,C,F are collinear [07] ⇒  ED:EB = CD:CF [08]
003. ∠DAE = ∠EAB [04] & E,D,B are collinear [03] ⇒  ED:EB = AD:AB [09]
004. ED:EB = CD:CF [08] & DC = DA [01] & ED:EB = AD:AB [09] ⇒  AD:AB = AD:FC [10]
005. ED:AD = ED:AD [02] & AD:AB = AD:FC [10] ⇒  AB = FC
==========================

 

 

195. examples/complete2/unsolved/complete_008_ex-gao_ex160_e121.gex

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

 

○ 번역 

 

선분 AB가 주어져 있습니다. D는 선분 BA의 중점입니다. C는 A를 지나고 AB에 수직한 직선 위에 있습니다. E는 C를 중심으로 하고 A를 지나는 원 위에 있습니다. F는 직선 DE 위에 있고, C를 중심으로 하고 A를 지나는 원 위에 있습니다. G는 C를 중심으로 하고 F를 지나는 원 위에 있고, 직선 FB 위에 있습니다. H는 직선 BE 위에 있고, C를 중심으로 하고 A를 지나는 원 위에 있습니다. 선분 AB와 선분 GH가 서로 평행임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
B,A,C are collinear [00]
CB = CA [01]
AD ⟂ AB [02]
DE = DA [03]
F,C,E are collinear [04]
DF = DA [05]
G,B,F are collinear [06]
DG = DF [07]
DH = DA [08]
H,B,E are collinear [09]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. DF = DA [05] & DE = DA [03] ⇒  D is the circumcenter of \Delta AFE [10]
002. D is the circumcenter of \Delta AFE [10] & AD ⟂ AB [02] ⇒  ∠BAF = ∠AEF [11]
003. B,A,C are collinear [00] & E,C,F are collinear [04] & ∠BAF = ∠AEF [11] ⇒  ∠EAC = ∠CFA [12]
004. B,A,C are collinear [00] & E,C,F are collinear [04] ⇒  ∠ECA = ∠FCA [13]
005. ∠EAC = ∠CFA [12] & ∠ECA = ∠FCA [13] (Similar Triangles)⇒  CE:AC = AC:CF [14]
006. CE:AC = AC:CF [14] & BC = AC [01] ⇒  CE:BC = BC:CF [15]
007. B,A,C are collinear [00] & E,C,F are collinear [04] ⇒  ∠ECB = ∠FCB [16]
008. CE:BC = BC:CF [15] & ∠ECB = ∠FCB [16] (Similar Triangles)⇒  ∠CEB = ∠FBC [17]
009. DF = DA [05] & DH = DA [08] & DE = DA [03] & DG = DF [07] ⇒  F,E,H,G are concyclic [18]
010. F,E,H,G are concyclic [18] ⇒  ∠FEH = ∠FGH [19]
011. F,B,G are collinear [06] & ∠CEB = ∠FBC [17] & B,A,C are collinear [00] & ∠FEH = ∠FGH [19] & F,C,E are collinear [04] & H,B,E are collinear [09] ⇒  ∠HGB = ∠ABG [20]
012. ∠HGB = ∠ABG [20] ⇒  HG ∥ BA
==========================

 

 

196. examples/complete2/unsolved/complete_018_ex-gao_ex160_4_010.gex

a b c d = isquare a b c d; e = mirror e a b; f = midpoint f b a; g = on_tline g f d f, angle_bisector g c b e; h = foot h g a b ? cong d f g f

 

○ 번역 

 

정사각형 ABCD가 주어져 있습니다. B는 EA의 중점입니다. F는 선분 BA의 중점입니다. G는 F를 지나고 DF에 수직인 직선 위에 있으며, ∠CBE의 이등분선 위에 있습니다. H는 G에서 AB로 내린 수선의 발입니다. 선분 DF와 선분 GF의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
AB = BC [00]
AB ⟂ BC [01]
AB ∥ CD [02]
AD ∥ BC [03]
BA = BE [04]
B,A,E are collinear [05]
B,A,F are collinear [06]
FG ⟂ DF [07]
∠CBG = ∠GBE [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. BA = BE [04] & AB = BC [00] ⇒  B is the circumcenter of \Delta CEA [09]
002. BA = BE [04] & AB = BC [00] ⇒  BC = BE [10]
003. B is the circumcenter of \Delta CEA [09] & B,A,E are collinear [05] ⇒  CE ⟂ AC [11]
004. FG ⟂ DF [07] & CE ⟂ AC [11] ⇒  ∠DFG = ∠ECA [12]
005. AB ∥ CD [02] & BC ∥ AD [03] ⇒  ∠ABC = ∠CDA [13]
006. BC ∥ AD [03] ⇒  ∠ACB = ∠CAD [14]
007. ∠ABC = ∠CDA [13] & ∠ACB = ∠CAD [14] (Similar Triangles)⇒  BA:BC = DC:DA [15]
008. ∠ABC = ∠CDA [13] & ∠ACB = ∠CAD [14] (Similar Triangles)⇒  CB = AD [16]
009. ∠ABC = ∠CDA [13] & ∠ACB = ∠CAD [14] (Similar Triangles)⇒  AB = CD [17]
010. BA:BC = DC:DA [15] & AB = BC [00] ⇒  DC = DA [18]
011. AB = BC [00] & DC = DA [18] ⇒  CA ⟂ BD [19]
012. BC = BE [10] & ∠CBG = ∠GBE [08] (SAS)⇒  GC = GE [20]
013. BC = BE [10] & GC = GE [20] ⇒  CE ⟂ BG [21]
014. ∠DFG = ∠ECA [12] & CA ⟂ BD [19] & BG ⟂ CE [21] & CE ⟂ AC [11] ⇒  ∠DFG = ∠DBG [22]
015. ∠DFG = ∠DBG [22] ⇒  B,D,G,F are concyclic [23]
016. B,A,E are collinear [05] & BA = BE [04] ⇒  B is midpoint of AE [24]
017. B,A,E are collinear [05] & BC ⟂ AB [01] ⇒  CB ⟂ AE [25]
018. B is midpoint of AE [24] & CB ⟂ AE [25] ⇒  CA = CE [26]
019. AB = CD [17] & BA = BE [04] ⇒  EB = CD [27]
020. CB = AD [16] & CA = CE [26] & EB = CD [27] (SSS)⇒  ∠BEC = ∠ACD [28]
021. B,A,F are collinear [06] & ∠BEC = ∠ACD [28] & B,A,E are collinear [05] & CA ⟂ BD [19] & BG ⟂ CE [21] & CE ⟂ AC [11] & AB ∥ CD [02] ⇒  ∠FBG = ∠DBF [29]
022. B,D,G,F are concyclic [23] & ∠FBG = ∠DBF [29] ⇒  DF = FG
==========================

 

 

197. examples/complete2/unsolved/complete_005_Other_unsolved_82.gex

a b c = triangle a b c; o = incenter o a b c; i = foot i c a o; e = on_tline e a a o; j = foot j c a e; l = foot l c b o ? coll i l j

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. O는 삼각형 ABC의 내심입니다. I는 C에서 AO로 내린 수선의 발입니다. E는 A를 지나고 AO에 수직한 직선 위에 있습니다. J는 C에서 AE로 내린 수선의 발이고, L은 C에서 BO로 내린 수선의 발입니다. 점 I, L, J가 한 선 위에 존재함을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
∠BAD = ∠DAC [00]
∠ACD = ∠DCB [01]
A,D,E are collinear [02]
CE ⟂ AD [03]
AD ⟂ FA [04]
A,G,F are collinear [05]
AF ⟂ GC [06]
H,D,B are collinear [07]
CH ⟂ BD [08]

 * Auxiliary Constructions:
I : Points
AI = AC [09]
DI = DC [10]

 * Proof steps:
001. A,D,E are collinear [02] & H,D,B are collinear [07] & CH ⟂ BD [08] & CE ⟂ AD [03] ⇒  ∠DEC = ∠DHC [11]
002. ∠DEC = ∠DHC [11] ⇒  C,H,D,E are concyclic [12]
003. C,H,D,E are concyclic [12] ⇒  ∠CDH = ∠CEH [13]
004. AI = AC [09] & DI = DC [10] (SSS)⇒  ∠IAD = ∠DAC [14]
005. AI = AC [09] & DI = DC [10] (SSS)⇒  ∠(AI-CD) = ∠(DI-AC) [15]
006. AI = AC [09] & DI = DC [10] ⇒  AD ⟂ IC [16]
007. ∠IAD = ∠DAC [14] & ∠BAD = ∠DAC [00] ⇒  ∠BAD = ∠IAD [17]
008. ∠BAD = ∠IAD [17] ⇒  AB ∥ AI [18]
009. AB ∥ AI [18] ⇒  A,B,I are collinear [19]
010. ∠ACD = ∠DCB [01] & ∠(AI-CD) = ∠(DI-AC) [15] ⇒  ∠DCB = ∠DIA [20]
011. A,B,I are collinear [19] & ∠AID = ∠BCD [20] & AI ∥ AB [18] ⇒  ∠BID = ∠BCD [21]
012. ∠BID = ∠BCD [21] ⇒  C,D,B,I are concyclic [22]
013. C,D,B,I are concyclic [22] ⇒  ∠CDB = ∠CIB [23]
014. A,G,F are collinear [05] & ∠CDH = ∠CEH [13] & H,D,B are collinear [07] & ∠CDB = ∠CIB [23] & AD ⟂ IC [16] & CE ⟂ AD [03] & A,B,I are collinear [19] & AB ∥ AI [18] & AD ⟂ FA [04] ⇒  ∠BAG = ∠(HE-AG) [24]
015. ∠BAG = ∠(HE-AG) [24] ⇒  AB ∥ HE [25]
016. A,D,E are collinear [02] & A,G,F are collinear [05] & CE ⟂ AD [03] & AD ⟂ FA [04] & AF ⟂ GC [06] ⇒  ∠AEC = ∠AGC [26]
017. ∠AEC = ∠AGC [26] ⇒  C,A,G,E are concyclic [27]
018. C,A,G,E are concyclic [27] ⇒  ∠CAE = ∠CGE [28]
019. ∠CAE = ∠CGE [28] & A,D,E are collinear [02] & AF ⟂ GC [06] & CE ⟂ AD [03] & AD ⟂ FA [04] & ∠BAD = ∠DAC [00] ⇒  ∠BAD = ∠(GE-AD) [29]
020. ∠BAD = ∠(GE-AD) [29] ⇒  AB ∥ GE [30]
021. AB ∥ EH [25] & AB ∥ EG [30] ⇒  EG ∥ EH [31]
022. EG ∥ EH [31] ⇒  H,G,E are collinear
==========================

 

 

198. examples/complete2/unsolved/complete_014_7_Book_00EE_07_E057-41.gex

a b c = triangle a b c; d = foot d c a b; e = free e; f = on_circle f c e; g = on_line g d f, on_circle g c e; h = on_line h d e, on_circle h c e; i = on_line i f h, on_line i a b; j = on_line j e g, on_line j a b ? cong j d d i

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 C에서 AB로 내린 수선의 발입니다. E는 자유롭게 선택된 점입니다. F는 C를 중심으로 하고 E를 지나는 원 위에 있습니다. G는 직선 DF 위에 있고, C를 중심으로 하고 E를 지나는 원 위에 있습니다. H는 직선 DE 위에 있고, C를 중심으로 하고 E를 지나는 원 위에 있습니다. I는 직선 FH와 직선 AB의 교점입니다. J는 직선 EG와 직선 AB의 교점입니다. 선분 JD와 선분 DI의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I J : Points
D,B,A are collinear [00]
CD ⟂ AB [01]
CF = CE [02]
∠(DF-AB) = ∠(DF-AB) [03]
CG = CE [04]
D,G,F are collinear [05]
CH = CE [06]
D,E,H are collinear [07]
H,F,I are collinear [08]
B,I,A are collinear [09]
B,J,A are collinear [10]
G,J,E are collinear [11]

 * Auxiliary Constructions:
K L M : Points
KG = KF [12]
D,L,F are collinear [13]
DL = DF [14]
AM = AL [15]
BM = BL [16]

 * Proof steps:
001. AM = AL [15] & BM = BL [16] (SSS)⇒  ∠LAB = ∠BAM [17]
002. AM = AL [15] & BM = BL [16] ⇒  AB ⟂ LM [18]
003. B,J,A are collinear [10] & ∠LAB = ∠BAM [17] ⇒  ∠LAJ = ∠JAM [19]
004. AM = AL [15] & ∠LAJ = ∠JAM [19] (SAS)⇒  ∠LJA = ∠AJM [20]
005. D,B,A are collinear [00] & ∠LAB = ∠BAM [17] ⇒  ∠LAD = ∠DAM [21]
006. AM = AL [15] & ∠LAD = ∠DAM [21] (SAS)⇒  ∠LDA = ∠ADM [22]
007. AM = AL [15] & ∠LAD = ∠DAM [21] (SAS)⇒  DL = DM [23]
008. DL = DF [14] & DL = DM [23] ⇒  DM = DF [24]
009. DL = DF [14] & DL = DM [23] ⇒  D is the circumcenter of \Delta LMF [25]
010. CF = CE [02] & CG = CE [04] ⇒  CG = CF [26]
011. CG = CF [26] & KG = KF [12] ⇒  GF ⟂ CK [27]
012. D,L,F are collinear [13] & GF ⟂ CK [27] & D,G,F are collinear [05] ⇒  KC ⟂ DL [28]
013. B,J,A are collinear [10] & B,I,A are collinear [09] & AB ⟂ LM [18] ⇒  JI ⟂ LM [29]
014. KC ⟂ DL [28] & JI ⟂ LM [29] ⇒  ∠(KC-JI) = ∠DLM [30]
015. KC ⟂ DL [28] & JI ⟂ LM [29] ⇒  ∠(KC-LM) = ∠(DL-JI) [31]
016. D,L,F are collinear [13] & B,J,A are collinear [10] & B,I,A are collinear [09] & ∠(KC-JI) = ∠DLM [30] ⇒  ∠(DL-KC) = ∠(LM-JI) [32]
017. B,J,A are collinear [10] & B,I,A are collinear [09] & ∠LDA = ∠ADM [22] & D,L,F are collinear [13] & D,B,A are collinear [00] & ∠(KC-LM) = ∠(DL-JI) [31] ⇒  ∠(KC-LM) = ∠(JI-DM) [33]
018. ∠(DL-KC) = ∠(LM-JI) [32] & ∠(KC-LM) = ∠(JI-DM) [33] ⇒  ∠DLM = ∠LMD [34]
019. ∠DLM = ∠LMD [34] & D,L,F are collinear [13] & AB ⟂ LM [18] & CD ⟂ AB [01] ⇒  ∠MDC = ∠CDF [35]
020. DM = DF [24] & ∠MDC = ∠CDF [35] (SAS)⇒  CM = CF [36]
021. CH = CE [06] & CF = CE [02] & CM = CF [36] ⇒  H,F,M,E are concyclic [37]
022. H,F,M,E are concyclic [37] & CF = CE [02] & CH = CE [06] & CG = CE [04] ⇒  M,G,F,E are concyclic [38]
023. M,G,F,E are concyclic [38] ⇒  ∠GEM = ∠GFM [39]
024. D is the circumcenter of \Delta LMF [25] & D,L,F are collinear [13] ⇒  LM ⟂ MF [40]
025. G,J,E are collinear [11] & B,J,A are collinear [10] & D,B,A are collinear [00] & ∠LDA = ∠ADM [22] & D,L,F are collinear [13] & ∠GEM = ∠GFM [39] & D,G,F are collinear [05] & LM ⟂ MF [40] & LM ⟂ AB [18] ⇒  ∠JEM = ∠JDM [41]
026. ∠JEM = ∠JDM [41] ⇒  D,M,J,E are concyclic [42]
027. D,M,J,E are concyclic [42] ⇒  ∠DJM = ∠DEM [43]
028. E,F,H,M are concyclic [37] ⇒  ∠EHF = ∠EMF [44]
029. H,F,I are collinear [08] & B,I,A are collinear [09] & D,B,A are collinear [00] & B,J,A are collinear [10] & ∠LJA = ∠AJM [20] & ∠DJM = ∠DEM [43] & ∠EHF = ∠EMF [44] & D,E,H are collinear [07] & LM ⟂ MF [40] & LM ⟂ AB [18] ⇒  ∠FID = ∠LJD [45]
030. B,I,A are collinear [09] & D,B,A are collinear [00] & D,L,F are collinear [13] & B,J,A are collinear [10] & ∠(DF-AB) = ∠(DF-AB) [03] ⇒  ∠FDI = ∠LDJ [46]
031. ∠FID = ∠LJD [45] & ∠FDI = ∠LDJ [46] (Similar Triangles)⇒  DF:DL = DI:DJ [47]
032. DF:DL = DI:DJ [47] & DL = DF [14] ⇒  DI = DJ
==========================

 

 

199. examples/complete2/unsolved/complete_015_7_Book_00EE_08_E059-55.gex

a b = segment a b; c = on_circle c a b; d = lc_tangent d b a, lc_tangent d c a; e = on_circle e a b; f = on_line f d e, on_circle f a b; g = angle_bisector g f b e, on_line g d e ? cong d b d g

 

○ 번역 : 추후 업데이트

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
AC = AB [00]
BD ⟂ AB [01]
AE = AB [02]
AF = AB [03]
F,D,E are collinear [04]
G,D,E are collinear [05]
∠FBG = ∠GBE [06]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AC = AB [00] & AF = AB [03] & AE = AB [02] ⇒  B,C,F,E are concyclic [07]
002. B,C,F,E are concyclic [07] ⇒  ∠BFC = ∠BEC [08]
003. B,C,F,E are concyclic [07] ⇒  ∠BCF = ∠BEF [09]
004. ∠BCF = ∠BEF [09] & F,D,E are collinear [04] ⇒  ∠BCF = ∠BED [10]
005. AC = AB [00] ⇒  ∠ACB = ∠CBA [11]
006. AE = AB [02] & AC = AB [00] ⇒  AC = AE [12]
007. AC = AE [12] ⇒  ∠ACE = ∠CEA [13]
008. AE = AB [02] ⇒  ∠ABE = ∠BEA [14]
009. BD ⟂ AB [01] & ∠FBG = ∠GBE [06] & ∠BFC = ∠BEC [08] & ∠BCF = ∠BED [10] & ∠ACB = ∠CBA [11] & ∠ACE = ∠CEA [13] & ∠ABE = ∠BEA [14] (Angle chase)⇒  ∠DBG = ∠(BG-DE) [15]
010. G,D,E are collinear [05] & ∠DBG = ∠(BG-DE) [15] ⇒  ∠DBG = ∠BGD [16]
011. ∠DBG = ∠BGD [16] ⇒  DB = DG
==========================

 

 

200. examples/complete2/unsolved/complete_005_Other_unsolved_E073-17.gex

a b c = triangle a b c; o = circumcenter o a b c; p = lc_tangent p a o, on_line p b c; d = on_circle d p a; e = intersection_lc e d o b; f = intersection_lc f d o c ? para e f p d

 

○ 번역 : 추후 업데이트

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
DB = DC [00]
DA = DB [01]
E,B,C are collinear [02]
AE ⟂ AD [03]
EF = EA [04]
DB = DG [05]
G,F,B are collinear [06]
F,H,C are collinear [07]
DC = DH [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. DB = DC [00] & DA = DB [01] ⇒  D is the circumcenter of \Delta ACB [09]
002. D is the circumcenter of \Delta ACB [09] & AE ⟂ AD [03] ⇒  ∠EAC = ∠ABC [10]
003. C,E,B are collinear [02] & ∠ABC = ∠EAC [10] ⇒  ∠ABE = ∠EAC [11]
004. C,E,B are collinear [02] ⇒  ∠AEB = ∠AEC [12]
005. C,E,B are collinear [02] ⇒  ∠BEF = ∠CEF [13]
006. ∠ABE = ∠EAC [11] & ∠AEB = ∠AEC [12] (Similar Triangles)⇒  AE:EB = EC:AE [14]
007. AE:EB = EC:AE [14] & FE = AE [04] ⇒  FE:EB = EC:FE [15]
008. FE:EB = EC:FE [15] & ∠BEF = ∠CEF [13] (Similar Triangles)⇒  ∠EBF = ∠CFE [16]
009. DB = DG [05] & DB = DC [00] & DC = DH [08] ⇒  G,H,B,C are concyclic [17]
010. B,C,H,G are concyclic [17] ⇒  ∠BCH = ∠BGH [18]
011. F,H,C are collinear [07] & ∠EBF = ∠CFE [16] & E,B,C are collinear [02] & ∠BCH = ∠BGH [18] & G,F,B are collinear [06] ⇒  ∠GHF = ∠EFH [19]
012. ∠GHF = ∠EFH [19] ⇒  GH ∥ FE
==========================

 

입력: 2024.08.07 13:24