1.12. Geometric applications
Tree problem
In the island there are only 2 trees, A and B, and the remnants of a hanging place.
Start at the hanging place and count the steps to go in a straight line to tree A. When you arrive, turn 90º to the left and walk the same amount of steps. Where you stopped, place a mark on the ground, and call this point A'
Go back to the hanging place and count the steps to tree B, also in a straight line. When there, turn 90º to the right and walk the same amount of steps forward and place a mark on the ground. This is point B'
Bury the treasure box at the mid-point of A' and B'.
-
H : Hanging place
-
A : tree A
-
B : tree B
-
A': the first mark on the ground
-
B': the second mark
-
T : Location of the treasure box
Prove that we can find the location of the treasure box even if the hanging place disappeared in the island. Show that the location of the treasure box does not depend on the location of the hanging place
Use the geometric meaning that multiplication by the imaginary unit is rotation by 90 degrees counterclockwise.
We verify below that the location T of the tree can be recovered from the other
three points using complex number addition and multiplication.
T = (A+B)/2+ I*(A-B)/2.
example {H A B A' B' T: ℚ[i]}
(h1 : A' = A+I*(A-H) ) -- A' is the first mark
(h2 : B' = B-I*(B-H) ) -- B' is the second mark
(h3 : T = (A'+B')/2 ) -- T is the midpoint of A' and B'
: T = (A+B)/2+ I*(A-B)/2 := H:ℚ[i]A:ℚ[i]B:ℚ[i]A':ℚ[i]B':ℚ[i]T:ℚ[i]h1:A' = A + I * (A - H)h2:B' = B - I * (B - H)h3:T = (A' + B') / 2⊢ T = (A + B) / 2 + I * (A - B) / 2
H:ℚ[i]A:ℚ[i]B:ℚ[i]A':ℚ[i]B':ℚ[i]T:ℚ[i]h1:A' = A + I * (A - H)h2:B' = B - I * (B - H)h3:T = (A' + B') / 2⊢ (A + I * (A - H) + (B - I * (B - H))) / 2 = (A + B) / 2 + I * (A - B) / 2
All goals completed! 🐙
Napolean problem
Draw an arbitrary polygon with 4 sides.
Label the vertices by A, B, C and D. On each side,
we draw a square with this side as the base. Label the midpoint
of the four squares by P, Q, R and S.
Show that the line PR is perpendicular to the line QS.
-
Pis the midpoint of the square with basedAB. -
Qis the midpoint of the square with basedBC. -
Ris the midpoint of the square with basedCD. -
Sis the midpoint of the square with basedDA.
Again, we leverage the geometric meaning that mulitplication by I is
the same as rotation by 90 degrees counter-clockwise. We will show below that
Q-S = I*(P-R). We need the theorem I^2=-1, which is proved earlier.
The proof is just substitution and then doing some algebra.
theorem Napolean_problem (A B C D P Q R S : ℚ[i])
(hP : P = (A+B)/2 + I*(A-B)/2)
(hQ : Q = (B+C)/2 + I*(B-C)/2)
(hR : R = (C+D)/2 + I*(C-D)/2)
(hS : S = (D+A)/2 + I*(D-A)/2)
: Q-S = I*(P-R) := A:ℚ[i]B:ℚ[i]C:ℚ[i]D:ℚ[i]P:ℚ[i]Q:ℚ[i]R:ℚ[i]S:ℚ[i]hP:P = (A + B) / 2 + I * (A - B) / 2hQ:Q = (B + C) / 2 + I * (B - C) / 2hR:R = (C + D) / 2 + I * (C - D) / 2hS:S = (D + A) / 2 + I * (D - A) / 2⊢ Q - S = I * (P - R)
A:ℚ[i]B:ℚ[i]C:ℚ[i]D:ℚ[i]P:ℚ[i]Q:ℚ[i]R:ℚ[i]S:ℚ[i]hP:P = (A + B) / 2 + I * (A - B) / 2hQ:Q = (B + C) / 2 + I * (B - C) / 2hR:R = (C + D) / 2 + I * (C - D) / 2hS:S = (D + A) / 2 + I * (D - A) / 2⊢ (B + C) / 2 + I * (B - C) / 2 - ((D + A) / 2 + I * (D - A) / 2) =
I * ((A + B) / 2 + I * (A - B) / 2 - ((C + D) / 2 + I * (C - D) / 2))
A:ℚ[i]B:ℚ[i]C:ℚ[i]D:ℚ[i]P:ℚ[i]Q:ℚ[i]R:ℚ[i]S:ℚ[i]hP:P = (A + B) / 2 + I * (A - B) / 2hQ:Q = (B + C) / 2 + I * (B - C) / 2hR:R = (C + D) / 2 + I * (C - D) / 2hS:S = (D + A) / 2 + I * (D - A) / 2⊢ B + C + I * (B - C) - (D + A + I * (D - A)) = I * (A + B + I * (A - B) - (C + D + I * (C - D))) -- clear denominator
A:ℚ[i]B:ℚ[i]C:ℚ[i]D:ℚ[i]P:ℚ[i]Q:ℚ[i]R:ℚ[i]S:ℚ[i]hP:P = (A + B) / 2 + I * (A - B) / 2hQ:Q = (B + C) / 2 + I * (B - C) / 2hR:R = (C + D) / 2 + I * (C - D) / 2hS:S = (D + A) / 2 + I * (D - A) / 2⊢ B + B * I + C - C * I - I * D + I * A - D - A =
B * I - B * I ^ 2 - C * I - C * I ^ 2 - I * D + I * A + I ^ 2 * D + I ^ 2 * A
A:ℚ[i]B:ℚ[i]C:ℚ[i]D:ℚ[i]P:ℚ[i]Q:ℚ[i]R:ℚ[i]S:ℚ[i]hP:P = (A + B) / 2 + I * (A - B) / 2hQ:Q = (B + C) / 2 + I * (B - C) / 2hR:R = (C + D) / 2 + I * (C - D) / 2hS:S = (D + A) / 2 + I * (D - A) / 2⊢ B + B * I + C - C * I - I * D + I * A - D - A = B * I - B * -1 - C * I - C * -1 - I * D + I * A + -1 * D + -1 * A -- simplify using I^2 = -1
All goals completed! 🐙
end complex_number_game