【국제수학올림피아드】 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.

 

○ 풀이. Evan Chen의 풀이 

○ 풀이. AlphaGeometry를 사용할 때, 새로운 점을 추가하는 AlphaGeometry 모드로 풀립니다. (∵ 더 어려운 문제) (ref)

 

==========================
 * From theorem premises:
A B C D E F G H I J K : Points
AD ⟂ BC [00]
BA:DA = BA:DA [01]
BD ⟂ AC [02]
B,E,C are collinear [03]
D,E,A are collinear [04]
F,B,C are collinear [05]
FB = FC [06]
GB = GC [07]
GA = GB [08]
AH ⟂ DH [09]
GH = GA [10]
DI ⟂ HI [11]
GI = GA [12]
JH = JD [13]
JI = JH [14]
KE = KI [15]
KI = KF [16]

 * Auxiliary Constructions:
L M : Points
L,C,A are collinear [17]
LC = LA [18]
M,H,A are collinear [19]
MH = MA [20]

 * Proof steps:
001. KE = KI [15] & KI = KF [16] ⇒  KF = KE [21]
002. KF = KE [21] ⇒  ∠KFE = ∠FEK [22]
003. ∠KFE = ∠FEK [22] & F,B,C are collinear [05] & B,E,C are collinear [03] ⇒  ∠(FK-BC) = ∠(BC-EK) [23]
004. KI = KF [16] ⇒  ∠KFI = ∠FIK [24]
005. KE = KI [15] ⇒  ∠KEI = ∠EIK [25]
006. M,H,A are collinear [19] & MH = MA [20] ⇒  M is midpoint of AH [26]
007. JH = JD [13] & JI = JH [14] ⇒  J is the circumcenter of \Delta HDI [27]
008. M,H,A are collinear [19] & DI ⟂ HI [11] & AH ⟂ DH [09] ⇒  ∠MHD = ∠HID [28]
009. J is the circumcenter of \Delta HDI [27] & ∠MHD = ∠HID [28] ⇒  HM ⟂ JH [29]
010. HM ⟂ JH [29] & AH ⟂ DH [09] & M,H,A are collinear [19] ⇒  D,H,J are collinear [30]
011. D,H,J are collinear [30] & JH = JD [13] ⇒  J is midpoint of HD [31]
012. M is midpoint of AH [26] & J is midpoint of HD [31] ⇒  MJ ∥ AD [32]
013. JM ∥ AD [32] & D,H,J are collinear [30] & M,H,A are collinear [19] ⇒  DH:HJ = DA:MJ [33]
014. DA:MJ = DH:HJ [33] & DJ = HJ [13] ⇒  DA:MJ = DH:DJ [34]
015. F,B,C are collinear [05] & FB = FC [06] ⇒  F is midpoint of CB [35]
016. L,C,A are collinear [17] & LC = LA [18] ⇒  L is midpoint of CA [36]
017. F is midpoint of CB [35] & L is midpoint of CA [36] ⇒  FL ∥ BA [37]
018. FL ∥ AB [37] & F,B,C are collinear [05] & L,C,A are collinear [17] ⇒  BC:BA = FC:FL [38]
019. FC:FL = BC:BA [38] & FB = FC [06] ⇒  FB:FL = BC:BA [39]
020. FB = FC [06] & GB = GC [07] ⇒  BC ⟂ FG [40]
021. GA = GB [08] & GB = GC [07] ⇒  GC = GA [41]
022. GC = GA [41] & LC = LA [18] ⇒  CA ⟂ GL [42]
023. BC ⟂ FG [40] & AD ⟂ BC [00] & CA ⟂ GL [42] & BD ⟂ AC [02] ⇒  ∠ADB = ∠FGL [43]
024. CA ⟂ GL [42] & BD ⟂ AC [02] & AB ∥ FL [37] ⇒  ∠ABD = ∠FLG [44]
025. ∠ADB = ∠FGL [43] & ∠ABD = ∠FLG [44] (Similar Triangles)⇒  DA:BA = GF:FL [45]
026. FB:FL = BC:BA [39] & DA:BA = GF:FL [45] ⇒  BC:FB = DA:GF [46]
027. F is midpoint of CB [35] & J is midpoint of HD [31] ⇒  FB:BC = JD:DH [47]
028. BC:FB = DA:GF [46] & FB = FC [06] & FB:BC = JD:DH [47] & JH = JD [13] & DH:HJ = DA:MJ [33] ⇒  DA:MJ = DA:GF [48]
029. BA:DA = BA:DA [01] & DA:MJ = DA:GF [48] ⇒  MJ = GF [49]
030. GH = GA [10] & GI = GA [12] ⇒  GI = GH [50]
031. GI = GH [50] & JI = JH [14] ⇒  IH ⟂ GJ [51]
032. GI = GH [50] & JI = JH [14] (SSS)⇒  ∠GIJ = ∠JHG [52]
033. AD ∥ JM [32] & IH ⟂ GJ [51] & DI ⟂ HI [11] & BC ⟂ FG [40] & AD ⟂ BC [00] ⇒  ∠MJG = ∠FGJ [53]
034. MJ = GF [49] & ∠MJG = ∠FGJ [53] (SAS)⇒  ∠(JM-FG) = ∠(GM-FJ) [54]
035. GH = GA [10] & MH = MA [20] ⇒  HA ⟂ GM [55]
036. GH = GA [10] & MH = MA [20] ⇒  MH:MA = GH:GA [56]
037. D,H,J are collinear [30] & ∠(JM-FG) = ∠(GM-FJ) [54] & BC ⟂ FG [40] & AD ⟂ BC [00] & JM ∥ AD [32] & HA ⟂ GM [55] & AH ⟂ DH [09] ⇒  JD ∥ JF [57]
038. JD ∥ JF [57] ⇒  D,F,J are collinear [58]
039. D,E,A are collinear [04] & F,B,C are collinear [05] & AD ⟂ BC [00] ⇒  DE ⟂ FB [59]
040. H,M,A are collinear [19] & AH ⟂ DH [09] ⇒  MH ⟂ DH [60]
041. DE ⟂ FB [59] & MH ⟂ DH [60] ⇒  ∠(DE-MH) = ∠(FB-DH) [61]
042. F,B,C are collinear [05] & B,E,C are collinear [03] & D,E,A are collinear [04] & D,F,J are collinear [58] & D,H,J are collinear [30] & ∠(DE-MH) = ∠(FB-DH) [61] & M,H,A are collinear [19] ⇒  ∠FED = ∠DHA [62]
043. D,E,A are collinear [04] & D,F,J are collinear [58] & D,H,J are collinear [30] ⇒  ∠FDE = ∠HDA [63]
044. D,E,A are collinear [04] & D,F,J are collinear [58] & D,H,J are collinear [30] ⇒  ∠FDA = ∠HDE [64]
045. ∠FED = ∠DHA [62] & ∠FDE = ∠HDA [63] (Similar Triangles)⇒  DF:DA = DE:DH [65]
046. DF:DA = DE:DH [65] & ∠FDA = ∠HDE [64] (Similar Triangles)⇒  FA:DA = HE:DH [66]
047. DA:MJ = DH:DJ [34] & FA:DA = HE:DH [66] ⇒  MJ:FA = DJ:HE [67]
048. MJ:FA = DJ:HE [67] & JH = JD [13] & GF = MJ [49] ⇒  HJ:HE = FG:FA [68]
049. F,B,C are collinear [05] & B,E,C are collinear [03] & D,E,A are collinear [04] & D,F,J are collinear [58] & D,H,J are collinear [30] & ∠(DE-MH) = ∠(FB-DH) [61] & M,H,A are collinear [19] ⇒  ∠FEA = ∠FHA [69]
050. ∠FEA = ∠FHA [69] ⇒  H,F,E,A are concyclic [70]
051. H,F,E,A are concyclic [70] ⇒  ∠HFA = ∠HEA [71]
052. D,F,J are collinear [58] & D,H,J are collinear [30] & ∠HFA = ∠HEA [71] & D,E,A are collinear [04] & JM ∥ AD [32] & BC ⟂ FG [40] & AD ⟂ BC [00] ⇒  ∠JHE = ∠AFG [72]
053. HJ:HE = FG:FA [68] & ∠JHE = ∠AFG [72] (Similar Triangles)⇒  JH:JE = GF:GA [73]
054. HJ:HE = FG:FA [68] & ∠JHE = ∠AFG [72] (Similar Triangles)⇒  ∠HJE = ∠AGF [74]
055. JH:JE = GF:GA [73] & MJ = GF [49] & GI = GA [12] & IJ = HJ [14] ⇒  JI:JE = GF:GI [75]
056. MH:MA = GH:GA [56] & M,H,A are collinear [19] ⇒  ∠HGM = ∠MGA [76]
057. ∠GIJ = ∠JHG [52] & D,H,J are collinear [30] & HA ⟂ GM [55] & AH ⟂ DH [09] ⇒  ∠IGM = ∠(IJ-GH) [77]
058. ∠HGM = ∠MGA [76] & ∠IGM = ∠(IJ-GH) [77] ⇒  ∠AGI = ∠(GM-IJ) [78]
059. D,E,A are collinear [04] & ∠HJE = ∠AGF [74] & D,F,J are collinear [58] & D,H,J are collinear [30] & BC ⟂ FG [40] & AD ⟂ BC [00] & JM ∥ AD [32] & ∠(JM-FG) = ∠(GM-FJ) [54] ⇒  ∠(GM-JE) = ∠(GA-DE) [79]
060. ∠AGI = ∠(GM-IJ) [78] & ∠(GM-JE) = ∠(GA-DE) [79] ⇒  ∠(GI-DE) = ∠IJE [80]
061. ∠(GI-DE) = ∠IJE [80] & D,E,A are collinear [04] & JM ∥ AD [32] & BC ⟂ FG [40] & AD ⟂ BC [00] ⇒  ∠IJE = ∠IGF [81]
062. JI:JE = GF:GI [75] & ∠IJE = ∠IGF [81] (Similar Triangles)⇒  ∠JIE = ∠IFG [82]
063. ∠JIE = ∠IFG [82] & BC ⟂ FG [40] & AD ⟂ BC [00] & JM ∥ AD [32] ⇒  ∠JIE = ∠(FI-JM) [83]
064. AD ⟂ BC [00] & ∠(FK-BC) = ∠(BC-EK) [23] & ∠KFI = ∠FIK [24] & ∠KEI = ∠EIK [25] & JM ∥ AD [32] & ∠JIE = ∠(FI-JM) [83] (Angle chase)⇒  IJ ∥ IK [84]
065. IJ ∥ IK [84] ⇒  I,K,J are collinear
==========================

 

 

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.

 

○ 풀이. Evan Chen의 풀이 

○ 풀이. AlphaGeometry를 사용할 때, 새로운 점을 추가하지 않는 DD+AR 모드로 풀립니다. (ref)

 

==========================
 * 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
==========================

 

 

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.

 

○ 풀이. Evan Chen의 풀이 

○ 풀이. AlphaGeometry를 사용할 때, 새로운 점을 추가하지 않는 DD+AR 모드로 풀립니다. (ref)

 

==========================
 * 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
==========================

 

 

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 Γ.

 

○ 풀이. Evan Chen의 풀이 

○ 풀이. AlphaGeometry를 사용할 때, 새로운 점을 추가하지 않는 DD+AR 모드로 풀립니다. (ref)

 

==========================
 * 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
==========================

 

 

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.

 

○ 풀이. Evan Chen의 풀이 

○ 풀이. AlphaGeometry를 사용할 때, 새로운 점을 추가하는 AlphaGeometry 모드로 풀립니다. (∵ 더 어려운 문제) (ref)

 

 

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°.

 

○ 풀이. Evan Chen의 풀이 

○ 풀이. AlphaGeometry를 사용할 때, 새로운 점을 추가하는 AlphaGeometry 모드로 풀립니다. (∵ 더 어려운 문제) (ref)

 

 

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.

 

○ 풀이. Evan Chen의 풀이 

○ 풀이. AlphaGeometry를 사용할 때, 새로운 점을 추가하는 AlphaGeometry 모드로 풀립니다. (∵ 더 어려운 문제) (ref)

 

 

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.

 

○ 풀이. Evan Chen의 풀이 

○ 풀이. AlphaGeometry를 사용할 때, 새로운 점을 추가하는 AlphaGeometry 모드로 풀립니다. (∵ 더 어려운 문제) (ref)

 

입력: 2024.05.05 21:10