ag4masses/outputs/solved/castillon-lemma-ag-ok.log

I0211 17:53:45.675628 140166174494720 graph.py:498] castillon_lemma
I0211 17:53:45.676038 140166174494720 graph.py:499] a b = segment a b; c = on_circle c a b; d = on_line d a b, lc_tangent d c a; e = foot e c a b; f = on_circle f a b; g = on_tline g d a b, lc_tangent g f a; h = on_line h d g, on_line h e f; i = on_circle i a b; j = on_circle j a b, on_line j i g; k = on_circle k a b, on_line k i h ? coll e j k
I0211 17:56:14.703040 140166174494720 alphageometry.py:191] 
==========================
 * From theorem premises:
A B C D E F G H I J K : Points
AC = AB [00]
D,A,B are collinear [01]
CD ⟂ AC [02]
CE ⟂ AB [03]
A,E,B are collinear [04]
AF = AB [05]
∠BAF = ∠BAF [06]
AB ⟂ GD [07]
FG ⟂ AF [08]
F,H,E are collinear [09]
D,G,H are collinear [10]
AI = AB [11]
AJ = AB [12]
G,J,I are collinear [13]
AK = AB [14]
H,K,I are collinear [15]

 * Auxiliary Constructions:
: Points


 * Proof steps:
001. AB ⟂ GD [07] & CE ⟂ AB [03] ⇒  GD ∥ CE [16]
002. AI = AB [11] & AK = AB [14] & AC = AB [00] & AF = AB [05] & AJ = AB [12] ⇒  J,C,B,K are concyclic [17]
003. J,C,B,K are concyclic [17] ⇒  ∠JBC = ∠JKC [18]
004. J,C,B,K are concyclic [17] ⇒  ∠JCB = ∠JKB [19]
005. AC = AB [00] ⇒  ∠ACB = ∠CBA [20]
006. AK = AB [14] & AC = AB [00] ⇒  AC = AK [21]
007. AC = AK [21] ⇒  ∠ACK = ∠CKA [22]
008. AK = AB [14] ⇒  ∠ABK = ∠BKA [23]
009. CE ⟂ AB [03] & DG ∥ CE [16] & ∠JBC = ∠JKC [18] & ∠JCB = ∠JKB [19] & ∠ACB = ∠CBA [20] & ∠ACK = ∠CKA [22] & ∠ABK = ∠BKA [23] (Angle chase)⇒  ∠(DG-BJ) = ∠BCJ [24]
010. ∠(DG-BJ) = ∠BCJ [24] & DG ∥ CE [16] & ∠BCJ = ∠BKJ [19] ⇒  ∠BKJ = ∠(DG-JB) [25]
011. AI = AB [11] & AF = AB [05] & AJ = AB [12] ⇒  A is the circumcenter of \Delta FIJ [26]
012. A is the circumcenter of \Delta FIJ [26] & FG ⟂ AF [08] ⇒  ∠GFI = ∠FJI [27]
013. G,J,I are collinear [13] & ∠GFI = ∠FJI [27] ⇒  ∠FJG = ∠GFI [28]
014. G,J,I are collinear [13] ⇒  ∠FGJ = ∠FGI [29]
015. ∠FJG = ∠GFI [28] & ∠FGJ = ∠FGI [29] (Similar Triangles)⇒  FJ:FG = FI:GI [30]
016. ∠FJG = ∠GFI [28] & ∠FGJ = ∠FGI [29] (Similar Triangles)⇒  FJ:GJ = FI:FG [31]
017. D,A,B are collinear [01] & FG ⟂ AF [08] & CE ⟂ AB [03] & CE ∥ DG [16] ⇒  ∠GDA = ∠GFA [32]
018. ∠GDA = ∠GFA [32] ⇒  D,F,A,G are concyclic [33]
019. D,F,A,G are concyclic [33] ⇒  ∠FDG = ∠FAG [34]
020. D,F,A,G are concyclic [33] ⇒  ∠DFG = ∠DAG [35]
021. A,E,B are collinear [04] & CE ⟂ AB [03] & CD ⟂ AC [02] ⇒  ∠ACD = ∠CEA [36]
022. D,A,B are collinear [01] & AB ⟂ DG [07] ⇒  DA ⟂ DG [37]
023. DA ⟂ DG [37] & CD ⟂ AC [02] ⇒  ∠ADC = ∠(DG-CA) [38]
024. DA ⟂ DG [37] & CD ⟂ AC [02] ⇒  ∠DAC = ∠GDC [39]
025. D,A,B are collinear [01] & ∠ADC = ∠(DG-CA) [38] & DG ∥ CE [16] ⇒  ∠ADC = ∠ECA [40]
026. ∠ACD = ∠CEA [36] & ∠ADC = ∠ECA [40] (Similar Triangles)⇒  AC:AD = AE:AC [41]
027. AC:AD = AE:AC [41] & AC = AB [00] & FA = AB [05] ⇒  AE:AF = AF:AD [42]
028. A,E,B are collinear [04] & D,A,B are collinear [01] & ∠BAF = ∠BAF [06] ⇒  ∠EAF = ∠DAF [43]
029. AE:AF = AF:AD [42] & ∠EAF = ∠DAF [43] (Similar Triangles)⇒  ∠AEF = ∠DFA [44]
030. F,H,E are collinear [09] & ∠DFG = ∠DAG [35] & D,A,B are collinear [01] & ∠AEF = ∠DFA [44] & A,E,B are collinear [04] ⇒  ∠AFH = ∠FGA [45]
031. FG ⟂ AF [08] & ∠AFH = ∠FGA [45] ⇒  ∠GFH = ∠FAG [46]
032. F,H,E are collinear [09] & ∠FDG = ∠FAG [34] & DG ∥ CE [16] & ∠GFH = ∠FAG [46] ⇒  ∠HFG = ∠GDF [47]
033. D,G,H are collinear [10] & CE ∥ DG [16] ⇒  ∠FGD = ∠FGH [48]
034. ∠HFG = ∠GDF [47] & ∠FGD = ∠FGH [48] (Similar Triangles)⇒  DF:FG = FH:GH [49]
035. ∠HFG = ∠GDF [47] & ∠FGD = ∠FGH [48] (Similar Triangles)⇒  DF:DG = FH:FG [50]
036. FJ:FG = FI:GI [30] & FJ:GJ = FI:FG [31] & DF:FG = FH:GH [49] & DF:DG = FH:FG [50] (Ratio chase)⇒  GI:GH = DG:GJ [51]
037. G,J,I are collinear [13] & D,G,H are collinear [10] ⇒  ∠DGJ = ∠HGI [52]
038. GI:GH = DG:GJ [51] & ∠DGJ = ∠HGI [52] (Similar Triangles)⇒  ∠GDJ = ∠HIG [53]
039. AI = AB [11] & AK = AB [14] & AC = AB [00] & AF = AB [05] & AJ = AB [12] ⇒  J,B,K,I are concyclic [54]
040. J,B,K,I are concyclic [54] ⇒  ∠JBK = ∠JIK [55]
041. ∠GDJ = ∠HIG [53] & DG ∥ CE [16] & ∠JBK = ∠JIK [55] & G,J,I are collinear [13] & H,K,I are collinear [15] ⇒  ∠KBJ = ∠GDJ [56]
042. ∠BKJ = ∠(DG-JB) [25] & ∠KBJ = ∠GDJ [56] ⇒  ∠KJB = ∠BJD [57]
043. A,E,B are collinear [04] & D,A,B are collinear [01] ⇒  B,D,E are collinear [58]
044. A,E,B are collinear [04] & D,A,B are collinear [01] & CE ⟂ AB [03] ⇒  ∠DEC = ∠CEA [59]
045. A,E,B are collinear [04] & ∠DAC = ∠GDC [39] & D,A,B are collinear [01] & DG ∥ CE [16] ⇒  ∠DCE = ∠CAE [60]
046. ∠DEC = ∠CEA [59] & ∠DCE = ∠CAE [60] (Similar Triangles)⇒  CD:AC = CE:AE [61]
047. AC:AD = AE:AC [41] & AC = AB [00] & JA = AB [12] ⇒  AE:AJ = AJ:AD [62]
048. A,E,B are collinear [04] & D,A,B are collinear [01] ⇒  ∠EAJ = ∠DAJ [63]
049. AE:AJ = AJ:AD [62] & ∠EAJ = ∠DAJ [63] (Similar Triangles)⇒  EA:EJ = JA:JD [64]
050. EA:EJ = JA:JD [64] & AJ = AB [12] & CA = AB [00] ⇒  CA:DJ = AE:JE [65]
051. CA:DC = AE:CE [61] & CA:DJ = AE:JE [65] ⇒  DC:CE = DJ:JE [66]
052. CD ⟂ AC [02] & CE ⟂ AB [03] & ∠ACB = ∠CBA [20] (Angle chase)⇒  ∠DCB = ∠BCE [67]
053. ∠DCB = ∠BCE [67] & B,D,E are collinear [58] ⇒  DB:EB = DC:CE [68]
054. DC:CE = DJ:JE [66] & DB:EB = DC:CE [68] ⇒  BD:BE = JD:JE [69]
055. BD:BE = JD:JE [69] & B,D,E are collinear [58] ⇒  ∠BJD = ∠EJB [70]
056. ∠KJB = ∠BJD [57] & ∠BJD = ∠EJB [70] ⇒  ∠EJB = ∠KJB [71]
057. ∠EJB = ∠KJB [71] ⇒  JE ∥ JK [72]
058. EJ ∥ JK [72] ⇒  J,K,E are collinear
==========================

I0211 17:56:14.704421 140166174494720 alphageometry.py:195] Solution written to /home/tong_peng/pyvenv/agtest/ag.out.