【AlphaGeometry】 jgex_ag_231 기하 문제 풀이 [21-40]

jgex_ag_231 기하 문제 풀이 [21-40]

 

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

---

 

21. examples/complete2/013/complete_002_6_GDD_FULL_41-60_52.gex

e c d = r_triangle e c d; o = midpoint o d c; a = on_tline a c c d, on_tline a e e o; f = on_line f c a, on_line f d e ? cong a e a f

 

○ 번역 

 

삼각형 ECD가 주어져 있으며, ∠E가 직각입니다. O는 선분 DC의 중점입니다. A는 C를 지나고 CD와 수직인 직선과 E를 지나고 EO와 수직인 직선의 교점입니다. 점 F는 직선 CA와 DE의 교점입니다. 선분 AE와 선분 AF의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

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

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. F,B,E are collinear [05] & BE ⟂ BC [04] ⇒  FB ⟂ BC [07]
002. AE ⟂ AD [03] & FB ⟂ BC [07] ⇒  ∠(AE-FB) = ∠(AD-BC) [08]
003. B,C,D are collinear [01] & F,B,E are collinear [05] & ∠(AE-FB) = ∠(AD-BC) [08] ⇒  ∠ADB = ∠AEF [09]
004. F,C,A are collinear [06] & AB ⟂ AC [00] ⇒  BA ⟂ FC [10]
005. BA ⟂ FC [10] & FB ⟂ BC [07] ⇒  ∠ABC = ∠CFB [11]
006. B,C,D are collinear [01] & F,C,A are collinear [06] & F,B,E are collinear [05] & ∠ABC = ∠CFB [11] ⇒  ∠ABD = ∠AFE [12]
007. ∠ADB = ∠AEF [09] & ∠ABD = ∠AFE [12] (Similar Triangles)⇒  DA:DB = EA:EF [13]
008. B,C,D are collinear [01] & DC = DB [02] ⇒  D is midpoint of BC [14]
009. AB ⟂ AC [00] & D is midpoint of BC [14] ⇒  BD = AD [15]
010. DA:DB = EA:EF [13] & BD = AD [15] ⇒  EA = EF
==========================

 

 

22. examples/complete2/014/complete_008_7_Book_LLL_L053-1.gex

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

 

○ 번역 

 

삼각형 BCD가 주어져 있습니다. 점 E는 B에서 CD로 내린 수선의 발입니다. A는 자유롭게 선택된 점입니다. 점 F는 A에서 CD로 내린 수선의 발입니다. G는 선분 BA의 중점입니다. 선분 FG와 선분 GE의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
D,B,C are collinear [00]
AD ⟂ BC [01]
F,B,C are collinear [02]
BC ⟂ FE [03]
G,A,E are collinear [04]
GA = GE [05]

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

 * Proof steps:
001. F,B,C are collinear [02] & D,B,C are collinear [00] & AD ⟂ BC [01] ⇒  AD ⟂ DF [08]
002. F,H,A are collinear [06] & HF = HA [07] ⇒  H is midpoint of AF [09]
003. AD ⟂ DF [08] & H is midpoint of AF [09] ⇒  FH = DH [10]
004. AD ⟂ DF [08] & H is midpoint of AF [09] ⇒  AH = DH [11]
005. AH = DH [11] ⇒  ∠HDA = ∠DAH [12]
006. G,A,E are collinear [04] & GA = GE [05] ⇒  G is midpoint of AE [13]
007. G is midpoint of AE [13] & H is midpoint of AF [09] ⇒  GH ∥ EF [14]
008. F,H,A are collinear [06] & ∠HDA = ∠DAH [12] & GH ∥ EF [14] & BC ⟂ FE [03] & AD ⟂ BC [01] ⇒  ∠FHG = ∠GHD [15]
009. FH = DH [10] & ∠FHG = ∠GHD [15] (SAS)⇒  GF = GD
==========================

 

 

23. examples/complete2/014/complete_007_7_Book_LLL_L058-9.gex

a b = segment a b; c = on_bline c a b; d = on_tline d b a b; e = intersection_lt e c d a a b ? cong e c c d

 

○ 번역 : 추후 업데이트

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E : Points
CA = CB [00]
BD ⟂ AB [01]
AB ⟂ EA [02]
C,D,E are collinear [03]

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

 * Proof steps:
001. D,A,F are collinear [04] & FD = FA [05] ⇒  F is midpoint of DA [06]
002. BD ⟂ AB [01] & F is midpoint of DA [06] ⇒  AF = BF [07]
003. CA = CB [00] & AF = BF [07] ⇒  AB ⟂ CF [08]
004. AB ⟂ EA [02] & BD ⟂ AB [01] & AB ⟂ CF [08] ⇒  CF ∥ EA [09]
005. CF ∥ EA [09] & C,D,E are collinear [03] & D,A,F are collinear [04] ⇒  FD:FA = CD:CE [10]
006. FD:FA = CD:CE [10] & FD = FA [05] ⇒  CD = CE
==========================

 

 

24. examples/complete2/007/complete_003_6_GDD_FULL_more_E015-6.gex

a b c = triangle a b c; d = midpoint d a c; e = midpoint e b a; f = midpoint f c b; g = on_pline g d a f, on_pline g f a c ? para c e g b

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 선분 AC의 중점입니다. E는 선분 BA의 중점입니다. F는 선분 CB의 중점입니다. 선분 GD와 AF가 평행하고, 선분 GF와 AC가 평행하도록 G가 정의됩니다. 선분 CE와 선분 GB가 서로 평행임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
C,A,D are collinear [00]
DA = DC [01]
E,B,A are collinear [02]
EB = EA [03]
C,B,F are collinear [04]
FC = FB [05]
GF ∥ AC [06]
GD ∥ AF [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. C,B,F are collinear [04] & FC = FB [05] ⇒  F is midpoint of CB [08]
002. E,B,A are collinear [02] & EB = EA [03] ⇒  E is midpoint of AB [09]
003. E is midpoint of AB [09] & F is midpoint of CB [08] ⇒  EF ∥ AC [10]
004. EF ∥ AC [10] & FG ∥ AC [06] ⇒  FG ∥ FE [11]
005. FG ∥ FE [11] ⇒  E,F,G are collinear [12]
006. AF ∥ DG [07] & EF ∥ FG [11] ⇒  ∠AFE = ∠DGF [13]
007. C,A,D are collinear [00] & DA = DC [01] ⇒  D is midpoint of CA [14]
008. D is midpoint of CA [14] & F is midpoint of CB [08] ⇒  DF ∥ AB [15]
009. E,B,A are collinear [02] & AB ∥ DF [15] & EF ∥ FG [11] ⇒  ∠AEF = ∠DFG [16]
010. ∠AFE = ∠DGF [13] & ∠AEF = ∠DFG [16] (Similar Triangles)⇒  FA:GD = FE:GF [17]
011. C,A,D are collinear [00] & AF ∥ DG [07] & AC ∥ FG [06] ⇒  ∠FAD = ∠DGF [18]
012. C,A,D are collinear [00] & AC ∥ FG [06] ⇒  ∠FDA = ∠DFG [19]
013. ∠FAD = ∠DGF [18] & ∠FDA = ∠DFG [19] (Similar Triangles)⇒  FA = DG [20]
014. E,F,G are collinear [12] & FA:GD = FE:GF [17] & FA = DG [20] ⇒  F is midpoint of EG [21]
015. F is midpoint of CB [08] & F is midpoint of EG [21] ⇒  CE ∥ BG
==========================

 

 

25. examples/complete2/007/complete_003_6_GDD_FULL_more_E022-9.gex

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

 

○ 번역 : 추후 업데이트 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
DB = DA [00]
DA = DC [01]
A,E,C are collinear [02]
∠CBE = ∠EBA [03]
DB = DF [04]
F,E,B are collinear [05]
FG ⟂ DF [06]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. DB = DA [00] & DB = DF [04] ⇒  D is the circumcenter of \Delta FAB [07]
002. D is the circumcenter of \Delta FAB [07] & FG ⟂ DF [06] ⇒  ∠GFA = ∠FBA [08]
003. DB = DA [00] & DA = DC [01] & DB = DF [04] ⇒  A,F,B,C are concyclic [09]
004. A,F,B,C are concyclic [09] ⇒  ∠AFB = ∠ACB [10]
005. A,E,C are collinear [02] & ∠GFA = ∠FBA [08] & F,E,B are collinear [05] & ∠CBE = ∠EBA [03] & ∠AFB = ∠ACB [10] ⇒  ∠EAF = ∠GFA [11]
006. ∠EAF = ∠GFA [11] ⇒  AE ∥ GF [12]
007. AE ∥ GF [12] & A,E,C are collinear [02] ⇒  AC ∥ FG
==========================

 

 

26. examples/complete2/007/complete_012_7_Book_00EE_02_E028-2.gex

a b c = triangle a b c; d e = square a c d e; g f = square c b g f ? perp d b f a

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. ACDE는 AC를 한 변으로 하는 정사각형이고, CBGF는 CB를 한 변으로 하는 정사각형입니다. DB와 FA가 서로 수직임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D F G : Points
AC = CD [00]
AC ⟂ CD [01]
CB = BF [02]
BC ⟂ BF [03]
CB ∥ FG [04]
CG ∥ BF [05]

 * Auxiliary Constructions:
E : Points
AE ∥ CD [06]

 * Proof steps:
001. BC ∥ FG [04] & BF ∥ CG [05] ⇒  ∠FGC = ∠CBF [07]
002. CG ∥ BF [05] ⇒  ∠FCG = ∠CFB [08]
003. ∠FGC = ∠CBF [07] & ∠FCG = ∠CFB [08] (Similar Triangles)⇒  CG = FB [09]
004. CG = FB [09] & CB = BF [02] ⇒  CB = CG [10]
005. AC ⟂ CD [01] & CD ∥ AE [06] ⇒  AC ⟂ EA [11]
006. BC ⟂ BF [03] & BF ∥ CG [05] & BC ∥ FG [04] ⇒  GC ⟂ GF [12]
007. AC ⟂ EA [11] & GC ⟂ GF [12] ⇒  ∠ACG = ∠(AE-FG) [13]
008. AC ⟂ EA [11] & GC ⟂ GF [12] ⇒  ∠CAE = ∠FGC [14]
009. ∠ACG = ∠(AE-FG) [13] & CG ∥ BF [05] & AE ∥ CD [06] & BC ∥ FG [04] ⇒  ∠ACG = ∠DCB [15]
010. AC = CD [00] & CB = CG [10] & ∠ACG = ∠DCB [15] (SAS)⇒  ∠(AG-BD) = ∠GCB [16]
011. AC = CD [00] & CB = CG [10] & ∠ACG = ∠DCB [15] (SAS)⇒  ∠DCA = ∠(BD-AG) [17]
012. ∠(AG-BD) = ∠GCB [16] & CG ∥ BF [05] & ∠CAE = ∠FGC [14] & AE ∥ CD [06] & BC ∥ FG [04] & ∠DCA = ∠(BD-AG) [17] ⇒  DB ⟂ GA
==========================

 

 

27. examples/complete2/007/complete_012_7_Book_00EE_05_E051-22.gex

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

 

○ 번역 

 

선분 AB가 주어져 있습니다. C는 선분 BA의 중점입니다. 점 D는 B를 지나고 AB에 수직인 선 위에 있습니다. 점 E는 선 AD 위에 있으며, 중심이 C이고 A를 지나는 원 위에 있습니다. 점 F는 E를 지나고 AB에 평행한 직선 위에 있으며, 중심이 C이고 E인 원 위에 있습니다. 점 G는 D에서 선분 AF에 내린 수선의 발입니다. 선분 AF와 선분 FG의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
CB = CA [00]
A,C,B are collinear [01]
BD ⟂ AB [02]
CE = CA [03]
A,D,E are collinear [04]
CF = CE [05]
FE ∥ AB [06]
F,A,G are collinear [07]
DG ⟂ AF [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. CF = CE [05] & CE = CA [03] & CB = CA [00] ⇒  C is the circumcenter of \Delta BFA [09]
002. CF = CE [05] & CE = CA [03] & CB = CA [00] ⇒  F,A,E,B are concyclic [10]
003. A,C,B are collinear [01] & AB ⟂ BD [02] ⇒  CB ⟂ BD [11]
004. C is the circumcenter of \Delta BFA [09] & CB ⟂ BD [11] ⇒  ∠ABD = ∠AFB [12]
005. CB = CA [00] & CE = CA [03] ⇒  C is the circumcenter of \Delta BAE [13]
006. C is the circumcenter of \Delta BAE [13] & A,C,B are collinear [01] ⇒  BE ⟂ EA [14]
007. BE ⟂ EA [14] & A,D,E are collinear [04] ⇒  BE ⟂ AD [15]
008. A,C,B are collinear [01] & BD ⟂ AB [02] ⇒  DB ⟂ AC [16]
009. BE ⟂ AD [15] & DB ⟂ AC [16] ⇒  ∠ADB = ∠(EB-AC) [17]
010. F,A,E,B are concyclic [10] ⇒  ∠FAE = ∠FBE [18]
011. F,A,E,B are concyclic [10] ⇒  ∠FEA = ∠FBA [19]
012. F,A,G are collinear [07] & ∠ABD = ∠AFB [12] & ∠ADB = ∠(EB-AC) [17] & A,C,B are collinear [01] & ∠FAE = ∠FBE [18] & A,D,E are collinear [04] ⇒  ∠BFA = ∠GFB [20]
013. F,A,G are collinear [07] & DG ⟂ AF [08] & BD ⟂ AB [02] ⇒  ∠DBA = ∠DGA [21]
014. ∠DBA = ∠DGA [21] ⇒  G,A,D,B are concyclic [22]
015. G,A,D,B are concyclic [22] ⇒  ∠GAD = ∠GBD [23]
016. DG ⟂ AF [08] & DB ⟂ AC [16] ⇒  ∠(DG-AC) = ∠(FA-DB) [24]
017. A,C,B are collinear [01] & ∠(DG-AC) = ∠(FA-DB) [24] ⇒  ∠(FA-DG) = ∠(DB-AC) [25]
018. C is the circumcenter of \Delta BFA [09] & A,C,B are collinear [01] ⇒  FA ⟂ BF [26]
019. A,C,B are collinear [01] & ∠FEA = ∠FBA [19] & A,D,E are collinear [04] & EF ∥ AB [06] & FA ⟂ BF [26] & DG ⟂ AF [08] ⇒  ∠(DG-AC) = ∠CAD [27]
020. ∠(FA-DG) = ∠(DB-AC) [25] & ∠(DG-AC) = ∠CAD [27] ⇒  ∠FAC = ∠BDA [28]
021. F,A,G are collinear [07] & ∠GAD = ∠GBD [23] & ∠FAC = ∠BDA [28] & A,C,B are collinear [01] ⇒  ∠BAF = ∠FGB [29]
022. ∠BFA = ∠GFB [20] & ∠BAF = ∠FGB [29] (Similar Triangles)⇒  FA = FG
==========================

 

 

28. examples/complete2/007/complete_005_Other_other_E075-25-sss.gex

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

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 선분 CB의 중점입니다. E는 선분 AC의 중점입니다. F는 선분 BA의 중점입니다. 점 G는 A에서 선분 BC로 내린 수선의 발입니다. ∠FDE=∠FGE임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
B,C,D are collinear [00]
DC = DB [01]
E,A,C are collinear [02]
EA = EC [03]
B,A,F are collinear [04]
FB = FA [05]
B,C,G are collinear [06]
AG ⟂ BC [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. B,C,G are collinear [06] & BC ⟂ AG [07] ⇒  CG ⟂ GA [08]
002. E,A,C are collinear [02] & EA = EC [03] ⇒  E is midpoint of CA [09]
003. CG ⟂ GA [08] & E is midpoint of CA [09] ⇒  AE = GE [10]
004. B,C,G are collinear [06] & BC ⟂ AG [07] ⇒  BG ⟂ GA [11]
005. B,A,F are collinear [04] & FB = FA [05] ⇒  F is midpoint of BA [12]
006. BG ⟂ GA [11] & F is midpoint of BA [12] ⇒  AF = GF [13]
007. AE = GE [10] & AF = GF [13] (SSS)⇒  ∠EAF = ∠FGE [14]
008. B,C,D are collinear [00] & DC = DB [01] ⇒  D is midpoint of BC [15]
009. D is midpoint of BC [15] & F is midpoint of BA [12] ⇒  DF ∥ CA [16]
010. D is midpoint of BC [15] & E is midpoint of CA [09] ⇒  DE ∥ BA [17]
011. ∠EAF = ∠FGE [14] & E,A,C are collinear [02] & B,A,F are collinear [04] & AC ∥ DF [16] & AB ∥ DE [17] ⇒  ∠FDE = ∠FGE
==========================

 

 

29. examples/complete2/007/complete_001_6_GDD_FULL_01-20_01.gex

a b c = triangle a b c; d = foot d c a b; e = foot e b a c; f = midpoint f c b; g = midpoint g d e ? perp f g d e 

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 C에서 선분 AB로 내린 수선의 발이고, E는 B에서 선분 AC로 내린 수선의 발입니다. F는 선분 CB의 중점이고, G는 선분 DE의 중점입니다. 선분 FG와 선분 DE가 서로 수직임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
B,A,D are collinear [00]
CD ⟂ AB [01]
E,A,C are collinear [02]
BE ⟂ AC [03]
F,B,C are collinear [04]
FC = FB [05]
GD = GE [06]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. E,A,C are collinear [02] & AC ⟂ BE [03] ⇒  CE ⟂ EB [07]
002. F,B,C are collinear [04] & FC = FB [05] ⇒  F is midpoint of CB [08]
003. CE ⟂ EB [07] & F is midpoint of CB [08] ⇒  BF = EF [09]
004. B,D,A are collinear [00] & AB ⟂ CD [01] ⇒  BD ⟂ DC [10]
005. BD ⟂ DC [10] & F is midpoint of CB [08] ⇒  BF = DF [11]
006. BF = EF [09] & BF = DF [11] ⇒  FD = FE [12]
007. FD = FE [12] & GD = GE [06] ⇒  DE ⟂ FG
==========================

 

 

30. examples/complete2/007/complete_000_2_PWW_B016x.gex

a b c = triangle a b c; d = midpoint d b c; e = midpoint e c a; f = midpoint f b a; g = parallelogram d a e g ? cong c f g b

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 선분 BC의 중점입니다. E는 선분 CA의 중점입니다. F는 선분 BA의 중점입니다. DAEG는 평행사변형입니다. 선분 CF와 선분 GB의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
DB = DC [00]
B,D,C are collinear [01]
E,C,A are collinear [02]
EC = EA [03]
B,F,A are collinear [04]
FB = FA [05]
DA ∥ EG [06]
DG ∥ AE [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. B,D,C are collinear [01] & DB = DC [00] ⇒  D is midpoint of BC [08]
002. B,F,A are collinear [04] & FB = FA [05] ⇒  F is midpoint of BA [09]
003. D is midpoint of BC [08] & F is midpoint of BA [09] ⇒  DF ∥ CA [10]
004. DG ∥ AE [07] & E,C,A are collinear [02] & DF ∥ AC [10] ⇒  DF ∥ DG [11]
005. AD ∥ EG [06] & DF ∥ DG [11] ⇒  ∠ADF = ∠EGD [12]
006. E,C,A are collinear [02] & EC = EA [03] ⇒  E is midpoint of CA [13]
007. D is midpoint of BC [08] & E is midpoint of CA [13] ⇒  DE ∥ BA [14]
008. B,F,A are collinear [04] & AB ∥ DE [14] & DF ∥ DG [11] ⇒  ∠AFD = ∠EDG [15]
009. ∠ADF = ∠EGD [12] & ∠AFD = ∠EDG [15] (Similar Triangles)⇒  DA:GE = DF:GD [16]
010. C,A,E are collinear [02] & AD ∥ EG [06] & DG ∥ AE [07] ⇒  ∠ADG = ∠GEA [17]
011. E,C,A are collinear [02] & DG ∥ AE [07] ⇒  ∠AGD = ∠GAE [18]
012. ∠ADG = ∠GEA [17] & ∠AGD = ∠GAE [18] (Similar Triangles)⇒  AD = GE [19]
013. DA:GE = DF:GD [16] & AD = GE [19] ⇒  DF = GD [20]
014. DF ∥ DG [11] ⇒  G,D,F are collinear [21]
015. B,D,C are collinear [01] & F,D,G are collinear [21] ⇒  ∠CDF = ∠BDG [22]
016. DB = DC [00] & DF = GD [20] & ∠CDF = ∠BDG [22] (SAS)⇒  FC = GB
==========================

 

 

31. examples/complete2/007/complete_001_6_GDD_FULL_61-80_66.gex

a b c = triangle a b c; d = foot d c a b; e = on_tline e a b c, on_line e c d; f = midpoint f a e; g = midpoint g c b ? perp d g d f

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. D는 C에서 AB로 내린 수선의 발입니다. 점 E는 A를 지나고 BC와 수직인 선 위에 있으며, 선분 CD 위에 있습니다. F는 선분 AE의 중점이고, G는 선분 CB의 중점입니다. 선분 DG와 선분 DF가 서로 수직임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
A,B,D are collinear [00]
CD ⟂ AB [01]
C,D,E are collinear [02]
AE ⟂ BC [03]
A,F,E are collinear [04]
FA = FE [05]
B,C,G are collinear [06]
GC = GB [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. A,B,D are collinear [00] & C,D,E are collinear [02] & AB ⟂ CD [01] ⇒  AD ⟂ DE [08]
002. A,F,E are collinear [04] & FA = FE [05] ⇒  F is midpoint of AE [09]
003. AD ⟂ DE [08] & F is midpoint of AE [09] ⇒  EF = DF [10]
004. EF = DF [10] & FA = FE [05] ⇒  F is the circumcenter of \Delta EDA [11]
005. A,F,E are collinear [04] & BC ⟂ AE [03] ⇒  BC ⟂ AF [12]
006. CD ⟂ AB [01] & BC ⟂ AF [12] ⇒  ∠BAF = ∠DCB [13]
007. A,B,D are collinear [00] & AB ⟂ CD [01] ⇒  BD ⟂ DC [14]
008. B,C,G are collinear [06] & GC = GB [07] ⇒  G is midpoint of BC [15]
009. BD ⟂ DC [14] & G is midpoint of BC [15] ⇒  CG = DG [16]
010. CG = DG [16] ⇒  ∠GCD = ∠CDG [17]
011. C,D,E are collinear [02] & A,B,D are collinear [00] & ∠BAF = ∠DCB [13] & A,F,E are collinear [04] & ∠GCD = ∠CDG [17] & B,C,G are collinear [06] ⇒  ∠GDE = ∠DAE [18]
012. F is the circumcenter of \Delta EDA [11] & ∠GDE = ∠DAE [18] ⇒  DF ⟂ DG
==========================

 

 

32. examples/complete2/007/complete_016_7_Book_00EE_06_E051-30.gex

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

 

○ 번역 : 추후 업데이트 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
CB = CA [00]
CD = CA [01]
B,E,A are collinear [02]
DE ⟂ CD [03]
∠DEF = ∠FEA [04]
F,D,A are collinear [05]
FA:EA = FA:EA [06]
G,E,F are collinear [07]
G,B,D are collinear [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. B,E,A are collinear [02] & G,E,F are collinear [07] & ∠DEF = ∠FEA [04] ⇒  ∠FEA = ∠DEG [09]
002. CB = CA [00] & CD = CA [01] ⇒  C is the circumcenter of \Delta DBA [10]
003. C is the circumcenter of \Delta DBA [10] & DE ⟂ CD [03] ⇒  ∠EDB = ∠DAB [11]
004. F,D,A are collinear [05] & B,E,A are collinear [02] & G,B,D are collinear [08] & ∠DAB = ∠EDB [11] ⇒  ∠FAE = ∠EDG [12]
005. ∠FEA = ∠DEG [09] & ∠FAE = ∠EDG [12] (Similar Triangles)⇒  GD:FA = ED:EA [13]
006. ∠DEF = ∠FEA [04] & F,D,A are collinear [05] ⇒  FD:FA = ED:EA [14]
007. GD:FA = ED:EA [13] & FD:FA = ED:EA [14] ⇒  FD:FA = GD:FA [15]
008. FD:FA = GD:FA [15] & FA:EA = FA:EA [06] ⇒  GD = FD
==========================

 

 

33. examples/complete2/007/complete_016_7_Book_00EE_06_E051-24.gex

a b = segment a b; c = midpoint c b a; d = on_circle d c a; e = on_line e b d; f = circle f d c e; g = on_pline g e a b, on_circle g f c ? cong g e c b

 

○ 번역 

 

선분 AB가 주어져 있습니다. C는 선분 AB의 중점입니다. 점 D는 C를 중심으로 하고 A를 지나는 원 위에 있습니다. 점 E는 직선 BD 위에 있습니다. F는 삼각형 DCE의 외심입니다. 점 G는 점 E를 지나고 AB에 평행한 직선 위에 있으며, 중심이 F이고 C를 지나는 원 위에 있습니다. 선분 GE와 선분 CB의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
B,A,C are collinear [00]
CB = CA [01]
CD = CA [02]
B,E,D are collinear [03]
FD = FC [04]
FC = FE [05]
GE ∥ AB [06]
FG = FC [07]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. B,A,C are collinear [00] & AB ∥ EG [06] ⇒  ∠ECB = ∠CEG [08]
002. FD = FC [04] & FG = FC [07] & FC = FE [05] ⇒  E,D,C,G are concyclic [09]
003. E,D,C,G are concyclic [09] ⇒  ∠EDC = ∠EGC [10]
004. CD = CA [02] & CB = CA [01] ⇒  CB = CD [11]
005. CB = CD [11] ⇒  ∠CBD = ∠BDC [12]
006. B,E,D are collinear [03] & B,A,C are collinear [00] & ∠EDC = ∠EGC [10] & EG ∥ AB [06] & ∠CBD = ∠BDC [12] ⇒  ∠EBC = ∠CGE [13]
007. ∠ECB = ∠CEG [08] & ∠EBC = ∠CGE [13] (Similar Triangles)⇒  CB = EG
==========================

 

 

34. examples/complete2/007/complete_013_7_Book_00EE_11_E077-37.gex

a b = segment a b; c = midpoint c b a; d = on_circle d c b; e = foot e d a b; f = lc_tangent f d c; g = on_line g d f ? eqangle d f d a d a d e

 

○ 번역 : 추후 업데이트

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F : Points
CB = CA [00]
A,B,C are collinear [01]
CD = CB [02]
DE ⟂ AB [03]
DF ⟂ CD [04]

 * Auxiliary Constructions:
G : Points
G,F,D are collinear [05]

 * Proof steps:
001. CD = CB [02] & CB = CA [00] ⇒  C is the circumcenter of \Delta DBA [06]
002. C is the circumcenter of \Delta DBA [06] & A,B,C are collinear [01] ⇒  BD ⟂ AD [07]
003. DE ⟂ AB [03] & BD ⟂ AD [07] ⇒  ∠ADB = ∠(ED-AB) [08]
004. G,F,D are collinear [05] & CD ⟂ DF [04] ⇒  CD ⟂ DG [09]
005. C is the circumcenter of \Delta DBA [06] & CD ⟂ DG [09] ⇒  ∠GDB = ∠DAB [10]
006. G,F,D are collinear [05] & ∠GDB = ∠DAB [10] ⇒  ∠(BD-GF) = ∠BAD [11]
007. ∠ADB = ∠(ED-AB) [08] & ∠(BD-GF) = ∠BAD [11] ⇒  ∠(AD-GF) = ∠EDA [12]
008. ∠(AD-GF) = ∠EDA [12] & G,F,D are collinear [05] ⇒  ∠ADF = ∠EDA
==========================

 

 

35. examples/complete2/007/complete_013_7_Book_00EE_07_E059-54-1.gex

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

 

○ 번역 

 

선분 AB가 주어져 있습니다. C는 선분 AB의 중점입니다. D는 C에 대한 B의 대칭점입니다. 점 E는 C를 중심으로 하고 A를 지나는 원과 B를 중심으로 하고 C를 지나는 원 위에 있습니다. 점 F는 B를 지나고 선분 AB에 수직인 선과 선분 AE의 교점입니다. 점 G는 선분 BF와 DE의 교점입니다. 선분 EG와 선분 GF의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
CB = CA [00]
A,B,C are collinear [01]
BC = BD [02]
C,B,D are collinear [03]
CE = CA [04]
BE = BC [05]
A,F,E are collinear [06]
BF ⟂ AB [07]
E,G,D are collinear [08]
B,G,F are collinear [09]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. CE = CA [04] & CB = CA [00] ⇒  C is the circumcenter of \Delta BEA [10]
002. C is the circumcenter of \Delta BEA [10] & A,B,C are collinear [01] ⇒  BE ⟂ AE [11]
003. BE = BC [05] & BC = BD [02] ⇒  B is the circumcenter of \Delta DEC [12]
004. B is the circumcenter of \Delta DEC [12] & B,D,C are collinear [03] ⇒  DE ⟂ CE [13]
005. D,G,E are collinear [08] & A,E,F are collinear [06] & BE ⟂ AE [11] & DE ⟂ CE [13] ⇒  ∠GEC = ∠(AF-BE) [14]
006. A,B,C are collinear [01] & B,G,F are collinear [09] & AB ⟂ BF [07] ⇒  CB ⟂ BG [15]
007. C is the circumcenter of \Delta BEA [10] & CB ⟂ BG [15] ⇒  ∠GBE = ∠BAE [16]
008. CE = CA [04] ⇒  ∠CEA = ∠EAC [17]
009. A,E,F are collinear [06] & B,G,F are collinear [09] & ∠GBE = ∠BAE [16] & ∠CEA = ∠EAC [17] & A,B,C are collinear [01] ⇒  ∠(EC-AF) = ∠EBG [18]
010. ∠GEC = ∠(AF-BE) [14] & ∠(EC-AF) = ∠EBG [18] ⇒  ∠(EG-AF) = ∠(AF-BG) [19]
011. D,G,E are collinear [08] & A,F,E are collinear [06] & B,G,F are collinear [09] & ∠(EG-AF) = ∠(AF-BG) [19] ⇒  ∠GEF = ∠EFG [20]
012. ∠GEF = ∠EFG [20] ⇒  GE = GF
==========================

 

 

36. examples/complete2/007/complete_008_ex-gao_ex160_e201f.gex

a b c = triangle a b c; d e = square a b d e; f = foot f a b c; g = on_line g a f, eqdistance g a b c ? perp g b c d

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. ABDE는 선분 AB를 한 변으로 하는 정사각형입니다. 점 F는 A에서 BC로 내린 수선의 발입니다. 점 G는 선 AF 위에 있으며, 점 G에서 점 A까지의 거리와 선분 BC의 길이가 같습니다. 선분 GB와 선분 CD가 서로 수직임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D F G : Points
AB = BD [00]
AB ⟂ BD [01]
AF ⟂ BC [02]
GA = BC [03]
A,G,F are collinear [04]

 * Auxiliary Constructions:
E : Points
AB ∥ DE [05]
AE ∥ BD [06]

 * Proof steps:
001. AB ⟂ BD [01] & AB ∥ DE [05] & BD ∥ AE [06] ⇒  ED ⟂ AE [07]
002. A,G,F are collinear [04] & BC ⟂ AF [02] ⇒  BC ⟂ AG [08]
003. ED ⟂ AE [07] & BC ⟂ AG [08] ⇒  ∠(ED-AG) = ∠(AE-BC) [09]
004. ED ⟂ AE [07] & BC ⟂ AG [08] ⇒  ∠(ED-BC) = ∠EAG [10]
005. A,G,F are collinear [04] & ∠(ED-AG) = ∠(AE-BC) [09] & AB ∥ DE [05] & AE ∥ BD [06] ⇒  ∠DBC = ∠BAG [11]
006. AB = BD [00] & GA = BC [03] & ∠DBC = ∠BAG [11] (SAS)⇒  ∠DCB = ∠BGA [12]
007. AB = BD [00] & GA = BC [03] & ∠DBC = ∠BAG [11] (SAS)⇒  ∠ABD = ∠(BG-CD) [13]
008. ∠DCB = ∠BGA [12] & A,G,F are collinear [04] & ∠(ED-BC) = ∠EAG [10] & AB ∥ DE [05] & AE ∥ BD [06] & ∠ABD = ∠(BG-CD) [13] ⇒  GB ⟂ CD
==========================

 

 

37. examples/complete2/000/complete_016_ex-gao_gao_M_M020-52.gex

a b = segment a b; c = on_circle c a b; d = on_circle d a b; e = on_circle e a b, on_pline e d b c ? cong d c e b

 

○ 번역 

 

선분 AB가 주어져 있습니다. 점 C, D, E는 모두 A를 중심으로 하고 B를 지나는 원 위에 있습니다. 선분 ED와 선분 BC는 평행합니다. 선분 DC와 선분 EB의 길이가 같음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E : Points
AC = AB [00]
AD = AB [01]
AE = AB [02]
ED ∥ BC [03]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AD = AB [01] & AE = AB [02] & AC = AB [00] ⇒  B,C,E,D are concyclic [04]
002. BC ∥ DE [03] ⇒  ∠BCE = ∠DEC [05]
003. B,C,E,D are concyclic [04] & ∠BCE = ∠DEC [05] ⇒  BE = DC
==========================

 

 

38. examples/complete2/000/complete_010_Other_gao_L_L190-7.gex

a b = segment a b; c = nsquare c b a; d = psquare d a b; e = on_line e b d; f = foot f e b c; g = foot g e d c ? cong e a g f

 

○ 번역 : 추후 업데이트 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D E F G : Points
BC ⟂ AB [00]
CB = BA [01]
DA = AB [02]
AB ⟂ DA [03]
D,E,B are collinear [04]
F,C,B are collinear [05]
BC ⟂ FE [06]
G,D,C are collinear [07]
EG ⟂ CD [08]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. C,F,B are collinear [05] & G,D,C are collinear [07] & EG ⟂ CD [08] & BC ⟂ AB [00] & BC ⟂ FE [06] ⇒  ∠CFE = ∠CGE [09]
002. ∠CFE = ∠CGE [09] ⇒  G,E,C,F are concyclic [10]
003. DA = AB [02] & CB = BA [01] ⇒  CB = AD [11]
004. AB ⟂ DA [03] & BC ⟂ AB [00] ⇒  ∠CBD = ∠ADB [12]
005. CB = AD [11] & ∠CBD = ∠ADB [12] (SAS)⇒  ∠(BC-AD) = ∠(CD-AB) [13]
006. G,D,C are collinear [07] & BC ⟂ FE [06] & BC ⟂ AB [00] & ∠(BC-AD) = ∠(CD-AB) [13] & AB ⟂ DA [03] ⇒  ∠GEF = ∠EGC [14]
007. G,E,C,F are concyclic [10] & ∠GEF = ∠EGC [14] ⇒  GF = EC [15]
008. DA = AB [02] ⇒  ∠ADB = ∠DBA [16]
009. D,E,B are collinear [04] & ∠ADB = ∠DBA [16] & AB ⟂ DA [03] & BC ⟂ AB [00] ⇒  ∠CBE = ∠EBA [17]
010. CB = BA [01] & ∠CBE = ∠EBA [17] (SAS)⇒  EC = EA [18]
011. GF = EC [15] & EC = EA [18] ⇒  EA = GF
==========================

 

 

39. examples/complete2/000/complete_007_7_Book_LLL_L017-11.gex

c a = segment c a; b = on_tline b c c a; d = foot d c a b ? eqangle a c a d c b c d

 

○ 번역 

 

선분 CA가 주어져 있습니다. 점 B는 C를 지나고 선분 CA에 수직인 직선 위에 있습니다. 점 D는 점 C에서 선분 AB에 내린 수선의 발입니다. ∠CAD = ∠ABD임을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

==========================
 * From theorem premises:
A B C D : Points
AC ⟂ AB [00]
B,D,C are collinear [01]
AD ⟂ BC [02]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. B,D,C are collinear [01] & BC ⟂ AD [02] ⇒  BD ⟂ AD [03]
002. BD ⟂ AD [03] & AC ⟂ AB [00] ⇒  ∠DBA = ∠DAC
==========================

 

 

40. examples/complete2/000/complete_016_ex-gao_gao_M_M024-94.gex

a b c = triangle a b c; d = on_circle d a b, on_circle d c b; e = on_line e d a, on_circle e a d; f = on_line f d c, on_circle f c d ? coll e b f

 

○ 번역 

 

삼각형 ABC가 주어져 있습니다. 점 D는 A를 중심으로 하고 B를 지나는 원과 C를 중심으로 하고 B를 지나는 원의 교점입니다. 점 E는 직선 DA 위에 있으며, A를 중심으로 하고 D를 지나는 원 위에 있습니다. 점 F는 직선 DC 위에 있으며, C를 중심으로 하고 D를 지나는 원 위에 있습니다. 점 E, B, F가 한 직선 위에 있음을 증명하시오.

 

○ 풀이 : AlphaGeometry를 사용한 풀이

 

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

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. CD = CB [00] & CF = CD [04] ⇒  C is the circumcenter of \Delta FBD [06]
002. C is the circumcenter of \Delta FBD [06] & D,C,F are collinear [05] ⇒  BD ⟂ FB [07]
003. AD = AB [01] & AE = AD [02] ⇒  A is the circumcenter of \Delta EBD [08]
004. A is the circumcenter of \Delta EBD [08] & D,E,A are collinear [03] ⇒  BE ⟂ BD [09]
005. BD ⟂ FB [07] & BE ⟂ BD [09] ⇒  E,B,F are collinear
==========================

 

입력: 2024.08.07 13:24