jgex_ag_231 기하 문제 풀이 [161-180]
추천글 : 【AlphaGeometry】 jgex_ag_231 문제 재구성 및 풀이
161. examples/complete2/unsolved2/complete_010_Other_Auxiliary_ye_aux_think2.gex
c a b = iso_triangle c a b; d = on_line d a c; e = on_line e b c, eqdistance e b d a; f = on_line f a b, on_line f d e; g = on_pline g f a c, on_line g b c ? midp f d e
○ 번역
CA = CB인 이등변삼각형 CAB가 주어져 있습니다. D는 직선 AC 위에 있습니다. E는 직선 BC 위에 있고, EB = DA입니다. F는 직선 AB와 직선 DE의 교점입니다. G는 F를 지나고 AC에 평행한 직선 위에 있으며, 직선 BC 위에 있습니다. 점 F가 선분 DE의 중점임을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F : Points
∠ABC = ∠BCA [00]
D,A,B are collinear [01]
EC = DB [02]
C,A,E are collinear [03]
D,F,E are collinear [04]
C,F,B are collinear [05]
* Auxiliary Constructions:
I : Points
IF = BD [06]
IB = DF [07]
* Proof steps:
001. EC = DB [02] & IF = BD [06] ⇒ IF = EC [08]
002. IF = BD [06] & IB = DF [07] (SSS)⇒ ∠DBF = ∠IFB [09]
003. IF = BD [06] & IB = DF [07] (SSS)⇒ ∠DFB = ∠IBF [10]
004. C,F,B are collinear [05] & C,A,E are collinear [03] & ∠ABC = ∠BCA [00] & ∠DBF = ∠IFB [09] & D,A,B are collinear [01] ⇒ ∠IFC = ∠FCE [11]
005. IF = EC [08] & ∠IFC = ∠FCE [11] (SAS)⇒ CI = FE [12]
006. IF = EC [08] & ∠IFC = ∠FCE [11] (SAS)⇒ ∠ICF = ∠CFE [13]
007. ∠ICF = ∠CFE [13] & C,F,B are collinear [05] & D,F,E are collinear [04] & ∠DFB = ∠IBF [10] ⇒ ∠IBC = ∠BCI [14]
008. ∠IBC = ∠BCI [14] ⇒ IB = IC [15]
009. D,F,E are collinear [04] & CI = FE [12] & IB = IC [15] & IB = DF [07] ⇒ F is midpoint of DE
==========================
162. examples/complete2/unsolved2/complete_012_7_Book_00EE_02_E023-21.gex
a b = segment a b; c = on_tline c b a b; d = on_circle d a b; f = midpoint f c b; g = on_line g d f, on_circle g a b; h = intersection_lc h c a g; e = on_line e c d, on_circle e a b ? para b c h e
○ 번역 : 추후 업데이트
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F G H : Points
BC ⟂ AB [00]
AD = AB [01]
E,B,C are collinear [02]
EC = EB [03]
AF = AB [04]
E,D,F are collinear [05]
G,C,F are collinear [06]
AF = AG [07]
AH = AB [08]
C,D,H are collinear [09]
* Auxiliary Constructions:
: Points
* Proof steps:
001. AF = AB [04] & AD = AB [01] ⇒ A is the circumcenter of \Delta BFD [10]
002. E,B,C are collinear [02] & AB ⟂ BC [00] ⇒ AB ⟂ BE [11]
003. A is the circumcenter of \Delta BFD [10] & AB ⟂ BE [11] ⇒ ∠EBF = ∠BDF [12]
004. E,B,C are collinear [02] & ∠EBF = ∠BDF [12] & E,D,F are collinear [05] ⇒ ∠EBF = ∠BDE [13]
005. E,B,C are collinear [02] & E,D,F are collinear [05] ⇒ ∠BED = ∠BEF [14]
006. ∠EBF = ∠BDE [13] & ∠BED = ∠BEF [14] (Similar Triangles)⇒ EB:ED = EF:EB [15]
007. EB:ED = EF:EB [15] & EC = EB [03] ⇒ EC:ED = EF:EC [16]
008. E,B,C are collinear [02] & E,D,F are collinear [05] ⇒ ∠CEF = ∠CED [17]
009. EC:ED = EF:EC [16] & ∠CEF = ∠CED [17] (Similar Triangles)⇒ ∠ECF = ∠CDE [18]
010. AF = AB [04] & AH = AB [08] & AF = AG [07] & AD = AB [01] ⇒ G,D,H,F are concyclic [19]
011. G,D,H,F are concyclic [19] ⇒ ∠GHD = ∠GFD [20]
012. G,C,F are collinear [06] & E,B,C are collinear [02] & ∠ECF = ∠CDE [18] & ∠GHD = ∠GFD [20] & C,D,H are collinear [09] & E,D,F are collinear [05] ⇒ ∠HGC = ∠(EB-GC) [21]
013. ∠HGC = ∠(EB-GC) [21] ⇒ GH ∥ EB [22]
014. GH ∥ EB [22] & E,B,C are collinear [02] ⇒ GH ∥ BC
==========================
163. examples/complete2/unsolved2/complete_006_7_Book_LLL_yL252-6.gex
a c d = triangle a c d; b = on_pline b c d a, on_pline b a d c; e = on_line e a c; g = on_line g a b, on_pline g e a d; f = on_line f a d, on_pline f e c d; h = on_line h e g, on_line h c d; i = on_line i b c, on_line i e f ? para f g h i
○ 번역
삼각형 ACD가 주어져 있습니다. B는 C를 지나고 DA에 평행한 직선 위에 있고, A를 지나고 DC에 평행한 직선 위에 있습니다. E는 직선 AC 위에 있습니다. G는 직선 AB 위에 있고, E를 지나고 AD에 평행한 직선 위에 있습니다. F는 직선 AD 위에 있고, E를 지나고 CD에 평행한 직선 위에 있습니다. H는 직선 EG와 CD의 교점이고, I는 직선 BC와 EF의 교점입니다. 선분 FG와 선분 HI가 서로 평행임을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F G H I : Points
DB ∥ CA [00]
DA ∥ CB [01]
E,A,B are collinear [02]
F,A,D are collinear [03]
A,G,C are collinear [04]
C,H,B are collinear [05]
E,H,F are collinear [06]
I,D,B are collinear [07]
E,G,I are collinear [08]
* Auxiliary Constructions:
: Points
* Proof steps:
001. I,D,B are collinear [07] & C,G,A are collinear [04] & BD ∥ AC [00] ⇒ IB ∥ GA [09]
002. IB ∥ GA [09] & E,G,I are collinear [08] & E,A,B are collinear [02] ⇒ EI:GI = EB:AB [10]
003. H,C,B are collinear [05] & A,D,F are collinear [03] & AD ∥ BC [01] ⇒ HB ∥ FA [11]
004. HB ∥ FA [11] & E,H,F are collinear [06] & E,A,B are collinear [02] ⇒ EH:HF = EB:AB [12]
005. EI:GI = EB:AB [10] & EH:HF = EB:AB [12] ⇒ EH:HF = EI:IG [13]
006. EH:HF = EI:IG [13] & E,H,F are collinear [06] & E,G,I are collinear [08] ⇒ HI ∥ FG
==========================
164. examples/complete2/unsolved2/complete_015_7_Book_00EE_08_E059-59.gex
a b c = triangle a b c; d = angle_bisector d b a c; e = on_pline e c b d, on_pline e b c d; f = on_line f b e, on_line f a c; g = on_line g c e, on_line g a b ? cong b g c f
○ 번역
삼각형 ABC가 주어져 있습니다. D는 ∠BAC의 이등분선 위에 있습니다. E는 C를 지나고 BD에 평행한 직선 위에 있고, B를 지나고 CD에 평행한 직선 위에 있습니다. F는 직선 BE와 AC의 교점이며, G는 직선 CE와 AB의 교점입니다. 선분 BG와 선분 CF의 길이가 같음을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F G : Points
∠BAD = ∠DAC [00]
EC ∥ BD [01]
EB ∥ CD [02]
A,F,C are collinear [03]
F,B,E are collinear [04]
A,G,B are collinear [05]
G,C,E are collinear [06]
* Auxiliary Constructions:
H I : Points
A,H,D are collinear [07]
BH = BD [08]
F,I,C are collinear [09]
H,B,I are collinear [10]
* Proof steps:
001. A,H,D are collinear [07] & F,I,C are collinear [09] & A,F,C are collinear [03] & ∠BAD = ∠DAC [00] ⇒ ∠BAD = ∠HAI [11]
002. BH = BD [08] ⇒ ∠BDH = ∠DHB [12]
003. A,H,D are collinear [07] & H,B,I are collinear [10] & ∠BDH = ∠DHB [12] ⇒ ∠BDA = ∠AHI [13]
004. ∠BAD = ∠HAI [11] & ∠BDA = ∠AHI [13] (Similar Triangles)⇒ ∠ABD = ∠HIA [14]
005. ∠BAD = ∠HAI [11] & ∠BDA = ∠AHI [13] (Similar Triangles)⇒ AB:AD = AI:AH [15]
006. A,F,C are collinear [03] & A,G,B are collinear [05] & ∠ABD = ∠HIA [14] & H,B,I are collinear [10] & F,I,C are collinear [09] & BD ∥ CE [01] ⇒ ∠ECF = ∠GBH [16]
007. H,B,I are collinear [10] & F,I,C are collinear [09] & A,F,C are collinear [03] & A,G,B are collinear [05] & G,C,E are collinear [06] & ∠ABD = ∠HIA [14] & BD ∥ CE [01] ⇒ ∠BIA = ∠AGC [17]
008. F,I,C are collinear [09] & A,F,C are collinear [03] & A,G,B are collinear [05] ⇒ ∠BAI = ∠GAC [18]
009. ∠BIA = ∠AGC [17] & ∠BAI = ∠GAC [18] (Similar Triangles)⇒ AB:AC = AI:AG [19]
010. AB:AD = AI:AH [15] & AB:AC = AI:AG [19] ⇒ AD:AC = AH:AG [20]
011. A,G,B are collinear [05] & A,H,D are collinear [07] & ∠DAC = ∠BAD [00] ⇒ ∠DAC = ∠GAH [21]
012. AD:AC = AH:AG [20] & ∠DAC = ∠GAH [21] (Similar Triangles)⇒ ∠DCA = ∠AGH [22]
013. F,B,E are collinear [04] & A,F,C are collinear [03] & A,G,B are collinear [05] & ∠DCA = ∠AGH [22] & CD ∥ BE [02] ⇒ ∠EFC = ∠BGH [23]
014. ∠ECF = ∠GBH [16] & ∠EFC = ∠BGH [23] (Similar Triangles)⇒ CE:BH = CF:BG [24]
015. CE ∥ BD [01] & BE ∥ CD [02] ⇒ ∠CEB = ∠BDC [25]
016. BE ∥ CD [02] ⇒ ∠CBE = ∠BCD [26]
017. ∠CEB = ∠BDC [25] & ∠CBE = ∠BCD [26] (Similar Triangles)⇒ CE = BD [27]
018. CE:BH = CF:BG [24] & BH = BD [08] & CE = BD [27] ⇒ CF = BG
==========================
165. examples/complete2/unsolved2/complete_013_7_Book_00EE_10_E072-16.gex
a b c = triangle a b c; d = parallelogram a b c d; e = on_line e c d; f = on_line f a d, eqdistance f c a e; g = on_line g a e, on_line g c f ? eqangle g a g b g b g c
○ 번역
삼각형 ABC와 평행사변형 ABCD가 주어져 있습니다. E는 직선 CD 위에 있고, F는 직선 AD 위에 있으며, FC = AE입니다. G는 직선 AE와 CF의 교점입니다. ∠AGB = ∠BGC임을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F G : Points
AB ∥ CD [00]
AD ∥ BC [01]
E,D,C are collinear [02]
D,A,F are collinear [03]
FC = AE [04]
E,G,A are collinear [05]
G,C,F are collinear [06]
* Auxiliary Constructions:
H : Points
A,H,B are collinear [07]
C,H,F are collinear [08]
* Proof steps:
001. E,D,C are collinear [02] & A,H,B are collinear [07] & AB ∥ CD [00] ⇒ EC ∥ AH [09]
002. G,C,F are collinear [06] & C,H,F are collinear [08] ⇒ C,H,G are collinear [10]
003. EC ∥ AH [09] & E,G,A are collinear [05] & G,C,H are collinear [10] ⇒ GA:GH = EA:CH [11]
004. D,A,F are collinear [03] & AD ∥ BC [01] ⇒ CB ∥ FA [12]
005. CB ∥ FA [12] & C,H,F are collinear [08] & A,H,B are collinear [07] ⇒ CH:CF = BH:BA [13]
006. GA:GH = EA:CH [11] & CH:CF = BH:BA [13] & FC = AE [04] ⇒ BA:BH = GA:GH [14]
007. BA:BH = GA:GH [14] & A,H,B are collinear [07] ⇒ ∠AGB = ∠BGH [15]
008. E,G,A are collinear [05] & G,C,F are collinear [06] & ∠AGB = ∠BGH [15] & C,H,F are collinear [08] & C,H,G are collinear [10] ⇒ ∠AGB = ∠BGC
==========================
166. examples/complete2/unsolved2/complete_003_6_GDD_FULL_more_E023-19.gex
c a b = r_triangle c a b; d = foot d c a b; e = on_line e c d, angle_bisector e b a c; f = on_line f a b, angle_bisector f d c b; g = on_line g b c, on_line g a e ? para e f c b
○ 번역
∠C가 직각인 직각삼각형 CAB가 주어져 있습니다. D는 C에서 AB로 내린 수선의 발입니다. E는 직선 CD 위에 있으며, ∠BAC의 이등분선 위에 있습니다. F는 직선 AB 위에 있으며, ∠DCB의 이등분선 위에 있습니다. G는 직선 BC와 AE의 교점입니다. 선분 EF와 CB가 서로 평행임을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F : Points
AB ⟂ AC [00]
C,B,D are collinear [01]
AD ⟂ BC [02]
A,E,D are collinear [03]
∠EBC = ∠ABE [04]
∠DAF = ∠FAC [05]
C,F,B are collinear [06]
* Auxiliary Constructions:
: Points
* Proof steps:
001. C,F,B are collinear [06] & C,B,D are collinear [01] ⇒ F,C,D are collinear [07]
002. ∠DAF = ∠FAC [05] & F,C,D are collinear [07] ⇒ FD:CF = AD:CA [08]
003. C,B,D are collinear [01] & AD ⟂ BC [02] ⇒ ∠CDA = ∠ADB [09]
004. A,E,D are collinear [03] & C,B,F are collinear [06] & AD ⟂ BC [02] ⇒ AE ⟂ CF [10]
005. AE ⟂ CF [10] & AB ⟂ AC [00] ⇒ ∠EAC = ∠(CF-BA) [11]
006. C,B,D are collinear [01] & ∠EAC = ∠(CF-BA) [11] & A,E,D are collinear [03] & C,F,B are collinear [06] ⇒ ∠CAD = ∠ABD [12]
007. ∠CDA = ∠ADB [09] & ∠CAD = ∠ABD [12] (Similar Triangles)⇒ AD:CA = BD:BA [13]
008. C,B,D are collinear [01] & ∠ABE = ∠EBC [04] ⇒ ∠ABE = ∠EBD [14]
009. ∠ABE = ∠EBD [14] & A,E,D are collinear [03] ⇒ ED:AE = BD:BA [15]
010. FD:CF = AD:CA [08] & AD:CA = BD:BA [13] & ED:AE = BD:BA [15] ⇒ DE:EA = DF:FC [16]
011. DE:EA = DF:FC [16] & A,E,D are collinear [03] & F,C,D are collinear [07] ⇒ EF ∥ AC
==========================
167. examples/complete2/unsolved2/complete_010_Other_Auxiliary_ye_aux_ll43.gex
a b = segment a b; c = on_dia c a b, on_bline c a b; d = midpoint d a c; e = foot e c b d; f = on_line f c e, on_line f a b ? eqangle d c d b d f d a
○ 번역
선분 가 주어져 있습니다. AC와 AB는 수직하고, C는 선분 AB의 수직이등분선 위에 있습니다. D는 선분 A의 중점이고, E는 C에서 BD로 내린 수선의 발입니다. F는 직선 C와 AB의 교점입니다. ∠CDB = ∠FDA임을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F : Points
CA = CB [00]
AC ⟂ BC [01]
∠CAB = ∠ABC [02]
D,C,A are collinear [03]
DA = DC [04]
∠(AC-BD) = ∠(AC-BD) [05]
E,D,B are collinear [06]
CE ⟂ BD [07]
F,B,A are collinear [08]
E,F,C are collinear [09]
* Auxiliary Constructions:
G : Points
G,B,A are collinear [10]
GB = GA [11]
* Proof steps:
001. CA = CB [00] & GB = GA [11] ⇒ AB ⟂ CG [12]
002. CA = CB [00] & GB = GA [11] ⇒ GB:GA = CB:CA [13]
003. E,D,B are collinear [06] & G,B,A are collinear [10] & AB ⟂ CG [12] & CE ⟂ BD [07] ⇒ ∠CEB = ∠CGB [14]
004. ∠CEB = ∠CGB [14] ⇒ E,G,B,C are concyclic [15]
005. E,G,B,C are concyclic [15] ⇒ ∠EGB = ∠ECB [16]
006. G,B,A are collinear [10] & F,B,A are collinear [08] & F,E,C are collinear [09] & ∠EGB = ∠ECB [16] ⇒ ∠FGE = ∠BCF [17]
007. E,F,C are collinear [09] & F,B,A are collinear [08] & ∠EGB = ∠ECB [16] & G,B,A are collinear [10] ⇒ ∠FEG = ∠CBF [18]
008. ∠FGE = ∠BCF [17] & ∠FEG = ∠CBF [18] (Similar Triangles)⇒ EF:FB = EG:BC [19]
009. E,D,B are collinear [06] & CE ⟂ BD [07] ⇒ ∠CED = ∠BEC [20]
010. D,A,C are collinear [03] & BC ⟂ AC [01] ⇒ BC ⟂ DC [21]
011. E,D,B are collinear [06] & E,F,C are collinear [09] & BD ⟂ CE [07] ⇒ ED ⟂ EF [22]
012. BC ⟂ DC [21] & ED ⟂ EF [22] ⇒ ∠(BC-EF) = ∠CDE [23]
013. BC ⟂ DC [21] & ED ⟂ EF [22] ⇒ ∠(BC-ED) = ∠(DC-EF) [24]
014. D,A,C are collinear [03] & E,D,B are collinear [06] & ∠(BC-EF) = ∠CDE [23] & E,F,C are collinear [09] ⇒ ∠CDE = ∠BCE [25]
015. ∠CED = ∠BEC [20] & ∠CDE = ∠BCE [25] (Similar Triangles)⇒ DC:CB = DE:CE [26]
016. ∠CED = ∠BEC [20] & ∠CDE = ∠BCE [25] (Similar Triangles)⇒ DC:DE = CB:CE [27]
017. DC:BC = ED:EC [26] & DA = DC [04] & CA = BC [00] ⇒ AD:AC = ED:EC [28]
018. AD:AC = ED:EC [28] & D,C,A are collinear [03] ⇒ ∠DEA = ∠AEC [29]
019. GB:GA = CB:CA [13] & G,B,A are collinear [10] ⇒ ∠BCG = ∠GCA [30]
020. D,C,A are collinear [03] & DA = DC [04] ⇒ D is midpoint of AC [31]
021. G,B,A are collinear [10] & GB = GA [11] ⇒ G is midpoint of AB [32]
022. D is midpoint of AC [31] & G is midpoint of AB [32] ⇒ DG ∥ CB [33]
023. D,A,C are collinear [03] & ∠BCG = ∠GCA [30] & BC ∥ DG [33] ⇒ ∠DGC = ∠GCD [34]
024. ∠DGC = ∠GCD [34] ⇒ DC = DG [35]
025. DC:DE = CB:CE [27] & DC = DG [35] & CA = BC [00] ⇒ DE:DG = CE:CA [36]
026. E,D,B are collinear [06] & ∠(BC-ED) = ∠(DC-EF) [24] & D,C,A are collinear [03] & E,F,C are collinear [09] & BC ∥ DG [33] ⇒ ∠EDG = ∠ECA [37]
027. DE:DG = CE:CA [36] & ∠EDG = ∠ECA [37] (Similar Triangles)⇒ ∠DEG = ∠CEA [38]
028. E,D,B are collinear [06] & ∠DEA = ∠AEC [29] & ∠DEG = ∠CEA [38] ⇒ ∠DEG = ∠AEB [39]
029. D,A,C are collinear [03] & E,D,B are collinear [06] & CE ⟂ BD [07] & AC ⟂ BC [01] ⇒ ∠DCB = ∠CED [40]
030. D,A,C are collinear [03] & E,D,B are collinear [06] & ∠(AC-BD) = ∠(AC-BD) [05] ⇒ ∠CDE = ∠CDB [41]
031. ∠DCB = ∠CED [40] & ∠CDE = ∠CDB [41] (Similar Triangles)⇒ DC:DE = DB:DC [42]
032. DC:DE = DB:DC [42] & DC = DG [35] ⇒ DG:DB = DE:DG [43]
033. E,D,B are collinear [06] & BC ∥ DG [33] ⇒ ∠GDB = ∠GDE [44]
034. DG:DB = DE:DG [43] & ∠GDB = ∠GDE [44] (Similar Triangles)⇒ ∠DGB = ∠GED [45]
035. E,D,B are collinear [06] & ∠DGB = ∠GED [45] & G,B,A are collinear [10] ⇒ ∠DGE = ∠ABE [46]
036. ∠DEG = ∠AEB [39] & ∠DGE = ∠ABE [46] (Similar Triangles)⇒ EG:DG = EB:BA [47]
037. E,F,C are collinear [09] & E,D,B are collinear [06] & ∠DEA = ∠AEC [29] ⇒ ∠FEA = ∠AEB [48]
038. ∠FEA = ∠AEB [48] & F,B,A are collinear [08] ⇒ EF:FA = EB:BA [49]
039. EG:DG = EB:BA [47] & EF:FA = EB:BA [49] & DC = DG [35] ⇒ EF:FA = EG:DC [50]
040. EF:FB = EG:BC [19] & EF:FA = EG:DC [50] ⇒ FB:BC = FA:DC [51]
041. FB:BC = FA:DC [51] & DC = DG [35] & DA = DC [04] ⇒ BF:BC = AF:AD [52]
042. F,B,A are collinear [08] & D,C,A are collinear [03] & ∠ABC = ∠CAB [02] ⇒ ∠FBC = ∠DAF [53]
043. BF:BC = AF:AD [52] & ∠FBC = ∠DAF [53] (Similar Triangles)⇒ ∠FCB = ∠ADF [54]
044. D,A,C are collinear [03] & ∠FCB = ∠ADF [54] & E,F,C are collinear [09] & ∠(BC-EF) = ∠CDE [23] & E,D,B are collinear [06] ⇒ ∠CDB = ∠FDA
==========================
168. examples/complete2/unsolved2/complete_010_Other_Auxiliary_aux2_22.gex
c a b = iso_triangle c a b; d = on_line d a c; e = on_line e b c, eqdistance e b a d; f = on_line f a b, on_line f d e ? cong d f e f
○ 번역
CA = CB인 이등변삼각형 CAB가 주어져 있습니다. D는 직선 AC 위에 있습니다. E는 직선 BC 위에 있고, EB = AD입니다. F는 직선 AB와 직선 DE의 교점입니다. 선분 DF와 선분 EF의 길이가 같음을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F : Points
∠CBA = ∠ACB [00]
B,D,A are collinear [01]
EC = BD [02]
C,E,A are collinear [03]
C,B,F are collinear [04]
F,E,D are collinear [05]
* Auxiliary Constructions:
G : Points
GC = BD [06]
GC ∥ BD [07]
* Proof steps:
001. GC = BD [06] & EC = BD [02] ⇒ CE = CG [08]
002. C,E,A are collinear [03] & C,B,F are collinear [04] & ∠ACB = ∠CBA [00] & GC ∥ BD [07] & B,D,A are collinear [01] ⇒ ∠ECF = ∠FCG [09]
003. CE = CG [08] & ∠ECF = ∠FCG [09] (SAS)⇒ FE = FG [10]
004. CE = CG [08] & ∠ECF = ∠FCG [09] (SAS)⇒ ∠EFC = ∠CFG [11]
005. B,A,D are collinear [01] & GC ∥ BD [07] ⇒ ∠BDC = ∠GCD [12]
006. GC = BD [06] & ∠BDC = ∠GCD [12] (SAS)⇒ ∠DBC = ∠CGD [13]
007. E,F,D are collinear [05] & ∠EFC = ∠CFG [11] & C,B,F are collinear [04] & ∠DBC = ∠CGD [13] & B,D,A are collinear [01] & GC ∥ BD [07] ⇒ ∠FDG = ∠DGF [14]
008. ∠FDG = ∠DGF [14] ⇒ FD = FG [15]
009. FE = FG [10] & FD = FG [15] ⇒ DF = EF
==========================
169. examples/complete2/unsolved2/complete_014_7_Book_00EE_09_E066-04.gex
a b = segment a b; c = lc_tangent c b a; d = midpoint d b c; e = on_circle e a b; f = on_line f d e, on_circle f a b ? eqangle e c c d d f f c
○ 번역 : 추후 업데이트
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F : Points
BC ⟂ AB [00]
C,D,B are collinear [01]
DB = DC [02]
AE = AB [03]
D,E,F are collinear [04]
AF = AB [05]
* Auxiliary Constructions:
: Points
* Proof steps:
001. AE = AB [03] & AF = AB [05] ⇒ A is the circumcenter of \Delta BEF [06]
002. A is the circumcenter of \Delta BEF [06] & BC ⟂ AB [00] ⇒ ∠CBE = ∠BFE [07]
003. D,E,F are collinear [04] & C,D,B are collinear [01] & ∠CBE = ∠BFE [07] ⇒ ∠BFD = ∠DBE [08]
004. C,D,B are collinear [01] & D,E,F are collinear [04] ⇒ ∠BDF = ∠BDE [09]
005. ∠BFD = ∠DBE [08] & ∠BDF = ∠BDE [09] (Similar Triangles)⇒ DB:DF = DE:DB [10]
006. DB:DF = DE:DB [10] & DB = DC [02] ⇒ CD:DF = DE:CD [11]
007. D,E,F are collinear [04] & C,D,B are collinear [01] ⇒ ∠FDC = ∠EDC [12]
008. CD:DF = DE:CD [11] & ∠FDC = ∠EDC [12] (Similar Triangles)⇒ ∠DFC = ∠ECD
==========================
170. examples/complete2/unsolved2/complete_014_7_Book_00EE_08_E061-66.gex
a b = segment a b; c = s_angle b a c 60; d = foot d a b c; e = foot e b a c; g = circumcenter g b c a; f = on_line f a d, on_line f b e ? cong a f a g
○ 번역
선분 AB가 주어져 있으며, ∠BAC = 60°입니다. 점 D는 A에서 BC 위로 내린 수선의 발이며, 점 E는 B에서 AC 위로 내린 수선의 발입니다. 점 G는 삼각형 BCA의 외심이고, 점 F는 선분 AD와 BE의 교점입니다. 이때 AF = AG임을 증명하여라.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F G : Points
∠CAB = 1_PI/3 [00]
∠BAC = 2_PI/3 [01]
AD ⟂ BC [02]
C,B,D are collinear [03]
C,A,E are collinear [04]
BE ⟂ AC [05]
FC = FA [06]
FB = FC [07]
A,G,D are collinear [08]
E,B,G are collinear [09]
* Auxiliary Constructions:
: Points
* Proof steps:
001. FC = FA [06] & FB = FC [07] ⇒ FB = FA [10]
002. FB = FA [10] ⇒ ∠FBA = ∠BAF [11]
003. FB = FC [07] ⇒ ∠FBC = ∠BCF [12]
004. FC = FA [06] ⇒ ∠FAC = ∠ACF [13]
005. ∠CAB = 1_PI/3 [00] & AD ⟂ BC [02] & ∠FBA = ∠BAF [11] & ∠FBC = ∠BCF [12] & ∠FAC = ∠ACF [13] (Angle chase)⇒ ∠(AD-BF) = 1_PI/3 [14]
006. ∠CAB = 1_PI/3 [00] & AD ⟂ BC [02] & ∠FBA = ∠BAF [11] & ∠FBC = ∠BCF [12] & ∠FAC = ∠ACF [13] (Angle chase)⇒ ∠(AD-CF) = 2_PI/3 [15]
007. C,B,D are collinear [03] & C,A,E are collinear [04] & BE ⟂ AC [05] & AD ⟂ BC [02] ⇒ ∠BDA = ∠BEA [16]
008. ∠BDA = ∠BEA [16] ⇒ A,B,E,D are concyclic [17]
009. A,B,E,D are concyclic [17] ⇒ ∠ABD = ∠AED [18]
010. A,B,E,D are concyclic [17] ⇒ ∠DAB = ∠DEB [19]
011. ∠ABD = ∠AED [18] & C,B,D are collinear [03] & C,A,E are collinear [04] ⇒ ∠ABC = ∠(AC-DE) [20]
012. A,D,G are collinear [08] & ∠(AD-BF) = 1_PI/3 [14] & ∠CAB = 1_PI/3 [00] & ∠ABD = ∠AED [18] & C,B,D are collinear [03] & C,A,E are collinear [04] ⇒ ∠(ED-CB) = ∠(AG-BF) [21]
013. C,B,D are collinear [03] & A,G,D are collinear [08] & C,A,E are collinear [04] & B,E,G are collinear [09] & BE ⟂ AC [05] & AD ⟂ BC [02] ⇒ ∠CDG = ∠CEG [22]
014. ∠CDG = ∠CEG [22] ⇒ C,E,G,D are concyclic [23]
015. C,E,G,D are concyclic [23] ⇒ ∠CGE = ∠CDE [24]
016. ∠CGE = ∠CDE [24] & E,B,G are collinear [09] & C,B,D are collinear [03] ⇒ ∠GCB = ∠BED [25]
017. ∠GCB = ∠BED [25] & ∠ABC = ∠(AC-DE) [20] ⇒ ∠(BE-CG) = ∠CAB [26]
018. ∠CAB = 1_PI/3 [00] & ∠FBA = ∠BAF [11] & ∠FAC = ∠ACF [13] (Angle chase)⇒ ∠BFC = 1_PI/3 [27]
019. E,B,G are collinear [09] & ∠(BE-CG) = ∠CAB [26] & ∠CAB = 1_PI/3 [00] & ∠BFC = 1_PI/3 [27] ⇒ ∠BFC = ∠BGC [28]
020. ∠BFC = ∠BGC [28] ⇒ C,B,G,F are concyclic [29]
021. C,B,G,F are concyclic [29] ⇒ ∠BCG = ∠BFG [30]
022. C,B,G,F are concyclic [29] ⇒ ∠CBG = ∠CFG [31]
023. ∠(ED-CB) = ∠(AG-BF) [21] & ∠BCG = ∠BFG [30] ⇒ ∠(ED-CG) = ∠AGF [32]
024. A,D,G are collinear [08] & ∠ABD = ∠AED [18] & C,B,D are collinear [03] & C,A,E are collinear [04] & ∠BAC = 2_PI/3 [01] & ∠(AD-CF) = 2_PI/3 [15] ⇒ ∠(AG-CF) = ∠(CB-ED) [33]
025. A,D,G are collinear [08] & ∠BCG = ∠DEB [25] & ∠DAB = ∠DEB [19] ⇒ ∠GAB = ∠BCG [34]
026. ∠(AG-CF) = ∠(CB-ED) [33] & ∠GAB = ∠BCG [34] ⇒ ∠(CF-DE) = ∠(AB-CG) [35]
027. ∠CAB = 1_PI/3 [00] & BE ⟂ AC [05] (Angle chase)⇒ ∠EBA = 5_PI/6 [36]
028. ∠CAB = 1_PI/3 [00] & ∠FBA = ∠BAF [11] & ∠FBC = ∠BCF [12] & ∠FAC = ∠ACF [13] (Angle chase)⇒ ∠CBF = 5_PI/6 [37]
029. ∠EBA = 5_PI/6 [36] & ∠CBF = 5_PI/6 [37] ⇒ ∠CBF = ∠EBA [38]
030. ∠FBA = ∠BAF [11] & ∠CBF = ∠EBA [38] ⇒ ∠BAF = ∠CBE [39]
031. ∠BAF = ∠CBE [39] & ∠CBG = ∠CFG [31] & E,B,G are collinear [09] ⇒ ∠CFG = ∠BAF [40]
032. ∠(CF-DE) = ∠(AB-CG) [35] & ∠CFG = ∠BAF [40] ⇒ ∠(DE-CG) = ∠GFA [41]
033. A,D,G are collinear [08] & ∠(ED-CG) = ∠AGF [32] & ∠(DE-CG) = ∠GFA [41] ⇒ ∠GFA = ∠AGF [42]
034. ∠GFA = ∠AGF [42] ⇒ AF = AG
==========================
171. examples/complete2/unsolved2/complete_011_7_Book_00EE_03_E037-24.gex
a b c = triangle a b c; d = circle d b a c; e = lc_tangent e a d, on_line e b c; f = angle_bisector f b e a, on_line f a b; g = on_line g a c, on_line g e f; h = angle_bisector h b a c, on_line h b c ? perp f e a h
○ 번역 : 추후 업데이트
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F H : Points
DB = DA [00]
DA = DC [01]
E,C,B are collinear [02]
AE ⟂ AD [03]
∠BEF = ∠FEA [04]
A,F,B are collinear [05]
H,C,B are collinear [06]
∠BAH = ∠HAC [07]
* Auxiliary Constructions:
: Points
* Proof steps:
001. H,C,B are collinear [06] & E,C,B are collinear [02] & ∠BEF = ∠FEA [04] ⇒ ∠FEA = ∠HEF [08]
002. DB = DA [00] & DA = DC [01] ⇒ D is the circumcenter of \Delta ABC [09]
003. D is the circumcenter of \Delta ABC [09] & AE ⟂ AD [03] ⇒ ∠BAE = ∠BCA [10]
004. ∠AEF = ∠FEB [04] & A,F,B are collinear [05] ⇒ FB:AF = EB:AE [11]
005. B,C,E are collinear [02] & ∠ACB = ∠EAB [10] ⇒ ∠ACE = ∠EAB [12]
006. B,C,E are collinear [02] ⇒ ∠AEC = ∠AEB [13]
007. ∠ACE = ∠EAB [12] & ∠AEC = ∠AEB [13] (Similar Triangles)⇒ AB:AC = EB:AE [14]
008. ∠BAH = ∠HAC [07] & H,C,B are collinear [06] ⇒ HB:HC = AB:AC [15]
009. FB:AF = EB:AE [11] & AB:AC = EB:AE [14] & HB:HC = AB:AC [15] ⇒ BH:HC = BF:FA [16]
010. BH:HC = BF:FA [16] & H,C,B are collinear [06] & A,F,B are collinear [05] ⇒ HF ∥ CA [17]
011. A,F,B are collinear [05] & H,C,B are collinear [06] & E,C,B are collinear [02] & ∠BAE = ∠BCA [10] & AC ∥ FH [17] ⇒ ∠FAE = ∠EHF [18]
012. ∠FEA = ∠HEF [08] & ∠FAE = ∠EHF [18] (Similar Triangles)⇒ EA = EH [19]
013. A,F,B are collinear [05] & ∠BAH = ∠HAC [07] & AC ∥ FH [17] ⇒ ∠FAH = ∠AHF [20]
014. ∠FAH = ∠AHF [20] ⇒ FA = FH [21]
015. EA = EH [19] & FA = FH [21] ⇒ AH ⟂ EF
==========================
172. examples/complete2/unsolved2/complete_014_7_Book_00EE_08_E061-65.gex
a b c d = isquare a b c d; e = s_angle c d e 15, s_angle d c e -15; f = reflect f e a c ? contri e a b a b e
○ 번역 : 추후 업데이트
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E : Points
AB = BC [00]
AB ⟂ BC [01]
AB ∥ CD [02]
AD ∥ BC [03]
∠EDC = 1_PI/12 [04]
∠ECD = 1_1PI/12 [05]
* Auxiliary Constructions:
F : Points
CE = CF [06]
AE = AF [07]
* Proof steps:
001. ∠EDC = 1_PI/12 [04] & AB ∥ CD [02] ⇒ ∠(DE-AB) = 1_PI/12 [08]
002. ∠ECD = 1_1PI/12 [05] & AB ∥ CD [02] ⇒ ∠(CE-AB) = 1_1PI/12 [09]
003. ∠EDC = 1_PI/12 [04] & AB ∥ CD [02] & ∠(CE-AB) = 1_1PI/12 [09] ⇒ ∠ECD = ∠CDE [10]
004. ∠ECD = ∠CDE [10] ⇒ EC = ED [11]
005. EC = ED [11] & CE = CF [06] ⇒ FC = ED [12]
006. BC ∥ AD [03] & AB ∥ CD [02] ⇒ ∠BAD = ∠DCB [13]
007. BC ∥ AD [03] & AB ∥ CD [02] ⇒ ∠ADC = ∠DAB [14]
008. BC ∥ AD [03] & AB ∥ CD [02] ⇒ ∠ABC = ∠CDA [15]
009. AD ∥ BC [03] ⇒ ∠BDA = ∠DBC [16]
010. AD ∥ BC [03] ⇒ ∠ACB = ∠CAD [17]
011. ∠BAD = ∠DCB [13] & ∠BDA = ∠DBC [16] (Similar Triangles)⇒ BA = DC [18]
012. ∠BAD = ∠DCB [13] & ∠BDA = ∠DBC [16] (Similar Triangles)⇒ DA = BC [19]
013. AB = BC [00] & BA = DC [18] ⇒ CD = CB [20]
014. AB ⟂ BC [01] & BC ∥ AD [03] ⇒ AD ⟂ AB [21]
015. AB ⟂ BC [01] & ∠(CE-AB) = 1_1PI/12 [09] (Angle chase)⇒ ∠BCE = 7_PI/12 [22]
016. AB ⟂ BC [01] & ∠(DE-AB) = 1_PI/12 [08] (Angle chase)⇒ ∠(DE-BC) = 7_PI/12 [23]
017. ∠BCE = 7_PI/12 [22] & ∠(DE-BC) = 7_PI/12 [23] & BC ∥ AD [03] ⇒ ∠EDA = ∠BCE [24]
018. EC = ED [11] & DA = BC [19] & ∠EDA = ∠BCE [24] (SAS)⇒ AE = BE [25]
019. AE = BE [25] & AE = AF [07] ⇒ AF = BE [26]
020. AB ⟂ BC [01] & BC ∥ AD [03] & AB ∥ CD [02] ⇒ ∠BAD = ∠BCD [27]
021. ∠BAD = ∠BCD [27] ⇒ A,D,C,B are concyclic [28]
022. A,D,C,B are concyclic [28] & ∠ADC = ∠DAB [14] ⇒ AC = DB [29]
023. AF = BE [26] & FC = ED [12] & AC = DB [29] (SSS)⇒ ∠(AC-BD) = ∠(CF-DE) [30]
024. AF = BE [26] & FC = ED [12] & AC = DB [29] (SSS)⇒ ∠(AF-BE) = ∠(AC-BD) [31]
025. ∠ABC = ∠CDA [15] & ∠ACB = ∠CAD [17] (Similar Triangles)⇒ BA:BC = DC:DA [32]
026. BA:BC = DC:DA [32] & AB = BC [00] ⇒ DC = DA [33]
027. DC = DA [33] & AB = BC [00] ⇒ AC ⟂ DB [34]
028. AE = AF [07] & CE = CF [06] ⇒ EF ⟂ AC [35]
029. ∠(AC-BD) = ∠(CF-DE) [30] & AC ⟂ DB [34] & EF ⟂ AC [35] ⇒ FC ⟂ ED [36]
030. AD ⟂ AB [21] & FC ⟂ ED [36] ⇒ ∠(AB-DE) = ∠(AD-CF) [37]
031. ∠(AB-DE) = ∠(AD-CF) [37] & AD ∥ BC [03] & AB ∥ CD [02] ⇒ ∠FCB = ∠EDC [38]
032. FC = ED [12] & CD = CB [20] & ∠FCB = ∠EDC [38] (SAS)⇒ BF = CE [39]
033. FC = ED [12] & CD = CB [20] & ∠FCB = ∠EDC [38] (SAS)⇒ ∠BFC = ∠CED [40]
034. CE = CF [06] ⇒ ∠CFE = ∠FEC [41]
035. AE = BE [25] & EC = ED [11] & AC = DB [29] (SSS)⇒ ∠(AC-DE) = ∠(CE-BD) [42]
036. AB = BC [00] ⇒ ∠BAC = ∠ACB [43]
037. AB ⟂ BC [01] & ∠(DE-AB) = 1_PI/12 [08] & ∠BAC = ∠ACB [43] (Angle chase)⇒ ∠(DE-AC) = 1_PI/3 [44]
038. AB ⟂ BC [01] & ∠(CE-AB) = 1_1PI/12 [09] & ∠BAC = ∠ACB [43] & ∠CFE = ∠FEC [41] & EF ⟂ AC [35] (Angle chase)⇒ ∠ECF = 1_PI/3 [45]
039. ∠CFE = ∠FEC [41] & ∠(AC-DE) = ∠(CE-BD) [42] & AC ⟂ DB [34] & EF ⟂ AC [35] & ∠(DE-AC) = 1_PI/3 [44] & ∠ECF = 1_PI/3 [45] ⇒ ∠ECF = ∠CFE [46]
040. ∠ECF = ∠CFE [46] ⇒ EC = EF [47]
041. BF = CE [39] & EC = EF [47] ⇒ FE = FB [48]
042. DE = CF [12] & DC = CB [20] ⇒ DE:DC = CF:CB [49]
043. DE:DC = CF:CB [49] & ∠FCB = ∠EDC [38] (Similar Triangles)⇒ ED:EC = FC:FB [50]
044. ED:EC = FC:FB [50] & EC = ED [11] ⇒ FC = FB [51]
045. ∠(DE-AB) = 1_PI/12 [08] & ∠(CE-AB) = 1_1PI/12 [09] (Angle chase)⇒ ∠CED = 5_PI/6 [52]
046. AB ⟂ BC [01] & ∠(DE-AB) = 1_PI/12 [08] & ∠BAC = ∠ACB [43] & EF ⟂ AC [35] (Angle chase)⇒ ∠FED = 1_PI/6 [53]
047. ∠(AF-BE) = ∠(AC-BD) [31] & AC ⟂ DB [34] & EF ⟂ AC [35] ⇒ AF ⟂ EB [54]
048. AF ⟂ EB [54] & AD ⟂ AB [21] ⇒ ∠FAB = ∠(BE-AD) [55]
049. ∠FAB = ∠(BE-AD) [55] & AD ∥ BC [03] ⇒ ∠FAB = ∠EBC [56]
050. AB = BC [00] & AF = BE [26] & ∠FAB = ∠EBC [56] (SAS)⇒ ∠ABC = ∠(BF-CE) [57]
051. AD ⟂ AB [21] & EF ⟂ AC [35] ⇒ ∠BAD = ∠(EF-AC) [58]
052. ∠ABC = ∠(BF-CE) [57] & ∠BAD = ∠(EF-AC) [58] & AD ∥ BC [03] & AC ⟂ DB [34] & EF ⟂ AC [35] ⇒ ∠(DB-AC) = ∠(FB-EC) [59]
053. ∠(DB-AC) = ∠(FB-EC) [59] & ∠(ED-AC) = ∠(DB-EC) [42] ⇒ ∠EDB = ∠DBF [60]
054. ∠BFC = ∠CED [40] & ∠CED = 5_PI/6 [52] & ∠FED = 1_PI/6 [53] & AC ⟂ DB [34] & EF ⟂ AC [35] & ∠EDB = ∠DBF [60] ⇒ ∠EFB = ∠BFC [61]
055. FE = FB [48] & FC = FB [51] & ∠EFB = ∠BFC [61] (SAS)⇒ BE = CB [62]
056. AB = BC [00] & BE = CB [62] & AE = BE [25] ⇒ EA = AB [63]
057. BE = CB [62] & AB = BC [00] ⇒ AB = BE [64]
058. EA = AB [63] & AB = BE [64] & BE = EA [25] (SSS)⇒ ΔEAB is congruent to ΔABE
==========================
173. examples/complete2/unsolved2/complete_012_7_Book_00EE_11_E076-31.gex
a b c = triangle a b c; d = angle_bisector d c b a, on_line d a c; e = angle_bisector e a c b, on_line e a b; f = on_line f d e, on_line f b c; g = on_line g a b ? eqangle a g a f a f a c
○ 번역
삼각형 ABC가 주어져 있습니다. D는 ∠CBA의 이등분선 위에 있으며, 직선 AC 위에 있습니다. E는 ∠ACB의 이등분선 위에 있으며, 직선 AB 위에 있습니다. F는 직선 DE와 직선 BC의 교점이고, G는 직선 AB 위에 있습니다. ∠GAF = ∠FAC임을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F G : Points
C,A,D are collinear [00]
∠DBC = ∠ABD [01]
B,A,E are collinear [02]
∠ACE = ∠ECB [03]
B,F,C are collinear [04]
D,F,E are collinear [05]
B,A,G are collinear [06]
* Auxiliary Constructions:
H I : Points
BH = BC [07]
DH = DC [08]
IF ∥ AD [09]
E,H,I are collinear [10]
* Proof steps:
001. IF ∥ AD [09] & C,A,D are collinear [00] ⇒ FI ∥ AC [11]
002. BH = BC [07] & DH = DC [08] (SSS)⇒ ∠DBC = ∠HBD [12]
003. ∠DBC = ∠HBD [12] & ∠DBC = ∠ABD [01] ⇒ ∠ABD = ∠HBD [13]
004. ∠ABD = ∠HBD [13] ⇒ BA ∥ BH [14]
005. B,A,G are collinear [06] & AB ∥ BH [14] ⇒ BH ∥ BG [15]
006. BH ∥ BG [15] ⇒ B,H,G are collinear [16]
007. AB ∥ BH [14] ⇒ B,A,H are collinear [17]
008. B,H,G are collinear [16] & B,A,H are collinear [17] & E,H,I are collinear [10] & B,A,E are collinear [02] ⇒ B,A,I are collinear [18]
009. FI ∥ AC [11] & B,F,C are collinear [04] & B,A,I are collinear [18] ⇒ BF:BI = CF:AI [19]
010. FI ∥ AC [11] & B,F,C are collinear [04] & B,A,I are collinear [18] ⇒ BF:BC = BI:BA [20]
011. ∠ACE = ∠ECB [03] & B,A,E are collinear [02] ⇒ BE:BC = EA:CA [21]
012. B,F,C are collinear [04] & B,A,E are collinear [02] & ∠CBD = ∠DBA [01] ⇒ ∠FBD = ∠DBE [22]
013. ∠FBD = ∠DBE [22] & D,F,E are collinear [05] ⇒ DE:DF = BE:BF [23]
014. B,H,G are collinear [16] & B,A,H are collinear [17] & E,H,I are collinear [10] & B,A,E are collinear [02] ⇒ E,I,A are collinear [24]
015. FI ∥ DA [09] & D,F,E are collinear [05] & E,I,A are collinear [24] ⇒ DE:DF = EA:AI [25]
016. DE:DF = BE:BF [23] & DE:DF = EA:AI [25] ⇒ EA:AI = BE:BF [26]
017. BE:BC = EA:CA [21] & EA:AI = BE:BF [26] ⇒ AI:CA = BF:BC [27]
018. BF:BC = BI:BA [20] & AI:CA = BF:BC [27] ⇒ AI:CA = BI:BA [28]
019. BF:BI = CF:AI [19] & AI:CA = BI:BA [28] ⇒ CF:BF = CA:BA [29]
020. CF:BF = CA:BA [29] & B,F,C are collinear [04] ⇒ ∠BAF = ∠FAC [30]
021. B,A,G are collinear [06] & ∠BAF = ∠FAC [30] ⇒ ∠GAF = ∠FAC
==========================
174. examples/complete2/unsolved2/complete_010_Other_Auxiliary_ye_aux_y1.gex
a b c = triangle a b c; d = angle_bisector d a b c, on_dia d b c; e = angle_bisector e b a c, on_dia e a c ? para d e a b
○ 번역
삼각형 ABC가 주어져 있습니다. D는 ∠ABC의 이등분선 위에 있으며, BD와 CD가 수직입니다. E는 ∠BAC의 이등분선 위에 있으며, AE와 CE가 수직입니다. 선분 DE와 선분 AB가 서로 평행임을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E : Points
∠ABD = ∠DBC [00]
BD ⟂ CD [01]
AE ⟂ CE [02]
∠BAE = ∠EAC [03]
* Auxiliary Constructions:
F G : Points
B,F,C are collinear [04]
FC = FB [05]
C,G,A are collinear [06]
GC = GA [07]
* Proof steps:
001. B,F,C are collinear [04] & FC = FB [05] ⇒ F is midpoint of CB [08]
002. BD ⟂ CD [01] & F is midpoint of CB [08] ⇒ BF = DF [09]
003. BF = DF [09] ⇒ ∠FDB = ∠DBF [10]
004. C,G,A are collinear [06] & GC = GA [07] ⇒ G is midpoint of CA [11]
005. F is midpoint of CB [08] & G is midpoint of CA [11] ⇒ FG ∥ BA [12]
006. ∠ABD = ∠DBC [00] & ∠FDB = ∠DBF [10] & B,F,C are collinear [04] & AB ∥ FG [12] ⇒ ∠FDB = ∠(FG-BD) [13]
007. ∠FDB = ∠(FG-BD) [13] ⇒ DF ∥ FG [14]
008. DF ∥ FG [14] ⇒ D,F,G are collinear [15]
009. AE ⟂ CE [02] & G is midpoint of CA [11] ⇒ AG = EG [16]
010. AG = EG [16] ⇒ ∠GEA = ∠EAG [17]
011. ∠GEA = ∠EAG [17] & C,G,A are collinear [06] & ∠BAE = ∠EAC [03] & AB ∥ FG [12] ⇒ ∠(FG-EA) = ∠GEA [18]
012. ∠(FG-EA) = ∠GEA [18] ⇒ FG ∥ EG [19]
013. FG ∥ EG [19] ⇒ E,F,G are collinear [20]
014. C,B,F are collinear [04] & C,G,A are collinear [06] ⇒ ∠BCA = ∠FCG [21]
015. C,G,A are collinear [06] & AB ∥ FG [12] ⇒ ∠BAC = ∠FGC [22]
016. ∠BCA = ∠FCG [21] & ∠BAC = ∠FGC [22] (Similar Triangles)⇒ ∠CBA = ∠CFG [23]
017. D,F,G are collinear [15] & E,F,G are collinear [20] & ∠CBA = ∠CFG [23] & B,F,C are collinear [04] ⇒ DE ∥ AB
==========================
175. examples/complete2/unsolved2/complete_004_6_GDD_FULL_21-40_40.gex
a b c = triangle a b c; i = incenter i a b c; e = on_pline e i a b, on_line e a c ? cong e i e a
○ 번역
삼각형 ABC가 주어져 있습니다. I는 삼각형 ABC의 내심입니다. 점 E는 I를 지나고 AB에 평행한 직선 위에 있으며, 직선 AC 위에 있습니다. 선분 EI와 선분 EA의 길이가 같음을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E : Points
∠DAB = ∠CAD [00]
E,C,A are collinear [01]
ED ∥ AB [02]
* Auxiliary Constructions:
: Points
* Proof steps:
001. E,C,A are collinear [01] & ∠CAD = ∠DAB [00] & AB ∥ DE [02] ⇒ ∠EAD = ∠ADE [03]
002. ∠EAD = ∠ADE [03] ⇒ EA = ED
==========================
176. examples/complete2/unsolved2/complete_014_7_Book_00EE_09_E069-8.gex
a b c = triangle a b c; d = parallelogram a b c d; e = eqangle2 e d a b ? eqangle d a a e e c c d
○ 번역
삼각형 ABC와 평행사변형 ABCD가 주어져 있습니다. ∠EDA = EBA입니다. ∠DAE = ∠ECD임을 증명하시오.
○ 풀이 : AlphaGeometry를 이용한 결과 다음과 같은 에러가 발생
numericals.InvalidQuadSolveError
177. examples/complete2/unsolved2/complete_011_7_Book_00EE_04_E051-9.gex
a b = segment a b; c = s_angle b a c 30; d = mirror d b c; e = foot e d a b ? cong d e a c
○ 번역
선분 AB가 주어져 있습니다. ∠BAC = 30°입니다. C는 DB의 중점입니다. E는 D에서 AB로 내린 수선의 발입니다. 선분 DE와 선분 AC의 길이가 같음을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E : Points
∠CAB = 1_PI/6 [00]
B,D,C are collinear [01]
CB = CD [02]
B,E,A are collinear [03]
DE ⟂ AB [04]
* Auxiliary Constructions:
F : Points
DF = DE [05]
EF = ED [06]
* Proof steps:
001. B,E,A are collinear [03] & DE ⟂ AB [04] ⇒ DE ⟂ EB [07]
002. B,D,C are collinear [01] & CB = CD [02] ⇒ C is midpoint of DB [08]
003. DE ⟂ EB [07] & C is midpoint of DB [08] ⇒ DC = EC [09]
004. DF = DE [05] & EF = ED [06] ⇒ FE = FD [10]
005. DC = EC [09] & FE = FD [10] ⇒ ED ⟂ CF [11]
006. EF = ED [06] ⇒ ∠EFD = ∠FDE [12]
007. FE = FD [10] ⇒ ∠FED = ∠EDF [13]
008. ∠CAB = 1_PI/6 [00] & DE ⟂ AB [04] & ∠EFD = ∠FDE [12] & ∠FED = ∠EDF [13] (Angle chase)⇒ AC ∥ DF [14]
009. ED ⟂ CF [11] & DE ⟂ AB [04] & DF ∥ AC [14] ⇒ ∠DFC = ∠CAB [15]
010. B,D,C are collinear [01] & ED ⟂ CF [11] & DE ⟂ AB [04] ⇒ ∠DCF = ∠CBA [16]
011. ∠DFC = ∠CAB [15] & ∠DCF = ∠CBA [16] (Similar Triangles)⇒ DC:CB = DF:CA [17]
012. DC:CB = DF:CA [17] & CB = CD [02] & DF = DE [05] ⇒ DE = AC
==========================
178. examples/complete2/unsolved2/complete_003_6_GDD_FULL_21-40_27.gex
a b c = triangle a b c; h = orthocenter h a b c; o = circumcenter o a b c; o3 = circumcenter o3 a h b; o1 = circumcenter o1 b h c; o2 = circumcenter o2 c h a ? cong h o1 h o2
○ 번역
삼각형 ABC가 주어져 있습니다. H는 삼각형 ABC의 수심이고, O는 삼각형 ABC의 외심입니다. O3는 삼각형 AHB의 외심이며, O1은 삼각형 BHC의 외심, O2는 삼각형 CHA의 외심입니다. 선분 HO1과 선분 HO2의 길이가 같음을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D G H : Points
AD ⟂ BC [00]
BD ⟂ AC [01]
GD = GC [02]
GB = GD [03]
HC = HD [04]
HD = HA [05]
* Auxiliary Constructions:
: Points
* Proof steps:
001. GD = GC [02] & HC = HD [04] (SSS)⇒ ∠GHD = ∠CHG [06]
002. GD = GC [02] ⇒ ∠GDC = ∠DCG [07]
003. GB = GD [03] ⇒ ∠GDB = ∠DBG [08]
004. GB = GD [03] & GD = GC [02] ⇒ GC = GB [09]
005. GC = GB [09] ⇒ ∠GCB = ∠CBG [10]
006. HD = HA [05] ⇒ ∠HDA = ∠DAH [11]
007. HC = HD [04] ⇒ ∠HDC = ∠DCH [12]
008. HC = HD [04] & HD = HA [05] ⇒ HA = HC [13]
009. HA = HC [13] ⇒ ∠HAC = ∠ACH [14]
010. AD ⟂ BC [00] & BD ⟂ AC [01] & ∠GDC = ∠DCG [07] & ∠GDB = ∠DBG [08] & ∠GCB = ∠CBG [10] & ∠HDA = ∠DAH [11] & ∠HDC = ∠DCH [12] & ∠HAC = ∠ACH [14] (Angle chase)⇒ DG ∥ CH [15]
011. ∠CHG = ∠GHD [06] & CH ∥ DG [15] ⇒ ∠DGH = ∠GHD [16]
012. ∠DGH = ∠GHD [16] ⇒ DG = DH
==========================
179. examples/complete2/unsolved2/complete_017_ex-gao_ex160_4_e08.gex
a b c = triangle a b c; d = on_line d b c, angle_bisector d b a c; e = on_pline e d a c, on_line e a b; f = on_pline f e b c, on_line f a c ? cong e a f c
○ 번역
삼각형 가 주어져 있습니다. D는 직선 B 위에 있으며, ∠BAC의 이등분선 위에 있습니다. E는 D를 지나고 AC에 평행한 직선 위에 있고, 직선 AB 위에 있습니다. F는 E를 지나고 BC에 평행한 직선 위에 있으며, 직선 A 위에 있습니다. 선분 EA와 선분 FC의 길이가 같음을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F : Points
C,B,D are collinear [00]
∠BAD = ∠DAC [01]
ED ∥ AC [02]
E,B,A are collinear [03]
C,A,F are collinear [04]
FE ∥ BC [05]
* Auxiliary Constructions:
: Points
* Proof steps:
001. C,B,D are collinear [00] & C,F,A are collinear [04] & BC ∥ EF [05] & DE ∥ AC [02] ⇒ ∠CDE = ∠EFC [06]
002. C,F,A are collinear [04] & DE ∥ AC [02] ⇒ ∠CED = ∠ECF [07]
003. ∠CDE = ∠EFC [06] & ∠CED = ∠ECF [07] (Similar Triangles)⇒ ED = CF [08]
004. E,B,A are collinear [03] & ∠BAD = ∠DAC [01] & AC ∥ DE [02] ⇒ ∠EAD = ∠ADE [09]
005. ∠EAD = ∠ADE [09] ⇒ EA = ED [10]
006. ED = CF [08] & EA = ED [10] ⇒ EA = FC
==========================
180. examples/complete2/unsolved2/complete_015_7_Book_00EE_06_E051-29.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 = on_line f b e, on_line f c d; g = on_line g d e, on_pline g f b c; h = on_circle h a b, on_dia h g a ? cong f g g h
○ 번역
선분 AB가 주어져 있으며, 점 C, D, E는 모두 A를 중심으로 하고 B를 지나는 원 위에 있습니다. F는 직선 BE와 CD의 교점입니다. G는 직선 DE 위에 있고, F를 지나고 BC에 평행한 직선 위에 있습니다. H는 A를 중심으로 하고 B를 지나는 원 위에 있으며, GH와 AH가 수직입니다. 선분 FG와 선분 GH의 길이가 같음을 증명하시오.
○ 풀이 : AlphaGeometry를 사용한 풀이
==========================
* From theorem premises:
A B C D E F G H : Points
AC = AB [00]
AD = AB [01]
AE = AB [02]
B,E,F are collinear [03]
C,D,F are collinear [04]
G,D,E are collinear [05]
GF ∥ BC [06]
AH = AB [07]
GH ⟂ AH [08]
* Auxiliary Constructions:
: Points
* Proof steps:
001. AD = AB [01] & AE = AB [02] & AC = AB [00] ⇒ B,C,D,E are concyclic [09]
002. B,C,D,E are concyclic [09] ⇒ ∠BED = ∠BCD [10]
003. B,E,F are collinear [03] & G,D,E are collinear [05] & C,D,F are collinear [04] & ∠BED = ∠BCD [10] & BC ∥ FG [06] ⇒ ∠FEG = ∠GFD [11]
004. G,D,E are collinear [05] ⇒ ∠FGE = ∠FGD [12]
005. ∠FEG = ∠GFD [11] & ∠FGE = ∠FGD [12] (Similar Triangles)⇒ EF:GF = DF:GD [13]
006. ∠FEG = ∠GFD [11] & ∠FGE = ∠FGD [12] (Similar Triangles)⇒ EF:GE = DF:GF [14]
007. AD = AB [01] & AH = AB [07] & AE = AB [02] ⇒ A is the circumcenter of \Delta HDE [15]
008. A is the circumcenter of \Delta HDE [15] & GH ⟂ AH [08] ⇒ ∠EHG = ∠EDH [16]
009. A is the circumcenter of \Delta HDE [15] & GH ⟂ AH [08] ⇒ ∠GHD = ∠HED [17]
010. G,D,E are collinear [05] & ∠EDH = ∠EHG [16] ⇒ ∠GDH = ∠EHG [18]
011. G,D,E are collinear [05] & ∠GHD = ∠HED [17] ⇒ ∠GHD = ∠HEG [19]
012. ∠GDH = ∠EHG [18] & ∠GHD = ∠HEG [19] (Similar Triangles)⇒ GD:HG = HG:GE [20]
013. EF:GF = DF:GD [13] & EF:GE = DF:GF [14] & GD:HG = HG:GE [20] (Ratio chase)⇒ GF = HG
==========================
입력: 2024.08.07 13:24
'▶ 자연과학 > ▷ 기하학' 카테고리의 다른 글
| 【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [201-220] (0) | 2024.08.23 |
|---|---|
| 【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [181-200] (0) | 2024.08.18 |
| 【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [141-160] (0) | 2024.08.16 |
| 【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [121-140] (0) | 2024.08.16 |
| 【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [101-120] (0) | 2024.08.11 |
최근댓글