본문 바로가기

Contact English

【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [121-140]

 

jgex_ag_231 기하 문제 풀이 [121-140]

 

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


 

121. examples/complete2/010/complete_001_6_GDD_FULL_01-20_20.gex

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

 

 번역 

 

삼각형 ABC가 주어져 있습니다. D는 A에서 BC로 내린 수선의 발이고, E는 B에서 AC로 내린 수선의 발입니다. H는 직선 AD와 BE의 교점에 있습니다. G는 H에서 AB로 내린 수선의 발입니다. ∠EGH = ∠HGD임을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
D,B,C are collinear [00]
AD ⟂ BC [01]
E,A,C are collinear [02]
BE ⟂ AC [03]
D,A,F are collinear [04]
E,B,F are collinear [05]
G,B,A are collinear [06]
FG ⟂ AB [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. B,G,A are collinear [06] & D,F,A are collinear [04] & D,B,C are collinear [00] & AD ⟂ BC [01] & FG ⟂ AB [07] ⇒  ∠FGB = ∠FDB [08]
002. ∠FGB = ∠FDB [08] ⇒  G,D,B,F are concyclic [09]
003. G,D,B,F are concyclic [09] ⇒  ∠GDB = ∠GFB [10]
004. D,B,C are collinear [00] & AD ⟂ BC [01] ⇒  DA ⟂ DB [11]
005. E,A,C are collinear [02] & BE ⟂ AC [03] ⇒  EB ⟂ EA [12]
006. DA ⟂ DB [11] & EB ⟂ EA [12] ⇒  ∠DAE = ∠DBE [13]
007. B,G,A are collinear [06] & E,F,B are collinear [05] & E,A,C are collinear [02] & BE ⟂ AC [03] & FG ⟂ AB [07] ⇒  ∠FGA = ∠FEA [14]
008. ∠FGA = ∠FEA [14] ⇒  G,F,E,A are concyclic [15]
009. G,F,E,A are concyclic [15] ⇒  ∠GFA = ∠GEA [16]
010. ∠GDB = ∠GFB [10] & D,B,C are collinear [00] & E,B,F are collinear [05] & ∠DAE = ∠DBE [13] & E,A,C are collinear [02] & ∠GFA = ∠GEA [16] & D,A,F are collinear [04] ⇒  ∠EGF = ∠FGD
==========================

 

 

 

122. examples/complete2/010/complete_002_6_GDD_FULL_41-60_57.gex

a b c = triangle a b c; d = foot d a b c; o = midpoint o a d; e = on_line e a b, on_circle e o d; f = on_line f a c, on_circle f o d ? cyclic b c e f

 

 번역 

 

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

 

풀이 : AlphaGeometry를 사용한 풀이

 

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

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. EG = ED [06] & EA = ED [02] ⇒  E is the circumcenter of \Delta DGA [07]
002. E is the circumcenter of \Delta DGA [07] & E,A,D are collinear [01] ⇒  DG ⟂ GA [08]
003. G,A,C are collinear [05] & D,A,E are collinear [01] & AD ⟂ BC [00] & DG ⟂ GA [08] ⇒  ∠CGD = ∠(CB-EA) [09]
004. EF = ED [04] & EG = ED [06] & EA = ED [02] ⇒  F,G,A,D are concyclic [10]
005. F,G,A,D are concyclic [10] ⇒  ∠FGD = ∠FAD [11]
006. D,A,E are collinear [01] & F,A,B are collinear [03] & ∠FGD = ∠FAD [11] ⇒  ∠DGF = ∠(EA-FB) [12]
007. ∠CGD = ∠(CB-EA) [09] & ∠DGF = ∠(EA-FB) [12] ⇒  ∠CGF = ∠CBF [13]
008. ∠FGC = ∠FBC [13] ⇒  F,C,G,B are concyclic
==========================

 

 

123. examples/complete2/010/complete_010_Other_Auxiliary_ye_aux_ppara.gex

a b c d = eq_trapezoid a b c d; e = on_pline e b a d, on_line e c d ? eqangle a d a b b a b c

 

 번역 

 

ABCD는 AB와 CD가 평행하고, AD = BC인 등변사다리꼴입니다. 점 E는 B를 지나고 AD에 평행한 직선 위에 있으며, 직선 CD 위에 있습니다. ∠DAB = ∠ABC임을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D : Points
DC ∥ AB [00]
DA = BC [01]

 * Auxiliary Constructions:
E : Points
C,D,E are collinear [02]
EB ∥ AD [03]

 * Proof steps:
001. C,D,E are collinear [02] & CD ∥ AB [00] & BE ∥ AD [03] ⇒  ∠DEB = ∠BAD [04]
002. BE ∥ AD [03] ⇒  ∠DBE = ∠BDA [05]
003. ∠DEB = ∠BAD [04] & ∠DBE = ∠BDA [05] (Similar Triangles)⇒  BE = DA [06]
004. BE = DA [06] & DA = BC [01] ⇒  BC = BE [07]
005. BC = BE [07] ⇒  ∠BCE = ∠CEB [08]
006. ∠BCE = ∠CEB [08] & C,D,E are collinear [02] & CD ∥ AB [00] & BE ∥ AD [03] ⇒  ∠CBA = ∠BAD
==========================

 

 

124. examples/complete2/003/complete_003_6_GDD_FULL_more_E013-3.gex

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

 

 번역 : 추후 업데이트

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
BC ⟂ AB [00]
AD = AB [01]
E,C,D are collinear [02]
AE = AB [03]
E,F,D are collinear [04]
FD = FE [05]
CG ⟂ AG [06]
AG = AB [07]
AG = AH [08]
G,H,F are collinear [09]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. CG ⟂ AG [06] & BC ⟂ AB [00] ⇒  ∠ABC = ∠AGC [10]
002. ∠ABC = ∠AGC [10] ⇒  C,B,G,A are concyclic [11]
003. C,B,G,A are concyclic [11] ⇒  ∠BCA = ∠BGA [12]
004. AG = AH [08] & AG = AB [07] ⇒  A is the circumcenter of \Delta BHG [13]
005. A is the circumcenter of \Delta BHG [13] & BC ⟂ AB [00] ⇒  ∠CBH = ∠BGH [14]
006. ∠BCA = ∠BGA [12] & ∠BGH = ∠CBH [14] ⇒  ∠AGH = ∠(CA-BH) [15]
007. AD = AB [01] & AE = AB [03] ⇒  AE = AD [16]
008. AE = AD [16] & FD = FE [05] ⇒  ED ⟂ AF [17]
009. E,F,D are collinear [04] & E,C,D are collinear [02] & ED ⟂ AF [17] & BC ⟂ AB [00] ⇒  ∠ABC = ∠AFC [18]
010. ∠ABC = ∠AFC [18] ⇒  C,B,F,A are concyclic [19]
011. C,B,F,A are concyclic [19] & C,B,G,A are concyclic [11] ⇒  G,F,A,C are concyclic [20]
012. G,F,A,C are concyclic [20] ⇒  ∠GFC = ∠GAC [21]
013. E,C,D are collinear [02] & ∠AGH = ∠(CA-BH) [15] & G,H,F are collinear [09] & ∠GFC = ∠GAC [21] & E,F,D are collinear [04] ⇒  ∠ECA = ∠(BH-CA) [22]
014. ∠ECA = ∠(BH-CA) [22] ⇒  EC ∥ BH [23]
015. E,C,D are collinear [02] & EC ∥ BH [23] ⇒  DE ∥ BH
==========================

 

 

125. examples/complete2/003/complete_005_Other_ndgs_01.gex

b c a = triangle b c a; d = intersection_cc d b a c; e = on_circle e b c; g = intersection_lc g e a d; f = on_circle f b c; h = intersection_lc h f a c ? para g h e f

 

 번역 : 추후 업데이트 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
AB = AD [00]
CB = CD [01]
AE = AB [02]
D,F,E are collinear [03]
CD = CF [04]
AG = AB [05]
CB = CH [06]
G,B,H are collinear [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AB = AD [00] & AG = AB [05] & AE = AB [02] ⇒  D,B,G,E are concyclic [08]
002. D,B,G,E are concyclic [08] ⇒  ∠GBD = ∠GED [09]
003. CD = CF [04] & CB = CD [01] & CB = CH [06] ⇒  D,B,F,H are concyclic [10]
004. D,B,F,H are concyclic [10] ⇒  ∠DBH = ∠DFH [11]
005. D,F,E are collinear [03] & ∠GBD = ∠GED [09] & ∠DBH = ∠DFH [11] & G,B,H are collinear [07] ⇒  ∠HFD = ∠(GE-DF) [12]
006. ∠HFD = ∠(GE-DF) [12] ⇒  FH ∥ GE
==========================

 

 

126. examples/complete2/003/complete_013_7_Book_00EE_10_E072-12.gex

b a c = triangle b a c; d = on_circle d a b, on_circle d c b; e = on_tline e d b d, on_circle e a b; f = on_circle f c d, on_line f d e; h = on_circle h a b, on_line h b f; g = on_circle g c b, on_line g b e ? eqangle d h d b d b d g

 

 번역 

 

삼각형 BAC가 주어져 있습니다. D는 A를 중심으로 하고 B를 지나는 원 위에 있고, C를 중심으로 하고 B를 지나는 원 위에 있습니다. E는 D를 지나고 BD에 수직인 선 위에 있으며, A를 중심으로 하고 B를 지나는 원 위에 있습니다. F는 C를 중심으로 하고 D를 지나는 원 위에 있으며, 직선 DE 위에 있습니다. H는 A를 중심으로 하고 B를 지나는 원 위에 있으며, 직선 BF 위에 있습니다. G는 C를 중심으로 하고 B를 지나는 원 위에 있으며, 직선 BE 위에 있습니다. ∠HDB = ∠BDG임을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
BD = BA [00]
CD = CA [01]
BE = BA [02]
DE ⟂ AD [03]
CF = CD [04]
D,F,E are collinear [05]
F,G,A are collinear [06]
BG = BA [07]
E,H,A are collinear [08]
CH = CA [09]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. BD = BA [00] & BG = BA [07] & BE = BA [02] ⇒  D,G,E,A are concyclic [10]
002. D,G,E,A are concyclic [10] ⇒  ∠DEG = ∠DAG [11]
003. D,G,E,A are concyclic [10] ⇒  ∠GDA = ∠GEA [12]
004. CF = CD [04] & CD = CA [01] & CH = CA [09] ⇒  D,F,H,A are concyclic [13]
005. D,F,H,A are concyclic [13] ⇒  ∠DFH = ∠DAH [14]
006. D,F,H,A are concyclic [13] ⇒  ∠FHD = ∠FAD [15]
007. E,H,A are collinear [08] & F,G,A are collinear [06] & ∠DEG = ∠DAG [11] & DE ⟂ AD [03] & ∠DFH = ∠DAH [14] & D,F,E are collinear [05] ⇒  ∠FHE = ∠FGE [16]
008. F,G,A are collinear [06] & ∠FHD = ∠FAD [15] ⇒  ∠FHD = ∠(FG-DA) [17]
009. ∠FHE = ∠FGE [16] & ∠FHD = ∠(FG-DA) [17] ⇒  ∠EHD = ∠(EG-DA) [18]
010. ∠EHD = ∠(EG-DA) [18] & E,H,A are collinear [08] & ∠GDA = ∠GEA [12] ⇒  ∠GDA = ∠ADH
==========================

 

 

127. examples/complete2/003/complete_010_Other_Auxiliary_ye_aux_wang3.gex

a b c d = isquare a b c d; f = angle_bisector f a d b, on_line f a c; g = foot g c d f; e = on_line e b d, on_line e a c; h = on_line h c g, on_line h a d; i = on_line i b d, on_line i c g; x = midpoint x a h ? cong a x e i

 

 번역 : 추후 업데이트

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I J : Points
AB ∥ CD [00]
AD ∥ BC [01]
∠ADE = ∠EDB [02]
E,F,D are collinear [03]
CF ⟂ DE [04]
A,C,G are collinear [05]
B,D,G are collinear [06]
F,H,C are collinear [07]
A,H,D are collinear [08]
F,I,C are collinear [09]
I,B,D are collinear [10]
A,H,J are collinear [11]
JA = JH [12]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. J,H,A are collinear [11] & JA = JH [12] ⇒  J is midpoint of HA [13]
002. AB ∥ CD [00] & A,C,G are collinear [05] & B,D,G are collinear [06] ⇒  CD:AB = GC:GA [14]
003. BC ∥ AD [01] & AB ∥ CD [00] ⇒  ∠ADC = ∠CBA [15]
004. CD ∥ AB [00] ⇒  ∠ACD = ∠CAB [16]
005. ∠ADC = ∠CBA [15] & ∠ACD = ∠CAB [16] (Similar Triangles)⇒  CD = AB [17]
006. A,C,G are collinear [05] & CD:AB = GC:GA [14] & CD = AB [17] ⇒  G is midpoint of AC [18]
007. J is midpoint of HA [13] & G is midpoint of AC [18] ⇒  JG ∥ HC [19]
008. F,I,C are collinear [09] & F,H,C are collinear [07] & JG ∥ HC [19] ⇒  HI ∥ JG [20]
009. A,H,J are collinear [11] & A,H,D are collinear [08] ⇒  D,H,J are collinear [21]
010. I,B,D are collinear [10] & B,D,G are collinear [06] ⇒  D,I,G are collinear [22]
011. HI ∥ JG [20] & D,H,J are collinear [21] & D,I,G are collinear [22] ⇒  HD:ID = HJ:IG [23]
012. F,H,C are collinear [07] & F,D,E are collinear [03] & F,I,C are collinear [09] & CF ⟂ DE [04] ⇒  ∠HFD = ∠DFI [24]
013. A,H,D are collinear [08] & F,D,E are collinear [03] & I,B,D are collinear [10] & ∠ADE = ∠EDB [02] ⇒  ∠HDF = ∠FDI [25]
014. ∠HFD = ∠DFI [24] & ∠HDF = ∠FDI [25] (Similar Triangles)⇒  DH = DI [26]
015. HD:ID = HJ:IG [23] & DH = DI [26] & JA = JH [12] ⇒  AJ = GI
==========================

 

 

128. examples/complete2/003/complete_003_6_GDD_FULL_more_E022-8.gex

b a c = triangle b a c; d = on_circle d a b, on_circle d c b; e = on_circle e c b; f = intersection_lc f e a d; g = intersection_lc g e a b; h = on_tline h e c e ? para h e g f

 

 번역 : 추후 업데이트 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
BD = BA [00]
CD = CA [01]
CE = CA [02]
BD = BF [03]
F,E,D are collinear [04]
BA = BG [05]
E,A,G are collinear [06]
EH ⟂ CE [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. BD = BF [03] & BD = BA [00] & BA = BG [05] ⇒  F,A,G,D are concyclic [08]
002. F,A,G,D are concyclic [08] ⇒  ∠FGA = ∠FDA [09]
003. CE = CA [02] & CD = CA [01] ⇒  C is the circumcenter of \Delta EAD [10]
004. C is the circumcenter of \Delta EAD [10] & EH ⟂ CE [07] ⇒  ∠HEA = ∠EDA [11]
005. ∠FGA = ∠FDA [09] & E,A,G are collinear [06] & F,E,D are collinear [04] & ∠HEA = ∠EDA [11] ⇒  ∠HEA = ∠(FG-EA) [12]
006. ∠HEA = ∠(FG-EA) [12] ⇒  HE ∥ FG
==========================

 

 

129. examples/complete2/003/complete_008_ex-gao_ex160_206.gex

a b c = triangle a b c; e d = square b a e d; f g = square a c f g; h = on_line h b e, on_line h a d; i = on_pline i e a g, on_pline i g a e ? perp c h h i

 

 번역 

 

삼각형 ABC가 주어져 있습니다. BAED는 BA를 한 변으로 하는 정사각형이고, ACFG는 AC를 한 변으로 하는 정사각형입니다. 점 H는 직선 BE와 AD의 교점에 있습니다. 점 I는 E를 지나고 AG에 평행한 직선 위에 있고, G를 지나고 AE에 평행한 직선 위에 있습니다. 선분 CH와 선분 HI가 서로 수직임을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
AB ⟂ AD [00]
BA = AD [01]
BA ∥ DE [02]
BE ∥ AD [03]
AC = CF [04]
AC ⟂ CF [05]
AG ∥ CF [06]
AC ∥ FG [07]
E,A,H are collinear [08]
D,H,B are collinear [09]
ID ∥ AG [10]
IG ∥ AD [11]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AB ∥ DE [02] & E,A,H are collinear [08] & D,H,B are collinear [09] ⇒  EA:DB = EH:DH [12]
002. AB ⟂ AD [00] & AD ∥ BE [03] & AB ∥ DE [02] ⇒  ∠ABE = ∠ADE [13]
003. ∠ABE = ∠ADE [13] ⇒  E,A,D,B are concyclic [14]
004. AB ∥ DE [02] & AD ∥ BE [03] ⇒  ∠EDA = ∠DEB [15]
005. AB ∥ DE [02] & AD ∥ BE [03] ⇒  ∠ABE = ∠EDA [16]
006. AB ∥ DE [02] & AD ∥ BE [03] ⇒  ∠BED = ∠DAB [17]
007. E,A,D,B are concyclic [14] & ∠EDA = ∠DEB [15] ⇒  EA = DB [18]
008. EA:DB = EH:DH [12] & EA = DB [18] ⇒  EH = DH [19]
009. BE ∥ AD [03] ⇒  ∠AEB = ∠EAD [20]
010. ∠ABE = ∠EDA [16] & ∠AEB = ∠EAD [20] (Similar Triangles)⇒  AB = ED [21]
011. BA = AD [01] & AB = ED [21] ⇒  DE = DA [22]
012. CF ∥ AG [06] & AC ∥ FG [07] ⇒  ∠AGF = ∠FCA [23]
013. FG ∥ AC [07] ⇒  ∠AFG = ∠FAC [24]
014. ∠AGF = ∠FCA [23] & ∠AFG = ∠FAC [24] (Similar Triangles)⇒  AG = FC [25]
015. ∠AGF = ∠FCA [23] & ∠AFG = ∠FAC [24] (Similar Triangles)⇒  CF:CA = GA:GF [26]
016. AG = FC [25] & CF:CA = GA:GF [26] & AC = CF [04] ⇒  FG = FC [27]
017. AC = CF [04] ⇒  ∠CAF = ∠AFC [28]
018. ∠CAF = ∠AFC [28] & DI ∥ AG [10] & AG ∥ CF [06] & AC ∥ FG [07] ⇒  ∠AFC = ∠GFA [29]
019. FG = FC [27] & ∠AFC = ∠GFA [29] (SAS)⇒  AG = AC [30]
020. DI ∥ AG [10] & AD ∥ GI [11] ⇒  ∠DAG = ∠GID [31]
021. AG ∥ DI [10] ⇒  ∠DGA = ∠GDI [32]
022. ∠DAG = ∠GID [31] & ∠DGA = ∠GDI [32] (Similar Triangles)⇒  GA = DI [33]
023. AG = AC [30] & GA = DI [33] ⇒  DI = AC [34]
024. AB ⟂ AD [00] & AD ∥ GI [11] & AB ∥ DE [02] ⇒  IG ⟂ ED [35]
025. AC ⟂ CF [05] & AC ∥ FG [07] & DI ∥ AG [10] & AG ∥ CF [06] ⇒  FG ⟂ DI [36]
026. IG ⟂ ED [35] & FG ⟂ DI [36] ⇒  ∠IGF = ∠EDI [37]
027. IG ⟂ ED [35] & FG ⟂ DI [36] ⇒  ∠(GI-DE) = ∠(DI-FG) [38]
028. IG ⟂ ED [35] & FG ⟂ DI [36] ⇒  ∠(GI-DE) = ∠(FG-DI) [39]
029. ∠IGF = ∠EDI [37] & GI ∥ AD [11] & AC ∥ FG [07] & AB ∥ DE [02] ⇒  ∠EDI = ∠DAC [40]
030. DE = DA [22] & DI = AC [34] & ∠EDI = ∠DAC [40] (SAS)⇒  IE = CD [41]
031. ∠IGF = ∠EDI [37] & GI ∥ AD [11] & AC ∥ FG [07] & AB ∥ DE [02] & DI ∥ AG [10] ⇒  ∠CAD = ∠GAB [42]
032. AC = AG [30] & BA = AD [01] & ∠CAD = ∠GAB [42] (SAS)⇒  ∠(BG-CD) = ∠BAD [43]
033. AC = AG [30] & BA = AD [01] & ∠CAD = ∠GAB [42] (SAS)⇒  ∠CAG = ∠(CD-BG) [44]
034. ∠(BG-CD) = ∠BAD [43] & ∠(GI-DE) = ∠(DI-FG) [38] & GI ∥ AD [11] & AB ∥ DE [02] & AG ∥ CF [06] & DI ∥ AG [10] & AC ∥ FG [07] & ∠CAG = ∠(CD-BG) [44] ⇒  CD ⟂ GB [45]
035. DE ∥ AB [02] ⇒  ∠BDE = ∠DBA [46]
036. ∠BED = ∠DAB [17] & ∠BDE = ∠DBA [46] (Similar Triangles)⇒  AD:AB = EB:ED [47]
037. AD:AB = EB:ED [47] & BA = AD [01] ⇒  EB = ED [48]
038. EB = ED [48] & BA = AD [01] ⇒  BD ⟂ AE [49]
039. D,H,B are collinear [09] & AE ⟂ BD [49] ⇒  EA ⟂ DH [50]
040. CD ⟂ GB [45] & EA ⟂ DH [50] ⇒  ∠CDH = ∠(GB-EA) [51]
041. AB ∥ DE [02] & DI ∥ AG [10] ⇒  ∠EDI = ∠BAG [52]
042. AB = ED [21] & GA = DI [33] & ∠EDI = ∠BAG [52] (SAS)⇒  ∠(DE-AB) = ∠(EI-BG) [53]
043. D,H,B are collinear [09] & A,E,H are collinear [08] & ∠CDH = ∠(GB-EA) [51] & ∠(DE-AB) = ∠(EI-BG) [53] & AB ∥ DE [02] ⇒  ∠HDC = ∠HEI [54]
044. EH = DH [19] & IE = CD [41] & ∠HDC = ∠HEI [54] (SAS)⇒  ∠DHC = ∠EHI [55]
045. BE ∥ AD [03] & E,A,H are collinear [08] & D,H,B are collinear [09] ⇒  AE:DB = AH:DH [56]
046. AE:DB = AH:DH [56] & EA = DB [18] ⇒  AH = DH [57]
047. AC = AG [30] & ED = EB [48] ⇒  AC:AG = ED:EB [58]
048. ∠(GI-DE) = ∠(FG-DI) [39] & GI ∥ AD [11] & AB ∥ DE [02] & AC ∥ FG [07] & AG ∥ CF [06] & DI ∥ AG [10] & AD ∥ BE [03] ⇒  ∠CAG = ∠BED [59]
049. AC:AG = ED:EB [58] & ∠CAG = ∠BED [59] (Similar Triangles)⇒  ∠(CG-BE) = ∠(AG-BD) [60]
050. AC = AG [30] & DA = DE [22] ⇒  AC:AG = DA:DE [61]
051. ∠(GI-DE) = ∠(DI-FG) [38] & GI ∥ AD [11] & AB ∥ DE [02] & AG ∥ CF [06] & DI ∥ AG [10] & AC ∥ FG [07] ⇒  ∠CAG = ∠EDA [62]
052. AC:AG = DA:DE [61] & ∠CAG = ∠EDA [62] (Similar Triangles)⇒  ∠EAC = ∠(AD-CG) [63]
053. E,A,H are collinear [08] & D,H,B are collinear [09] & ∠(CG-BE) = ∠(AG-BD) [60] & BE ∥ AD [03] & DI ∥ AG [10] & ∠EAC = ∠(AD-CG) [63] ⇒  ∠HAC = ∠HDI [64]
054. AH = DH [57] & DI = AC [34] & ∠HAC = ∠HDI [64] (SAS)⇒  ∠AHC = ∠DHI [65]
055. ∠DHC = ∠EHI [55] & D,H,B are collinear [09] & E,A,H are collinear [08] & ∠AHC = ∠DHI [65] ⇒  CH ⟂ HI
==========================

 

 

130. examples/complete2/003/complete_013_7_Book_00EE_11_E077-38.gex

a b c = triangle a b c; d = circumcenter d a b c; e = lc_tangent e b d; f = angle_bisector f e b c, on_circle f d a; g = foot g f b c; h = foot h f b e ? eqangle b a a f f a a c

 

 번역 : 추후 업데이트

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
DA = DB [00]
DB = DC [01]
BE ⟂ BD [02]
DF = DA [03]
∠EBF = ∠FBC [04]

 * Auxiliary Constructions:
H : Points
B,H,E are collinear [05]

 * Proof steps:
001. DA = DB [00] & DF = DA [03] & DB = DC [01] ⇒  B,C,A,F are concyclic [06]
002. B,C,A,F are concyclic [06] ⇒  ∠FBC = ∠FAC [07]
003. DA = DB [00] & DF = DA [03] ⇒  D is the circumcenter of \Delta BAF [08]
004. B,H,E are collinear [05] & BD ⟂ BE [02] ⇒  DB ⟂ BH [09]
005. D is the circumcenter of \Delta BAF [08] & DB ⟂ BH [09] ⇒  ∠HBA = ∠BFA [10]
006. ∠FBC = ∠FAC [07] & ∠EBF = ∠FBC [04] & ∠HBA = ∠BFA [10] & B,H,E are collinear [05] ⇒  ∠BAF = ∠FAC
==========================

 

 

131. examples/complete2/003/complete_004_6_GDD_FULL_81-109_84.gex

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

 

 번역 

 

삼각형 ABC가 주어져 있습니다. D는 선분 BA의 중점이고, E는 선분 CB의 중점, F는 선분 AC의 중점입니다. G는 삼각형 DEF의 외심입니다. H는 E를 지나고 EG에 수직인 선 위에 있으며, 직선 AB 위에 있습니다. I는 직선 EH와 AC의 교점입니다. 점 B, H, C, I가 한 원 위에 있음을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
A,B,D are collinear [00]
DB = DA [01]
C,B,E are collinear [02]
EC = EB [03]
A,F,C are collinear [04]
FA = FC [05]
GD = GE [06]
GE = GF [07]
A,B,H are collinear [08]
EH ⟂ EG [09]
I,H,E are collinear [10]
A,C,I are collinear [11]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. GD = GE [06] & GE = GF [07] ⇒  G is the circumcenter of \Delta EDF [12]
002. I,H,E are collinear [10] & EG ⟂ EH [09] ⇒  GE ⟂ EI [13]
003. G is the circumcenter of \Delta EDF [12] & GE ⟂ EI [13] ⇒  ∠IED = ∠EFD [14]
004. A,B,D are collinear [00] & DB = DA [01] ⇒  D is midpoint of AB [15]
005. C,B,E are collinear [02] & EC = EB [03] ⇒  E is midpoint of BC [16]
006. D is midpoint of AB [15] & E is midpoint of BC [16] ⇒  DE ∥ AC [17]
007. A,F,C are collinear [04] & FA = FC [05] ⇒  F is midpoint of AC [18]
008. E is midpoint of BC [16] & F is midpoint of AC [18] ⇒  EF ∥ BA [19]
009. D is midpoint of AB [15] & F is midpoint of AC [18] ⇒  DF ∥ BC [20]
010. I,H,E are collinear [10] & C,I,A are collinear [11] & A,B,H are collinear [08] & ∠IED = ∠EFD [14] & DE ∥ AC [17] & EF ∥ AB [19] & DF ∥ BC [20] ⇒  ∠HIC = ∠HBC [21]
011. ∠HIC = ∠HBC [21] ⇒  C,B,I,H are concyclic
==========================

 

 

132. examples/complete2/003/complete_003_6_GDD_FULL_more_E022-10.gex

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

 

 번역 

 

선분 AB가 주어져 있습니다. 점 C, E, D는 모두 A를 중심으로 하고 B를 지나는 원 위에 있습니다. F는 직선 CE와 BD의 교점입니다. G는 점 E, F, B를 지나는 원의 중심입니다. H는 F를 지나고 FG에 수직인 선 위에 있습니다. 선분 HF와 CD가 서로 평행임을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
AC = AB [00]
AD = AB [01]
AE = AB [02]
D,F,C are collinear [03]
F,E,B are collinear [04]
GD = GF [05]
GF = GB [06]
FH ⟂ FG [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AD = AB [01] & AE = AB [02] & AC = AB [00] ⇒  D,E,B,C are concyclic [08]
002. D,E,B,C are concyclic [08] ⇒  ∠EBD = ∠ECD [09]
003. GD = GF [05] & GF = GB [06] ⇒  G is the circumcenter of \Delta FDB [10]
004. G is the circumcenter of \Delta FDB [10] & FH ⟂ FG [07] ⇒  ∠HFD = ∠FBD [11]
005. D,F,C are collinear [03] & ∠EBD = ∠ECD [09] & ∠HFD = ∠FBD [11] & F,E,B are collinear [04] ⇒  ∠HFD = ∠(EC-DF) [12]
006. ∠HFD = ∠(EC-DF) [12] ⇒  HF ∥ EC
==========================

 

 

133. examples/complete2/003/complete_011_7_Book_00EE_03_E037-25.gex

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

 

 번역 

 

선분 AB가 주어져 있습니다. C는 선분 BA의 중점입니다. 점 D는 C를 지나고 AB에 수직인 직선 위에 있으며, C를 중심으로 하고 A를 지나는 원 위에 있습니다. E는 C를 중심으로 하고 D를 지나는 원 위에 있으며, 직선 DC 위에 있습니다. F는 직선 AB 위에 있습니다. G는 직선 CD 위에 있고, C를 중심으로 하고 F를 지나는 원 위에 있습니다. H는 C를 중심으로 하고 E를 지나는 원 위에 있고, 직선 EF 위에 있습니다. I는 직선 BG 위에 있고, C를 중심으로 하고 A를 지나는 원 위에 있습니다. 선분 EH와 선분 BI가 서로 수직임을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
CB = CA [00]
B,C,A are collinear [01]
CD = CA [02]
CD ⟂ AB [03]
CE = CD [04]
C,D,E are collinear [05]
B,F,A are collinear [06]
CG = CF [07]
G,C,D are collinear [08]
H,F,E are collinear [09]
G,I,B are collinear [10]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. CE = CD [04] & CD = CA [02] & CB = CA [00] ⇒  CB = CE [11]
002. B,C,A are collinear [01] & G,C,D are collinear [08] & C,D,E are collinear [05] & B,F,A are collinear [06] & CD ⟂ AB [03] ⇒  ∠BCG = ∠ECF [12]
003. CB = CE [11] & CG = CF [07] & ∠BCG = ∠ECF [12] (SAS)⇒  ∠BGC = ∠EFC [13]
004. CB = CE [11] & CG = CF [07] & ∠BCG = ∠ECF [12] (SAS)⇒  ∠CBG = ∠CEF [14]
005. H,F,E are collinear [09] & G,I,B are collinear [10] & ∠BGC = ∠EFC [13] & G,C,D are collinear [08] & B,F,A are collinear [06] & B,C,A are collinear [01] & ∠CBG = ∠CEF [14] & C,D,E are collinear [05] ⇒  EH ⟂ BI
==========================

 

 

134. examples/complete2/003/complete_016_7_Book_00EE_06_E051-25.gex

a b c = triangle a b c; d = foot d b a c; e = foot e c a b; g = circumcenter g b c a; h = intersection_lc h g g a; f = on_line f b d, on_line f c e; i = on_line i b c, on_line i f h ? cong f i i h

 

 번역 : 추후 업데이트 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
BD ⟂ AC [00]
CE ⟂ AB [01]
FC = FA [02]
FB = FC [03]
FA = FG [04]
F,A,G are collinear [05]
B,H,D are collinear [06]
C,E,H are collinear [07]
I,G,H are collinear [08]
C,I,B are collinear [09]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. FC = FA [02] & FA = FG [04] ⇒  F is the circumcenter of \Delta ACG [10]
002. F is the circumcenter of \Delta ACG [10] & F,A,G are collinear [05] ⇒  AC ⟂ CG [11]
003. B,H,D are collinear [06] & AC ⟂ CG [11] & BD ⟂ AC [00] ⇒  CG ∥ BH [12]
004. CG ∥ BH [12] & I,G,H are collinear [08] & C,I,B are collinear [09] ⇒  GC:HB = IG:IH [13]
005. B,H,D are collinear [06] & AC ⟂ CG [11] & BD ⟂ AC [00] ⇒  ∠BCG = ∠CBH [14]
006. FB = FC [03] & FC = FA [02] & FA = FG [04] ⇒  F is the circumcenter of \Delta ABG [15]
007. F is the circumcenter of \Delta ABG [15] & F,A,G are collinear [05] ⇒  AB ⟂ BG [16]
008. C,E,H are collinear [07] & B,H,D are collinear [06] & AB ⟂ BG [16] & CE ⟂ AB [01] & AC ⟂ CG [11] & BD ⟂ AC [00] ⇒  ∠BGC = ∠CHB [17]
009. ∠BCG = ∠CBH [14] & ∠BGC = ∠CHB [17] (Similar Triangles)⇒  CG = BH [18]
010. GC:HB = IG:IH [13] & CG = BH [18] ⇒  IG = IH
==========================

 

 

135. examples/complete2/003/complete_013_7_Book_00EE_10_E074-20.gex

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

 

 번역 

 

삼각형 ABC가 주어져 있습니다. D는 직선 AB 위에 있습니다. E는 D에서 BC로 내린 수선의 발이고, F는 E에서 AB로 내린 수선의 발입니다. G는 직선 BC 위에 있고, H는 G에서 AB로 내린 수선의 발입니다. I는 H에서 BC로 내린 수선의 발입니다. ∠GDH = ∠IFD임을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H I : Points
∠CBA = ∠CBA [00]
B,D,A are collinear [01]
DE ⟂ BC [02]
E,B,C are collinear [03]
F,B,A are collinear [04]
EF ⟂ AB [05]
B,G,C are collinear [06]
H,B,A are collinear [07]
AB ⟂ HG [08]
I,B,C are collinear [09]
BC ⟂ IH [10]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. F,B,A are collinear [04] & I,B,C are collinear [09] & DE ⟂ BC [02] & EF ⟂ AB [05] & BC ⟂ IH [10] ⇒  ∠EFB = ∠BIH [11]
002. E,B,C are collinear [03] & F,B,A are collinear [04] & I,B,C are collinear [09] & H,B,A are collinear [07] ⇒  ∠EBF = ∠IBH [12]
003. ∠EFB = ∠BIH [11] & ∠EBF = ∠IBH [12] (Similar Triangles)⇒  HB:EB = IB:FB [13]
004. H,B,A are collinear [07] & E,B,C are collinear [03] & DE ⟂ BC [02] & EF ⟂ AB [05] & AB ⟂ HG [08] ⇒  ∠GHB = ∠BED [14]
005. B,G,C are collinear [06] & H,B,A are collinear [07] & E,B,C are collinear [03] & B,D,A are collinear [01] ⇒  ∠GBH = ∠EBD [15]
006. ∠GHB = ∠BED [14] & ∠GBH = ∠EBD [15] (Similar Triangles)⇒  BG:BD = HB:EB [16]
007. HB:EB = IB:FB [13] & BG:BD = HB:EB [16] ⇒  BG:BD = BI:BF [17]
008. B,G,C are collinear [06] & B,D,A are collinear [01] & I,B,C are collinear [09] & F,B,A are collinear [04] & ∠CBA = ∠CBA [00] ⇒  ∠GBD = ∠IBF [18]
009. BG:BD = BI:BF [17] & ∠GBD = ∠IBF [18] (Similar Triangles)⇒  ∠BGD = ∠BIF [19]
010. H,B,A are collinear [07] & B,D,A are collinear [01] & F,B,A are collinear [04] & ∠BGD = ∠BIF [19] & B,G,C are collinear [06] & I,B,C are collinear [09] ⇒  ∠GDH = ∠IFD
==========================

 

 

136. examples/complete2/003/complete_017_ex-gao_ex160_4_003.gex

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

 

 번역 

 

선분 AB가 주어져 있습니다. 점 C는 A를 중심으로 하고 B를 지나는 원 위에 있습니다. 점 E는 직선 BC 위에 있습니다. D는 C를 지나고 AC에 수직인 직선 위에 있고, B를 지나고 AB에 수직인 직선 위에 있습니다. F는 E를 지나고 AE에 수직인 직선 위에 있고, 직선 CD 위에 있습니다. G는 직선 EF 위에 있고, A를 중심으로 하고 B를 지나는 원 위에 있습니다. H는 직선 EF와 BD의 교점입니다. 선분 CF와 선분 HB의 길이가 같음을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F H : Points
AC = AB [00]
B,D,C are collinear [01]
BE ⟂ AB [02]
CE ⟂ AC [03]
F,C,E are collinear [04]
DF ⟂ AD [05]
B,E,H are collinear [06]
F,D,H are collinear [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. F,C,E are collinear [04] & AC ⟂ CE [03] ⇒  CA ⟂ FC [08]
002. BE ⟂ AB [02] & CA ⟂ FC [08] ⇒  ∠(BE-FC) = ∠BAC [09]
003. B,E,H are collinear [06] & F,C,E are collinear [04] & ∠(BE-FC) = ∠BAC [09] ⇒  ∠HBA = ∠FCA [10]
004. F,C,E are collinear [04] & DF ⟂ AD [05] & CE ⟂ AC [03] ⇒  ∠ACF = ∠ADF [11]
005. ∠ACF = ∠ADF [11] ⇒  F,D,C,A are concyclic [12]
006. F,D,C,A are concyclic [12] ⇒  ∠FDC = ∠FAC [13]
007. B,E,H are collinear [06] & F,D,H are collinear [07] & DF ⟂ AD [05] & BE ⟂ AB [02] ⇒  ∠HBA = ∠HDA [14]
008. ∠HBA = ∠HDA [14] ⇒  B,D,H,A are concyclic [15]
009. B,D,H,A are concyclic [15] ⇒  ∠BDH = ∠BAH [16]
010. ∠FDC = ∠FAC [13] & B,D,C are collinear [01] & ∠BDH = ∠BAH [16] & F,D,H are collinear [07] ⇒  ∠BAH = ∠CAF [17]
011. ∠HBA = ∠FCA [10] & ∠BAH = ∠CAF [17] (Similar Triangles)⇒  BA:CA = BH:CF [18]
012. BA:CA = BH:CF [18] & AC = AB [00] ⇒  BH = CF
==========================

 

 

137. examples/complete2/003/complete_015_7_Book_00EE_08_E059-56.gex

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

 

 번역 

 

삼각형 ABC가 주어져 있습니다. D는 B에서 AC로 내린 수선의 발이고, E는 A에서 BC로 내린 수선의 발입니다. F는 직선 BD와 AE의 교점입니다. G는 점 B, F, A를 지나는 원의 중심입니다. H는 직선 BC 위에 있으며, G를 중심으로 하고 A를 지나는 원 위에 있습니다. I는 직선 AC 위에 있으며, G를 중심으로 하고 A를 지나는 원 위에 있습니다. 선분 FC와 선분 FI의 길이가 같음을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G I : Points
C,A,D are collinear [00]
BD ⟂ AC [01]
B,E,C are collinear [02]
AE ⟂ BC [03]
B,D,F are collinear [04]
F,A,E are collinear [05]
GB = GF [06]
GF = GA [07]
GI = GA [08]
C,A,I are collinear [09]

 * Auxiliary Constructions:
H : Points
B,H,C are collinear [10]

 * Proof steps:
001. GB = GF [06] & GF = GA [07] & GI = GA [08] ⇒  B,A,I,F are concyclic [11]
002. B,A,I,F are concyclic [11] ⇒  ∠BFI = ∠BAI [12]
003. B,A,I,F are concyclic [11] ⇒  ∠BIA = ∠BFA [13]
004. C,A,D are collinear [00] & B,E,C are collinear [02] & AE ⟂ BC [03] & BD ⟂ AC [01] ⇒  ∠ADB = ∠AEB [14]
005. ∠ADB = ∠AEB [14] ⇒  B,A,E,D are concyclic [15]
006. B,A,E,D are concyclic [15] ⇒  ∠BAD = ∠BED [16]
007. C,A,D are collinear [00] & F,B,D are collinear [04] & C,B,E are collinear [02] & F,A,E are collinear [05] & AE ⟂ BC [03] & BD ⟂ AC [01] ⇒  ∠CDF = ∠CEF [17]
008. ∠CDF = ∠CEF [17] ⇒  C,E,D,F are concyclic [18]
009. C,E,D,F are concyclic [18] ⇒  ∠CED = ∠CFD [19]
010. F,B,D are collinear [04] & ∠BFI = ∠BAI [12] & C,A,I are collinear [09] & ∠BAD = ∠BED [16] & C,A,D are collinear [00] & B,E,C are collinear [02] & ∠CED = ∠CFD [19] ⇒  ∠CFD = ∠DFI [20]
011. C,A,I are collinear [09] & C,A,D are collinear [00] ⇒  D,C,I are collinear [21]
012. ∠CFD = ∠DFI [20] & D,C,I are collinear [21] ⇒  DC:DI = FC:FI [22]
013. C,A,D are collinear [00] & C,A,I are collinear [09] & BD ⟂ AC [01] ⇒  ∠CDB = ∠BDI [23]
014. B,H,C are collinear [10] & F,A,E are collinear [05] & BC ⟂ AE [03] ⇒  BH ⟂ FA [24]
015. BH ⟂ FA [24] & BD ⟂ AC [01] ⇒  ∠HBD = ∠FAC [25]
016. ∠BIA = ∠BFA [13] & C,A,I are collinear [09] & B,D,F are collinear [04] & F,A,E are collinear [05] & ∠HBD = ∠FAC [25] & B,H,C are collinear [10] ⇒  ∠CBD = ∠DBI [26]
017. ∠CDB = ∠BDI [23] & ∠CBD = ∠DBI [26] (Similar Triangles)⇒  DC = DI [27]
018. DC:DI = FC:FI [22] & DC = DI [27] ⇒  FC = FI
==========================

 

 

138. examples/complete2/003/complete_014_7_Book_00EE_07_E059-52.gex

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

 

 번역 : 추후 업데이트

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
AC = AB [00]
AD ⟂ AB [01]
AD = AB [02]
AB ⟂ EB [03]
AD ⟂ ED [04]
CF ⟂ AC [05]
G,C,F are collinear [06]
E,G,B are collinear [07]
E,H,D are collinear [08]
H,C,B are collinear [09]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. G,C,F are collinear [06] & CF ⟂ AC [05] ⇒  GC ⟂ CA [10]
002. E,G,B are collinear [07] & AB ⟂ BE [03] ⇒  AB ⟂ EG [11]
003. GC ⟂ CA [10] & AB ⟂ EG [11] ⇒  ∠CGE = ∠CAB [12]
004. G,C,F are collinear [06] & E,H,D are collinear [08] & ∠CGE = ∠CAB [12] & E,G,B are collinear [07] & AB ⟂ EB [03] & AD ⟂ AB [01] & AD ⟂ ED [04] ⇒  ∠GCA = ∠BEH [13]
005. G,E,B are collinear [07] & G,C,F are collinear [06] & ∠CGE = ∠CAB [12] ⇒  ∠GBA = ∠GCA [14]
006. ∠GBA = ∠GCA [14] ⇒  C,G,A,B are concyclic [15]
007. C,G,A,B are concyclic [15] ⇒  ∠CAG = ∠CBG [16]
008. H,C,B are collinear [09] & ∠CAG = ∠CBG [16] & E,G,B are collinear [07] ⇒  ∠GAC = ∠EBH [17]
009. ∠GCA = ∠BEH [13] & ∠GAC = ∠EBH [17] (Similar Triangles)⇒  CA:EB = CG:EH [18]
010. AB ⟂ EB [03] & AD ⟂ AB [01] & AD ⟂ ED [04] ⇒  ∠EBA = ∠ADE [19]
011. AD ⟂ ED [04] & AD ⟂ AB [01] ⇒  ∠EAB = ∠AED [20]
012. ∠EBA = ∠ADE [19] & ∠EAB = ∠AED [20] (Similar Triangles)⇒  EB = AD [21]
013. CA:EB = CG:EH [18] & AC = AB [00] & AD = AB [02] & EB = AD [21] ⇒  CG = EH
==========================

 

 

139. examples/complete2/004/complete_002_6_GDD_FULL_01-20_13.gex

a b c = triangle a b c; d = parallelogram a b c d; e = foot e b a c; f = foot f a b d; g = foot g d a c; h = foot h c b d ? para e f g h

 

 번역 

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G H : Points
AB ∥ CD [00]
A,C,E are collinear [01]
BE ⟂ AC [02]
B,D,F are collinear [03]
AF ⟂ BD [04]
A,G,C are collinear [05]
AC ⟂ GD [06]
B,D,H are collinear [07]
BD ⟂ HC [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. F,D,B are collinear [03] & A,C,E are collinear [01] & BE ⟂ AC [02] & AF ⟂ BD [04] ⇒  ∠BFA = ∠BEA [09]
002. ∠BFA = ∠BEA [09] ⇒  A,F,B,E are concyclic [10]
003. A,F,B,E are concyclic [10] ⇒  ∠AFE = ∠ABE [11]
004. B,D,H are collinear [07] & A,G,C are collinear [05] & BE ⟂ AC [02] & AF ⟂ BD [04] & BD ⟂ HC [08] & AC ⟂ GD [06] ⇒  ∠CHD = ∠CGD [12]
005. ∠CHD = ∠CGD [12] ⇒  G,C,D,H are concyclic [13]
006. G,C,D,H are concyclic [13] ⇒  ∠GDC = ∠GHC [14]
007. ∠AFE = ∠ABE [11] & AB ∥ CD [00] & ∠GDC = ∠GHC [14] & AC ⟂ GD [06] & BE ⟂ AC [02] & BD ⟂ HC [08] & AF ⟂ BD [04] ⇒  ∠GHC = ∠(FE-CH) [15]
008. ∠GHC = ∠(FE-CH) [15] ⇒  GH ∥ FE
==========================

 

 

140. examples/complete2/004/complete_006_Other_Auxiliary_E092-5.gex

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

 

 번역 

 

삼각형 ABC와 평행사변형 ABCD가 주어져 있습니다. E는 ∠DAB의 이등분선 위에 있고, AE와 DE는 수직합니다. F는 B에서 AE로 내린 수선의 발입니다. G는 C에서 BF로 내린 수선의 발입니다. H는 선분 DE와 CG의 교점입니다. 선분 EG와 선분 AB가 서로 평행임을 증명하시오.

 

풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
AD ∥ BC [00]
AB ∥ CD [01]
AE ⟂ DE [02]
∠DAE = ∠EAB [03]
F,E,A are collinear [04]
AE ⟂ FB [05]
B,F,G are collinear [06]
BF ⟂ GC [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. G,B,F are collinear [06] & F,E,A are collinear [04] & AE ⟂ DE [02] & AE ⟂ FB [05] & BF ⟂ GC [07] ⇒  ∠BGC = ∠AFB [08]
002. F,E,A are collinear [04] & ∠DAE = ∠EAB [03] & AD ∥ BC [00] & AB ∥ CD [01] & BF ⟂ GC [07] & AE ⟂ DE [02] & AE ⟂ FB [05] ⇒  ∠BCG = ∠FAB [09]
003. ∠BGC = ∠AFB [08] & ∠BCG = ∠FAB [09] (Similar Triangles)⇒  BG:BF = BC:BA [10]
004. CD ∥ AB [01] ⇒  ∠BDC = ∠DBA [11]
005. BC ∥ AD [00] & CD ∥ AB [01] ⇒  ∠BCD = ∠DAB [12]
006. ∠BDC = ∠DBA [11] & ∠BCD = ∠DAB [12] (Similar Triangles)⇒  DC = BA [13]
007. ∠BDC = ∠DBA [11] & ∠BCD = ∠DAB [12] (Similar Triangles)⇒  BC = DA [14]
008. F,E,A are collinear [04] & AE ⟂ DE [02] & AE ⟂ FB [05] ⇒  ∠BFA = ∠AED [15]
009. F,E,A are collinear [04] & ∠BAE = ∠EAD [03] ⇒  ∠BAF = ∠EAD [16]
010. ∠BFA = ∠AED [15] & ∠BAF = ∠EAD [16] (Similar Triangles)⇒  AB:AD = AF:AE [17]
011. BG:BF = BC:BA [10] & DC = BA [13] & AB:AD = AF:AE [17] & BC = DA [14] ⇒  FA:EA = BF:BG [18]
012. FA:EA = BF:BG [18] & B,F,G are collinear [06] & F,E,A are collinear [04] ⇒  BA ∥ GE
==========================

 

입력: 2024.08.07 13:24