已知 △ABC 以及三个角α、β、γ，其中 α+β+γ=π，求作一点 P，使其到直线 BC、CA、AB 的垂足D、E、F满 ...
“作一个已知形状的三角形，使其顶点落在三条给定的直线上”比其对偶问题
“作一个已知形状的三角形，使其三边所在直线经过给定三点”
好像要麻烦一点。并且前者可以从后者得到解决。
对于楼主首页问题，可用复平面解析方法证明，程序代码见
http://kuing.infinityfreeapp.com/forum.php?mod=viewthread&tid=11171&pid=55264&page=1&extra=#pid55264 TSC999 发表于 2023-7-22 06:31
对于楼主首页问题，可用复平面解析方法证明，程序代码见
http://kuing.infinityfreeapp.com/forum.php?mod ...
http://kuing.infinityfreeapp.com/forum.php?mod=redirect&goto=findpost&ptid=11171&pid=55264
20楼才是你的代码，我把20楼的精确链接给你复制过来了 本帖最后由 hejoseph 于 2023-7-24 17:31 编辑
作图问题是这样得到的：若点 \(D\)、\(E\)、\(F\) 分别在直线 \(BC\)、\(CA\)、\(AB\) 上，且 \(\triangle DEF\) 的三个内角是固定的已知值，\(\odot AEF\)、\(\odot BFD\)、\(\odot CDE\) 共点于 \(P\)，那么点 \(P\) 是一个定点，与点 \(D\)、\(E\)、\(F\) 的位置无关。若点 \(D\)、\(E\)、\(F\) 共线，那么点 \(P\) 必定在 \(\triangle ABC\) 的外接圆上，这也是 Simson 定理的逆定理。 这命题推广到四面体能成立吗？ 为了让alphageometry也参与贡献。咱们翻译一下老胡的题目，先做一个圆$O$，在其上任取三点$O_1, O_2,O_3$,记三个圆两两相交的其他交点分别是$D,E,F$，也就是$O_1,O_2$交于$O,F$,$O_1,O_3$交于$O,E$,$O_2,O_3$交于$O,D$
设圆$O_1$上的自由点是$A$，那么$AF$交圆$O_2$于$B$,$AE$交圆$O_3$于$C$，那么就是要证明$B,D,C$共线，且$OA=OB=OC$。 geogebra按照上面的描述画的图
翻译成alphageometry的命题陈述的语法就是两个命题：
o = free; o1 = free; a = on_circle a o1 o; o2 = on_circle o2 o o1; f = on_circle f o1 o, on_circle f o2 o; o3 = on_circle o3 o o1; e = on_circle e o1 o, on_circle e o3 o; d = on_circle d o2 o, on_circle d o3 o; b = on_line b a f, on_circle b o2 o; c = on_line c a e, on_circle c o3 e ? coll b c d
o = free; o1 = free; a = on_circle a o1 o; o2 = on_circle o2 o o1; f = on_circle f o1 o, on_circle f o2 o; o3 = on_circle o3 o o1; e = on_circle e o1 o, on_circle e o3 o; d = on_circle d o2 o, on_circle d o3 o; b = on_line b a f, on_circle b o2 o; c = on_line c a e, on_circle c o3 e ? cong o a o b o c
然后输出的人类可读的证明如下：
证明输入的那个图里的$B,D,C$共线
alphageometry的输出图形把输入命题的点都重置了。重新标记了，如图：
==========================
* From theorem premises:
A B C D E F G H I J : Points
BC = BA
BE = BA
DE = DA
FG = FA
BG = BA
FH = FA
DH = DA
DI = DA
I,C,E are collinear
FJ = FG
C,J,G are collinear
* Auxiliary Constructions:
: Points
* Proof steps:
001. FG = FA & FJ = FG & FH = FA ⇒H,A,J,G are concyclic
002. H,A,J,G are concyclic ⇒∠HAG = ∠HJG
003. BC = BA & BG = BA & BE = BA ⇒A,C,E,G are concyclic
004. A,C,E,G are concyclic ⇒∠CEA = ∠CGA
005. DE = DA & DI = DA & DH = DA ⇒H,A,I,E are concyclic
006. H,A,I,E are concyclic ⇒∠HAE = ∠HIE
007. ∠HAG = ∠HJG & C,J,G are collinear & ∠CEA = ∠CGA & ∠HAE = ∠HIE & I,C,E are collinear ⇒∠IHA = ∠JHA
008. ∠IHA = ∠JHA ⇒HI ∥ HJ
009. HI ∥ HJ ⇒H,I,J are collinear
==========================
再让他证明输入图的$OA = OB$，如下(alphageometry的输出图形把输入命题的点都重置了。重新标记了)
==========================
* From theorem premises:
A B C D E I : Points
BC = BA
AD = AB
DE = DA
BE = BA
I,E,C are collinear
DI = DA
* Auxiliary Constructions:
F G H : Points
AF = AB
BG = BA
FG = FA
DH = DA
FH = FA
* Proof steps:
001. BG = BA & AF = AB & FG = FA ⇒GF = GB
002. AF = AB & GF = GB ⇒BF ⟂ AG
003. AF = AB & AD = AB ⇒AD = AF
004. DH = DA & AD = AB & AF = AB & FH = FA ⇒HF = HD
005. AD = AF & HF = HD ⇒DF ⟂ AH
006. BF ⟂ AG & DF ⟂ AH ⇒∠(BF-AG) = ∠(AH-DF)
007. FG = FA & AF = AB ⇒AB = GF
008. AD = AB & DE = DA ⇒AB = ED
009. AB = GF & AB = ED ⇒DE = GF
010. BG = BA & AF = AB ⇒FA = BG
011. AB = GF & FA = BG (SSS)⇒AB ∥ FG
012. BE = BA & AD = AB ⇒AD = EB
013. DE = BA & AD = EB (SSS)⇒DE ∥ AB
014. AB ∥ FG & DE ∥ AB ⇒∠DEF = ∠GFE
015. DE = GF & ∠DEF = ∠GFE (SAS)⇒∠(DE-FG) = ∠(DF-EG)
016. ∠(BF-AG) = ∠(AH-DF) & ∠(DE-FG) = ∠(DF-EG) & AB ∥ FG & DE ∥ AB ⇒∠(FB-AG) = ∠(AH-GE)
017. DH = DA & DI = DA & DE = DA ⇒H,A,E,I are concyclic
018. H,A,E,I are concyclic ⇒∠HAI = ∠HEI
019. DH = DA & AD = AB & AF = AB ⇒AF = HD
020. FH = FA & AF = AB & AD = AB ⇒DA = FH
021. DA = FH & AF = HD (SSS)⇒AF ∥ DH
022. AF ∥ DH & DE ∥ AB ⇒∠EDH = ∠BAF
023. DE = BA & AF = HD & ∠EDH = ∠BAF (SAS)⇒∠(DE-AB) = ∠(EH-BF)
024. I,E,C are collinear & ∠HAI = ∠HEI & ∠(DE-AB) = ∠(EH-BF) & DE ∥ AB ⇒∠HAI = ∠(FB-IE)
025. ∠(FB-AG) = ∠(AH-GE) & ∠HAI = ∠(FB-IE) ⇒∠(GE-IA) = ∠(AG-IE)
026. BE = BA & BG = BA & BC = BA ⇒A,E,G,C are concyclic
027. A,E,G,C are concyclic ⇒∠AGE = ∠ACE
028. I,E,C are collinear & ∠(GE-IA) = ∠(AG-IE) & ∠AGE = ∠ACE ⇒∠ACI = ∠CIA
029. ∠ACI = ∠CIA ⇒AC = AI
==========================
页:
1
[2]