Theory Complex_Triangles
theory Complex_Triangles
imports Complex_Trigonometry Third_Unity_Root
begin
lemma similar_triangles':
assumes h:"a ≠ 0 ∧ b ≠ 0 ∧ 0 ≠ c ∧ a' ≠ 0 ∧ b'≠0 ∧ c'≠0"
and h1:‹∠ (-a) b = ∠ (-a') b'› ‹∠ (-b') c' = ∠ (-b) c›
shows ‹∠ (-c) a = ∠ (-c') a'›
proof -
have ‹⇂∠ (-a) b + ∠ (-b) c + ∠ (-c) a⇃ = pi›
using angle_sum_triangle' h by auto
also have ‹⇂∠ (-a') b' + ∠ (-b') c' + ∠ (-c') a'⇃ = pi›
using angle_sum_triangle' h by auto
also have ‹⇂∠ (-a') b' + ∠ (-b') c' + ∠ (-c) a⇃ = pi›
using ‹⇂∠ (- a) b + ∠ (- b) c + ∠ (- c) a⇃ = pi› h1(1,2) by auto
then have ‹⇂∠ (- c) a⇃ = ⇂∠ (- c') a'⇃›
by (smt (verit) ‹⇂∠ (- a') b' + ∠ (- b') c' + ∠ (- c') a'⇃ = pi› add.inverse_inverse ang_vec_bounded
ang_vec_opposite1 ang_vec_opposite2 ang_vec_opposite_opposite ang_vec_plus_pi1 ang_vec_plus_pi2
canon_ang_diff canon_ang_id h neg_0_equal_iff_equal)
ultimately show ?thesis
by (metis ang_vec_bounded canon_ang_id)
qed
lemma similar_triangles:
assumes h:"a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ a' ≠ b' ∧ b'≠ c' ∧ c'≠a'"
and h1:‹∠ (c-a) (b-a) = ∠ (c'-a') (b'-a')› ‹∠ (a-b) (c-b) = ∠ (a'-b') (c'-b')›
shows ‹ ∠ (b-c) (a-c) = ∠ (b'-c') (a'-c')›
proof -
have ‹a-b≠0› ‹b-c≠0› ‹a-c≠0› ‹a'-b'≠0› ‹b'-c'≠0› ‹c'-a'≠0›
using h by auto
then show ?thesis
by (smt (z3) diff_numeral_special(12) h1(1,2) minus_diff_eq similar_triangles')
qed
lemma similar_triangles_c:
assumes h:"a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ a' ≠ b' ∧ b'≠ c' ∧ c'≠a'"
and h1:‹angle_c c a b = angle_c c' a' b'› ‹angle_c a b c = angle_c a' b' c'›
shows ‹angle_c b c a = angle_c b' c' a'›
proof -
have ‹a-b≠0› ‹b-c≠0› ‹a-c≠0› ‹a'-b'≠0› ‹b'-c'≠0› ‹c'-a'≠0›
using h by auto
then show ?thesis
unfolding angle_c_def
by (metis angle_c_def h h1(1,2) similar_triangles)
qed
lemmas congruent_ctriangleD = congruent_ctriangle.sides congruent_ctriangle.angles
lemma congruent_ctriangles_sss:
assumes h:"a ≠ b ∧ b ≠ c ∧ a ≠ c"
and h1:‹cmod (b - a)= cmod (b'-a')› ‹cmod (b - c) = cmod (b' - c')› ‹cmod (c - a) = cmod (c' - a')›
shows ‹congruent_ctriangle a b c a' b' c'›
proof -
{fix c b a c' b' a'
assume h:"a ≠ b ∧ b ≠ c ∧ a ≠ c"
and h1:‹cmod (b - a)= cmod (b'-a')› ‹cmod (b - c) = cmod (b' - c')› ‹cmod (c - a) = cmod (c' - a')›
then have h':‹a'≠b' ∧ b'≠c' ∧ c'≠a'›
by auto
have ‹cos (∠ (c-a) (b-a)) = ((cdist b c)⇧2 - (cdist a c)⇧2 - (cdist a b)⇧2 ) / (- 2*(cdist a c)*(cdist a b)) ›
using law_of_cosines' h by auto
moreover have ‹cos (∠ (c'-a') (b'-a')) = ((cdist b' c')⇧2 - (cdist a' c')⇧2 - (cdist a' b')⇧2 ) / (- 2*(cdist a' c')*(cdist a' b')) ›
using law_of_cosines' h h' by auto
ultimately have f0:‹cos (∠ (c-a) (b-a)) = cos (∠ (c'-a') (b'-a'))›
by (metis cdist_def h1(1,2,3) norm_minus_commute)
have ‹∠ (c-a) (b-a) ∈ {-pi .. pi}› ‹∠ (c'-a') (b'-a') ∈ {-pi..pi}›
unfolding ang_vec_def
using canon_ang(1,2) less_eq_real_def by auto
with f0 have ‹∠ (c-a) (b-a) = ∠ (c'-a') (b'-a') ∨ ∠ (c-a) (b-a) = - ∠ (c'-a') (b'-a')›
unfolding ang_vec_def
by (smt (verit) arccos_cos2 arccos_minus_1 arccos_unique canon_ang(1,2))}note dem=this
then show ?thesis
by (metis (mono_tags, lifting) angle_c_def cdist_def
congruent_ctriangle_def h h1(1) h1(2) h1(3) norm_minus_commute)
qed
lemma congruent_ctriangleI_sss:
assumes h:"a ≠ b ∧ b ≠ c ∧ a ≠ c"
and h1:‹cdist a b = cdist a' b'› ‹cdist b c = cdist b' c'› ‹cdist a c = cdist a' c'›
shows ‹congruent_ctriangle a b c a' b' c'›
using cdist_def congruent_ctriangles_sss h1(1,2,3) h
by (metis dist_commute dist_complex_def)
lemmas congruent_ctriangle_sss = congruent_ctriangleD[OF congruent_ctriangleI_sss]
lemma isosceles_triangles:
assumes ‹cdist a b = cdist b c›
shows ‹angle_c b c a = angle_c b a c ∨ angle_c b c a = - angle_c b a c ›
by (metis assms cdist_commute cdist_def congruent_ctriangle_sss(14) norm_eq_zero right_minus_eq)
lemma non_collinear_independant:"¬ collinear a b c ⟹ a ≠ b ∧ b ≠ c ∧ a ≠ c"
using collinear_ex_real by force
lemma congruent_ctriangleI_sas:
assumes ‹a1 ≠ b1 ∧ b1 ≠ c1 ∧ a1 ≠ c1›
assumes h1:"cdist a1 b1 = cdist a2 b2"
assumes h2:"cdist b1 c1 = cdist b2 c2"
assumes h3:"angle_c a1 b1 c1 = angle_c a2 b2 c2 ∨ angle_c a1 b1 c1 = - angle_c a2 b2 c2"
shows "congruent_ctriangle a1 b1 c1 a2 b2 c2"
proof (rule congruent_ctriangleI_sss)
have h1':"cdist a1 b1 = cdist b2 a2"
using cdist_commute h1 by auto
show "cdist a1 c1 = cdist a2 c2"
proof (rule power2_eq_imp_eq)
show "(cdist a1 c1)⇧2 = (cdist a2 c2)⇧2"
apply(insert law_of_cosines[of a1 c1 b1] law_of_cosines[of a2 c2 b2])
apply(subst (asm) (1 2) h2) apply(subst (asm) (1 2) h1'[symmetric])
using assms unfolding angle_c_def
by (smt (verit) congruent_ctriangle_sss(7) angle_c_commute angle_c_def
cos_minus)
qed simp_all
show "a1 ≠ b1 ∧ b1 ≠ c1 ∧ a1 ≠ c1"
"cdist a1 b1 = cdist a2 b2"
"cdist b1 c1 = cdist b2 c2" using assms cdist_commute by auto
qed
lemmas congruent_ctriangle_sas = congruent_ctriangleD[OF congruent_ctriangleI_sas]
lemma congruent_ctriangleI_aas:
assumes h1:"angle_c a1 b1 c1 = angle_c a2 b2 c2"
assumes h2:"angle_c b1 c1 a1 = angle_c b2 c2 a2"
assumes h3:"cdist a1 b1 = cdist a2 b2"
assumes h4:"¬collinear a1 b1 c1" "¬collinear a2 b2 c2"
shows "congruent_ctriangle a1 b1 c1 a2 b2 c2"
proof (rule congruent_ctriangleI_sas)
from h4 have neq: "a1 ≠ b1" unfolding collinear_def by auto
with assms(3) have neq': "a2 ≠ b2" by auto
have h0:‹a1 ≠ b1› ‹b1 ≠ c1› ‹a1 ≠ c1›
using assms(4) non_collinear_independant by auto
have h0':‹a2 ≠ b2› ‹b2 ≠ c2› ‹a2 ≠ c2›
using assms(5) non_collinear_independant by auto
have A: "angle_c c1 a1 b1 = angle_c c2 a2 b2" using neq neq' assms
apply(insert angle_sum_triangle_c[of a1 b1 c1] angle_sum_triangle_c[of a2 b2 c2])
by (metis h0 assms(5) h1 h2 non_collinear_independant similar_triangles_c)
have ‹-∠ (b1 - c1) (a1 - c1) = - ∠ (b2 - c2) (a2 - c2)›
using h2 unfolding angle_c_def by auto
then have A1:‹angle_c a1 c1 b1 = angle_c a2 c2 b2›
using h2 unfolding angle_c_def
apply(cases ‹angle_c a1 c1 b1 = pi›)
apply (metis ang_vec_def angle_c_def canon_ang_uminus_pi minus_diff_eq)
by (metis ang_vec_sym ang_vec_sym_pi)
have ‹∠ (b1 - a1) (c1 - a1) = ∠ (b2 - a2) (c2 - a2)›
by (metis ang_vec_sym ang_vec_sym_pi angle_c_def A)
have sine1:‹ sin (angle_c a1 c1 b1) * cdist c1 b1 = sin (angle_c b1 a1 c1) * cdist a1 b1›
by (metis h0 law_of_sines)
have sine2:‹sin (angle_c a2 c2 b2) * cdist c2 b2 = sin (angle_c b2 a2 c2) * cdist a2 b2›
by (metis assms(5) law_of_sines non_collinear_independant)
have ‹¬collinear a2 b2 c2 ⟹ sin (angle_c a2 c2 b2) ≠ 0›
unfolding collinear_def angle_c_def
using angle_c_def collinear_sin_neq_0 h4(2) by presburger
have h3':‹cdist b1 a1 = cdist b2 a2›
using h3 cdist_commute by auto
have A2:‹angle_c b1 a1 c1 = angle_c b2 a2 c2›
using ‹∠ (b1 - a1) (c1 - a1) = ∠ (b2 - a2) (c2 - a2)› angle_c_def by auto
have ‹ cdist c1 b1 = sin (angle_c b2 a2 c2) * cdist a2 b2 / sin (angle_c a2 c2 b2) ∧
cdist c2 b2 = sin (angle_c b2 a2 c2) * cdist a2 b2 / sin (angle_c a2 c2 b2) ›
apply(cases ‹ sin (angle_c a2 c2 b2) = 0›)
apply (simp add:
‹¬ Elementary_Complex_Geometry.collinear a2 b2 c2 ⟹ sin (angle_c a2 c2 b2) ≠ 0›
‹¬ Elementary_Complex_Geometry.collinear a2 b2 c2›)
by (metis A1 A2 h3 nonzero_mult_div_cancel_left sine1 sine2)
then show "cdist b1 c1 = cdist b2 c2"
using cdist_commute by auto
show "a1 ≠ b1 ∧ b1 ≠ c1 ∧ a1 ≠ c1"
"cdist a1 b1 = cdist a2 b2"
"angle_c a1 b1 c1 = angle_c a2 b2 c2 ∨ angle_c a1 b1 c1 = - angle_c a2 b2 c2"
using assms h0 neq by auto
qed
lemmas congruent_ctriangle_aas = congruent_ctriangleD[OF congruent_ctriangleI_aas]
lemma congruent_ctriangleI_asa:
assumes "angle_c a1 b1 c1 = angle_c a2 b2 c2"
assumes "cdist a1 b1 = cdist a2 b2"
assumes h0:"angle_c b1 a1 c1 = angle_c b2 a2 c2"
assumes h4:"¬collinear a1 b1 c1" "¬collinear a2 b2 c2"
shows "congruent_ctriangle a1 b1 c1 a2 b2 c2"
proof (rule congruent_ctriangleI_aas)
from assms have neq: "a1 ≠ b1" "a2 ≠ b2" unfolding collinear_def by auto
show "angle_c b1 c1 a1 = angle_c b2 c2 a2"
apply (rule similar_triangles_c)
using assms(4,5) non_collinear_independant apply auto[1]
using h0 unfolding angle_c_def
apply (metis ang_vec_sym ang_vec_sym_pi)
using angle_c_def assms(1) by auto
qed fact+
lemmas congruent_ctriangle_asa = congruent_ctriangleD[OF congruent_ctriangleI_asa]
lemma orientation_respect_letter_order:
assumes "angle_c a b c = angle_c b a c" "¬ collinear a b c"
shows "False"
by (smt (verit, ccfv_threshold) angle_c_commute assms(1)
assms(2) collinear_sin_neq_0 collinear_sym1 similar_triangles_c sin_pi sin_zero)
lemma isoscele_iff_pr_cis_qr:
assumes h':‹q≠r›
shows ‹(cdist q r = cdist p r) ⟷ (p-r) = cis(angle_c q r p)*(q-r)›
proof (rule iffI)
assume h:‹(cdist q r = cdist p r)›
then have f0:‹cmod(p-r) = cmod(q-r)›
by (simp add: norm_minus_commute)
have ‹(p-r)/(q-r) = (p-r)*cnj(q-r)/cmod(q-r)^2›
using complex_div_cnj by blast
have f1:‹Re ((p-r)*cnj(q-r)) = cmod(p-r)*cmod(q-r)*cos(angle_c q r p)›
by (metis (no_types, lifting) ang_cos cdist_commute cdist_def h(1))
have f2: ‹Im ((p-r)*cnj(q-r)) = cmod(p-r)*cmod(q-r)* sin(angle_c q r p)›
using ang_sin h(1) by auto
then have ‹ (p-r)*cnj(q-r)/cmod(q-r)^2 = cmod(p-r)*cmod(q-r)*cis(angle_c q r p)/cmod(q-r)^2›
apply(intro complex_eqI)
using f1 f2 by auto
then have f3:‹(p-r)/(q-r) = cmod(p-r)*cmod(q-r)*cis(angle_c q r p)/cmod(q-r)^2›
by (simp add: ‹(p - r) / (q - r) = (p - r) * cnj (q - r) / cor ((cmod (q - r))⇧2)›)
have ‹(p-r)/(q-r) = cis (angle_c q r p)›
apply(subst f3) apply(subst f0) by(simp add:h h' power2_eq_square)
then show ‹p - r = cis (angle_c q r p) * (q - r)›
using divide_eq_eq h h' by force
next
assume ‹p - r = cis (angle_c q r p) * (q - r) ›
have ‹(p-r)/(q-r) = (p-r)*cnj(q-r)/cmod(q-r)^2›
using complex_div_cnj by blast
have f1:‹Re ((p-r)*cnj(q-r)) = cmod(p-r)*cmod(q-r)*cos(angle_c q r p)›
using ang_cos by fastforce
have f2: ‹Im ((p-r)*cnj(q-r)) = cmod(p-r)*cmod(q-r)* sin(angle_c q r p)›
using ang_sin by fastforce
then have f4:‹ (p-r)*cnj(q-r)/cmod(q-r)^2 = cmod(p-r)*cmod(q-r)*cis(angle_c q r p)/cmod(q-r)^2›
apply(intro complex_eqI)
using f1 f2 by auto
then have f3:‹(p-r)/(q-r) = cmod(p-r)*cmod(q-r)*cis(angle_c q r p)/cmod(q-r)^2›
by (simp add: ‹(p - r) / (q - r) = (p - r) * cnj (q - r) / cor ((cmod (q - r))⇧2)›)
have ‹cmod(p-r)*cmod(q-r)*cis(angle_c q r p)/cmod(q-r)^2 = cis (angle_c q r p)›
using ‹p - r = cis (angle_c q r p) * (q - r)› ‹q ≠ r› f3 by auto
then have ‹cmod(p-r)*cmod(q-r)/cmod(q-r)^2 = 1›
by (metis f4 ‹q ≠ r› cmod_power2 complex_mod_cnj complex_mod_mult_cnj complex_mult_cnj
eq_iff_diff_eq_0 nonzero_norm_divide norm_cis norm_eq_zero norm_mult power_not_zero)
then show ‹cdist q r = cdist p r›
by (metis cdist_commute cdist_def eq_divide_eq_1 mult.commute power2_eq_square real_divide_square_eq)
qed
lemma equilateral_imp_pi3:
assumes ‹q≠r› "cdist q r = cdist p r" "cdist p r = cdist p q"
shows "⇂(angle_c q r p)⇃ = pi/3 ∨ ⇂(angle_c q r p)⇃ = -pi/3"
"(angle_c q r p) = (angle_c p q r) ∧ (angle_c q r p) = (angle_c r p q)"
proof -
have f0:‹q≠r ∧ r≠p ∧ p≠q› using assms by(auto)
have ‹angle_c q r p ≠ 0 ∧ angle_c q r p ≠ pi›
by (smt (verit, best) Re_complex_of_real angle_c_commute angle_c_commute_pi assms(1) assms(2)
assms(3) cdist_commute cdist_def congruent_ctriangle_sss(20) cor_cmod_real isoscele_iff_pr_cis_qr
minus_complex.simps(1) minus_complex.simps(2) minus_diff_eq mult_minus_right norm_eq_zero right_minus_eq)
then have f1:‹¬collinear q r p›
using collinear_angle f0 by blast
then have f1':‹¬collinear p q r›
by (simp add: collinear_sym1 collinear_sym2)
have f12:‹(angle_c q r p) = angle_c r p q ∨ (angle_c q r p) = - angle_c r p q›
apply(rule congruent_ctriangle_sss)
using f0 assms by(auto simp:norm_minus_commute)
have f4:‹(angle_c q r p) = angle_c p q r ∨ (angle_c q r p) = - angle_c p q r›
apply(rule congruent_ctriangle_sss)
using f0 assms by(auto simp:norm_minus_commute)
have f5:‹(angle_c q r p) ≠ pi›
using f1
by (metis angle_c_commute canon_ang_sin canon_ang_uminus_pi collinear_sin_neq_0 f1' pi_canonical
sin_pi)
from f4 have ‹ ⇂(angle_c q r p) + (angle_c r p q) + (angle_c p q r)⇃ = pi›
using angle_sum_triangle_c[of p q r] f0 by auto
have ‹∀x∈{-pi..0}. 3*x ≠ pi›
by (metis atLeastAtMost_iff dual_order.trans mult_eq_0_iff mult_less_cancel_right2 numeral_le_one_iff
pi_ge_zero pi_neq_zero semiring_norm(70) verit_comp_simplify1(3) verit_la_disequality)
also have the_x:‹∃!x∈{-pi<..pi}. 3*x = pi›
by(auto intro:exI[where x=‹pi/3›])
moreover have ‹(angle_c x y z) ∈{-pi<..pi}› for x y z
using ang_c_in by auto
have ‹x∈{-3*pi<..3*pi} ∧ x-2*pi = pi ⟹ ( x = 3*pi)› for x k::real
by(auto simp:)
have ‹x∈{-3*pi<..3*pi} ∧ x-2*k*pi = pi ∧ ( k≥2 ∨ k≤ - 2) ⟹ False› for x and k::int
proof -
assume h:‹x∈{-3*pi<..3*pi} ∧ x-2*k*pi = pi ∧ ( k≥2 ∨ k≤ -2)›
then have f0:‹ r = 2 ⟹ x - 2* r*pi ≤ -pi› for r by auto
also have f1:‹k > 2 ⟹ x - 2* k*pi < x-2*2*pi›
by(auto)
have f3:‹x-2*2*pi ≤ -pi›
using f0[of 2] by(auto simp:abs_real_def)
then have f2:‹ k > 2 ⟹ x - 2* k*pi < -pi›
using f1 by argo
ultimately have f3:‹ k ≥2 ⟹ x-2* k*pi ≤ -pi›
apply(cases ‹abs k=2›) using f0 by(auto)
have f0':‹r=-2 ⟹ x - 2*r*pi > pi› for r ::int
using h by(auto)
have ‹x+2*2*pi > pi› using h by auto
also have ‹k< -2 ⟹ x -2*k*pi > x - 2*(-2)*pi›
using f0'[of 2]
proof -
assume a1: "k < - 2"
have f2: "pi < x - real_of_int (- 4) * pi"
using f0' by force
have "k + k ≤ - 4"
using a1 by force
then show ?thesis
using f2 by (metis (no_types) diff_left_mono h mult.commute mult_2_right of_int_le_iff ordered_comm_semiring_class.comm_mult_left_mono pi_ge_zero verit_comp_simplify1(3))
qed
ultimately have f4:‹k ≤ -2 ⟹ x-2* k*pi > pi›
apply(cases ‹k=-2›) using h
‹k < - 2 ⟹ x - 2 * - 2 * pi < x - real_of_int (2 * k) * pi› by auto
show False
using f3 f4 h by force
qed
then have possible_k:‹x∈{-3*pi<..3*pi} ∧ x-2*k*pi = pi ⟹ k=-1 ∨ k=1 ∨ k=0› for k::int and x
by force
have ang_3_in:‹y∈{-3*pi<..3*pi} ∧ ⇂y⇃ = pi ⟷ y=pi ∨ y = 3*pi ∨ y=-pi› for y
proof(rule iffI)
assume hyp:‹y ∈ {- 3 * pi<..3 * pi} ∧ ⇂y⇃ = pi›
have ‹∃k. y - 2*k*pi = pi›
by (metis add_diff_cancel_left' diff_add_cancel divide_self_if field_sum_of_halves mult.commute mult_1 mult_2
pi_neq_zero times_divide_eq_right)
with hyp show ‹y = pi ∨ y=3*pi ∨ y= -pi›
using hyp possible_k canon_ang_pi_3pi[of y] canon_ang_id canon_ang_uminus_pi
by (smt (verit, del_insts) canon_ang_minus_3pi_minus_pi greaterThanAtMost_iff)
next
assume ‹y = pi ∨ y = 3 * pi ∨ y = - pi›
then show ‹y ∈ {- 3 * pi<..3 * pi} ∧ ⇂y⇃ = pi›
by(auto simp:canon_ang_uminus_pi canon_ang_pi_3pi)
qed
ultimately have ‹⇂3*(angle_c q r p)⇃ = pi ⟹ angle_c q r p = -pi/3 ∨ angle_c q r p = pi/3›
proof -
assume ‹⇂3*(angle_c q r p)⇃ = pi›
have ‹3*(angle_c q r p) ∈ {-3*pi<..3*pi}›
using ang_c_in by auto
then have f0:‹3*(angle_c q r p) = -pi ∨ 3*(angle_c q r p) = pi ∨ 3*(angle_c q r p) = 3*pi›
using ang_3_in ‹⇂3*(angle_c q r p)⇃ = pi› by blast
then have ‹3*(angle_c q r p) = 3*pi ⟹ False›
using collinear_sin_neq_pi by (simp add: f5)
then show ‹angle_c q r p = -pi/3 ∨ angle_c q r p = pi/3›
using f0 by auto
qed
have f2:‹⇂angle_c x y z ⇃ = angle_c x y z› for x y z::complex
using ang_vec_bounded angle_c_def canon_ang_id by fastforce
then have ‹⇂3*(angle_c q r p)⇃ = pi›
apply (cases ‹(angle_c q r p) = - angle_c r p q›)
apply(simp add:f1 f2)
apply (metis add.commute add.right_inverse add.right_neutral angle_sum_triangle_c canon_ang_uminus_pi f0 f2 f4 f5)
by (smt (verit) ‹⇂angle_c q r p + angle_c r p q + angle_c p q r⇃ = pi›
‹angle_c q r p = angle_c p q r ∨ angle_c q r p = - angle_c p q r›
‹angle_c q r p = angle_c r p q ∨ angle_c q r p = - angle_c r p q› canon_ang_uminus_pi
f2)
then have ‹angle_c q r p = -pi/3 ∨ angle_c q r p = pi/3›
using ‹⇂3 * angle_c q r p⇃ = pi ⟹ angle_c q r p = - pi / 3 ∨ angle_c q r p = pi / 3› by auto
then show ‹⇂angle_c q r p⇃ = pi / 3 ∨ ⇂angle_c q r p⇃ = - pi / 3›
using f2 by auto
then show ‹angle_c q r p = angle_c p q r ∧ angle_c q r p = angle_c r p q›
by (smt (verit, del_insts) ‹⇂angle_c q r p + angle_c r p q + angle_c p q r⇃ = pi›
f12 collinear_sin_neq_0 collinear_sym1 f1' f2 f4 f5 sin_pi)
qed
lemma isosceles_triangle_converse:
assumes "angle_c a b c = angle_c c a b" "¬collinear a b c"
shows "dist a c = dist b c"
by (metis assms(1) assms(2) cdist_def collinear_sin_neq_0 collinear_sym1 congruent_ctriangle_asa(8)
congruent_ctriangle_asa(9) dist_complex_def law_of_sines mult_cancel_left non_collinear_independant)
lemma pi3_imp_equilateral:
assumes ‹q≠r› ‹p≠q› ‹r≠p›
and ‹(angle_c q p r) = pi/3 ∨ (angle_c q p r) = -pi/3›
and ‹(angle_c q p r) = (angle_c r q p)›
and ‹(angle_c q p r) = (angle_c p r q)›
shows ‹cdist p r = cdist q r ∧ cdist p r = cdist p q›
proof(safe)
have f0:‹¬ collinear q p r›
using assms(1-3) unfolding collinear_def
by (smt (verit, ccfv_SIG) arccos_one_half arcsin_one_half arcsin_plus_arccos assms(4)
collinear_angle collinear_def divide_le_eq_1_pos divide_pos_pos minus_divide_left
pi_def pi_gt_zero pi_half)
then show ‹cdist p r = cdist q r›
using isosceles_triangle_converse[of q p r] assms
by (simp add: dist_complex_def norm_minus_commute)
show ‹cdist p r = cdist p q ›
using f0 isosceles_triangle_converse[of p r q] assms
by (metis ‹cdist p r = cdist q r› cdist_def collinear_iff dist_commute dist_norm)
qed
lemma pi3_isoscele_imp_equilateral:
assumes ‹q≠r› ‹p≠q› "cdist q r = cdist p r"
and "⇂(angle_c q p r)⇃ = pi/3 ∨ ⇂(angle_c q p r)⇃ = -pi/3"
shows ‹cdist p q = cdist r q›
proof( - )
have f:‹angle_c p q r = (angle_c r p q)›
by (smt (verit, best) angle_c_commute angle_c_commute_pi assms(2) assms(3) cdist_commute
collinear_angle isosceles_triangles orientation_respect_letter_order)
have f0:‹r≠p›
using assms(1) assms(3) by force
then have ‹cdist q p = cdist r q›
by (smt (verit) congruent_ctriangle_sss(19) add_divide_distrib ang_vec_bounded
angle_c_commute angle_c_def angle_sum_triangle_c arccos_minus_one_half arccos_one_half arcsin_minus_one_half
arcsin_one_half arcsin_plus_arccos assms(2) assms(3) assms(4) canon_ang_id canon_ang_minus_3pi_minus_pi
cdist_commute field_sum_of_halves law_of_sines mult_cancel_right pi3_imp_equilateral sin_gt_zero sin_periodic_pi)
then show ‹cdist p q = cdist r q›
using cdist_commute by force
qed
lemma pi3_isoscele_imp_equilateral':
assumes ‹q≠r› ‹p≠q› "cdist q r = cdist p r"
and "⇂(angle_c q p r)⇃ = pi/3 ∨ ⇂(angle_c q p r)⇃ = -pi/3"
shows ‹cdist p r = cdist p q›
by (metis assms(2) assms(3) assms(4) cdist_commute pi3_isoscele_imp_equilateral)
lemma equilateral_caracterization:‹q≠r ⟹ (cdist q r = cdist p r ∧ cdist p r = cdist p q)
⟷ ((p-r) = cis(pi/3)*(q-r) ∨ (p-r) = cis(-pi/3)*(q-r))›
proof(rule iffI)
assume h: ‹q ≠ r› ‹cdist q r = cdist p r ∧ cdist p r = cdist p q ›
then have f1:‹p - r = cis (angle_c q r p) * (q - r) ∨ p - r = cis (- angle_c q r p) * (q - r)›
using isoscele_iff_pr_cis_qr by blast
have f0:‹q≠r ∧ r ≠ p ∧ p ≠ q› using h by auto
have ‹angle_c q r p = pi/3 ∨ angle_c q r p = -pi/3›
using equilateral_imp_pi3(1)[of q r p]
by (metis ang_vec_bounded angle_c_def canon_ang_id h(1) h(2))
then show ‹p - r = cis (pi / 3) * (q - r) ∨ p - r = cis (- pi / 3) * (q - r)›
using f1
by (metis add.inverse_inverse minus_divide_left)
next
assume h:‹q ≠ r› ‹p - r = cis (pi / 3) * (q - r) ∨ p - r = cis (- pi / 3) * (q - r)›
have ‹(p-r)/(q-r) = (p-r)*cnj(q-r)/cmod(q-r)^2›
using complex_div_cnj by blast
have f1:‹Re ((p-r)*cnj(q-r)) = cmod(p-r)*cmod(q-r)*cos(angle_c q r p)›
using ang_cos by force
have f2: ‹Im ((p-r)*cnj(q-r)) = cmod(p-r)*cmod(q-r)* sin(angle_c q r p)›
using ang_sin h(1) by auto
then have ‹ (p-r)*cnj(q-r)/cmod(q-r)^2 = cmod(p-r)*cmod(q-r)*cis(angle_c q r p)/cmod(q-r)^2›
apply(intro complex_eqI)
using f1 f2 by auto
then have f3:‹(p-r)/(q-r) = cmod(p-r)*cmod(q-r)*cis(angle_c q r p)/cmod(q-r)^2›
by (simp add: ‹(p - r) / (q - r) = (p - r) * cnj (q - r) / cor ((cmod (q - r))⇧2)›)
have ‹(p-r)/(q-r) = cis (angle_c q r p)›
apply(subst f3)
by (smt (z3) ‹(p - r) * cnj (q - r) / cor ((cmod (q - r))⇧2) = cor (cmod (p - r) * cmod (q - r))
* cis (angle_c q r p) / cor ((cmod (q - r))⇧2)› cis_divide cis_mult cis_neq_zero cis_zero
cmod_cor_divide complex_mod_cnj eq_iff_diff_eq_0 f3 h(1) h(2) nonzero_mult_divide_mult_cancel_left
nonzero_mult_divide_mult_cancel_right norm_cis norm_mult numeral_One of_real_1 of_real_divide
power2_less_0 times_divide_eq_left)
then have fpi:‹angle_c q r p = pi/3 ∨ angle_c q r p = -pi/3›
using h ang_c_in
by (smt (verit, best) add_divide_distrib ang_vec_bounded angle_c_def arccos_one_half
arcsin_one_half arcsin_plus_arccos cis_inj diff_eq_diff_eq diff_numeral_special(9)
divide_nonneg_pos field_sum_of_halves nonzero_divide_eq_eq)
then have ff:‹cdist p r = cdist q r›
by (metis ‹(p - r) / (q - r) = cis (angle_c q r p)› h(1) isoscele_iff_pr_cis_qr nonzero_divide_eq_eq right_minus_eq)
then have ‹angle_c p q r = angle_c q p r ∨ angle_c p q r = -angle_c q p r ›
by (metis congruent_ctriangle_sss(13) cdist_commute cdist_def norm_eq_zero right_minus_eq)
then have f10:‹⇂angle_c p q r + angle_c q r p + angle_c r p q⇃ = pi›
by (metis ‹angle_c q r p = pi / 3 ∨ angle_c q r p = - pi / 3› angle_c_neq0 angle_sum_triangle_c
divide_eq_0_iff h(1) neg_equal_0_iff_equal pi_neq_zero zero_neq_numeral)
then have ‹⇂angle_c q p r⇃ = pi / 3 ∨ ⇂angle_c q p r⇃ = - pi / 3›
by (smt (verit) ‹angle_c p q r = angle_c q p r ∨ angle_c p q r = - angle_c q p r›
add_divide_distrib ang_pos_pos ang_vec_bounded ang_vec_sym angle_c_def arccos_minus_one_half
arccos_one_half arcsin_minus_one_half arcsin_one_half arcsin_plus_arccos canon_ang_id
canon_ang_minus_3pi_minus_pi canon_ang_pi_3pi field_sum_of_halves fpi)
show ‹cdist q r = cdist p r ∧ cdist p r = cdist p q›
apply(rule conjI)
using ff apply(auto simp: norm_minus_commute)[1]
apply(rule pi3_isoscele_imp_equilateral')
using h(1) apply auto[1]
apply (metis ‹angle_c q r p = pi / 3 ∨ angle_c q r p = - pi / 3›
angle_c_neq0 divide_eq_0_iff neg_equal_0_iff_equal pi_neq_zero zero_neq_numeral)
using ff apply presburger
using ‹⇂angle_c q p r⇃ = pi / 3 ∨ ⇂angle_c q p r⇃ = - pi / 3› by blast
qed
lemmas equilateral_imp_prcispi3 = equilateral_caracterization[THEN iffD1]
lemmas prcispi3_imp_equilateral = equilateral_caracterization[THEN iffD2]
lemma equilateral_caracterization_neg:
fixes p q r::complex
assumes h1:‹p≠r›
shows ‹(cdist p r = cdist p q ∧ cdist p q = cdist q r ∧ angle_c q r p = -pi/3)
⟷ p + root3 * q + root3 ^ 2 * r = 0›
proof(rule iffI)
assume h:‹cdist p r = cdist p q ∧ cdist p q = cdist q r ∧ angle_c q r p = -pi/3›
then have ‹p-r = cis(-pi/3)*(q-r)›
using h1 isoscele_iff_pr_cis_qr[of q r p]
by force
with h have ‹p-r+cis(2*pi/3)*(q-r) = 0›
apply(simp add:cis.code)
apply(subst sin_120)
apply(intro complex_eqI)
using cos_120 cos_60 sin_120 sin_60
by(auto simp add:field_simps)
then have ‹p + root3*q - (root3+1)*r = 0› by(auto simp:field_simps root3_def)
then show ‹p + root3 * q + root3^2 * r = 0›
by (metis (no_types, lifting) add.commute eq_iff_diff_eq_0 left_diff_distrib
ring_class.ring_distribs(2) root3_eq_0)
next
assume h:‹p + root3 * q + root3^2 * r = 0›
then have ‹p + root3*q - (root3+1)*r = 0›
by (metis add.commute add_diff_cancel_left diff_numeral_special(9) left_diff_distrib ring_class.ring_distribs(2)
root3_eq_0)
then have ‹p-r+root3*(q-r) = 0›
by(auto simp:field_simps)
have ‹-root3 = cis(-pi/3)›
using cos_120 cos_60 sin_120 sin_60
by (auto intro:complex_eqI simp: root3_def)
then have f1':‹p - r = cis(-pi/3)*(q-r)›
by (metis ‹p - r + root3 * (q - r) = 0› eq_neg_iff_add_eq_0 mult_minus_left)
then have f1:‹p - r = cis(pi/3)*(q-r) ∨ p - r = cis(-pi/3)*(q-r)›
by auto
then have f2:‹cmod (p-r) = cmod (q-r)›
by(auto simp:norm_mult)
then have f3:‹dist p r = dist q r›
by (simp add: dist_complex_def)
have ang_dem:‹angle_c q r p = -pi/3›
proof -
have *:‹q≠r›
using f2 h1 by auto
then have **:‹(p - r) / (q-r) = cis(-pi/3)›
using f1' by auto
have ***:‹ angle_c q r p = Arg ((p - r) /(q-r))›
by (metis ang_vec_def angle_c_def arg_div f1' h1 mult_zero_right right_minus_eq)
then have ‹Arg ((p - r) /(q-r)) = ⇂-pi/3⇃›
by (simp add:arg_cis **)
then show ?thesis using * ** ***
using canon_ang_id pi_ge_two by force
qed
have ‹cmod (q - p) = cmod (r - q)›
using f2
by (metis cdist_def dist_eq_0_iff equilateral_caracterization f1' f3)
then show ‹cdist p r = cdist p q ∧ cdist p q = cdist q r ∧ angle_c q r p = -pi/3›
using equilateral_caracterization[THEN iffD2, of q r p, OF _ f1]
using f2 ang_dem by(auto simp: f2 field_simps intro!:)
qed
end