【국제수학올림피아드】 IMO 기하 문제 풀이 (2015년 ~ 2019년)

IMO 기하 문제 풀이 (2015년 ~ 2019년)

 

추천글 : 【기하학】 IMO 기하 문제 풀이 종합 

---

 

IMO 2015, Problem 3. Let ABC be an acute triangle with AB > AC. Let Γ be its circumcircle, H its orthocenter, and F the foot of the altitude from A. Let M be the midpoint of BC. Let Q be the point on Γ such that ∠HQA = 90° and let K be the point on Γ such that ∠HKQ = 90°. Assume that the points A, B, C, K and Q are all different and lie on Γ in this order. Prove that the circumcircles of triangles KQH and FKM are tangent to each other.

 

○ 풀이. 추후 업데이트

 

 

IMO 2015, Problem 4. Triangle ABC has circumcircle Ω and circumcenter O. A circle Γ with center A intersects the segment BC at points D and E, such that B, D, E, and C are all different and lie on line BC in this order. Let F and G be the points of intersection of Γ and Ω, such that A, F, B, C, and G lie on Ω in this order. Let K = (BDF) ∩ AB ≠ B and L = (CGE) ∩ AC ≠ C and assume these points do not lie on line FG. Define X = FK ∩ GL. Prove that X lies on the line AO.

 

○ 풀이. AlphaGeometry (DDAR mode)

 

==========================
 * From theorem premises:
A B C O D E F G O1 O2 K L X : Points
OA = OB [00]
OB = OC [01]
C,D,B are collinear [02]
C,E,B are collinear [03]
AE = AD [04]
AF = AD [05]
OF = OA [06]
AG = AD [07]
OG = OA [08]
O_1F = O_1B [09]
O_1B = O_1D [10]
O_2G = O_2C [11]
O_2C = O_2E [12]
O_1K = O_1B [13]
A,B,K are collinear [14]
O_2L = O_2C [15]
C,A,L are collinear [16]
X,K,F are collinear [17]
X,G,L are collinear [18]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AG = AD [07] & AF = AD [05] ⇒  AF = AG [19]
002. O_2G = O_2C [11] & O_2L = O_2C [15] & O_2C = O_2E [12] ⇒  C,G,E,L are concyclic [20]
003. C,G,E,L are concyclic [20] ⇒  ∠CEG = ∠CLG [21]
004. C,D,B are collinear [02] & X,G,L are collinear [18] & ∠CEG = ∠CLG [21] & C,E,B are collinear [03] & C,A,L are collinear [16] ⇒  ∠ACD = ∠XGE [22]
005. AE = AD [04] & AG = AD [07] & AF = AD [05] ⇒  D,G,E,F are concyclic [23]
006. D,G,E,F are concyclic [23] ⇒  ∠DEG = ∠DFG [24]
007. C,D,B are collinear [02] & ∠DEG = ∠DFG [24] & C,E,B are collinear [03] ⇒  ∠FDC = ∠FGE [25]
008. ∠ACD = ∠XGE [22] & ∠FDC = ∠FGE [25] ⇒  ∠(CA-DF) = ∠XGF [26]
009. O_1F = O_1B [09] & O_1K = O_1B [13] & O_1B = O_1D [10] ⇒  D,K,B,F are concyclic [27]
010. D,K,B,F are concyclic [27] ⇒  ∠DKB = ∠DFB [28]
011. D,K,B,F are concyclic [27] ⇒  ∠DKF = ∠DBF [29]
012. OA = OB [00] & OG = OA [08] & OF = OA [06] ⇒  A,G,B,F are concyclic [30]
013. G,A,B,F are concyclic [30] ⇒  ∠AGF = ∠ABF [31]
014. AF = AG [19] ⇒  ∠GFA = ∠AGF [32]
015. A,G,B,F are concyclic [30] & OB = OC [01] & OA = OB [00] & OF = OA [06] ⇒  G,A,C,F are concyclic [33]
016. A,G,B,F are concyclic [30] & OB = OC [01] & OA = OB [00] & OF = OA [06] ⇒  G,B,C,F are concyclic [34]
017. G,A,C,F are concyclic [33] ⇒  ∠GCA = ∠GFA [35]
018. ∠DKB = ∠DFB [28] & A,B,K are collinear [14] & ∠AGF = ∠ABF [31] & ∠GFA = ∠AGF [32] & ∠GCA = ∠GFA [35] ⇒  ∠GCA = ∠KDF [36]
019. G,B,C,F are concyclic [34] ⇒  ∠CGF = ∠CBF [37]
020. X,K,F are collinear [17] & ∠CGF = ∠CBF [37] & ∠DKF = ∠DBF [29] & C,D,B are collinear [02] ⇒  ∠DKX = ∠CGF [38]
021. ∠GCA = ∠KDF [36] & ∠DKX = ∠CGF [38] ⇒  ∠(DF-XK) = ∠(CA-GF) [39]
022. X,K,F are collinear [17] & X,G,L are collinear [18] & ∠(CA-DF) = ∠XGF [26] & ∠(DF-XK) = ∠(CA-GF) [39] ⇒  ∠XFG = ∠FGX [40]
023. ∠XFG = ∠FGX [40] ⇒  XF = XG [41]
024. AF = AG [19] & XF = XG [41] ⇒  FG ⟂ AX [42]
025. OF = OA [06] & OG = OA [08] ⇒  OG = OF [43]
026. OG = OF [43] & AF = AG [19] ⇒  FG ⟂ AO [44]
027. FG ⟂ AX [42] & FG ⟂ AO [44] ⇒  X,O,A are collinear
==========================

 

○ 풀이. AlphaGeometry (AlphaGeometry mode)

 

==========================
 * From theorem premises:
A B C D E F G H I J K L M : Points
DA = DB [00]
DB = DC [01]
E,B,C are collinear [02]
F,B,C are collinear [03]
AF = AE [04]
AG = AE [05]
DG = DA [06]
AH = AE [07]
DH = DA [08]
IG = IB [09]
IB = IE [10]
JC = JF [11]
JH = JC [12]
IK = IB [13]
B,A,K are collinear [14]
L,A,C are collinear [15]
JL = JC [16]
G,K,M are collinear [17]
H,M,L are collinear [18]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AH = AE [07] & AG = AE [05] ⇒  AG = AH [19]
002. JC = JF [11] & JL = JC [16] & JH = JC [12] ⇒  F,L,H,C are concyclic [20]
003. F,L,H,C are concyclic [20] ⇒  ∠FHL = ∠FCL [21]
004. C,A,L are collinear [15] & E,C,B are collinear [02] & H,L,M are collinear [18] & ∠FHL = ∠FCL [21] & F,B,C are collinear [03] ⇒  ∠(LA-EB) = ∠MHF [22]
005. AG = AE [05] & AH = AE [07] & AF = AE [04] ⇒  F,E,G,H are concyclic [23]
006. F,E,G,H are concyclic [23] ⇒  ∠FEG = ∠FHG [24]
007. E,C,B are collinear [02] & ∠FEG = ∠FHG [24] & F,B,C are collinear [03] ⇒  ∠GEB = ∠GHF [25]
008. ∠(LA-EB) = ∠MHF [22] & ∠GEB = ∠GHF [25] ⇒  ∠(LA-GE) = ∠MHG [26]
009. IG = IB [09] & IK = IB [13] & IB = IE [10] ⇒  E,B,G,K are concyclic [27]
010. E,B,G,K are concyclic [27] ⇒  ∠EBG = ∠EKG [28]
011. E,B,G,K are concyclic [27] ⇒  ∠EGB = ∠EKB [29]
012. DA = DB [00] & DH = DA [08] & DG = DA [06] ⇒  H,G,A,B are concyclic [30]
013. DA = DB [00] & DG = DA [06] & DB = DC [01] & H,G,A,B are concyclic [30] ⇒  H,G,A,C are concyclic [31]
014. H,G,A,B are concyclic [30] & H,G,A,C are concyclic [31] ⇒  C,G,B,H are concyclic [32]
015. C,G,B,H are concyclic [32] ⇒  ∠CBG = ∠CHG [33]
016. ∠EBG = ∠EKG [28] & E,B,C are collinear [02] & ∠CBG = ∠CHG [33] ⇒  ∠CHG = ∠EKG [34]
017. G,B,H,A are concyclic [30] ⇒  ∠ABG = ∠AHG [35]
018. AG = AH [19] ⇒  ∠HGA = ∠AHG [36]
019. C,G,H,A are concyclic [31] ⇒  ∠HCA = ∠HGA [37]
020. C,A,L are collinear [15] & ∠EGB = ∠EKB [29] & B,A,K are collinear [14] & ∠ABG = ∠AHG [35] & ∠HGA = ∠AHG [36] & ∠HCA = ∠HGA [37] ⇒  ∠(HC-LA) = ∠KEG [38]
021. ∠CHG = ∠EKG [34] & ∠(HC-LA) = ∠KEG [38] ⇒  ∠(HG-LA) = ∠KGE [39]
022. G,K,M are collinear [17] & H,L,M are collinear [18] & ∠(LA-GE) = ∠MHG [26] & L,A,C are collinear [15] & ∠(HG-LA) = ∠KGE [39] ⇒  ∠MGH = ∠GHM [40]
023. ∠MGH = ∠GHM [40] ⇒  MG = MH [41]
024. AG = AH [19] & MG = MH [41] ⇒  GH ⟂ AM [42]
025. DH = DA [08] & DG = DA [06] ⇒  DG = DH [43]
026. DG = DH [43] & AG = AH [19] ⇒  GH ⟂ AD [44]
027. GH ⟂ AM [42] & GH ⟂ AD [44] ⇒  A,D,M are collinear
==========================

 

 

IMO 2016, Problem 1. In convex pentagon ABCDE with ∠B > 90°, let F be a point on AC such that ∠FBC = 90°. It is given that FA = FB, DA = DC, EA = ED, and rays AC and AD trisect ∠BAE. Let M be the midpoint of CF. Let X be the point such that AMXE is a parallelogram. Show that FX, EM, BD are concurrent.

 

○ 풀이. AlphaGeometry (DDAR mode)

 

==========================
 * From theorem premises:
A B Z F C D E M X Y : Points
∠BAF = ∠FBA [00]
∠BAF = ∠FAZ [01]
FA = FB [02]
F,A,C are collinear [03]
BC ⟂ BF [04]
Z,A,D are collinear [05]
∠DAC = ∠ACD [06]
DA = DC [07]
∠DAE = ∠EDA [08]
∠CAD = ∠DAE [09]
EA = ED [10]
F,M,C are collinear [11]
MC = MF [12]
EX ∥ AM [13]
EA ∥ MX [14]
E,M,Y are collinear [15]
F,X,Y are collinear [16]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. F,M,C are collinear [11] & F,A,C are collinear [03] & EX ∥ AM [13] ⇒  FM ∥ XE [17]
002. FM ∥ XE [17] & E,M,Y are collinear [15] & F,X,Y are collinear [16] ⇒  MY:FM = EY:XE [18]
003. F,M,C are collinear [11] & F,A,C are collinear [03] & EX ∥ AM [13] ⇒  ∠XEM = ∠AME [19]
004. MX ∥ AE [14] ⇒  ∠XME = ∠AEM [20]
005. ∠XEM = ∠AME [19] & ∠XME = ∠AEM [20] (Similar Triangles)⇒  EX = MA [21]
006. F,A,C are collinear [03] & Z,A,D are collinear [05] & ∠DAE = ∠EDA [08] & ∠CAD = ∠DAE [09] ⇒  ∠FAZ = ∠(ED-ZA) [22]
007. ∠FAZ = ∠(ED-ZA) [22] ⇒  FA ∥ ED [23]
008. EX ∥ AM [13] & F,M,C are collinear [11] & F,A,C are collinear [03] & FA ∥ ED [23] ⇒  ED ∥ EX [24]
009. ED ∥ EX [24] ⇒  X,E,D are collinear [25]
010. ∠BAF = ∠FBA [00] & ∠BAF = ∠FAZ [01] & ∠DAC = ∠ACD [06] & Z,A,D are collinear [05] & F,A,C are collinear [03] ⇒  ∠DCA = ∠FBA [26]
011. F,A,C are collinear [03] & ∠DAC = ∠ACD [06] & Z,A,D are collinear [05] & ∠BAF = ∠FAZ [01] ⇒  ∠BAF = ∠(DC-FA) [27]
012. ∠BAF = ∠(DC-FA) [27] ⇒  AB ∥ DC [28]
013. X,D,E are collinear [25] & ∠ABF = ∠ACD [26] & AB ∥ CD [28] & FA ∥ ED [23] & F,A,C are collinear [03] ⇒  ∠(DC-FB) = ∠(XE-DC) [29]
014. F,A,C are collinear [03] & ∠FAB = ∠ZAF [01] & Z,A,D are collinear [05] ⇒  ∠FAB = ∠DAC [30]
015. F,A,C are collinear [03] & ∠FAB = ∠ZAF [01] & Z,A,D are collinear [05] ⇒  ∠FAD = ∠BAC [31]
016. ∠FBA = ∠DCA [26] & ∠FAB = ∠DAC [30] (Similar Triangles)⇒  FB:DC = AB:AC [32]
017. FB:DC = AB:AC [32] & FA = FB [02] & AD = DC [07] ⇒  AF:AD = AB:AC [33]
018. AF:AD = AB:AC [33] & ∠FAD = ∠BAC [31] (Similar Triangles)⇒  ∠AFD = ∠ABC [34]
019. AF:AD = AB:AC [33] & ∠FAD = ∠BAC [31] (Similar Triangles)⇒  FA:FD = BA:BC [35]
020. X,D,E are collinear [25] & ∠AFD = ∠ABC [34] & F,A,C are collinear [03] & AB ∥ CD [28] & FA ∥ ED [23] ⇒  ∠DCB = ∠(XE-FD) [36]
021. ∠(DC-FB) = ∠(XE-DC) [29] & ∠DCB = ∠(XE-FD) [36] ⇒  ∠CDF = ∠FBC [37]
022. ∠AFD = ∠ABC [34] & F,A,C are collinear [03] & ∠BAF = ∠FBA [00] & AB ∥ CD [28] ⇒  ∠(FB-DC) = ∠(CB-FD) [38]
023. BC ⟂ BF [04] & ∠(FB-DC) = ∠(CB-FD) [38] ⇒  ∠CBF = ∠CDF [39]
024. BC ⟂ BF [04] & ∠(FB-DC) = ∠(CB-FD) [38] ⇒  ∠BCD = ∠BFD [40]
025. ∠CDF = ∠FBC [37] & AB ∥ CD [28] & ∠CBF = ∠CDF [39] ⇒  DC ⟂ FD [41]
026. M,C,F are collinear [11] & MC = MF [12] ⇒  M is midpoint of CF [42]
027. DC ⟂ FD [41] & M is midpoint of CF [42] ⇒  FM = DM [43]
028. ∠DAE = ∠EDA [08] & ∠CAD = ∠DAE [09] & F,A,C are collinear [03] & Z,A,D are collinear [05] & ∠BAF = ∠FAZ [01] & ∠BAF = ∠FBA [00] ⇒  ∠FBA = ∠EDA [44]
029. ∠CAD = ∠DAE [09] & F,A,C are collinear [03] & Z,A,D are collinear [05] & ∠FAB = ∠ZAF [01] ⇒  ∠FAB = ∠EAD [45]
030. ∠FBA = ∠EDA [44] & ∠FAB = ∠EAD [45] (Similar Triangles)⇒  BF:DE = BA:DA [46]
031. BF:DE = BA:DA [46] & DA = DC [07] & FA = FB [02] & AE = ED [10] ⇒  AF:AE = AB:AD [47]
032. F,A,C are collinear [03] & Z,A,D are collinear [05] & ∠DCA = ∠CAD [06] ⇒  ∠(DC-FA) = ∠FAZ [48]
033. F,A,C are collinear [03] & Z,A,D are collinear [05] & ∠CAD = ∠DAE [09] & AE ∥ MX [14] ⇒  ∠FAZ = ∠(ZA-XM) [49]
034. ∠(DC-FA) = ∠FAZ [48] & ∠FAZ = ∠(ZA-XM) [49] ⇒  ∠(DC-ZA) = ∠(FA-XM) [50]
035. F,A,C are collinear [03] & ∠(DC-ZA) = ∠(FA-XM) [50] & Z,A,D are collinear [05] & AB ∥ CD [28] & AE ∥ MX [14] ⇒  ∠FAE = ∠BAD [51]
036. AF:AE = AB:AD [47] & ∠FAE = ∠BAD [51] (Similar Triangles)⇒  ∠AFE = ∠ABD [52]
037. FA:FD = BA:BC [35] & FA = FB [02] ⇒  FB:FD = AB:CB [53]
038. ∠BCD = ∠BFD [40] & AB ∥ CD [28] ⇒  ∠CBA = ∠BFD [54]
039. FB:FD = AB:CB [53] & ∠CBA = ∠BFD [54] (Similar Triangles)⇒  ∠(BF-AC) = ∠DBA [55]
040. FB:FD = AB:CB [53] & ∠CBA = ∠BFD [54] (Similar Triangles)⇒  ∠CBD = ∠(AC-DF) [56]
041. FB:FD = AB:CB [53] & ∠CBA = ∠BFD [54] (Similar Triangles)⇒  ∠FBD = ∠CAB [57]
042. BC ⟂ BF [04] & M is midpoint of CF [42] ⇒  FM = BM [58]
043. BC ⟂ BF [04] & M is midpoint of CF [42] ⇒  CM = BM [59]
044. FM = BM [58] ⇒  ∠MBF = ∠BFM [60]
045. F,A,C are collinear [03] & ∠AFE = ∠ABD [52] & ∠(BF-AC) = ∠DBA [55] & ∠MBF = ∠BFM [60] & F,M,C are collinear [11] ⇒  ∠MBF = ∠EFA [61]
046. ∠BAF = ∠FAZ [01] & ∠BAF = ∠FBA [00] ⇒  ∠FBA = ∠FAZ [62]
047. F,A,C are collinear [03] & Z,A,D are collinear [05] & ∠BAF = ∠DAE [45] & AE ∥ MX [14] ⇒  ∠BAF = ∠(ZA-XM) [63]
048. ∠FBA = ∠FAZ [62] & ∠BAF = ∠(ZA-XM) [63] ⇒  ∠BFA = ∠(FA-XM) [64]
049. F,M,C are collinear [11] & F,A,C are collinear [03] & ∠BFA = ∠(FA-XM) [64] & AE ∥ MX [14] ⇒  ∠MFB = ∠EAF [65]
050. ∠MBF = ∠EFA [61] & ∠MFB = ∠EAF [65] (Similar Triangles)⇒  FB:AF = FM:AE [66]
051. FM = DM [43] & FB:AF = FM:AE [66] & FA = FB [02] & EA = ED [10] ⇒  DE = DM [67]
052. F,A,C are collinear [03] & ∠AFD = ∠ABC [34] & ∠CBA = ∠BFD [54] ⇒  ∠BFD = ∠DFA [68]
053. FA = FB [02] & ∠BFD = ∠DFA [68] (SAS)⇒  DB = DA [69]
054. FA = FB [02] & ∠BFD = ∠DFA [68] (SAS)⇒  ∠FBD = ∠DAF [70]
055. DB = DA [69] & DA = DC [07] ⇒  DC = DB [71]
056. DC = DB [71] & CM = BM [59] ⇒  CB ⟂ DM [72]
057. ∠FBD = ∠DAF [70] & F,A,C are collinear [03] & FA ∥ ED [23] & CB ⟂ DM [72] & BC ⟂ BF [04] ⇒  ∠EDB = ∠ADM [73]
058. DE = DM [67] & DB = DA [69] & ∠EDB = ∠ADM [73] (SAS)⇒  BE = AM [74]
059. EY:XE = MY:FM [18] & EX = MA [21] & BE = AM [74] & DM = FM [43] ⇒  EY:EB = MY:MD [75]
060. X,D,E are collinear [25] & ∠AFE = ∠ABD [52] & F,A,C are collinear [03] & AB ∥ CD [28] & FA ∥ ED [23] ⇒  ∠CDB = ∠XEF [76]
061. ∠CDB = ∠XEF [76] & ∠DCB = ∠(XE-FD) [36] ⇒  ∠CBD = ∠DFE [77]
062. ∠AFD = ∠ABC [34] & F,A,C are collinear [03] & ∠CBD = ∠(AC-DF) [56] & ∠CBD = ∠DFE [77] & AB ∥ CD [28] ⇒  ∠DFE = ∠DCB [78]
063. ∠DFE = ∠DCB [78] & DC ⟂ FD [41] ⇒  CB ⟂ FE [79]
064. ∠(DC-FB) = ∠(XE-DC) [29] & ∠CDB = ∠XEF [76] ⇒  ∠(CD-EF) = ∠FBD [80]
065. ∠(CD-EF) = ∠FBD [80] & AB ∥ CD [28] & ∠FBD = ∠CAB [57] & F,A,C are collinear [03] & ∠BAF = ∠FBA [00] ⇒  ∠(FB-DC) = ∠(FE-DC) [81]
066. ∠(FB-DC) = ∠(FE-DC) [81] ⇒  FB ∥ FE [82]
067. BF ∥ EF [82] ⇒  F,E,B are collinear [83]
068. E,M,Y are collinear [15] & CB ⟂ FE [79] & BC ⟂ DM [72] & BF ∥ EF [82] & F,E,B are collinear [83] ⇒  ∠YEB = ∠YMD [84]
069. EY:EB = MY:MD [75] & ∠YEB = ∠YMD [84] (Similar Triangles)⇒  ∠EYB = ∠MYD [85]
070. ∠EYB = ∠MYD [85] & E,M,Y are collinear [15] ⇒  BY ∥ DY [86]
071. BY ∥ DY [86] ⇒  Y,D,B are collinear
==========================

 

○ 풀이. AlphaGeometry (AlphaGeometry mode)

 

==========================
 * From theorem premises:
A B C D E F G H I J : Points
∠BAD = ∠DBA [00]
∠BAD = ∠DAC [01]
DA = DB [02]
E,A,D are collinear [03]
BE ⟂ BD [04]
C,F,A are collinear [05]
FA = FE [06]
∠FAE = ∠AEF [07]
GA = GF [08]
∠EAF = ∠FAG [09]
∠GAF = ∠AFG [10]
H,E,D are collinear [11]
HE = HD [12]
GI ∥ AH [13]
GA ∥ HI [14]
H,G,J are collinear [15]
D,I,J are collinear [16]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. H,E,D are collinear [11] & E,A,D are collinear [03] & GI ∥ AH [13] ⇒  GI ∥ HD [17]
002. GI ∥ HD [17] & H,G,J are collinear [15] & D,I,J are collinear [16] ⇒  GJ:GI = HJ:HD [18]
003. H,E,D are collinear [11] & E,A,D are collinear [03] & GI ∥ AH [13] ⇒  ∠AHG = ∠IGH [19]
004. AG ∥ HI [14] ⇒  ∠AGH = ∠IHG [20]
005. ∠AHG = ∠IGH [19] & ∠AGH = ∠IHG [20] (Similar Triangles)⇒  HA = GI [21]
006. C,F,A are collinear [05] & ∠BAD = ∠DBA [00] & ∠BAD = ∠DAC [01] & ∠EAF = ∠FAG [09] & E,A,D are collinear [03] & ∠GAF = ∠AFG [10] ⇒  ∠GFA = ∠DBA [22]
007. C,F,A are collinear [05] & ∠DAB = ∠CAD [01] & ∠EAF = ∠FAG [09] & E,A,D are collinear [03] ⇒  ∠GAF = ∠DAB [23]
008. ∠GFA = ∠DBA [22] & ∠GAF = ∠DAB [23] (Similar Triangles)⇒  FG:BD = FA:BA [24]
009. FG:BD = FA:BA [24] & FA = FE [06] & GA = GF [08] & AD = DB [02] ⇒  AF:AB = AG:AD [25]
010. C,F,A are collinear [05] & ∠BAD = ∠DAC [01] & ∠EAF = ∠FAG [09] & E,A,D are collinear [03] & ∠GAF = ∠AFG [10] & GI ∥ AH [13] & H,E,D are collinear [11] ⇒  ∠GFC = ∠(AB-GI) [26]
011. C,F,A are collinear [05] & ∠EAF = ∠FAG [09] & E,A,D are collinear [03] & AG ∥ HI [14] & GI ∥ AH [13] & H,E,D are collinear [11] ⇒  ∠(CF-HI) = ∠(GI-CF) [27]
012. ∠GFC = ∠(AB-GI) [26] & ∠(CF-HI) = ∠(GI-CF) [27] ⇒  ∠(GF-HI) = ∠(AB-CF) [28]
013. C,F,A are collinear [05] & ∠GAF = ∠AFG [10] & ∠EAF = ∠FAG [09] & E,A,D are collinear [03] & GI ∥ AH [13] & H,E,D are collinear [11] ⇒  ∠(GI-CF) = ∠GFC [29]
014. ∠(GI-CF) = ∠GFC [29] ⇒  GI ∥ GF [30]
015. C,F,A are collinear [05] & ∠(GF-HI) = ∠(AB-CF) [28] & AG ∥ HI [14] & GI ∥ FG [30] & GI ∥ AH [13] & H,E,D are collinear [11] & E,A,D are collinear [03] ⇒  ∠FAB = ∠GAD [31]
016. AF:AB = AG:AD [25] & ∠FAB = ∠GAD [31] (Similar Triangles)⇒  ∠FBA = ∠GDA [32]
017. E,A,D are collinear [03] & ∠BAD = ∠DBA [00] & ∠BAD = ∠DAC [01] & ∠FAE = ∠AEF [07] & C,F,A are collinear [05] ⇒  ∠FEA = ∠DBA [33]
018. C,F,A are collinear [05] & E,A,D are collinear [03] & ∠CAD = ∠DAB [01] ⇒  ∠FAE = ∠DAB [34]
019. C,F,A are collinear [05] & E,A,D are collinear [03] & ∠CAD = ∠DAB [01] ⇒  ∠EAB = ∠FAD [35]
020. ∠FEA = ∠DBA [33] & ∠FAE = ∠DAB [34] (Similar Triangles)⇒  EF:DB = EA:AB [36]
021. EA:AB = EF:DB [36] & FA = EF [06] & AD = DB [02] ⇒  AE:AB = AF:AD [37]
022. AE:AB = AF:AD [37] & ∠EAB = ∠FAD [35] (Similar Triangles)⇒  BE:BA = DF:DA [38]
023. AE:AB = AF:AD [37] & ∠EAB = ∠FAD [35] (Similar Triangles)⇒  ∠(BE-DF) = ∠BAD [39]
024. AE:AB = AF:AD [37] & ∠EAB = ∠FAD [35] (Similar Triangles)⇒  ∠EBA = ∠FDA [40]
025. BE:BA = DF:DA [38] & DA = DB [02] ⇒  EB:AB = FD:DB [41]
026. ∠FAE = ∠AEF [07] & C,F,A are collinear [05] & E,A,D are collinear [03] & ∠BAD = ∠DAC [01] & GI ∥ AH [13] & H,E,D are collinear [11] ⇒  ∠(AB-GI) = ∠(EF-GI) [42]
027. ∠(AB-GI) = ∠(EF-GI) [42] ⇒  AB ∥ EF [43]
028. ∠(BE-DF) = ∠BAD [39] & ∠BAD = ∠DBA [00] & AB ∥ EF [43] ⇒  ∠(DB-EF) = ∠(EB-FD) [44]
029. BE ⟂ BD [04] & ∠(DB-EF) = ∠(EB-FD) [44] ⇒  ∠BEF = ∠BDF [45]
030. BE ⟂ BD [04] & ∠(DB-EF) = ∠(EB-FD) [44] ⇒  ∠EBD = ∠EFD [46]
031. ∠BEF = ∠BDF [45] & AB ∥ EF [43] ⇒  ∠EBA = ∠BDF [47]
032. EB:AB = FD:DB [41] & ∠EBA = ∠BDF [47] (Similar Triangles)⇒  ∠FBD = ∠BAE [48]
033. H,E,D are collinear [11] & HE = HD [12] ⇒  H is midpoint of ED [49]
034. BE ⟂ BD [04] & H is midpoint of ED [49] ⇒  DH = BH [50]
035. BE ⟂ BD [04] & H is midpoint of ED [49] ⇒  EH = BH [51]
036. DH = BH [50] ⇒  ∠HBD = ∠BDH [52]
037. ∠FBA = ∠GDA [32] & GI ∥ FG [30] & GI ∥ AH [13] & H,E,D are collinear [11] & E,A,D are collinear [03] & ∠FBD = ∠BAE [48] & ∠HBD = ∠BDH [52] ⇒  ∠HBD = ∠GDA [53]
038. C,F,A are collinear [05] & ∠BAD = ∠DBA [00] & ∠BAD = ∠DAC [01] & ∠EAF = ∠FAG [09] & E,A,D are collinear [03] & ∠GAF = ∠AFG [10] ⇒  ∠GFC = ∠DBA [54]
039. C,F,A are collinear [05] & ∠DAB = ∠CAD [01] & ∠EAF = ∠FAG [09] & E,A,D are collinear [03] & AG ∥ HI [14] & GI ∥ AH [13] & H,E,D are collinear [11] ⇒  ∠(CF-HI) = ∠(AB-GI) [55]
040. ∠GFC = ∠DBA [54] & ∠(CF-HI) = ∠(AB-GI) [55] ⇒  ∠(FG-HI) = ∠(BD-GI) [56]
041. H,E,D are collinear [11] & E,A,D are collinear [03] & ∠(FG-HI) = ∠(BD-GI) [56] & AG ∥ HI [14] & GI ∥ FG [30] & GI ∥ AH [13] ⇒  ∠HDB = ∠GAD [57]
042. ∠HBD = ∠GDA [53] & ∠HDB = ∠GAD [57] (Similar Triangles)⇒  DB:AD = DH:AG [58]
043. ∠DAB = ∠ABD [00] & GI ∥ FG [30] & GI ∥ AH [13] & H,E,D are collinear [11] & E,A,D are collinear [03] & AB ∥ EF [43] ⇒  ∠GFE = ∠(EF-DB) [59]
044. ∠EBA = ∠FDA [40] & GI ∥ FG [30] & GI ∥ AH [13] & H,E,D are collinear [11] & E,A,D are collinear [03] & AB ∥ EF [43] ⇒  ∠GFD = ∠FEB [60]
045. ∠GFE = ∠(EF-DB) [59] & ∠GFD = ∠FEB [60] ⇒  ∠DBE = ∠EFD [61]
046. ∠DBE = ∠EFD [61] & AB ∥ EF [43] & ∠EBD = ∠EFD [46] ⇒  EF ⟂ FD [62]
047. EF ⟂ FD [62] & H is midpoint of ED [49] ⇒  DH = FH [63]
048. GA = GF [08] & DB:AD = DH:AG [58] & DA = DB [02] & DH = FH [63] ⇒  FH = FG [64]
049. ∠ABE = ∠FDB [47] & ∠EBA = ∠FDA [40] & GI ∥ FG [30] & GI ∥ AH [13] & H,E,D are collinear [11] & E,A,D are collinear [03] ⇒  ∠ADF = ∠FDB [65]
050. DA = DB [02] & ∠ADF = ∠FDB [65] (SAS)⇒  FA = FB [66]
051. DA = DB [02] & ∠ADF = ∠FDB [65] (SAS)⇒  ∠DAF = ∠FBD [67]
052. FA = FE [06] & FA = FB [66] ⇒  FB = FE [68]
053. FB = FE [68] & EH = BH [51] ⇒  BE ⟂ FH [69]
054. C,F,A are collinear [05] & ∠DAF = ∠FBD [67] & GI ∥ FG [30] & GI ∥ AH [13] & H,E,D are collinear [11] & E,A,D are collinear [03] & BE ⟂ FH [69] & BE ⟂ BD [04] ⇒  ∠HFA = ∠BFG [70]
055. FH = FG [64] & FA = FB [66] & ∠HFA = ∠BFG [70] (SAS)⇒  AH = BG [71]
056. GJ:GI = HJ:HD [18] & HA = GI [21] & AH = BG [71] & HF = HD [63] ⇒  GJ:GB = HJ:HF [72]
057. ∠FBA = ∠GDA [32] & GI ∥ FG [30] & GI ∥ AH [13] & H,E,D are collinear [11] & E,A,D are collinear [03] & AB ∥ EF [43] ⇒  ∠FGD = ∠EFB [73]
058. ∠GFE = ∠(EF-DB) [59] & ∠FGD = ∠EFB [73] ⇒  ∠DBF = ∠(EF-DG) [74]
059. ∠DBF = ∠(EF-DG) [74] & AB ∥ EF [43] & ∠FBD = ∠BAE [48] & E,A,D are collinear [03] & ∠BAD = ∠DBA [00] ⇒  ∠(DB-EF) = ∠(GD-EF) [75]
060. ∠(DB-EF) = ∠(GD-EF) [75] ⇒  DB ∥ GD [76]
061. BD ∥ DG [76] ⇒  G,D,B are collinear [77]
062. H,G,J are collinear [15] & G,D,B are collinear [77] & BE ⟂ FH [69] & BE ⟂ BD [04] ⇒  ∠JGB = ∠JHF [78]
063. GJ:GB = HJ:HF [72] & ∠JGB = ∠JHF [78] (Similar Triangles)⇒  ∠GJB = ∠HJF [79]
064. ∠GJB = ∠HJF [79] & H,G,J are collinear [15] ⇒  BJ ∥ FJ [80]
065. BJ ∥ FJ [80] ⇒  F,B,J are collinear
==========================

 

 

IMO 2017, Problem 4. Let R and S be different points on a circle Ω such that RS is not a diameter. Let ℓ be the tangent line to Ω at R. Point T is such that S is the midpoint of RT. Point J is chosen on minor arc RS of Ω so that the circumcircle Γ of triangle JST intersects ℓ at two distinct points. Let A be the common point of Γ and ℓ closer to R. Line AJ meets Ω again at K. Prove that line KT is tangent to Γ.

 

○ 풀이. AlphaGeometry (DDAR mode)

 

==========================
 * From theorem premises:
R S T O J O1 A K : Points
R,S,T are collinear [00]
SR = ST [01]
OR = OS [02]
OJ = OS [03]
O_1S = O_1T [04]
O_1J = O_1S [05]
O_1A = O_1S [06]
AR ⟂ OR [07]
OK = OS [08]
K,A,J are collinear [09]

 * Auxiliary Constructions:
B : Points
O_1B = O_1S [10]
OR ⟂ BR [11]

 * Proof steps:
001. O_1S = O_1T [04] & O_1B = O_1S [10] & O_1A = O_1S [06] ⇒  O_1 is the circumcenter of \Delta TBA [12]
002. O_1S = O_1T [04] & O_1B = O_1S [10] & O_1A = O_1S [06] ⇒  B,T,A,S are concyclic [13]
003. B,T,A,S are concyclic [13] ⇒  ∠BST = ∠BAT [14]
004. B,T,A,S are concyclic [13] & O_1S = O_1T [04] & O_1A = O_1S [06] & O_1J = O_1S [05] ⇒  B,A,J,S are concyclic [15]
005. B,A,J,S are concyclic [15] ⇒  ∠SBA = ∠SJA [16]
006. OR = OS [02] & OK = OS [08] & OJ = OS [03] ⇒  R,K,J,S are concyclic [17]
007. R,K,J,S are concyclic [17] ⇒  ∠RKJ = ∠RSJ [18]
008. OR ⟂ BR [11] & AR ⟂ OR [07] & ∠SBA = ∠SJA [16] & ∠RKJ = ∠RSJ [18] & K,A,J are collinear [09] ⇒  ∠SRK = ∠SBR [19]
009. OK = OS [08] & OR = OS [02] ⇒  O is the circumcenter of \Delta RKS [20]
010. O is the circumcenter of \Delta RKS [20] & OR ⟂ RB [11] ⇒  ∠BRK = ∠RSK [21]
011. OR ⟂ BR [11] & AR ⟂ OR [07] & ∠BRK = ∠RSK [21] ⇒  ∠RKS = ∠BRS [22]
012. ∠SRK = ∠SBR [19] & ∠RKS = ∠BRS [22] (Similar Triangles)⇒  SB:SR = SR:SK [23]
013. ∠SRK = ∠SBR [19] & ∠RKS = ∠BRS [22] ⇒  ∠RSK = ∠BSR [24]
014. SB:SR = SR:SK [23] & SR = ST [01] ⇒  BS:TS = TS:KS [25]
015. T,R,S are collinear [00] & ∠RSK = ∠BSR [24] ⇒  ∠TSK = ∠BST [26]
016. BS:TS = TS:KS [25] & ∠TSK = ∠BST [26] (Similar Triangles)⇒  ∠STK = ∠SBT [27]
017. ∠BST = ∠BAT [14] & R,S,T are collinear [00] & ∠STK = ∠SBT [27] ⇒  ∠KTB = ∠TAB [28]
018. O_1 is the circumcenter of \Delta TBA [12] & ∠KTB = ∠TAB [28] ⇒  O_1T ⟂ KT
==========================

 

○ 풀이. AlphaGeometry (AlphaGeometry mode)

 

==========================
 * From theorem premises:
A B C D E F G I : Points
C,A,B are collinear [00]
BA = BC [01]
DA = DB [02]
DE = DB [03]
FB = FC [04]
FE = FB [05]
FG = FB [06]
AG ⟂ AD [07]
DI = DB [08]
E,G,I are collinear [09]

 * Auxiliary Constructions:
H : Points
DA ⟂ HA [10]

 * Proof steps:
001. FB = FC [04] & FG = FB [06] & FE = FB [05] ⇒  F is the circumcenter of \Delta CGE [11]
002. DA = DB [02] & DI = DB [08] & DE = DB [03] ⇒  E,I,A,B are concyclic [12]
003. E,I,A,B are concyclic [12] ⇒  ∠EIA = ∠EBA [13]
004. FE = FB [05] & FG = FB [06] & FB = FC [04] ⇒  E,C,G,B are concyclic [14]
005. E,C,G,B are concyclic [14] ⇒  ∠EGC = ∠EBC [15]
006. E,C,G,B are concyclic [14] ⇒  ∠EGB = ∠ECB [16]
007. C,A,B are collinear [00] & ∠EIA = ∠EBA [13] & E,G,I are collinear [09] & ∠EGC = ∠EBC [15] ⇒  ∠GCA = ∠IAB [17]
008. DI = DB [08] & DA = DB [02] ⇒  D is the circumcenter of \Delta AIB [18]
009. D is the circumcenter of \Delta AIB [18] & DA ⟂ AH [10] ⇒  ∠HAI = ∠ABI [19]
010. C,A,B are collinear [00] & ∠HAI = ∠ABI [19] & DA ⟂ HA [10] & AG ⟂ AD [07] ⇒  ∠GAC = ∠AIB [20]
011. ∠GCA = ∠IAB [17] & ∠GAC = ∠AIB [20] (Similar Triangles)⇒  CG:AB = CA:AI [21]
012. CG:AB = CA:AI [21] & BA = BC [01] ⇒  CG:CB = CA:AI [22]
013. C,A,B are collinear [00] & ∠EIA = ∠EBA [13] & E,G,I are collinear [09] & ∠EGC = ∠EBC [15] ⇒  ∠GCB = ∠IAC [23]
014. CG:CB = CA:AI [22] & ∠GCB = ∠IAC [23] (Similar Triangles)⇒  ∠CGB = ∠ICA [24]
015. ∠CGB = ∠ICA [24] & C,A,B are collinear [00] & ∠EGB = ∠ECB [16] ⇒  ∠GEC = ∠GCI [25]
016. F is the circumcenter of \Delta CGE [11] & ∠GEC = ∠GCI [25] ⇒  CF ⟂ CI
==========================

 

 

IMO 2018, Problem 1. Let Γ be the circumcircle of acute triangle ABC. Points D and E lie on segments AB and AC, respectively, such that AD = AE. The perpendicular bisectors of BD and CE intersect the minor arcs AB and AC of Γ at points F and G, respectively. Prove that the lines DE and FG are parallel.

 

○ 풀이. 추후 업데이트 

 

 

IMO 2018, Problem 6. A convex quadrilateral ABCD satisfies AB · CD = BC · DA. Point X lies inside ABCD so that

 

∠XAB = ∠XCD and ∠XBC = ∠XDA.

 

Prove that ∠BXA + ∠DXC = 180°.

 

○ 풀이. 추후 업데이트

 

 

IMO 2019, Problem 2. In triangle ABC point A1 lies on side BC and point B₁ lies on side AC. Let P and Q be points on segments AA₁ and BB₁, respectively, such that PQ ∥ AB. Point P₁ is chosen on ray PB₁ beyond B₁ such that ∠PP₁C = ∠BAC. Point Q₁ is chosen on ray QA₁ beyond A₁ such that ∠CQ₁Q = ∠CBA. Prove that points P₁, Q₁, P, Q are cyclic.

 

○ 풀이. 추후 업데이트

 

 

IMO 2019, Problem 6. Let ABC be a triangle with incenter I and incircle ω. Let D, E, F denote the tangency points of ω with BC, CA, AB. The line through D perpendicular to EF meets ω again at R (other than D), and line AR meets ω again at P (other than R). Suppose the circumcircles of △PCE and △PBF meet again at Q (other than P). Prove that lines DI and PQ meet on the external ∠A-bisector.

 

○ 풀이. 추후 업데이트

 

입력: 2024.05.05 21:10