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

IMO 기하 문제 풀이 (2000년 ~ 2004년)

 

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

---

 

IMO 2000, Problem 1. Two circles G₁ and G₂ intersect at two points M and N. Let AB be the line tangent to these circles at A and B, respectively, so that M lies closer to AB than N. Let CD be the line parallel to AB and passing through the point M, with C on G₁ and D on G₂. Lines AC and BD meet at E; lines AN and CD meet at P; lines BN and CD meet at Q. Show that EP = EQ.

 

○ 풀이 : Evan Chen의 풀이 

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

 

==========================
 * From theorem premises:
A B G1 G2 M N C D E P Q : Points
AG_1 ⟂ AB [00]
BA ⟂ G_2B [01]
G_1M = G_1A [02]
G_2M = G_2B [03]
G_1N = G_1A [04]
G_2N = G_2B [05]
∠MAN = ∠MAN [06]
G_1C = G_1A [07]
CM ∥ AB [08]
∠CAN = ∠CAN [09]
G_2D = G_2B [10]
DM ∥ AB [11]
∠DBN = ∠DBN [12]
E,D,B are collinear [13]
E,A,C are collinear [14]
P,C,D are collinear [15]
P,A,N are collinear [16]
C,D,Q are collinear [17]
N,Q,B are collinear [18]
DQ:ND = DQ:ND [19]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. G_1N = G_1A [04] & G_1C = G_1A [07] & G_1M = G_1A [02] ⇒  A,C,N,M are concyclic [20]
002. A,C,N,M are concyclic [20] ⇒  ∠CAN = ∠CMN [21]
003. G_2M = G_2B [03] & G_2D = G_2B [10] & G_2N = G_2B [05] ⇒  N,D,B,M are concyclic [22]
004. N,D,B,M are concyclic [22] ⇒  ∠NBD = ∠NMD [23]
005. N,D,B,M are concyclic [22] ⇒  ∠DNB = ∠DMB [24]
006. E,D,B are collinear [13] & E,A,C are collinear [14] & ∠CAN = ∠CMN [21] & CM ∥ AB [08] & ∠NBD = ∠NMD [23] & DM ∥ AB [11] ⇒  ∠EBN = ∠EAN [25]
007. ∠EBN = ∠EAN [25] ⇒  E,A,N,B are concyclic [26]
008. E,A,N,B are concyclic [26] ⇒  ∠EAB = ∠ENB [27]
009. E,A,N,B are concyclic [26] ⇒  ∠ENA = ∠EBA [28]
010. G_2N = G_2B [05] & G_2D = G_2B [10] ⇒  G_2 is the circumcenter of \Delta BND [29]
011. G_2 is the circumcenter of \Delta BND [29] & G_2B ⟂ BA [01] ⇒  ∠DBA = ∠DNB [30]
012. DM ∥ AB [11] & CM ∥ AB [08] ⇒  MC ∥ MD [31]
013. MC ∥ MD [31] ⇒  C,D,M are collinear [32]
014. C,D,Q are collinear [17] & ∠DNB = ∠DBA [30] & DM ∥ AB [11] & C,D,M are collinear [32] ⇒  ∠DNB = ∠BDQ [33]
015. N,Q,B are collinear [18] & ∠DBN = ∠DBN [12] ⇒  ∠DBN = ∠DBQ [34]
016. ∠DNB = ∠BDQ [33] & ∠DBN = ∠DBQ [34] (Similar Triangles)⇒  BD:BN = BQ:BD [35]
017. G_1C = G_1A [07] & G_1M = G_1A [02] ⇒  G_1 is the circumcenter of \Delta ACM [36]
018. G_1 is the circumcenter of \Delta ACM [36] & AG_1 ⟂ AB [00] ⇒  ∠BAC = ∠AMC [37]
019. E,A,C are collinear [14] & ∠BAC = ∠AMC [37] & CM ∥ AB [08] ⇒  ∠BAE = ∠MAB [38]
020. G_2D = G_2B [10] & G_2M = G_2B [03] ⇒  G_2 is the circumcenter of \Delta BDM [39]
021. G_2 is the circumcenter of \Delta BDM [39] & G_2B ⟂ BA [01] ⇒  ∠ABD = ∠BMD [40]
022. E,D,B are collinear [13] & ∠ABD = ∠BMD [40] & DM ∥ AB [11] ⇒  ∠MBA = ∠ABE [41]
023. ∠BAE = ∠MAB [38] & ∠MBA = ∠ABE [41] (Similar Triangles)⇒  BM = BE [42]
024. ∠BAE = ∠MAB [38] & ∠MBA = ∠ABE [41] (Similar Triangles)⇒  AM = AE [43]
025. G_2N = G_2B [05] & G_2M = G_2B [03] ⇒  G_2 is the circumcenter of \Delta BNM [44]
026. G_2 is the circumcenter of \Delta BNM [44] & G_2B ⟂ BA [01] ⇒  ∠ABM = ∠BNM [45]
027. ∠ABM = ∠BNM [45] & ∠DNB = ∠DMB [24] & DM ∥ AB [11] ⇒  ∠DNB = ∠BNM [46]
028. N,D,B,M are concyclic [22] & ∠DNB = ∠BNM [46] ⇒  DB = BM [47]
029. BD:BN = BQ:BD [35] & BM = BE [42] & DB = BM [47] ⇒  EB:NB = QB:EB [48]
030. N,Q,B are collinear [18] & E,D,B are collinear [13] & ∠NBD = ∠NBD [12] ⇒  ∠QBE = ∠NBE [49]
031. EB:NB = QB:EB [48] & ∠QBE = ∠NBE [49] (Similar Triangles)⇒  ∠BQE = ∠NEB [50]
032. E,D,B are collinear [13] & E,C,A are collinear [14] & ∠EAB = ∠ENB [27] & ∠BQE = ∠NEB [50] & N,Q,B are collinear [18] & DM ∥ AB [11] & C,D,M are collinear [32] ⇒  ∠QED = ∠DCE [51]
033. C,D,Q are collinear [17] & E,D,B are collinear [13] & DM ∥ AB [11] & C,D,M are collinear [32] ⇒  ∠QDE = ∠CDE [52]
034. ∠QED = ∠DCE [51] & ∠QDE = ∠CDE [52] (Similar Triangles)⇒  EQ:DQ = EC:ED [53]
035. P,C,D are collinear [15] & E,C,A are collinear [14] & E,D,B are collinear [13] & ∠EAB = ∠ENB [27] & ∠BQE = ∠NEB [50] & N,Q,B are collinear [18] & DM ∥ AB [11] & C,D,M are collinear [32] ⇒  ∠PCE = ∠QED [54]
036. G_1M = G_1A [02] & G_1N = G_1A [04] ⇒  G_1 is the circumcenter of \Delta AMN [55]
037. G_1 is the circumcenter of \Delta AMN [55] & AG_1 ⟂ AB [00] ⇒  ∠MAB = ∠MNA [56]
038. C,D,M are collinear [32] & P,C,D are collinear [15] & ∠MNA = ∠MAB [56] & DM ∥ AB [11] ⇒  ∠MNA = ∠AMP [57]
039. P,A,N are collinear [16] & ∠MAN = ∠MAN [06] ⇒  ∠MAN = ∠MAP [58]
040. ∠MNA = ∠AMP [57] & ∠MAN = ∠MAP [58] (Similar Triangles)⇒  AM:AN = AP:AM [59]
041. G_1C = G_1A [07] & G_1N = G_1A [04] ⇒  G_1 is the circumcenter of \Delta ACN [60]
042. G_1 is the circumcenter of \Delta ACN [60] & AG_1 ⟂ AB [00] ⇒  ∠BAC = ∠ANC [61]
043. C,D,M are collinear [32] & ∠ANC = ∠BAC [61] & DM ∥ AB [11] ⇒  ∠ANC = ∠MCA [62]
044. A,C,N,M are concyclic [20] & ∠ANC = ∠MCA [62] ⇒  AC = MA [63]
045. AM:AN = AP:AM [59] & AC = MA [63] & AM = AE [43] ⇒  PA:EA = EA:AN [64]
046. E,A,C are collinear [14] & P,A,N are collinear [16] & ∠CAN = ∠CAN [09] ⇒  ∠EAN = ∠EAP [65]
047. PA:EA = EA:AN [64] & ∠EAN = ∠EAP [65] (Similar Triangles)⇒  ∠AEN = ∠EPA [66]
048. E,C,A are collinear [14] & C,D,Q are collinear [17] & E,D,B are collinear [13] & ∠ENA = ∠EBA [28] & ∠AEN = ∠EPA [66] & P,A,N are collinear [16] & DM ∥ AB [11] & C,D,M are collinear [32] ⇒  ∠PEC = ∠QDE [67]
049. ∠PCE = ∠QED [54] & ∠PEC = ∠QDE [67] (Similar Triangles)⇒  EP:DQ = EC:ED [68]
050. EQ:DQ = EC:ED [53] & EP:DQ = EC:ED [68] ⇒  EP:DQ = EQ:DQ [69]
051. EP:DQ = EQ:DQ [69] & DQ:ND = DQ:ND [19] ⇒  EQ = EP
==========================

 

 

IMO 2000, Problem 6. Let AH₁, BH₂, and CH₃ be the altitudes of an acute triangle ABC. The incircle ω of triangle ABC touches the sides BC, CA and AB at T₁, T₂ and T₃, respectively. Consider the reflections of the lines H₁H₂, H₂H₃, and H₃H₁ with respect to the lines T₁T₂, T₂T₃, and T₃T₁. Prove that these images form a triangle whose vertices lie on ω.

 

○ 풀이. Evan Chen의 풀이

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

 

==========================
 * From theorem premises:
A B C H E F G I J K L M N O P : Points
∠ACH = ∠HCB [00]
∠HAB = ∠CAH [01]
B,C,E are collinear [02]
BC ⟂ HE [03]
C,A,F are collinear [04]
CA ⟂ HF [05]
B,A,G are collinear [06]
GH ⟂ AB [07]
BC ⟂ IA [08]
B,C,I are collinear [09]
C,A,J are collinear [10]
CA ⟂ JB [11]
B,A,K are collinear [12]
AB ⟂ KC [13]
EI = EL [14]
FI = FL [15]
EJ = EM [16]
FJ = FM [17]
FJ = FN [18]
GJ = GN [19]
FK = FO [20]
GK = GO [21]
O,P,N are collinear [22]
M,P,L are collinear [23]

 * Auxiliary Constructions:
D Q : Points
BD ⟂ AC [24]
AD ⟂ BC [25]
A,H,Q are collinear [26]
BQ ⟂ AH [27]

 * Proof steps:
001. C,E,B are collinear [02] & C,A,F are collinear [04] & BD ⟂ AC [24] & AD ⟂ BC [25] & BC ⟂ HE [03] & CA ⟂ HF [05] ⇒  ∠HEC = ∠CFH [28]
002. C,E,B are collinear [02] & C,A,F are collinear [04] & ∠HCB = ∠ACH [00] ⇒  ∠HCE = ∠FCH [29]
003. ∠HEC = ∠CFH [28] & ∠HCE = ∠FCH [29] (Similar Triangles)⇒  HE = HF [30]
004. ∠HEC = ∠CFH [28] & ∠HCE = ∠FCH [29] (Similar Triangles)⇒  CE = CF [31]
005. C,J,A are collinear [10] & CA ⟂ JB [11] & BD ⟂ AC [24] & BC ⟂ IA [08] & AD ⟂ BC [25] & B,C,I are collinear [09] ⇒  ∠AJB = ∠AIB [32]
006. ∠AJB = ∠AIB [32] ⇒  B,A,J,I are concyclic [33]
007. B,A,J,I are concyclic [33] ⇒  ∠ABI = ∠AJI [34]
008. EJ = EM [16] & FJ = FM [17] (SSS)⇒  ∠EMF = ∠FJE [35]
009. EJ = EM [16] & FJ = FM [17] ⇒  EF ⟂ MJ [36]
010. EJ = EM [16] & FJ = FM [17] (SSS)⇒  ∠MFE = ∠EFJ [37]
011. C,E,B are collinear [02] & C,A,F are collinear [04] & BD ⟂ AC [24] & AD ⟂ BC [25] & BC ⟂ HE [03] & CA ⟂ HF [05] ⇒  ∠HEC = ∠HFC [38]
012. ∠HEC = ∠HFC [38] ⇒  C,F,E,H are concyclic [39]
013. C,F,E,H are concyclic [39] ⇒  ∠CEF = ∠CHF [40]
014. C,F,E,H are concyclic [39] ⇒  ∠CFE = ∠CHE [41]
015. EI = EL [14] & FI = FL [15] ⇒  IL ⟂ EF [42]
016. CA ⟂ JB [11] & BD ⟂ AC [24] & IL ⟂ EF [42] ⇒  ∠(BJ-CA) = ∠(FE-LI) [43]
017. FJ = FM [17] ⇒  ∠FMJ = ∠MJF [44]
018. ∠FMJ = ∠MJF [44] & C,J,A are collinear [10] & C,A,F are collinear [04] & EF ⟂ MJ [36] & IL ⟂ EF [42] ⇒  ∠(CA-LI) = ∠(LI-MF) [45]
019. ∠(BJ-CA) = ∠(FE-LI) [43] & ∠(CA-LI) = ∠(LI-MF) [45] ⇒  ∠(BJ-LI) = ∠EFM [46]
020. HE = HF [30] & CE = CF [31] ⇒  EF ⟂ HC [47]
021. ∠CEF = ∠CHF [40] & B,C,E are collinear [02] & CA ⟂ HF [05] & BD ⟂ AC [24] & ∠(BJ-LI) = ∠EFM [46] & CA ⟂ JB [11] & EF ⟂ MJ [36] & IL ⟂ EF [42] & EF ⟂ HC [47] ⇒  ∠(MF-CH) = ∠BCH [48]
022. ∠(MF-CH) = ∠BCH [48] ⇒  MF ∥ BC [49]
023. EI = EL [14] (SSS)⇒  ∠EIL = ∠ILE [50]
024. ∠EIL = ∠ILE [50] & B,C,I are collinear [09] & B,C,E are collinear [02] & EF ⟂ HC [47] & EF ⟂ JM [36] & IL ⟂ EF [42] & ∠ACH = ∠HCB [00] ⇒  ∠ACH = ∠(EL-CH) [51]
025. ∠ACH = ∠(EL-CH) [51] ⇒  CA ∥ EL [52]
026. B,C,I are collinear [09] & B,C,E are collinear [02] & ∠EMF = ∠FJE [35] & C,J,A are collinear [10] & C,A,F are collinear [04] & FM ∥ BC [49] & AC ∥ EL [52] ⇒  ∠IEJ = ∠MEL [53]
027. EI = EL [14] & EJ = EM [16] & ∠IEJ = ∠MEL [53] (SAS)⇒  ∠EIJ = ∠MLE [54]
028. B,G,A are collinear [06] & C,A,F are collinear [04] & BD ⟂ AC [24] & GH ⟂ AB [07] & CA ⟂ HF [05] ⇒  ∠HGA = ∠AFH [55]
029. B,A,G are collinear [06] & C,A,F are collinear [04] & ∠HAB = ∠CAH [01] ⇒  ∠HAG = ∠FAH [56]
030. ∠HGA = ∠AFH [55] & ∠HAG = ∠FAH [56] (Similar Triangles)⇒  AG = AF [57]
031. ∠HGA = ∠AFH [55] & ∠HAG = ∠FAH [56] (Similar Triangles)⇒  HG = HF [58]
032. ∠HGA = ∠AFH [55] & ∠HAG = ∠FAH [56] (Similar Triangles)⇒  ∠GHA = ∠AHF [59]
033. AG = AF [57] ⇒  ∠AGF = ∠GFA [60]
034. FJ = FN [18] & GJ = GN [19] (SSS)⇒  ∠NFG = ∠GFJ [61]
035. FJ = FN [18] & GJ = GN [19] ⇒  JN ⟂ FG [62]
036. ∠AGF = ∠GFA [60] & B,A,G are collinear [06] & C,A,F are collinear [04] & ∠NFG = ∠GFJ [61] & C,J,A are collinear [10] ⇒  ∠NFG = ∠(BA-GF) [63]
037. ∠NFG = ∠(BA-GF) [63] ⇒  FN ∥ BA [64]
038. M,P,L are collinear [23] & ∠ABI = ∠AJI [34] & B,C,I are collinear [09] & C,A,J are collinear [10] & ∠EIJ = ∠MLE [54] & B,C,E are collinear [02] & FM ∥ BC [49] & AC ∥ EL [52] & AB ∥ FN [64] ⇒  ∠(MP-BC) = ∠(FN-BC) [65]
039. ∠(MP-BC) = ∠(FN-BC) [65] ⇒  MP ∥ FN [66]
040. B,A,K are collinear [12] & C,J,A are collinear [10] & CA ⟂ JB [11] & BD ⟂ AC [24] & GH ⟂ AB [07] & AB ⟂ KC [13] ⇒  ∠CKB = ∠CJB [67]
041. ∠CKB = ∠CJB [67] ⇒  B,J,C,K are concyclic [68]
042. B,J,C,K are concyclic [68] ⇒  ∠BCJ = ∠BKJ [69]
043. FK = FO [20] & GK = GO [21] (SSS)⇒  ∠FOG = ∠GKF [70]
044. FK = FO [20] & GK = GO [21] (SSS)⇒  ∠OGF = ∠FGK [71]
045. FK = FO [20] & GK = GO [21] ⇒  FG ⟂ OK [72]
046. ∠OGF = ∠FGK [71] & B,A,K are collinear [12] & B,A,G are collinear [06] & ∠AGF = ∠GFA [60] & C,A,F are collinear [04] ⇒  ∠(CA-GF) = ∠OGF [73]
047. ∠(CA-GF) = ∠OGF [73] ⇒  CA ∥ OG [74]
048. C,J,A are collinear [10] & C,A,F are collinear [04] & ∠FOG = ∠GKF [70] & B,A,K are collinear [12] & B,A,G are collinear [06] & AB ∥ FN [64] & GO ∥ AC [74] ⇒  ∠NFO = ∠KFJ [75]
049. FJ = FN [18] & FK = FO [20] & ∠NFO = ∠KFJ [75] (SAS)⇒  ∠FNO = ∠KJF [76]
050. O,P,N are collinear [22] & ∠BCJ = ∠BKJ [69] & C,A,J are collinear [10] & B,A,K are collinear [12] & ∠FNO = ∠KJF [76] & C,A,F are collinear [04] & FN ∥ AB [64] & AC ∥ EL [52] ⇒  ∠(OP-EL) = ∠(BC-EL) [77]
051. ∠(OP-EL) = ∠(BC-EL) [77] ⇒  OP ∥ BC [78]
052. O,P,N are collinear [22] & P,M,L are collinear [23] & MP ∥ FN [66] & OP ∥ BC [78] & FM ∥ BC [49] ⇒  ∠NPM = ∠MFN [79]
053. FJ = FN [18] & FJ = FM [17] ⇒  FM = FN [80]
054. FJ = FN [18] & FJ = FM [17] ⇒  F is the circumcenter of \Delta JMN [81]
055. FM = FN [80] ⇒  ∠FMN = ∠MNF [82]
056. M,P,L are collinear [23] & ∠MNF = ∠FMN [82] & MP ∥ FN [66] ⇒  ∠NMP = ∠FMN [83]
057. ∠NPM = ∠MFN [79] & ∠NMP = ∠FMN [83] (Similar Triangles)⇒  NP = NF [84]
058. C,J,A are collinear [10] & CA ⟂ JB [11] & BD ⟂ AC [24] & A,H,Q are collinear [26] & BQ ⟂ AH [27] ⇒  ∠AJB = ∠AQB [85]
059. ∠AJB = ∠AQB [85] ⇒  B,A,Q,J are concyclic [86]
060. Q,A,B,J are concyclic [86] ⇒  ∠QAB = ∠QJB [87]
061. Q,A,B,J are concyclic [86] ⇒  ∠QBA = ∠QJA [88]
062. B,G,A are collinear [06] & C,A,F are collinear [04] & BD ⟂ AC [24] & GH ⟂ AB [07] & CA ⟂ HF [05] ⇒  ∠HGA = ∠HFA [89]
063. ∠HGA = ∠HFA [89] ⇒  A,F,H,G are concyclic [90]
064. A,F,H,G are concyclic [90] ⇒  ∠AHF = ∠AGF [91]
065. A,F,H,G are concyclic [90] ⇒  ∠AFG = ∠AHG [92]
066. BJ ⟂ CA [11] & OK ⟂ GF [72] ⇒  ∠(BJ-GF) = ∠(CA-OK) [93]
067. C,J,A are collinear [10] & C,A,F are collinear [04] & CA ⟂ JB [11] & BD ⟂ AC [24] & ∠QAB = ∠QJB [87] & A,H,Q are collinear [26] & ∠AHF = ∠AGF [91] & B,A,G are collinear [06] & CA ⟂ HF [05] & ∠(BJ-GF) = ∠(CA-OK) [93] & FG ⟂ OK [72] & JN ⟂ FG [62] ⇒  ∠FJN = ∠QJB [94]
068. CA ⟂ JB [11] & BD ⟂ AC [24] & JN ⟂ FG [62] & FG ⟂ OK [72] ⇒  ∠(BJ-CA) = ∠(GF-OK) [95]
069. FJ = FN [18] ⇒  ∠FNJ = ∠NJF [96]
070. ∠FNJ = ∠NJF [96] & C,J,A are collinear [10] & C,A,F are collinear [04] & FG ⟂ OK [72] & JN ⟂ FG [62] ⇒  ∠(CA-OK) = ∠(OK-FN) [97]
071. ∠(BJ-CA) = ∠(GF-OK) [95] & ∠(CA-OK) = ∠(OK-FN) [97] ⇒  ∠(BJ-OK) = ∠GFN [98]
072. HG = HF [58] & AG = AF [57] ⇒  HA ⟂ GF [99]
073. CA ⟂ JB [11] & BD ⟂ AC [24] & ∠(BJ-OK) = ∠GFN [98] & FG ⟂ OK [72] & JN ⟂ FG [62] & HA ⟂ GF [99] & BQ ⟂ AH [27] ⇒  ∠FNJ = ∠QBJ [100]
074. ∠FJN = ∠QJB [94] & ∠FNJ = ∠QBJ [100] (Similar Triangles)⇒  JF:JQ = JN:JB [101]
075. C,J,A are collinear [10] & C,A,F are collinear [04] & CA ⟂ JB [11] & BD ⟂ AC [24] ⇒  FJ ⟂ JB [102]
076. F is the circumcenter of \Delta JMN [81] & FJ ⟂ JB [102] ⇒  ∠BJM = ∠JNM [103]
077. CA ⟂ JB [11] & BD ⟂ AC [24] & JN ⟂ FG [62] & FG ⟂ OK [72] ⇒  ∠(CA-BJ) = ∠(GF-OK) [104]
078. CA ⟂ JB [11] & BD ⟂ AC [24] & ∠BJM = ∠JNM [103] & EF ⟂ MJ [36] & IL ⟂ EF [42] & FG ⟂ OK [72] & JN ⟂ FG [62] ⇒  ∠(BJ-LI) = ∠(OK-MN) [105]
079. ∠(CA-BJ) = ∠(GF-OK) [104] & ∠(BJ-LI) = ∠(OK-MN) [105] ⇒  ∠(AC-IL) = ∠(FG-MN) [106]
080. ∠(AC-IL) = ∠(FG-MN) [106] & EF ⟂ MJ [36] & IL ⟂ EF [42] & EF ⟂ HC [47] ⇒  ∠ACH = ∠(GF-MN) [107]
081. BQ ⟂ AH [27] & BA ⟂ CK [13] ⇒  ∠QBA = ∠(AH-CK) [108]
082. ∠AFG = ∠AHG [92] & C,A,F are collinear [04] & ∠QBA = ∠(AH-CK) [108] & AB ⟂ KC [13] & GH ⟂ AB [07] & ∠QBA = ∠QJA [88] & C,A,J are collinear [10] ⇒  ∠(CA-JQ) = ∠(GF-CA) [109]
083. ∠ACH = ∠(GF-MN) [107] & ∠(CA-JQ) = ∠(GF-CA) [109] ⇒  ∠(CH-MN) = ∠(JQ-AC) [110]
084. C,J,A are collinear [10] & C,A,F are collinear [04] & CA ⟂ JB [11] & BD ⟂ AC [24] & ∠BJM = ∠JNM [103] & ∠(CH-MN) = ∠(JQ-AC) [110] & EF ⟂ HC [47] & EF ⟂ JM [36] ⇒  ∠FJQ = ∠NJB [111]
085. JF:JQ = JN:JB [101] & ∠FJQ = ∠NJB [111] (Similar Triangles)⇒  ∠FQJ = ∠NBJ [112]
086. HE = HF [30] & HG = HF [58] ⇒  H is the circumcenter of \Delta GEF [113]
087. HE = HF [30] & HG = HF [58] ⇒  HG = HE [114]
088. C,A,F are collinear [04] & FH ⟂ AC [05] ⇒  HF ⟂ FC [115]
089. H is the circumcenter of \Delta GEF [113] & HF ⟂ FC [115] ⇒  ∠CFG = ∠FEG [116]
090. B,G,A are collinear [06] & A,H,Q are collinear [26] & BQ ⟂ AH [27] & GH ⟂ AB [07] ⇒  ∠HGB = ∠HQB [117]
091. ∠HGB = ∠HQB [117] ⇒  B,G,H,Q are concyclic [118]
092. B,G,A are collinear [06] & B,C,E are collinear [02] & AD ⟂ BC [25] & GH ⟂ AB [07] & BC ⟂ HE [03] ⇒  ∠HGB = ∠HEB [119]
093. ∠HGB = ∠HEB [119] ⇒  B,G,E,H are concyclic [120]
094. B,G,H,Q are concyclic [118] & B,G,E,H are concyclic [120] ⇒  B,G,E,Q are concyclic [121]
095. B,G,H,Q are concyclic [118] & B,G,E,H are concyclic [120] ⇒  G,E,Q,H are concyclic [122]
096. G,E,Q,H are concyclic [122] ⇒  ∠GEQ = ∠GHQ [123]
097. G,E,Q,H are concyclic [122] ⇒  ∠GEH = ∠GQH [124]
098. ∠CFG = ∠FEG [116] & C,A,F are collinear [04] & ∠AFG = ∠AHG [92] & ∠GEQ = ∠GHQ [123] & A,H,Q are collinear [26] ⇒  ∠QEG = ∠FEG [125]
099. ∠QEG = ∠FEG [125] ⇒  EQ ∥ FE [126]
100. HG = HE [114] ⇒  ∠HGE = ∠GEH [127]
101. A,H,Q are collinear [26] & ∠GHA = ∠AHF [59] ⇒  ∠GHQ = ∠QHF [128]
102. HG = HF [58] & ∠GHQ = ∠QHF [128] (SAS)⇒  ∠GQH = ∠HQF [129]
103. HG = HF [58] & ∠GHQ = ∠QHF [128] (SAS)⇒  QG = QF [130]
104. ∠GEQ = ∠GHQ [123] & A,H,Q are collinear [26] & ∠HGE = ∠GEH [127] & BC ⟂ HE [03] & AD ⟂ BC [25] & ∠GEH = ∠GQH [124] & ∠GQH = ∠HQF [129] & FG ⟂ HA [99] & OK ⟂ GF [72] ⇒  ∠(FQ-OK) = ∠(EQ-OK) [131]
105. ∠(FQ-OK) = ∠(EQ-OK) [131] ⇒  FQ ∥ EQ [132]
106. BJ ⟂ CA [11] & IL ⟂ EF [42] ⇒  ∠(BJ-FE) = ∠(CA-LI) [133]
107. CA ⟂ JB [11] & BD ⟂ AC [24] & ∠(BJ-FE) = ∠(CA-LI) [133] & EF ⟂ MJ [36] & IL ⟂ EF [42] & ∠(AC-IL) = ∠(FG-MN) [106] ⇒  ∠(GF-MN) = ∠(BJ-FE) [134]
108. CA ⟂ JB [11] & BD ⟂ AC [24] & ∠QAB = ∠QJB [87] & A,H,Q are collinear [26] & ∠AHF = ∠AGF [91] & B,A,G are collinear [06] & CA ⟂ HF [05] ⇒  ∠(GF-BJ) = ∠BJQ [135]
109. ∠(GF-MN) = ∠(BJ-FE) [134] & ∠(GF-BJ) = ∠BJQ [135] ⇒  ∠(MN-BJ) = ∠(FE-JQ) [136]
110. CA ⟂ JB [11] & BD ⟂ AC [24] & IL ⟂ EF [42] ⇒  ∠(CA-BJ) = ∠(FE-LI) [137]
111. CA ⟂ JB [11] & BD ⟂ AC [24] & ∠BJM = ∠JNM [103] & FG ⟂ OK [72] & JN ⟂ FG [62] & EF ⟂ MJ [36] & IL ⟂ EF [42] ⇒  ∠(BJ-OK) = ∠(LI-MN) [138]
112. ∠(CA-BJ) = ∠(FE-LI) [137] & ∠(BJ-OK) = ∠(LI-MN) [138] ⇒  ∠(AC-EF) = ∠(KO-MN) [139]
113. ∠CFG = ∠FEG [116] & C,A,F are collinear [04] & ∠(AC-EF) = ∠(KO-MN) [139] & FG ⟂ OK [72] & JN ⟂ FG [62] ⇒  ∠(OK-MN) = ∠FGE [140]
114. ∠(OK-MN) = ∠FGE [140] & OK ⟂ GF [72] ⇒  GE ⟂ MN [141]
115. ∠ACH = ∠HCB [00] & ∠CFE = ∠CHE [41] & C,A,F are collinear [04] & BC ⟂ HE [03] & AD ⟂ BC [25] ⇒  ∠(FE-DA) = ∠HCB [142]
116. B,G,E,H are concyclic [120] ⇒  ∠GEB = ∠GHB [143]
117. B,G,E,H are concyclic [120] ⇒  ∠GEH = ∠GBH [144]
118. ∠GEB = ∠GHB [143] & B,C,E are collinear [02] & ∠HGE = ∠GEH [127] & BC ⟂ HE [03] & AD ⟂ BC [25] ⇒  ∠(DA-GE) = ∠CBH [145]
119. ∠(FE-DA) = ∠HCB [142] & ∠(DA-GE) = ∠CBH [145] ⇒  ∠(CH-EF) = ∠(BH-EG) [146]
120. B,C,E are collinear [02] & EH ⟂ BC [03] ⇒  HE ⟂ EB [147]
121. H is the circumcenter of \Delta GEF [113] & HE ⟂ EB [147] ⇒  ∠BEG = ∠EFG [148]
122. B,G,A are collinear [06] & GH ⟂ AB [07] ⇒  HG ⟂ GB [149]
123. H is the circumcenter of \Delta GEF [113] & HG ⟂ GB [149] ⇒  ∠BGE = ∠GFE [150]
124. ∠BEG = ∠EFG [148] & B,C,E are collinear [02] & ∠BGE = ∠GFE [150] & B,A,G are collinear [06] & ∠GEH = ∠GBH [144] & BC ⟂ HE [03] & AD ⟂ BC [25] ⇒  ∠(DA-BH) = ∠(BC-GE) [151]
125. ∠(FE-DA) = ∠HCB [142] & ∠(DA-BH) = ∠(BC-GE) [151] ⇒  ∠(CH-EF) = ∠(EG-BH) [152]
126. ∠FQJ = ∠NBJ [112] & MJ ⟂ EF [36] & IL ⟂ EF [42] & EF ⟂ HC [47] & EQ ∥ EF [126] & FQ ∥ EQ [132] & CA ⟂ JB [11] & BD ⟂ AC [24] & ∠(MN-BJ) = ∠(FE-JQ) [136] & GE ⟂ MN [141] & ∠(CH-EF) = ∠(BH-EG) [146] & ∠(CH-EF) = ∠(EG-BH) [152] ⇒  ∠(BH-FE) = ∠(BN-FE) [153]
127. ∠(BH-FE) = ∠(BN-FE) [153] ⇒  BH ∥ BN [154]
128. BH ∥ BN [154] ⇒  B,H,N are collinear [155]
129. CA ⟂ JB [11] & BD ⟂ AC [24] & ∠QAB = ∠QJB [87] & A,H,Q are collinear [26] & FG ⟂ HA [99] & OK ⟂ GF [72] ⇒  ∠(OK-JQ) = ∠ABJ [156]
130. GK = GO [21] ⇒  ∠GOK = ∠OKG [157]
131. ∠GOK = ∠OKG [157] & B,A,K are collinear [12] & B,A,G are collinear [06] ⇒  ∠GOK = ∠(KO-AB) [158]
132. ∠(OK-JQ) = ∠ABJ [156] & ∠GOK = ∠(KO-AB) [158] ⇒  ∠(BJ-OK) = ∠(JQ-OG) [159]
133. MJ ⟂ EF [36] & IL ⟂ EF [42] & EF ⟂ HC [47] & EQ ∥ EF [126] & FQ ∥ EQ [132] & C,J,A are collinear [10] & C,A,F are collinear [04] & ∠MFE = ∠EFJ [37] ⇒  ∠MFQ = ∠QFJ [160]
134. FJ = FM [17] & ∠MFQ = ∠QFJ [160] (SAS)⇒  ∠FMQ = ∠QJF [161]
135. A,H,Q are collinear [26] & ∠(BJ-OK) = ∠(JQ-OG) [159] & CA ⟂ JB [11] & BD ⟂ AC [24] & FG ⟂ HA [99] & OK ⟂ GF [72] & AC ∥ GO [74] & ∠FMQ = ∠QJF [161] & C,J,A are collinear [10] & C,A,F are collinear [04] & CA ⟂ HF [05] ⇒  ∠FMQ = ∠FHQ [162]
136. ∠FMQ = ∠FHQ [162] ⇒  M,F,H,Q are concyclic [163]
137. M,F,H,Q are concyclic [163] ⇒  ∠MFQ = ∠MHQ [164]
138. B,A,Q,J are concyclic [86] & B,A,J,I are concyclic [33] ⇒  B,A,Q,I are concyclic [165]
139. B,A,Q,I are concyclic [165] ⇒  ∠QAB = ∠QIB [166]
140. A,H,Q are collinear [26] & B,A,G are collinear [06] & B,C,I are collinear [09] & B,C,E are collinear [02] & ∠QAB = ∠QIB [166] ⇒  ∠QAG = ∠QIE [167]
141. B,G,E,Q are concyclic [121] ⇒  ∠GQE = ∠GBE [168]
142. B,G,A are collinear [06] & B,C,I are collinear [09] & B,C,E are collinear [02] & ∠GQE = ∠GBE [168] ⇒  ∠QGA = ∠QEI [169]
143. ∠QAG = ∠QIE [167] & ∠QGA = ∠QEI [169] (Similar Triangles)⇒  GQ:GA = EQ:EI [170]
144. GQ:GA = EQ:EI [170] & EI = EL [14] & FQ = GQ [130] & AF = AG [57] ⇒  EQ:EL = FQ:FA [171]
145. MJ ⟂ EF [36] & IL ⟂ EF [42] & EF ⟂ HC [47] & EQ ∥ EF [126] & FQ ∥ EQ [132] & C,A,F are collinear [04] & EL ∥ AC [52] ⇒  ∠QEL = ∠QFA [172]
146. EQ:EL = FQ:FA [171] & ∠QEL = ∠QFA [172] (Similar Triangles)⇒  ∠EQL = ∠FQA [173]
147. ∠(GF-MN) = ∠(BJ-FE) [134] & ∠GFN = ∠(BJ-OK) [98] ⇒  ∠MNF = ∠(EF-KO) [174]
148. GE ⟂ MN [141] & ∠(CH-EF) = ∠(BH-EG) [146] & EF ⟂ MJ [36] & IL ⟂ EF [42] & EF ⟂ HC [47] & FQ ∥ EQ [132] & EQ ∥ EF [126] & ∠(CH-EF) = ∠(EG-BH) [152] & BH ∥ BN [154] ⇒  NB ∥ NM [175]
149. NB ∥ NM [175] ⇒  B,M,N are collinear [176]
150. B,H,N are collinear [155] & O,P,N are collinear [22] & ∠MFQ = ∠MHQ [164] & MJ ⟂ EF [36] & IL ⟂ EF [42] & EF ⟂ HC [47] & EQ ∥ EF [126] & FQ ∥ EQ [132] & A,H,Q are collinear [26] & OP ∥ BC [78] & FM ∥ BC [49] & ∠EQL = ∠FQA [173] & ∠MNF = ∠(EF-KO) [174] & FG ⟂ HA [99] & OK ⟂ GF [72] & GE ⟂ MN [141] & ∠(CH-EF) = ∠(BH-EG) [146] & ∠(CH-EF) = ∠(EG-BH) [152] & B,M,N are collinear [176] ⇒  ∠FNH = ∠HNP [177]
151. NP = NF [84] & ∠FNH = ∠HNP [177] (SAS)⇒  HF = HP [178]
152. HE = HF [30] & HF = HP [178] ⇒  HP = HE
==========================

 

 

IMO 2002, Problem 2. Let BC be a diameter of circle ω with center O. Let A be a point of circle ω such that 0° < ∠AOB < 120°. Let D be the midpoint of arc AB not containing C. Line ℓ passes through O and is parallel to line AD. Line ℓ intersects line AC at J. The perpendicular bisector of segment OA intersects circle ω at E and F. Prove that J is the incenter of triangle CEF.

 

○ 풀이. Evan Chen의 풀이 

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

 

==========================
 * From theorem premises:
A B C D E F G H : Points
CA = CB [00]
B,A,C are collinear [01]
CD = CA [02]
CE = CA [03]
ED = EA [04]
∠FCD = ∠CDF [05]
∠DFC = ∠DFC [06]
CF = CA [07]
FC = FD [08]
∠GCD = ∠CDG [09]
∠CGD = ∠CGD [10]
CG = CA [11]
GC = GD [12]
B,D,H are collinear [13]
HC ∥ DE [14]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. ∠FCD = ∠CDF [05] & ∠DFC = ∠DFC [06] (Similar Triangles)⇒  CD:CF = DC:DF [15]
002. CD:CF = DC:DF [15] & CF = CA [07] & CD = CA [02] ⇒  DC = DF [16]
003. ∠GCD = ∠CDG [09] & ∠CGD = ∠CGD [10] (Similar Triangles)⇒  CD:CG = DC:DG [17]
004. CG = CA [11] & CD = CA [02] ⇒  CD = CG [18]
005. CE = CA [03] & CD = CA [02] ⇒  CD = CE [19]
006. CD = CE [19] (SSS)⇒  ∠CDE = ∠DEC [20]
007. CD = CA [02] & ED = EA [04] ⇒  DA ⟂ CE [21]
008. CD = CA [02] & CA = CB [00] ⇒  C is the circumcenter of \Delta BDA [22]
009. C is the circumcenter of \Delta BDA [22] & B,A,C are collinear [01] ⇒  BD ⟂ AD [23]
010. B,D,H are collinear [13] & ∠CDE = ∠DEC [20] & DA ⟂ CE [21] & BD ⟂ AD [23] & DE ∥ CH [14] ⇒  ∠DCH = ∠CHD [24]
011. ∠DCH = ∠CHD [24] ⇒  DC = DH [25]
012. DC = DF [16] & CD:CG = DC:DG [17] & CD = CG [18] & DC = DH [25] ⇒  G,F,C,H are concyclic [26]
013. G,F,C,H are concyclic [26] ⇒  ∠GFH = ∠GCH [27]
014. CF = CA [07] & CG = CA [11] & GC = GD [12] ⇒  GD = CF [28]
015. DC = DF [16] & CD = CG [18] & GD = CF [28] (SSS)⇒  CG ∥ DF [29]
016. CD = CA [02] & CG = CA [11] & CA = CB [00] & CE = CA [03] & CF = CA [07] ⇒  G,D,F,E are concyclic [30]
017. G,D,F,E are concyclic [30] ⇒  ∠GDF = ∠GEF [31]
018. CD = CG [18] (SSS)⇒  ∠CDG = ∠DGC [32]
019. ∠GDF = ∠GEF [31] & ∠CDG = ∠DGC [32] & CG ∥ DF [29] & ∠GCD = ∠CDG [09] ⇒  ∠GCD = ∠GEF [33]
020. CD = CA [02] & CF = CA [07] & CA = CB [00] & CE = CA [03] ⇒  B,D,F,E are concyclic [34]
021. B,D,F,E are concyclic [34] ⇒  ∠EDB = ∠EFB [35]
022. ∠EDB = ∠EFB [35] & ∠CDE = ∠DEC [20] & DA ⟂ CE [21] & BD ⟂ AD [23] & DE ∥ CH [14] ⇒  ∠DCH = ∠EFB [36]
023. ∠GCD = ∠GEF [33] & ∠DCH = ∠EFB [36] ⇒  ∠GCH = ∠(EG-BF) [37]
024. B,D,H are collinear [13] & DA ⟂ CE [21] & BD ⟂ AD [23] & DE ∥ CH [14] ⇒  ∠HDE = ∠ECH [38]
025. DE ∥ CH [14] ⇒  ∠HED = ∠EHC [39]
026. ∠HDE = ∠ECH [38] & ∠HED = ∠EHC [39] (Similar Triangles)⇒  HD = EC [40]
027. FC = FD [08] & CF = CA [07] & CG = CA [11] ⇒  CG = FD [41]
028. B,D,H are collinear [13] & DA ⟂ CE [21] & BD ⟂ AD [23] & DF ∥ CG [29] ⇒  ∠HDF = ∠ECG [42]
029. HD = EC [40] & CG = FD [41] & ∠HDF = ∠ECG [42] (SAS)⇒  ∠DHF = ∠CEG [43]
030. ∠GFH = ∠GCH [27] & CG ∥ DF [29] & CH ∥ DE [14] & ∠GCH = ∠(EG-BF) [37] & ∠DHF = ∠CEG [43] & B,D,H are collinear [13] & DA ⟂ CE [21] & BD ⟂ AD [23] ⇒  ∠BFH = ∠HFG
==========================

 

 

IMO 2003, Problem 4. Let ABCD be a cyclic quadrilateral. Let P, Q and R be the feet of perpendiculars from D to lines BC, CA and AB, respectively. Show that PQ = QR if and only if the bisectors of angles ABC and ADC meet on segment AC.

 

○ 풀이. Evan Chen의 풀이 

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

 

==========================
 * From theorem premises:
A B C O B1 D1 X D P Q R : Points
OB = OC [00]
OA = OB [01]
OB_1 = OA [02]
B_1C = B_1A [03]
OD_1 = OA [04]
D_1C = D_1A [05]
B,X,B_1 are collinear [06]
A,X,C are collinear [07]
OD = OA [08]
D_1,X,D are collinear [09]
P,B,C are collinear [10]
DP ⟂ BC [11]
QC:QD = QC:QD [12]
A,Q,C are collinear [13]
DQ ⟂ AC [14]
A,B,R are collinear [15]
DR ⟂ AB [16]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. OD_1 = OA [04] & OD = OA [08] & OB_1 = OA [02] ⇒  A,D_1,D,B_1 are concyclic [17]
002. A,D_1,D,B_1 are concyclic [17] & OB = OC [00] & OA = OB [01] & OD_1 = OA [04] & OB_1 = OA [02] ⇒  A,B,C,D are concyclic [18]
003. A,B,C,D are concyclic [18] ⇒  ∠BAD = ∠BCD [19]
004. A,B,C,D are concyclic [18] ⇒  ∠ABD = ∠ACD [20]
005. A,B,C,D are concyclic [18] ⇒  ∠CAD = ∠CBD [21]
006. A,B,R are collinear [15] & A,Q,C are collinear [13] & DQ ⟂ AC [14] & DR ⟂ AB [16] ⇒  ∠ARD = ∠AQD [22]
007. ∠ARD = ∠AQD [22] ⇒  A,Q,D,R are concyclic [23]
008. A,Q,D,R are concyclic [23] ⇒  ∠ADQ = ∠ARQ [24]
009. OA = OB [01] & OB = OC [00] ⇒  OC = OA [25]
010. OC = OA [25] & D_1C = D_1A [05] ⇒  CA ⟂ OD_1 [26]
011. OC = OA [25] & D_1C = D_1A [05] (SSS)⇒  ∠CD_1O = ∠OD_1A [27]
012. OC = OA [25] & B_1C = B_1A [03] ⇒  CA ⟂ OB_1 [28]
013. OC = OA [25] & B_1C = B_1A [03] (SSS)⇒  ∠CB_1O = ∠OB_1A [29]
014. ∠BAD = ∠BCD [19] & ∠ADQ = ∠ARQ [24] & A,B,R are collinear [15] & CA ⟂ OD_1 [26] & AC ⟂ B_1O [28] & DQ ⟂ AC [14] ⇒  ∠RQD = ∠BCD [30]
015. CA ⟂ OD_1 [26] & AC ⟂ B_1O [28] & A,Q,C are collinear [13] & DQ ⟂ AC [14] & DR ⟂ AB [16] ⇒  ∠(D_1O-AQ) = ∠(DR-AB) [31]
016. A,Q,C are collinear [13] & ∠ACD = ∠ABD [20] ⇒  ∠(AQ-DC) = ∠ABD [32]
017. ∠(D_1O-AQ) = ∠(DR-AB) [31] & ∠(AQ-DC) = ∠ABD [32] ⇒  ∠(D_1O-DC) = ∠RDB [33]
018. ∠(D_1O-DC) = ∠RDB [33] & CA ⟂ OD_1 [26] & AC ⟂ B_1O [28] & DQ ⟂ AC [14] ⇒  ∠QDR = ∠CDB [34]
019. ∠RQD = ∠BCD [30] & ∠QDR = ∠CDB [34] (Similar Triangles)⇒  QD:QR = DC:BC [35]
020. OB = OC [00] & OA = OB [01] & OD_1 = OA [04] & OB_1 = OA [02] ⇒  D_1,B_1,B,C are concyclic [36]
021. OB = OC [00] & OA = OB [01] & OD_1 = OA [04] & OB_1 = OA [02] ⇒  D_1,B_1,A,B are concyclic [37]
022. D_1,B_1,B,C are concyclic [36] ⇒  ∠D_1B_1B = ∠D_1CB [38]
023. D_1,B_1,A,B are concyclic [37] ⇒  ∠D_1B_1B = ∠D_1AB [39]
024. B,X,B_1 are collinear [06] & ∠D_1B_1B = ∠D_1CB [38] & ∠CD_1O = ∠OD_1A [27] & CA ⟂ OD_1 [26] & AC ⟂ B_1O [28] & ∠D_1B_1B = ∠D_1AB [39] ⇒  ∠ABX = ∠XBC [40]
025. ∠ABX = ∠XBC [40] & A,X,C are collinear [07] ⇒  AX:AB = XC:BC [41]
026. A,D_1,D,B_1 are concyclic [17] & OB = OC [00] & OA = OB [01] & OD_1 = OA [04] & OB_1 = OA [02] ⇒  D_1,B_1,C,D are concyclic [42]
027. D_1,B_1,C,D are concyclic [42] ⇒  ∠D_1B_1C = ∠D_1DC [43]
028. D_1,B_1,A,D are concyclic [17] ⇒  ∠D_1B_1A = ∠D_1DA [44]
029. D_1,X,D are collinear [09] & ∠D_1B_1C = ∠D_1DC [43] & ∠CB_1O = ∠OB_1A [29] & CA ⟂ OD_1 [26] & AC ⟂ B_1O [28] & ∠D_1B_1A = ∠D_1DA [44] ⇒  ∠ADX = ∠XDC [45]
030. ∠ADX = ∠XDC [45] & A,X,C are collinear [07] ⇒  AX:AD = XC:DC [46]
031. AX:AB = XC:BC [41] & AX:AD = XC:DC [46] ⇒  DC:BC = AD:AB [47]
032. P,B,C are collinear [10] & A,Q,C are collinear [13] & DQ ⟂ AC [14] & DP ⟂ BC [11] ⇒  ∠CPD = ∠CQD [48]
033. ∠CPD = ∠CQD [48] ⇒  P,Q,D,C are concyclic [49]
034. P,Q,D,C are concyclic [49] ⇒  ∠PQC = ∠PDC [50]
035. ∠PQC = ∠PDC [50] & A,Q,C are collinear [13] & ∠ABD = ∠ACD [20] ⇒  ∠ABD = ∠QPD [51]
036. CA ⟂ OD_1 [26] & AC ⟂ B_1O [28] & A,Q,C are collinear [13] & P,B,C are collinear [10] & DQ ⟂ AC [14] & DP ⟂ BC [11] ⇒  ∠(D_1O-AQ) = ∠DPB [52]
037. A,Q,C are collinear [13] & P,B,C are collinear [10] & ∠CAD = ∠CBD [21] ⇒  ∠QAD = ∠PBD [53]
038. ∠(D_1O-AQ) = ∠DPB [52] & ∠QAD = ∠PBD [53] ⇒  ∠(D_1O-AD) = ∠PDB [54]
039. ∠(D_1O-AD) = ∠PDB [54] & CA ⟂ OD_1 [26] & AC ⟂ B_1O [28] & DQ ⟂ AC [14] ⇒  ∠QDP = ∠ADB [55]
040. ∠ABD = ∠QPD [51] & ∠QDP = ∠ADB [55] (Similar Triangles)⇒  QD:PQ = AD:AB [56]
041. QD:QR = DC:BC [35] & DC:BC = AD:AB [47] & QD:PQ = AD:AB [56] ⇒  QD:PQ = QD:QR [57]
042. QC:QD = QC:QD [12] & QD:PQ = QD:QR [57] ⇒  PQ = QR
==========================

 

 

IMO 2004, Problem 1. Let ABC be an acute-angled triangle with AB ≠ AC. The circle with diameter BC intersects the sides AB and AC at M and N respectively. Denote by O the midpoint of the side BC. The bisectors of the angles ∠BAC and ∠MON intersect at R. Prove that the circumcircles of the triangles BMR and CNR have a common point lying on the side BC.

 

○ 풀이. Evan Chen의 풀이 

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

 

==========================
 * From theorem premises:
A B C D E F G H I J : Points
DB = DC [00]
C,B,D are collinear [01]
A,B,E are collinear [02]
DE = DB [03]
DF = DB [04]
A,C,F are collinear [05]
∠BAG = ∠GAC [06]
∠EDG = ∠GDF [07]
HE = HG [08]
HB = HE [09]
IF = IG [10]
IC = IF [11]
HJ = HG [12]
IJ = IG [13]

 * Auxiliary Constructions:
K : Points
F,K,E are collinear [14]
KF = KE [15]

 * Proof steps:
001. HE = HG [08] & HJ = HG [12] & HB = HE [09] ⇒  E,J,B,G are concyclic [16]
002. E,J,B,G are concyclic [16] ⇒  ∠EBJ = ∠EGJ [17]
003. DB = DC [00] & DF = DB [04] & DE = DB [03] ⇒  E,C,B,F are concyclic [18]
004. DB = DC [00] & DF = DB [04] & DE = DB [03] ⇒  D is the circumcenter of \Delta CFE [19]
005. E,C,B,F are concyclic [18] ⇒  ∠EBC = ∠EFC [20]
006. DB = DC [00] & DF = DB [04] ⇒  DF = DC [21]
007. DF = DC [21] ⇒  ∠DFC = ∠FCD [22]
008. F,K,E are collinear [14] & ∠EBC = ∠EFC [20] & A,B,E are collinear [02] & A,C,F are collinear [05] & ∠DFC = ∠FCD [22] & C,B,D are collinear [01] ⇒  ∠(AC-FD) = ∠(AB-FK) [23]
009. DE = DB [03] & DF = DB [04] ⇒  DF = DE [24]
010. DF = DE [24] & KF = KE [15] ⇒  EF ⟂ DK [25]
011. DE = DB [03] & DB = DC [00] ⇒  D is the circumcenter of \Delta BEC [26]
012. D is the circumcenter of \Delta BEC [26] & C,B,D are collinear [01] ⇒  BE ⟂ EC [27]
013. A,B,E are collinear [02] & F,K,E are collinear [14] & EF ⟂ DK [25] & BE ⟂ EC [27] ⇒  ∠AEC = ∠FKD [28]
014. F,K,E are collinear [14] & KF = KE [15] ⇒  K is midpoint of FE [29]
015. D is the circumcenter of \Delta CFE [19] & K is midpoint of FE [29] ⇒  ∠FCE = ∠FDK [30]
016. ∠FCE = ∠FDK [30] & A,C,F are collinear [05] ⇒  ∠ACE = ∠FDK [31]
017. ∠AEC = ∠FKD [28] & ∠ACE = ∠FDK [31] (Similar Triangles)⇒  AE:FK = AC:FD [32]
018. AE:FK = AC:FD [32] & KF = KE [15] & CD = FD [21] ⇒  CA:CD = EA:EK [33]
019. C,B,D are collinear [01] & F,K,E are collinear [14] & A,B,E are collinear [02] & ∠EBC = ∠EFC [20] & A,C,F are collinear [05] ⇒  ∠ACD = ∠KEA [34]
020. CA:CD = EA:EK [33] & ∠ACD = ∠KEA [34] (Similar Triangles)⇒  DA:KA = DC:KE [35]
021. CA:CD = EA:EK [33] & ∠ACD = ∠KEA [34] (Similar Triangles)⇒  ∠CAD = ∠KAE [36]
022. ∠CAD = ∠KAE [36] & A,B,E are collinear [02] ⇒  ∠CAD = ∠KAB [37]
023. ∠BAG = ∠GAC [06] & ∠CAD = ∠KAB [37] (Angle chase)⇒  ∠GAK = ∠DAG [38]
024. DF = DE [24] & ∠EDG = ∠GDF [07] (SAS)⇒  GF = GE [39]
025. DF = DE [24] & ∠EDG = ∠GDF [07] (SAS)⇒  ∠DFG = ∠GED [40]
026. DF = DE [24] & GF = GE [39] ⇒  FE ⟂ DG [41]
027. FE ⟂ DG [41] & EF ⟂ DK [25] ⇒  K,D,G are collinear [42]
028. ∠GAK = ∠DAG [38] & K,D,G are collinear [42] ⇒  KG:DG = AK:AD [43]
029. DA:KA = DC:KE [35] & FD = CD [21] & KG:DG = AK:AD [43] & DE = FD [24] ⇒  GK:GD = EK:ED [44]
030. GK:GD = EK:ED [44] & K,D,G are collinear [42] ⇒  ∠KEG = ∠GED [45]
031. F,K,E are collinear [14] & ∠KEG = ∠GED [45] & ∠DFG = ∠GED [40] ⇒  ∠DFG = ∠(FK-EG) [46]
032. ∠(AC-FD) = ∠(AB-FK) [23] & ∠DFG = ∠(FK-EG) [46] ⇒  ∠(AC-FG) = ∠(AB-EG) [47]
033. IF = IG [10] & IJ = IG [13] & IC = IF [11] ⇒  F,J,C,G are concyclic [48]
034. F,J,C,G are concyclic [48] ⇒  ∠FCJ = ∠FGJ [49]
035. ∠EBJ = ∠EGJ [17] & A,B,E are collinear [02] & ∠(AC-FG) = ∠(AB-EG) [47] & ∠FCJ = ∠FGJ [49] & A,C,F are collinear [05] ⇒  ∠CJG = ∠BJG [50]
036. ∠CJG = ∠BJG [50] ⇒  JC ∥ JB [51]
037. CJ ∥ BJ [51] ⇒  J,C,B are collinear
==========================

 

 

IMO 2004, Problem 5. In a convex quadrilateral ABCD, the diagonal BD bisects neither the angle ABC nor the angle CDA. The point P lies inside ABCD and satisfies

 

∠PBC = ∠DBA and ∠PDC = ∠BDA.

 

Prove that ABCD is a cyclic quadrilateral if and only if AP = CP.

 

○ 풀이. Evan Chen의 풀이 

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

  

==========================
 * From theorem premises:
A B C O D P : Points
OA = OB [00]
OB = OC [01]
OD = OA [02]
∠PBC = ∠ABD [03]
∠PDC = ∠ADB [04]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. OA = OB [00] & OB = OC [01] ⇒  OC = OA [05]
002. OB = OC [01] & OA = OB [00] & OD = OA [02] ⇒  B,C,D,A are concyclic [06]
003. OB = OC [01] & OA = OB [00] & OD = OA [02] ⇒  OC = OD [07]
004. B,C,D,A are concyclic [06] ⇒  ∠BDC = ∠BAC [08]
005. B,C,D,A are concyclic [06] ⇒  ∠BCD = ∠BAD [09]
006. OC = OA [05] ⇒  ∠OCA = ∠CAO [10]
007. OB = OC [01] ⇒  ∠OCB = ∠CBO [11]
008. OC = OD [07] ⇒  ∠OCD = ∠CDO [12]
009. OA = OB [00] ⇒  ∠OAB = ∠ABO [13]
010. ∠PBC = ∠ABD [03] & ∠PDC = ∠ADB [04] & ∠BCD = ∠BAD [09] & ∠OCB = ∠CBO [11] & ∠OCD = ∠CDO [12] (Angle chase)⇒  ∠BPD = ∠BOD [14]
011. ∠BPD = ∠BOD [14] ⇒  B,O,P,D are concyclic [15]
012. B,O,P,D are concyclic [15] ⇒  ∠BPO = ∠BDO [16]
013. ∠PBC = ∠ABD [03] & ∠BDC = ∠BAC [08] & ∠OCA = ∠CAO [10] & ∠OCB = ∠CBO [11] & ∠OCD = ∠CDO [12] & ∠OAB = ∠ABO [13] & ∠BPO = ∠BDO [16] (Angle chase)⇒  ∠POA = ∠COP [17]
014. OC = OA [05] & ∠POA = ∠COP [17] (SAS)⇒  PC = PA
==========================

 

입력: 2024.05.05 18:42

수정: 2024.06.13 14:24