数学研发论坛

 找回密码
 欢迎注册
查看: 1045|回复: 1

[分享] mathematica 机器证明平面几何定理【例 3】

[复制链接]
发表于 2017-5-24 22:47:25 | 显示全部楼层 |阅读模式

马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。

您需要 登录 才可以下载或查看,没有帐号?欢迎注册

x
彭色列定理图.png

彭色列定理的最简单情况:从三角形 ABC 的外接圆上任意一点 $ Q $作内切圆的两条切线,设它们分别交外接圆于点$ Q1 $和$ Q2 $,则$ Q1Q2 $ 也是内切圆的切线 (如上图)。

程序如下:

  1. XI = 0; YI = 0;  (*  令三角形内切圆的半径为 1, 圆心位于坐标系原点  *)
  2. ZI = XI + YI I;  (*  三角形内切圆圆心 I 的复坐标  *)
  3. u =.; v =.;
  4. XB = u; YB = -1; XC = v; YC = -1;  (*  定义 B、C 点的坐标。BC 平行于横轴。u, v \
  5. 是独立变量,u<0, v>0  *)
  6. ZB = XB + YB I; ZC = XC + YC I;  (*  B、C 点的复坐标  *)

  7. (*  下面求 A 点的坐标  *)
  8. XA =.; YA =.; aa = {XA, YA} /.
  9.   Assuming[XA (YB - YC) + XB (YC - YA) + XC (YA - YB) > 0 ,
  10.    Solve[{(XA Sqrt[(XB - XC)^2 + (YB - YC)^2] +
  11.        XB Sqrt[(XA - XC)^2 + (YA - YC)^2] +
  12.        XC Sqrt[(XA - XB)^2 + (YA - YB)^2])/(
  13.       Sqrt[(XA - XB)^2 + (YA - YB)^2] +
  14.        Sqrt[(XB - XC)^2 + (YB - YC)^2] +
  15.        Sqrt[(XC - XA)^2 + (YC - YA)^2]) == 0, (
  16.       YA Sqrt[(XB - XC)^2 + (YB - YC)^2] +
  17.        YB Sqrt[(XA - XC)^2 + (YA - YC)^2] +
  18.        YC Sqrt[(XA - XB)^2 + (YA - YB)^2])/(
  19.       Sqrt[(XA - XB)^2 + (YA - YB)^2] +
  20.        Sqrt[(XB - XC)^2 + (YB - YC)^2] +
  21.        Sqrt[(XC - XA)^2 + (YC - YA)^2]) == 0, (
  22.       XA (YB - YC) + XB (YC - YA) + XC (YA - YB))/(
  23.       Sqrt[(XA - XB)^2 + (YA - YB)^2] +
  24.        Sqrt[(XB - XC)^2 + (YB - YC)^2] +
  25.        Sqrt[(XC - XA)^2 + (YC - YA)^2]) == 1}, {XA, YA }]];
  26. bb = aa[[1]];
  27. XA = bb[[1]];   (* A 点的横坐标 *)
  28. YA = bb[[2]];  (* A 点的纵坐标 *)
  29. ZA = Simplify[XA + YA I];  (* A 点的复坐标 *)

  30. Print["\!\(\*
  31. StyleBox["程序给出的证明如下",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  32. StyleBox[":",\nFontColor->RGBColor[0, 0, 1]]\) "];
  33. Print["\!\(\*
  34. StyleBox["\[EmptyUpTriangle]ABC",\nFontColor->RGBColor[0, 0, \
  35. 1]]\)\!\(\*
  36. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  37. StyleBox["各顶点的复坐标",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  38. StyleBox[":",\nFontColor->RGBColor[0, 0, 1]]\) "];
  39. Print["A = ", ZA];
  40. ZB = Simplify[XB + YB I];  (* B 点的复坐标 *)
  41. Print["B = ", ZB];
  42. ZC = Simplify[XC + YC I];  (* C 点的复坐标 *)
  43. Print["C = ", ZC];

  44. (* 三角形 ABC 外接圆圆心 O 的坐标:  *)
  45. XO = ((XA^2 (YB - YC) + XB^2 ( YC - YA) +
  46.      XC^2 ( YA - YB)) - (YA - YB ) ( YB - YC) (YC - YA))/(
  47.   2 XA (YB - YC) + 2 XB ( YC - YA) + 2 XC ( YA - YB));
  48. YO = -(((YA^2 (XB - XC) + YB^2 ( XC - XA) +
  49.       YC^2 ( XA - XB)) - (XA - XB ) ( XB - XC) (XC - XA))/(
  50.    2 XA (YB - YC) + 2 XB ( YC - YA) + 2 XC ( YA - YB)));
  51. ZO = Factor[XO + YO I];
  52. Print["\!\(\*
  53. StyleBox["\[EmptyUpTriangle]ABC",\nFontColor->RGBColor[0, 0, \
  54. 1]]\)\!\(\*
  55. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  56. StyleBox["外接圆圆心的复坐标",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  57. StyleBox[":",\nFontColor->RGBColor[0, 0, 1]]\) "];
  58. Print["O = ", ZO];

  59. (* 下面求三角形 ABC 外接圆的半径 R  *)
  60. R = Assuming[u < 0 && v > 0 && 1 + u v < 0,
  61.    Factor[Simplify[
  62.      Sqrt[((XA - XB)^2 + (YA - YB)^2)  ((XB - XC)^2 + (YB -
  63.           YC)^2) ((XC - XA)^2 + (YC - YA)^2)]/(
  64.      2 (XA (YB - YC) + XB (YC - YA) + XC (YA - YB)))]]];
  65. Print["\!\(\*
  66. StyleBox["\[EmptyUpTriangle]ABC",\nFontColor->RGBColor[0, 0, \
  67. 1]]\)\!\(\*
  68. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  69. StyleBox["外接圆的半径",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  70. StyleBox[":",\nFontColor->RGBColor[0, 0, 1]]\) "];
  71. Print["R = ", R];

  72. \[Alpha] =.;   (* 在内切圆 I 上任取一点 P, IP 直线与横轴的夹角为 \[Alpha] *)
  73. XP = Cos[\[Alpha]]; YP = Sin[\[Alpha]] ;
  74. ZP = Factor[XP + YP I];  (* P 点的复坐标 *)
  75. Print["\!\(\*
  76. StyleBox["在内切圆",\nFontColor->RGBColor[0, 0, 1]]\) \!\(\*
  77. StyleBox["I",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  78. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  79. StyleBox["上任取一点",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  80. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  81. StyleBox["P",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  82. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  83. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  84. StyleBox["IP",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  85. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  86. StyleBox["与横轴的夹角为\[Alpha]",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  87. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  88. StyleBox["时",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  89. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  90. StyleBox["P",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  91. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  92. StyleBox["点的复坐标",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  93. StyleBox[":",\nFontColor->RGBColor[0, 0, 1]]\) "];
  94. Print["P = ", ZP];

  95. (* 自 P 点作圆 I 的切线,交圆 O 于 Q1 和 Q2,下面求 Q1 及 Q2 的坐标 *)
  96. (* Q1Q2 直线的方程是 x Cos[\[Alpha]]+y Sin[\[Alpha]]=1, 三角形 ABC 外接圆的方程是 \
  97. (x-XO)^2+(y-YO)^2= R^2  *)
  98. x =.; y =.; aa = {{x, y}} /.
  99.   Simplify[Assuming[u < 0 && v > 0 && 1 + u v < 0,
  100.     Solve[{x  Cos[\[Alpha]] + y  Sin[\[Alpha]] ==
  101.        1, (x - XO)^2 + (y - YO)^2 == R^2}, {Factor[Simplify[x]],
  102.       Factor[Simplify[y]] }]]];
  103. bb1 = aa[[1]];(* 交点 Q2 *)
  104. bb2 = aa[[2]];(* 交点 Q1 *)
  105. cc1 = bb1[[1]]; XQ2 = cc1[[1]]; YQ2 = cc1[[2]];
  106. cc2 = bb2[[1]]; XQ1 = cc2[[1]]; YQ1 = cc2[[2]];
  107. ZQ1 = Simplify[XQ1 + YQ1 I];
  108. ZQ2 = Simplify[XQ2 + YQ2 I] ;
  109. Print["\!\(\*
  110. StyleBox["自",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  111. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  112. StyleBox["P",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  113. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  114. StyleBox["点作圆",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  115. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  116. StyleBox["I",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  117. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  118. StyleBox["的切线",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  119. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  120. StyleBox["交\[EmptyUpTriangle]ABC",\nFontColor->RGBColor[0, 0, 1]]\)\
  121. \!\(\*
  122. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  123. StyleBox["外接圆于",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  124. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  125. StyleBox["Q1",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  126. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  127. StyleBox["和",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  128. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  129. StyleBox["Q2",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  130. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  131. StyleBox["则",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  132. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  133. StyleBox["Q1",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  134. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  135. StyleBox["及",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  136. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  137. StyleBox["Q2",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  138. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  139. StyleBox["的复坐标为",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  140. StyleBox[":",\nFontColor->RGBColor[0, 0, 1]]\) "];
  141. Print["Q1 = ", ZQ1];
  142. Print["Q2 = ", ZQ2];

  143.      (* 从 Q1 向单位圆 I 作切线,交 \[CircleDot]O 于 Q 点。 则该切线的方程是
  144.   (XP XQ1^2+2 XQ1 YP YQ1-XP YQ1^2)x+ (YP YQ1^2+2YQ1 XP XQ1-YP XQ1^2 \
  145. )y =XQ1^2+YQ1^2  
  146. 从 Q2 向单位圆 I 作切线,交 \[CircleDot]O 于 Q 点。 则该切线的方程是
  147. (XP XQ2^2+2 XQ2 YP YQ2-XP YQ2^2)x+ (YP YQ2^2+2YQ2 XP XQ2-YP XQ2^2 )y \
  148. =XQ2^2+YQ2^2  
  149.   下面求上述两条切线的交点 Q 的坐标   *)
  150. x =.; y =.; aa = {{x, y}} /.
  151.   Simplify[Assuming[u < 0 && v > 0 && 1 + u v < 0,
  152.     Solve[{(XP XQ1^2 + 2 XQ1 YP YQ1 - XP YQ1^2) x + (YP YQ1^2 +
  153.            2 YQ1 XP XQ1 - YP XQ1^2 ) y ==
  154.        XQ1^2 + YQ1^2, (XP XQ2^2 + 2 XQ2 YP YQ2 -
  155.            XP YQ2^2) x + (YP YQ2^2 +2 YQ2 XP XQ2 -YP XQ2^2 ) y ==
  156.        XQ2^2 + YQ2^2}, {Factor[Simplify[x]], Factor[Simplify[y]] }]]];
  157. bb = aa[[1]];(* 交点 Q *)
  158. cc = bb[[1]];
  159. XQ = cc[[1]];
  160. YQ = cc[[2]];
  161. ZQ = Simplify[XQ + YQ I];   (* 交点 Q 的复坐标 *)
  162. Print["\!\(\*
  163. StyleBox["从",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  164. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  165. StyleBox["Q1",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  166. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  167. StyleBox["和",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  168. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  169. StyleBox["Q2",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  170. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  171. StyleBox["分别向",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  172. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  173. StyleBox["\[CircleDot]",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  174. StyleBox["I",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  175. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  176. StyleBox["作切线",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  177. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  178. StyleBox["两条切线相交于",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  179. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  180. StyleBox["Q",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  181. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  182. StyleBox["点",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  183. StyleBox["。",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  184. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  185. StyleBox["则",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  186. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  187. StyleBox["Q",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  188. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  189. StyleBox["点的复坐标为",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  190. StyleBox[":",\nFontColor->RGBColor[0, 0, 1]]\) "];
  191. Print["Q = ", ZQ];

  192. (* 下面验证 A、B、C、Q 四点是否共圆。若四个点的复坐标分别是 Z1,Z2,Z3,Z4, 则这四点共圆的充要条件是   
  193. \[OpenCurlyDoubleQuote]交比\[CloseCurlyDoubleQuote] \
  194. Z=((Z1-Z3)(Z2-Z4))/((Z1-Z4)(Z2-Z3)) 的虚部等于零,或者说 Z 是一个实数。   *)
  195. Z0 = Factor[
  196.    Simplify[((ZA - ZC) (ZB - ZQ))/((ZA - ZQ) (ZB -
  197.        ZC))]];   (* 计算 A、B、C、Q 四点的交比 *)
  198. Print["\!\(\*
  199. StyleBox["下面验证",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  200. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  201. StyleBox["Q",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  202. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  203. StyleBox["点是否在",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  204. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  205. StyleBox["\[EmptyUpTriangle]ABC",\nFontColor->RGBColor[0, 0, \
  206. 1]]\)\!\(\*
  207. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  208. StyleBox["的外接圆上",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  209. StyleBox["。",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  210. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  211. StyleBox["为此须计算",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  212. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  213. StyleBox["A",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  214. StyleBox["、",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  215. StyleBox["B",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  216. StyleBox["、",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  217. StyleBox["C",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  218. StyleBox["、",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  219. StyleBox["Q",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  220. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  221. StyleBox["四点复坐标的交比",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  222. StyleBox["。",\nFontColor->RGBColor[0, 0, 1]]\) "];
  223. Print["Z0 = ", Z0];
  224. (* 判断交比的虚部是否等于零。若等于零,则 A、B、C、Q 四点共圆。 *)

  225. If[Factor[ComplexExpand[Im[Z0]]] == 0 ,
  226.   Print["\!\(\*
  227. StyleBox["由于交比",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  228. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  229. StyleBox["Z0",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  230. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  231. StyleBox["的虚部等于零",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  232. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  233. StyleBox["所以",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  234. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  235. StyleBox["A",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  236. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  237. StyleBox["B",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  238. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  239. StyleBox["C",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  240. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  241. StyleBox["Q",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  242. StyleBox[" ",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  243. StyleBox["四点共圆",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  244. StyleBox[",",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  245. StyleBox["这就证明了彭色列定理成立",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  246. StyleBox["。",\nFontColor->RGBColor[0, 0, 1]]\)"]];
复制代码


彭色列定理,程序给出的证明.png
毋因群疑而阻独见  毋任己意而废人言
毋私小惠而伤大体  毋借公论以快私情
 楼主| 发表于 2017-5-24 22:54:05 | 显示全部楼层
这个程序大约运行了 20 多秒吧。
毋因群疑而阻独见  毋任己意而废人言
毋私小惠而伤大体  毋借公论以快私情
您需要登录后才可以回帖 登录 | 欢迎注册

本版积分规则

小黑屋|手机版|数学研发网 ( 苏ICP备07505100号 )

GMT+8, 2019-11-14 10:11 , Processed in 0.160455 second(s), 19 queries .

Powered by Discuz! X3.4

© 2001-2017 Comsenz Inc.

快速回复 返回顶部 返回列表