无字证明 by Steve Phelps

GeoGebra 命令及参数

1. Point(xAxis) → A
2. Point(xAxis) → B
3. Line(A, B) → t
4. Polygon(B, A, 4) → poly3, n, p, q, r, H, I
5. Semicircle(A, B) → c
6. Point(c) → C
7. Polygon(C, B, 4) → poly2, j, k, l, m, F, G
8. Centroid(poly2) → J
9. OrthogonalLine(J, n) → s
10. Polygon(A, C, 4) → poly1, f, g, h, i, D, E
11. Centroid(poly3) → K
12. Centroid(poly1) → L
13. Angle(A, C, B) → α
14. Intersect(s, j) → M
15. Intersect(s, l) → N
16. Midpoint(j) → O
17. Mirror(M, O) → M'
18. Mirror(M', J) → M''
19. OrthogonalLine(J, s) → a
20. Midpoint(k) → P
21. Intersect(a, k) → Q
22. Mirror(Q, P) → Q'
23. Mirror(Q, J) → Q'_1
24. Mirror(Q', J) → Q''
25. Polygon(J, M, B, Q') → q1, j_1, m_1, b, q'
26. Polygon(J, Q, F, M'') → q2, j_2, q_1, f_1, m''
27. Polygon(J, N, G, Q'') → q3, j_3, n_1, g_1, q''
28. Polygon(J, Q'_1, C, M') → q4, j_4, q'_1, c_1, m'
29. If(0 < o ≤ 1, Polygon[Translate[J, Vector[J, Dilate[J, 1 - o, A]]], Translate[M, Vector[J, Dilate[J, 1 - o, A]]], Translate[B, Vector[J, Dilate[J, 1 - o, A]]], Translate[Q', Vector[J, Dilate[J, 1 - o, A]]]], Polygon[Translate[J, A - J], Translate[M, A - J], Translate[B, A - J], Translate[Q', A - J]]) → q5
30. If(2 < o ≤ 3, Polygon[Translate[J, Vector[J, Dilate[J, 3 - o, H]]], Translate[Q, Vector[J, Dilate[J, 3 - o, H]]], Translate[F, Vector[J, Dilate[J, 3 - o, H]]], Translate[M'', Vector[J, Dilate[J, 3 - o, H]]]], Polygon[Translate[J, H - J], Translate[Q, H - J], Translate[F, H - J], Translate[M'', H - J]]) → q6
31. If(4 < o ≤ 5, Polygon[Translate[J, Vector[J, Dilate[J, 5 - o, I]]], Translate[N, Vector[J, Dilate[J, 5 - o, I]]], Translate[G, Vector[J, Dilate[J, 5 - o, I]]], Translate[Q'', Vector[J, Dilate[J, 5 - o, I]]]], Polygon[Translate[J, I - J], Translate[N, I - J], Translate[G, I - J], Translate[Q'', I - J]]) → q7
32. If(6 < o ≤ 7, Polygon[Translate[J, Vector[J, Dilate[J, 7 - o, B]]], Translate[Q'_1, Vector[J, Dilate[J, 7 - o, B]]], Translate[C, Vector[J, Dilate[J, 7 - o, B]]], Translate[M', Vector[J, Dilate[J, 7 - o, B]]]], Polygon[Translate[J, B - J], Translate[Q'_1, B - J], Translate[C, B - J], Translate[M', B - J]]) → q8
33. Polygon(J, M', M) → t1, m_2, j_5, d
34. Polygon(J, Q', Q) → t2, q_2, j_6, e
35. Polygon(J, M'', N) → t3, n_2, j_7, h_1
36. Polygon(J, Q'', Q'_1) → t4, i_1, j_8, k_1
37. If(8 < o ≤ 9, Polygon[Translate[J, Vector[J, Dilate[J, 9 - o, B]]], Translate[M', Vector[J, Dilate[J, 9 - o, B]]], Translate[M, Vector[J, Dilate[J, 9 - o, B]]]], Polygon[Translate[J, B - J], Translate[M', B - J], Translate[M, B - J]]) → t5
38. If(10 < o ≤ 11, Polygon[Translate[J, Vector[J, Dilate[J, 11 - o, A]]], Translate[Q', Vector[J, Dilate[J, 11 - o, A]]], Translate[Q, Vector[J, Dilate[J, 11 - o, A]]]], Polygon[Translate[J, A - J], Translate[Q', A - J], Translate[Q, A - J]]) → t6
39. If(12 < o ≤ 13, Polygon[Translate[J, Vector[J, Dilate[J, 13 - o, H]]], Translate[M'', Vector[J, Dilate[J, 13 - o, H]]], Translate[N, Vector[J, Dilate[J, 13 - o, H]]]], Polygon[Translate[J, H - J], Translate[M'', H - J], Translate[N, H - J]]) → t7
40. If(14 < o ≤ 15, Polygon[Translate[J, Vector[J, Dilate[J, 15 - o, I]]], Translate[Q'', Vector[J, Dilate[J, 15 - o, I]]], Translate[Q'_1, Vector[J, Dilate[J, 15 - o, I]]]], Polygon[Translate[J, I - J], Translate[Q'', I - J], Translate[Q'_1, I - J]]) → t8
41. Polygon(A, E, D, C) → q9, a_1, e_1, d_1, c_2
42. If(16 < o ≤ 17, Polygon[Translate[A, Vector[L, Dilate[L, 17 - o, K]]], Translate[E, Vector[L, Dilate[L, 17 - o, K]]], Translate[D, Vector[L, Dilate[L, 17 - o, K]]], Translate[C, Vector[L, Dilate[L, 17 - o, K]]]], Polygon[Translate[A, K - L], Translate[E, K - L], Translate[D, K - L], Translate[C, K - L]]) → q10