Theory Morley
theory Morley
imports Complex_Axial_Symmetry
begin
section ‹Rotations›
locale complex_rotation =
fixes A::complex and θ::real
begin
definition ‹r z = A + (z-A)*cis(θ)›
lemma cmod_inv_rotation:‹cmod (z-A) = cmod (r z - A)›
unfolding r_def
by (simp add: norm_mult)
lemma inner_ang:‹cos (∠ z1 z2)*(cmod z1 *cmod z2) = Re (innerprod z1 z2)›
proof -
have ‹Re (innerprod z1 z2) = Re (scalprod z1 z2)›
unfolding innerprod_def by(auto)
then show ?thesis
by (metis cos_cmod_scalprod mult.commute)
qed
lemma ang_eq_cos_theta:‹z≠A ⟹ cos (angle_c z A (r z)) = cos (θ)›
proof -
assume ‹z≠A›
then have ‹innerprod (z-A) ((r z - A)) = (z-A)*cis(θ)*cnj(z - A)›
unfolding innerprod_def r_def by auto
then have f0:‹innerprod (z-A) ((r z - A)) = cmod (z-A)^2*cis(θ)›
by (metis ab_semigroup_mult_class.mult_ac(1) complex_mult_cnj_cmod mult.commute)
then have ‹cos (angle_c z A (r z))*cmod (z-A)*cmod(z - A) = Re (innerprod (z-A) ((r z - A)))›
unfolding angle_c_def
by (metis inner_ang mult.assoc cmod_inv_rotation)
then have ‹cos (angle_c z A (r z)) = Re (cis θ)›
by (simp add: ‹z ≠ A› f0 power2_eq_square)
then show ?thesis
by(auto simp:cis.code)
qed
lemma cdist_dist:‹cdist = dist›
using cdist_commute dist_complex_def by fastforce
lemma ang_eq_theta:assumes h:‹z≠A› shows ‹angle_c z A (r z) = ⇂θ⇃›
proof(cases ‹angle_c z A (r z) = ⇂- θ⇃›)
case True
then have ‹r z = A + (z-A)*cis(-θ)›
by (metis add_diff_cancel_left' arg_cis cdist_def cis_cmod cis_neq_zero cmod_inv_rotation
isoscele_iff_pr_cis_qr mult.left_commute mult.right_neutral mult_cancel_left norm_cis
norm_minus_commute of_real_1 r_def right_minus_eq)
then show ?thesis
by (smt (verit, del_insts) True add_diff_cancel_left' angle_c_neq0 arg_cis arg_mult_eq
canon_ang_cos canon_ang_sin cis.code cis_cnj diff_add_cancel divisors_zero r_def)
next
case False
have ‹cos (angle_c z A (r z)) = cos (θ)›
using ang_eq_cos_theta h by auto
then show ?thesis
by (smt (verit, ccfv_threshold) cmod_inv_rotation r_def add_diff_cancel_left' angle_c_neq0
angle_c_sum arg_cis canon_ang_sin cdist_def cis.code cis_neq_zero divisors_zero eq_iff_diff_eq_0 h
isoscele_iff_pr_cis_qr nonzero_mult_div_cancel_left nonzero_mult_div_cancel_right norm_minus_commute)
qed
lemma inj_r:‹inj r›
unfolding inj_on_def by(auto simp:r_def)
lemma img_eqI:‹cdist A z1 = cdist A z2 ∧ angle_c z1 A z2 = θ ⟹ z2 = r z1›
apply(cases ‹z1 = A ∨ z2 = A›)
using r_def add_minus_cancel isoscele_iff_pr_cis_qr apply force
unfolding r_def
by (metis add.commute cdist_commute diff_add_cancel isoscele_iff_pr_cis_qr mult.commute)
lemma r_id_iff:‹⇂θ⇃ = 0 ⟷ r = id›
proof -
obtain cc :: "(complex ⇒ complex) ⇒ complex"
and cca :: "(complex ⇒ complex) ⇒ complex" where
f1: "∀f. (id = f ∨ f (cc f) ≠ cc f) ∧ ((∀c. f c = c) ∨ id ≠ f)"
by (metis (no_types) eq_id_iff)
have f2: "∀c ca ra. ca + (c - ca) * Complex (cos ra) (sin ra) = complex_rotation.r ca ra c"
by (simp add: complex_rotation.r_def cis.code)
then have "∀c ca. complex_rotation.r c 0 ca = ca"
by (metis (no_types) add_diff_cancel_left' cos_zero diff_diff_eq2
lambda_one mult.commute one_complex.code sin_zero)
then show ?thesis
using f2 f1
by (metis (lifting, full_types) ang_eq_theta angle_c_neq0
canon_ang_cos canon_ang_sin complex_i_not_zero)
qed
end
lemma axial_symmetry_eq:‹axial_symmetry B C P = axial_symmetry C B P› if ‹C≠B› for C B P
unfolding axial_symmetry_def[OF that] axial_symmetry_def[OF that[symmetric]]
by (metis (no_types, lifting) complex_cnj_cancel_iff eq_iff_diff_eq_0
minus_diff_eq nonzero_minus_divide_divide times_divide_eq_right)
lemma img_r_sym:
assumes h:‹z1 ≠ z2› ‹z ∉ line z1 z2›
shows ‹axial_symmetry z1 z2 z = complex_rotation.r z1 (⇂2*angle_c z z1 z2⇃) z›
proof -
interpret complex_rotation z1 "⇂2*angle_c z z1 z2⇃" .
let ?z = ‹axial_symmetry z1 z2 z›
from h have ‹z1≠z› ‹z2 ≠ z›
unfolding line_def Elementary_Complex_Geometry.collinear_def by(auto)
then have ‹angle_c ?z z1 z2 = -angle_c z z1 z2›
using angle_symmetry_eq h(1) h(2) by force
then have ‹angle_c z z1 ?z = ⇂2*angle_c z z1 z2⇃›
by (metis ‹z1 ≠ z› add.inverse_inverse angle_c_commute angle_c_commute_pi
angle_sum_symmetry h(1) mult_2_right mult_commute_abs)
have ‹ cdist z1 z = cdist z1 (axial_symmetry z1 z2 z)›
using axial_symmetry_dist1 h(1) by blast
then show ?thesis
apply(intro img_eqI)
by (metis ‹angle_c z z1 (axial_symmetry z1 z2 z) = ⇂2 * angle_c z z1 z2⇃›)
qed
lemma img_r_sym':
assumes h:‹z1 ≠ z2› ‹z∉line z1 z2›
shows ‹axial_symmetry z1 z2 z = complex_rotation.r z1 (⇂-2*angle_c z2 z1 z⇃) z›
by (metis angle_c_commute angle_c_neq0 axial_symmetry_eq_line
cancel_comm_monoid_add_class.diff_cancel complex_rotation.img_eqI
complex_rotation.r_def h(1,2) img_r_sym mult_eq_0_iff mult_minus_left
mult_minus_right pi_neq_zero two_pi_canonical)
lemma equality_for_pqr:
assumes 1:‹(a2::complex)*a3≠1› and 2:‹⋀z. h z = a3*z + b3› and 3:‹⋀z. g z = a2*z + b2› and 4:‹g (h z) = z›
shows ‹z = (a2*b3 + b2)/(1-a2*a3)›
proof -
have f21:‹g (h z) = a2*a3*z + a2*b3 +b2›
using assms by(auto simp:2 3field_simps)
then have ‹ g (h z) = a2*a3*z + a2*b3 +b2 ⟷ z*(1-a2*a3) = a2*b3 + b2›
by(auto simp:field_simps 4)
then have ‹a2*a3 ≠1 ⟹ z = (a2*b3 + b2)/(1-a2*a3)›
using f21 by(auto simp:field_simps)
then show ?thesis using 1 by auto
qed
lemma equality_for_comp:
assumes 2:‹⋀z. h z = (a3::complex)*z + b3› and 3:‹⋀z. g z = a2*z + b2›
and 4:‹⋀z. f z = a1*z +b1›
shows ‹((f∘f∘f)∘(g∘g∘g)∘(h∘h∘h)) z = (a1*a2*a3)^3*z +(a1^2+a1+1)*b1 +a1^3*(a2^2+a2+1)*b2
+a1^3*a2^3*(a3^2+a3+1)*b3 ›
using assms unfolding comp_def by(auto simp:fun_eq_iff power2_eq_square power3_eq_cube field_simps)
lemma eq_translation_id:
assumes ‹h = complex_rotation.r A 0› ‹h B = B›
shows ‹h = id›
using assms(1) complex_rotation.r_id_iff by auto
lemma r_eqI:
assumes ‹A = B› ‹θ1 = θ2›
shows ‹r A θ1 = r B θ2›
using assms(1) assms(2) by force
lemma r_eqI':
assumes ‹A = B› ‹θ1 = θ2›
shows ‹r A θ1 z = r B θ2 z›
using assms(1) assms(2) by force
lemma composed_rotations_same_center:
shows ‹(complex_rotation.r A θ1 ∘ complex_rotation.r A θ2) = complex_rotation.r A (θ1 + θ2)›
unfolding complex_rotation.r_def by (auto simp: fun_eq_iff cis_mult add_ac)
lemma composed_rotations:
assumes h:‹⇂θ1 + θ2⇃ ≠ 0›
shows ‹(complex_rotation.r A θ1 ∘ complex_rotation.r B θ2) =
complex_rotation.r ((A*(1-cis θ1) + B*cis θ1*(1-cis θ2))/(1-cis (θ1+θ2))) (θ1 + θ2)›
proof -
have ‹cis (θ1 + θ2) ≠ 1›
by (metis arg_cis assms cis_zero zero_canonical)
with h have ‹(complex_rotation.r A θ1 ∘ complex_rotation.r B θ2)
((A*(1-cis θ1) + B*cis θ1*(1-cis θ2))/(1-cis (θ1+θ2)))
= (A*(1-cis θ1) + B*cis θ1*(1-cis θ2))/(1-cis (θ1+θ2)) ›
unfolding complex_rotation.r_def using assms
by(auto simp:cis_mult field_simps intro!:)
with h show ?thesis
apply(cases ‹θ1 = 0 ∨ θ2 = 0›)
unfolding complex_rotation.r_def using assms
by(auto simp:cis_mult field_simps fun_eq_iff diff_divide_distrib add_divide_distrib intro!:)
qed
lemma composed_rotation_is_trans:
assumes ‹⇂θ1 + θ2⇃ = 0›
shows ‹(complex_rotation.r A θ1 ∘ complex_rotation.r B θ2) z = z + (B - A)*(cis(θ1) - 1)›
using assms
by (auto simp:complex_rotation.r_def add_divide_distrib diff_divide_distrib field_simps)
(metis add.commute canon_ang_cos canon_ang_sin cis.code cis_mult cis_zero lambda_one mult.commute)
section ‹Morley's theorem›
text ‹We begin by proving the Morley's theorem in the case where angles are positives
then using the congruence between two triangles with the same angles only not of the same sign
we prove Morley's theorem when angles are negatives.
We then proceed to conclude because in a triangle either angles are all negatives or all the
angles are positives depending on orientation.›
theorem Morley_pos:
assumes‹¬collinear A B C›
‹angle_c A B R = angle_c A B C / 3› (is ‹?abr = ?abc›)
"angle_c B A R = angle_c B A C / 3" (is ‹?bar = ?α›)
"angle_c B C P = angle_c B C A / 3" (is ‹?bcp = ?bca›)
"angle_c C B P = angle_c C B A / 3" (is ‹?cbp = ?β›)
"angle_c C A Q = angle_c C A B / 3" (is ‹?caq = ?cab›)
"angle_c A C Q = angle_c A C B / 3" (is ‹?acq = ?γ›)
and hhh:‹⇂angle_c B A C / 3+angle_c C B A / 3+angle_c A C B / 3⇃ = pi/3›
shows ‹cdist R P = cdist P Q ∧ cdist Q R = cdist P Q›
proof -
have bundle_line:‹A∉ line B C› ‹B∉ line A C› ‹C ∉ line A B› ‹A≠B› ‹B≠C› ‹C≠A›
using assms(1) non_collinear_independant by (auto simp:collinear_sym1 collinear_sym2 line_def)
{fix A B C γ
assume ABC_nline:‹A ∉ line B C›
and eq_3c:‹angle_c A C B = 3*γ›
then have neq_PI:‹abs γ < pi/3›
proof -
have ‹angle_c A C B ≠ pi›
using ABC_nline(1) unfolding line_def
by (metis angle_c_commute_pi collinear_iff mem_Collect_eq non_collinear_independant)
then have ‹angle_c A C B ∈ {-pi<..<pi}›
using ang_c_in less_eq_real_def by auto
then show ‹abs γ < pi/3›
using eq_3c by force
qed}note ang_inf_pi3=this
have ‹⇂angle_c B A C + angle_c C B A + angle_c A C B⇃ = pi›
by (metis collinear_def add.commute
angle_sum_triangle_c assms(1) collinear_sym1 collinear_sym2')
have eq_pi:‹⇂3*?α + 3*?β + 3*?γ⇃ = pi›
using ‹⇂angle_c B A C + angle_c C B A + angle_c A C B⇃ = pi› by force
then have neq_pi:‹⇂?β⇃ ≠ pi ∧ ⇂?γ⇃ ≠ pi ∧ ⇂?α⇃ ≠ pi›
by (smt (verit) ang_neg_neg angle_c_commute angle_c_neq0 assms
canon_ang_sin collinear_angle collinear_sin_neq_0 divide_eq_0_iff divide_nonneg_pos
minus_divide_left pi_neq_zero sin_pi sin_pi_minus zero_canonical)
moreover have ‹3*?α ≠ 0∧3*?β ≠ 0∧3*?γ ≠ 0›
using bundle_line collinear_sin_neq_0 line_def angle_c_commute assms(1) bundle_line(4)
bundle_line(5) bundle_line(6) collinear_iff assms(1) collinear_sin_neq_0
by (metis collinear_sym2' divide_eq_eq_numeral1(1) mem_Collect_eq mult.commute zero_neq_numeral)
ultimately have neq_0:‹⇂?β⇃ ≠ 0 ∧ ⇂?γ⇃ ≠ 0 ∧ ⇂?α⇃ ≠ 0›
by (metis ang_vec_def angle_c_def arg_cis assms(3) assms(5) assms(7) canon_ang_arg mult_zero_right)
interpret rot1: complex_rotation A "2*?α" .
interpret rot2: complex_rotation B "2*?β" .
interpret rot3: complex_rotation C "2*?γ" .
let ?f=‹rot1.r›
have f0:‹rot1.r A = A›
unfolding rot1.r_def by auto
have f1:‹rot2.r B = B›
unfolding rot2.r_def by auto
have f2:‹rot3.r C = C›
unfolding rot3.r_def by auto
have ‹cmod (rot3.r z - C) = cmod (z-C)› for z
using rot3.cmod_inv_rotation by presburger
have f2:‹B≠C›
by (metis collinear_def assms(1) collinear_sym1 collinear_sym2)
have f5:‹angle_c C B P = ?β› ‹angle_c P B C = -?β›
by (auto simp add: assms(5) angle_c_commute)
(metis angle_c_commute angle_c_commute_pi assms(5) neq_pi pi_canonical)
then have f3:‹P ∉ line C B›
by (smt (verit, ccfv_SIG) neq_0 neq_pi angle_c_commute angle_c_neq0 assms(4)
collinear_angle divide_eq_0_iff line_def mem_Collect_eq pi_canonical zero_canonical)
then have f3':‹P ∉ line B C›
using collinear_sym2' line_def by blast
then have f4:‹P≠C ∧ P≠B›
by (metis collinear_def collinear_sym1 collinear_sym2 line_def mem_Collect_eq)
then have ‹angle_c P B C = - angle_c (axial_symmetry B C P) B C›
using angle_symmetry_eq[OF f2 _ _ f3'] by auto
then have ‹angle_c (axial_symmetry B C P) B C = ?β›
using f5(2) by fastforce
have f13:‹angle_c P C B = ?γ›
by (smt (verit, ccfv_threshold) angle_c_commute angle_c_commute_pi assms(1) assms(4) assms(7)
collinear_sin_neq_0 nonzero_minus_divide_divide nonzero_minus_divide_right sin_pi)
let ?P'= ‹(axial_symmetry B C P)›
have ‹angle_c (axial_symmetry B C P) B P = ⇂2*?β⇃›
by (metis ‹P ≠ C ∧ P ≠ B› ‹angle_c (axial_symmetry B C P) B C = angle_c C B A / 3›
angle_sum_symmetry f2 f5(1) involution_symmetry mult.commute mult_2_right z1_inv)
have ‹cdist B (P) = cdist B ?P'›
by(auto)(metis cmod_axial_inv f2 z1_inv)
then have ‹cdist B (rot2.r P) = cdist B ?P'›
unfolding cdist_def
using rot2.cmod_inv_rotation by presburger
have f16:‹rot2.r ?P' = P›
by (metis ‹angle_c (axial_symmetry B C P) B P = ⇂2 * (angle_c C B A / 3)⇃›
‹cdist B P = cdist B (axial_symmetry B C P)› canon_ang_cos
canon_ang_sin cis.code complex_rotation.img_eqI complex_rotation.r_def)
have f10:‹angle_c P C B = ⇂?γ⇃›
by (metis ‹angle_c P C B = angle_c A C B / 3› ang_vec_def angle_c_def arg_cis canon_ang_arg)
from f10 have f11:‹angle_c B C ?P' = ⇂?γ⇃›
by (metis axial_symmetry_eq ‹P ≠ C ∧ P ≠ B› ‹angle_c P C B = angle_c A C B / 3› angle_c_commute
angle_symmetry angle_symmetry_eq_imp axial_symmetry_eq_line canon_ang_uminus_pi f2 f3 pi_canonical)
then have f12:‹angle_c P C ?P' = ⇂2*?γ⇃›
by (metis axial_symmetry_eq f13 angle_sum_symmetry f10 f2 f4 mult.commute mult_2_right)
then have f15:‹rot3.r P = ?P'›
by (metis axial_symmetry_eq canon_ang_cos canon_ang_sin cis.code f13 f2 f3 img_r_sym complex_rotation.r_def)
have P_inv:‹rot2.r (rot3.r P) = P›
using f16 f15 by presburger
let ?Q'=‹axial_symmetry A C Q›
have ‹angle_c C A Q = -?α›
by (metis angle_c_commute assms(1) assms(6) collinear_sin_neq_0
collinear_sym1 collinear_sym2' minus_divide_left sin_pi)
then have ‹angle_c Q A C = ?α›
by (metis add.inverse_inverse angle_c_commute canon_ang_uminus_pi neq_pi pi_canonical)
have ‹A≠C ∧ Q∉line A C›
by (metis ‹angle_c Q A C = angle_c B A C / 3› angle_c_neq0 assms(7) collinear_angle div_0
f10 f13 line_def mem_Collect_eq neq_0 neq_pi zero_canonical)
then have f17:‹rot1.r Q = ?Q'›
using img_r_sym[of A C Q]
using ‹angle_c Q A C = angle_c B A C / 3› canon_ang_cos canon_ang_sin cis.code complex_rotation.r_def
by presburger
then have ‹angle_c ?Q' C A = ?γ›
by (smt (verit, ccfv_SIG) ‹A ≠ C ∧ Q ∉ line A C› ‹angle_c Q A C = angle_c B A C / 3›
complex_rotation.ang_eq_theta angle_c_commute angle_symmetry angle_symmetry_eq_imp assms(7)
axial_symmetry_eq axial_symmetry_eq_line f10 f13 complex_rotation.img_eqI neq_0 neq_pi)
then have ‹angle_c A C Q = ?γ›
using assms(7) by blast
then have ‹angle_c ?Q' C Q =⇂2*?γ⇃›
by (metis ‹A ≠ C ∧ Q ∉ line A C› ‹angle_c (axial_symmetry A C Q) C A = angle_c A C B / 3›
‹angle_c Q A C = angle_c B A C / 3› angle_c_neq0 angle_sum_symmetry angle_symmetry_eq
axial_symmetry_eq involution_symmetry mult_2_right mult_commute_abs neg_equal_0_iff_equal
neq_0 zero_canonical)
then have f18:‹rot3.r ?Q' = Q›
using img_r_sym[of C A ?Q']
by (metis ‹A ≠ C ∧ Q ∉ line A C› axial_symmetry_dist1
axial_symmetry_eq canon_ang_cos canon_ang_sin cis.code
complex_rotation.img_eqI complex_rotation.r_def)
have Q_inv:‹rot3.r (rot1.r Q) = Q›
using f17 f18 by presburger
let ?R'=‹axial_symmetry A B R›
have ‹angle_c B A R = ?α›
by (simp add: assms(3))
then have ‹angle_c R A B = -?α›
by (metis angle_c_commute canon_ang_uminus_pi neq_pi pi_canonical)
have ‹angle_c R B A = ?β›
by (metis ‹angle_c (axial_symmetry B C P) B C = angle_c C B A / 3› angle_c_commute
angle_c_commute_pi assms(1) assms(2) collinear_sin_neq_0 collinear_sym1 minus_divide_left sin_pi)
have ‹A≠B ∧ R∉line A B›
by (metis (no_types, opaque_lifting) ‹angle_c Q A C = angle_c B A C / 3› ‹angle_c R A B = -
(angle_c B A C / 3)› angle_c_commute angle_c_commute_pi angle_c_neq0 assms(2) collinear_angle
collinear_sym2' diff_zero divide_eq_0_iff line_def mem_Collect_eq minus_diff_eq neg_equal_zero
neq_0 zero_canonical)
then have f17:‹rot2.r R = ?R'›
using img_r_sym[of B A R]
using ‹angle_c R B A = angle_c C B A / 3› axial_symmetry_eq
cis.code collinear_sym2 line_def complex_rotation.r_def by auto
then have ‹angle_c ?R' A B = ?α›
by (metis ‹A ≠ B ∧ R ∉ line A B› ‹angle_c R A B = - (angle_c B A C / 3)›
‹angle_c R B A = angle_c C B A / 3› add.inverse_inverse add.inverse_neutral angle_c_neq0
angle_symmetry_eq neq_0 zero_canonical)
then have f18:‹rot1.r ?R' = R›
using img_r_sym[of A B ?R']
by (metis ‹A ≠ B ∧ R ∉ line A B› axial_symmetry_eq canon_ang_cos canon_ang_sin cis.code
involution_symmetry line_is_inv complex_rotation.r_def z2_inv)
have R_inv:‹rot1.r (rot2.r R) = R›
using f17 f18 by presburger
let ?a1 = ‹cis(2*?α)› let ?b1=‹A*(1-?a1)› let ?a2=‹cis(2*?β)› let ?b2=‹B*(1-?a2)›
let ?a3=‹cis(2*?γ)› let ?b3=‹C*(1-?a3)›
have possi_abc:‹⇂?α+?β+?γ⇃ =pi/3 ∨ ⇂?α+?β+?γ⇃ = -pi/3 ∨ ⇂?α+?β+?γ⇃ = pi›
proof -
have ‹⇂?α+?β+?γ⇃∈{-pi<..pi}›
by (simp add: canon_ang(1) canon_ang(2))
then have ‹3*⇂?α+?β+?γ⇃ ∈ {-3*pi<..3*pi}›
by(auto)
then have ‹⇂⇂?α+?β+?γ⇃+⇂?α+?β+?γ⇃+⇂?α+?β+?γ⇃⇃ = ⇂?α+?β+?γ+?α+?β+?γ+?α+?β+?γ⇃›
by (smt (verit, ccfv_SIG) add.commute arg_cis canon_ang_arg
canon_ang_sum distrib_left is_num_normalize(1) mult_2)
then have ‹⇂3*⇂?α+?β+?γ⇃⇃=pi›
using eq_pi by argo
then have ‹3*⇂?α+?β+?γ⇃ = 3*pi ∨ 3*⇂?α+?β+?γ⇃ = -pi ∨ 3*⇂?α+?β+?γ⇃=pi›
by (smt (verit, del_insts) canon_ang(1) canon_ang(2) canon_ang_id
canon_ang_minus_3pi_minus_pi canon_ang_pi_3pi)
then show ?thesis
by force
qed
have jj:‹B ∉ line C A› ‹Q ∉ line A C› ‹R ∉ line A B›
using assms f3' ‹A ≠ C ∧ Q ∉ line A C› ‹A ≠ B ∧ R ∉ line A B›
by (simp_all add: collinear_sym1 collinear_sym2 line_def)
then have inf_pi3:‹abs ?α < pi/3› ‹abs ?β < pi/3› ‹abs ?γ < pi/3›
using ang_inf_pi3[of B C A ?α] ang_inf_pi3[of C A B ?β] ang_inf_pi3[of A B C ?γ]
by (auto simp add:collinear_sym2 collinear_sym1 assms line_def)
then have ‹abs (?α+?β+?γ) < pi›
by argo
have j1:‹⇂?α+?β+?γ⇃ = pi/3 ⟹ ?a1*?a2*?a3 = root3›
proof -
assume hh:‹⇂?α+?β+?γ⇃ = pi/3›
have f20:‹cis (2 * (angle_c B A C / 3)) * cis (2 * (angle_c C B A / 3)) * cis (2 * (angle_c A C B / 3))
= cis (2*(?α+?β+?γ))›
by (simp add: cis_mult)
then have f21:‹cis (2*(⇂?α+?β+?γ⇃)) = cis (2*(?α+?β+?γ))›
by (smt (verit, ccfv_threshold) canon_ang_cos canon_ang_sin canon_ang_sum cis.code)
with hh show ?thesis
by (metis (no_types, opaque_lifting) f21 f20 times_divide_eq_right root3_def)
qed
have ‹rot1.r∘rot1.r = complex_rotation.r A (4*?α)›
using composed_rotations_same_center by auto
have g10:‹((rot1.r∘rot1.r∘rot1.r)∘(rot2.r∘rot2.r∘rot2.r)∘(rot3.r ∘rot3.r∘rot3.r)) =
complex_rotation.r A (6*?α) ∘ complex_rotation.r B (6*?β) ∘ complex_rotation.r C (6*?γ)›
using composed_rotations_same_center by auto
have f26:‹⇂6*?α + 6*?β + 6*?γ⇃ = 0›
by (smt (verit, ccfv_SIG) canon_ang_sum eq_pi two_pi_canonical)
also have ‹⇂6*?γ⇃ ≠ 0›
proof (rule ccontr)
assume ‹¬ ⇂6 * (angle_c A C B / 3)⇃ ≠ 0›
then obtain k::int where ‹6 * ⇂(angle_c A C B / 3)⇃ = 2*k*pi›
by (metis add.commute add.inverse_neutral add_0 canon_ang(3)
diff_conv_add_uminus f10 f13 of_int_mult of_int_numeral)
then have ‹3*⇂(angle_c A C B / 3)⇃ = k*pi›
by force
then show False
by (metis (no_types, opaque_lifting) assms(1) collinear_sin_neq_0 divide_eq_eq_numeral1(1)
f10 f13 mult_1 sin_kpi times_divide_eq_left zero_neq_numeral)
qed
then have f24:‹⇂6*?α + 6*?β⇃ ≠ 0›
by (metis add.commute add.right_neutral arg_cis calculation
canon_ang_cos canon_ang_sin canon_ang_sum cis.code)
let ?A1=‹(A*(1-cis (6*?α)) + B*cis (6*?α)*(1-cis (6*?β)))/(1-cis (6*?β+6*?α))›
have g11:‹complex_rotation.r A (6*?α) ∘ complex_rotation.r B (6*?β) ∘ complex_rotation.r C (6*?γ) =
complex_rotation.r ?A1 (6*?α + 6*?β)∘ complex_rotation.r C (6*?γ) ›
using composed_rotations[of ‹6*?α› ‹6*?β› A B, OF f24]
by argo
then have f27:‹complex_rotation.r ?A1 (6*?α + 6*?β)∘ complex_rotation.r C (6*?γ) = (λz. z + (C -
(A * (1 - cis (6 * (angle_c B A C / 3))) + B * cis (6 * (angle_c B A C / 3)) * (1 - cis (6 * (angle_c C B A / 3)))) /
(1 - cis (6 * (angle_c C B A / 3) + 6 * (angle_c B A C / 3)))) *
(cis (6 * (angle_c B A C / 3) + 6 * (angle_c C B A / 3)) - 1))› (is ‹?l = (λz. z + ?A2)›)
using composed_rotation_is_trans[of ‹6*?α + 6*?β› ‹6*?γ› ?A1 C, OF f26]
by auto
have f30:‹2*angle_c A C B = 6*?γ›
by auto
have ‹axial_symmetry C B A = complex_rotation.r C (⇂2*angle_c A C B⇃) A›
using img_r_sym collinear_sym1 f2 jj(1) line_def by auto
then have first:‹complex_rotation.r C (6*?γ) A = axial_symmetry C B A› (is ‹?rr = ?axA›)
using canon_ang_cos canon_ang_sin cis.code f30 complex_rotation.r_def by presburger
have f31:‹axial_symmetry B C ?axA = complex_rotation.r B (⇂2*angle_c ?axA B C⇃) ?axA›
by (metis ‹A ≠ C ∧ Q ∉ line A C› ‹⇂6 * (angle_c A C B / 3)⇃ ≠ 0›
‹complex_rotation.r C (6 * (angle_c A C B / 3)) A = axial_symmetry C B A›
complex_rotation.ang_eq_theta angle_c_neq0
axial_symmetry_eq f2 img_r_sym involution_symmetry line_is_inv z1_inv)
have f32:‹angle_c C B A = 3*?β›
by simp
then have f33:‹angle_c ?axA B C = 3*?β›
by (smt (verit) ‹A ≠ B ∧ R ∉ line A B› ‹A ≠ C ∧ Q ∉ line A C› ‹⇂6 * (angle_c A C B / 3)⇃ ≠ 0›
‹complex_rotation.r C (6 * (angle_c A C B / 3)) A = axial_symmetry C B A›
complex_rotation.ang_eq_theta angle_c_commute angle_c_neq0 angle_symmetry_eq assms(1)
axial_symmetry_eq collinear_sin_neq_0 collinear_sym1 f2 line_is_inv sin_pi)
then have snd:‹complex_rotation.r B (6*?β) ((axial_symmetry B C A)) = A›
by (smt (verit, ccfv_SIG) ‹A ≠ C ∧ Q ∉ line A C› ‹⇂6 * (angle_c A C B / 3)⇃ ≠ 0›
‹complex_rotation.r C (6 * (angle_c A C B / 3)) A = axial_symmetry C B A›
complex_rotation.ang_eq_theta angle_c_neq0 axial_symmetry_eq canon_ang_cos canon_ang_sin
cis.code f2 img_r_sym involution_symmetry line_is_inv complex_rotation.r_def z1_inv)
then have thrd:‹complex_rotation.r A (6*?α) A = A›
unfolding complex_rotation.r_def by auto
then have ‹(complex_rotation.r A (6*?α) ∘ complex_rotation.r B (6*?β) ∘ complex_rotation.r C (6*?γ)) A = A›
apply(simp)
by (smt (verit, best) axial_symmetry_eq f30 f32 first snd)
then have g21:‹((rot1.r∘rot1.r∘rot1.r)∘(rot2.r∘rot2.r∘rot2.r)∘(rot3.r ∘rot3.r∘rot3.r)) = (λz. z + ?A2)›
apply(subst g10) apply(subst g11) apply(subst f27) by(simp add:fun_eq_iff)
then have ‹?A2 = 0›
by (metis ‹(complex_rotation.r A (6 * (angle_c B A C / 3)) ∘
complex_rotation.r B (6 * (angle_c C B A / 3)) ∘
complex_rotation.r C (6 * (angle_c A C B / 3))) A = A›
add_diff_cancel_left' cancel_comm_monoid_add_class.diff_cancel g10)
then have g22:‹((rot1.r∘rot1.r∘rot1.r)∘(rot2.r∘rot2.r∘rot2.r)∘(rot3.r ∘rot3.r∘rot3.r)) = id›
using g21 by(auto simp:fun_eq_iff)
have g20:‹rot1.r z = ?a1*z +?b1› ‹rot2.r z =?a2*z + ?b2› ‹rot3.r z = ?a3 * z + ?b3› for z
by(auto simp:field_simps complex_rotation.r_def)
then have ‹((rot1.r∘rot1.r∘rot1.r)∘(rot2.r∘rot2.r∘rot2.r)∘(rot3.r ∘rot3.r∘rot3.r)) z = (cis (2 * (angle_c B A C / 3)) * cis (2 * (angle_c C B A / 3))
* cis (2 * (angle_c A C B / 3))) ^ 3 * z +
((cis (2 * (angle_c B A C / 3)))⇧2 + cis (2 * (angle_c B A C / 3)) + 1) * (A * (1 - cis (2 * (angle_c B A C / 3)))) +
cis (2 * (angle_c B A C / 3)) ^ 3 * ((cis (2 * (angle_c C B A / 3)))⇧2 + cis (2 * (angle_c C B A / 3)) + 1) *
(B * (1 - cis (2 * (angle_c C B A / 3)))) +
cis (2 * (angle_c B A C / 3)) ^ 3 * cis (2 * (angle_c C B A / 3)) ^ 3 *
((cis (2 * (angle_c A C B / 3)))⇧2 + cis (2 * (angle_c A C B / 3)) + 1) *
(C * (1 - cis (2 * (angle_c A C B / 3))))› (is ‹?l z = ?A3 z›) for z
using equality_for_comp[of rot3.r ?a3 ?b3 rot2.r ?a2 ?b2 rot1.r ?a1 ?b1, OF g20(3) g20(2) g20(1)]
by blast
then have ‹z = ?A3 z› for z
by (metis g22 id_apply)
then have very_imp:‹((cis (2 * (angle_c B A C / 3)))⇧2 + cis (2 * (angle_c B A C / 3)) + 1) * (A * (1 - cis (2 * (angle_c B A C / 3)))) +
cis (2 * (angle_c B A C / 3)) ^ 3 * ((cis (2 * (angle_c C B A / 3)))⇧2 + cis (2 * (angle_c C B A / 3)) + 1) *
(B * (1 - cis (2 * (angle_c C B A / 3)))) +
cis (2 * (angle_c B A C / 3)) ^ 3 * cis (2 * (angle_c C B A / 3)) ^ 3 *
((cis (2 * (angle_c A C B / 3)))⇧2 + cis (2 * (angle_c A C B / 3)) + 1) *
(C * (1 - cis (2 * (angle_c A C B / 3)))) = 0›
by (metis comm_monoid_add_class.add_0 mult_zero_class.mult_zero_right)
{assume hhh:‹⇂?α+?β+?γ⇃ = pi/3›
have j5:‹?a1*?a2 ≠1›
proof(rule ccontr)
assume ‹¬ cis (2 * (angle_c B A C / 3)) * cis (2 * (angle_c C B A / 3)) ≠ 1›
then have ‹?a1*?a2 = cis 0›
using cis_zero by presburger
then have ‹⇂2*(?α+?β)⇃ = 0›
by (metis arg_cis cis_mult distrib_left zero_canonical)
then have t:‹⇂?α+?β⇃ = pi ∨ ⇂?α+?β⇃ = 0›
by (smt (verit, del_insts) canon_ang(1) canon_ang_id canon_ang_sum canon_ang_uminus)
then have ‹⇂?α+?β⇃ = 0 ⟹ False›
by (metis add_0 assms(1) canon_ang_sum collinear_sin_neq_0
divide_cancel_right f10 f13 hhh sin_pi zero_neq_numeral)
then have ‹⇂1/3*(3*?α+3*?β)⇃=pi› using t by(auto simp:algebra_simps)
then have ‹⇂(pi-⇂3*?γ⇃)⇃ = ⇂(3*?α+3*?β)⇃›
by (smt (verit, ccfv_SIG) canon_ang_diff eq_pi)
then have ‹⇂(pi/3-⇂?γ⇃)⇃ = pi›
by (smt (verit, best) ‹⇂angle_c B A C / 3 + angle_c C B A / 3⇃ = 0 ⟹ False›
canon_ang_diff hhh t)
then have ‹⇂?γ⇃ ∈ {0<..<pi/3}›
by (smt (verit, ccfv_SIG) add_divide_distrib ang_vec_bounded 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_pi_3pi divide_cancel_right f13 field_sum_of_halves)
then show False
using ‹⇂pi / 3 - ⇂angle_c A C B / 3⇃⇃ = pi› add_divide_distrib canon_ang_id by auto
qed
have r_eq_all:‹rot1.r z = ?a1*z + ?b1› ‹rot2.r z = ?a2*z + ?b2› ‹rot3.r z = ?a3*z+?b3› for z
by(auto simp:field_simps complex_rotation.r_def cis.code)
have f21:‹rot2.r (rot3.r P) = ?a2*?a3*P + ?a2*?b3 +?b2›
apply(subst r_eq_all(2)) apply(subst r_eq_all(3)) by(auto simp:field_simps)
then have ‹ rot2.r (rot3.r P) = ?a2*?a3*P + ?a2*?b3 +?b2 ⟷ P*(1-?a2*?a3) = ?a2*?b3 + ?b2›
by (smt (verit) add.commute add_diff_cancel_left' add_diff_eq f15
f16 mult.commute mult.right_neutral right_diff_distrib')
then have j2:‹?a2*?a3 ≠1 ⟹ P = (?a2*?b3 + ?b2)/(1-?a2*?a3)›
using f21 by(auto simp:field_simps)
have j4:‹?a1*?a3 ≠ 1›
proof(rule ccontr)
assume ‹¬ cis (2 * (angle_c B A C / 3)) * cis (2 * (angle_c A C B / 3)) ≠ 1›
then have ‹?a1*?a3 = cis 0›
using cis_zero by presburger
then have ‹⇂2*(?α+?γ)⇃ = 0›
by (metis arg_cis cis_mult distrib_left zero_canonical)
then have t:‹⇂?α+?γ⇃ = pi ∨ ⇂?α+?γ⇃ = 0›
by (smt (verit, del_insts) canon_ang(1) canon_ang_id canon_ang_sum canon_ang_uminus)
then have k0:‹⇂?α+?γ⇃ = 0 ⟹ False›
by (smt (verit, ccfv_SIG) ‹A ≠ B ∧ R ∉ line A B› ‹A ≠ C ∧ Q ∉ line A C›
‹¦angle_c B A C / 3 + angle_c C B A / 3 + angle_c A C B / 3¦ < pi›
‹angle_c (axial_symmetry A B R) A B = angle_c B A C / 3› ‹angle_c R A B = - (angle_c B A C / 3)›
‹angle_c R B A = angle_c C B A / 3› ang_pos_pos assms(3) canon_ang_id f2 f30 f32 neq_0 z1_inv)
then have ‹⇂1/3*(3*?α+3*?γ)⇃=pi› using t by(auto simp:algebra_simps)
then have ‹⇂(pi-⇂3*?β⇃)⇃ = ⇂(3*?α+3*?γ)⇃›
by (smt (verit, ccfv_SIG) canon_ang_diff eq_pi)
then have ‹⇂(pi/3-⇂?β⇃)⇃ = pi›
by (smt (verit, best) k0
canon_ang_diff hhh t)
then have k1:‹⇂?β⇃ ∈ {0<..<pi/3}›
by (smt (verit, del_insts) arccos_one_half arcsin_one_half arcsin_plus_arccos
canon_ang_id divide_nonneg_pos field_sum_of_halves inf_pi3(2) pi_ge_zero)
then show False
using k1 add_divide_distrib canon_ang_id ‹⇂pi / 3 - ⇂angle_c C B A / 3⇃⇃ = pi› by auto
qed
have j3:‹?a2*?a3 ≠ 1›
proof(rule ccontr)
assume ‹¬ cis (2 * (angle_c C B A / 3)) * cis (2 * (angle_c A C B / 3)) ≠ 1›
then have ‹?a2*?a3 = cis 0›
using cis_zero by presburger
then have ‹⇂2*(?β+?γ)⇃ = 0›
by (metis arg_cis cis_mult distrib_left zero_canonical)
then have t:‹⇂?β+?γ⇃ = pi ∨ ⇂?β+?γ⇃ = 0›
by (smt (verit, del_insts) canon_ang(1) canon_ang_id canon_ang_sum canon_ang_uminus)
then have k0:‹⇂?β+?γ⇃ = 0 ⟹ False›
by (smt (verit, ccfv_SIG) ‹A ≠ B ∧ R ∉ line A B› ‹A ≠ C ∧ Q ∉ line A C›
‹¦angle_c B A C / 3 + angle_c C B A / 3 + angle_c A C B / 3¦ < pi›
‹angle_c (axial_symmetry A B R) A B = angle_c B A C / 3› ‹angle_c R A B = - (angle_c B A C / 3)›
‹angle_c R B A = angle_c C B A / 3› ang_pos_pos assms(3) canon_ang_id f2 f30 f32 neq_0 z1_inv)
then have ‹⇂1/3*(3*?β+3*?γ)⇃=pi› using t by(auto simp:algebra_simps)
then have ‹⇂(pi-⇂3*?α⇃)⇃ = ⇂(3*?β+3*?γ)⇃›
by (smt (verit, ccfv_SIG) canon_ang_diff eq_pi)
then have ‹⇂(pi/3-⇂?α⇃)⇃ = pi›
by (smt (verit, best) k0
canon_ang_diff hhh t)
then have k1:‹⇂?α⇃ ∈ {0<..<pi/3}›
by (smt (verit, del_insts) arccos_one_half arcsin_one_half arcsin_plus_arccos
canon_ang_id divide_nonneg_pos field_sum_of_halves inf_pi3(1) pi_ge_zero)
then show False
using k1 add_divide_distrib canon_ang_id ‹⇂(pi/3-⇂?α⇃)⇃ = pi› by auto
qed
have f21':‹rot3.r (rot1.r Q) = ?a3*?a1*Q + ?a3*?b1 +?b3›
apply(subst r_eq_all(1)) apply(subst r_eq_all(3)) by(auto simp:field_simps)
have f21'':‹rot1.r (rot2.r R) = ?a1*?a2*R + ?a1*?b2 +?b1›
apply(subst r_eq_all(1)) apply(subst r_eq_all(2)) by(auto simp:field_simps)
have jjj:‹?a1 ≠ 0 ∧ ?a2 ≠ 0 ∧ ?a3 ≠ 0›
using cis_neq_zero by blast
then have eq_j:‹?a1*?a2*?a3 = root3›
using j1 hhh by blast
then have P_def:‹P = (?a2*?b3 + ?b2)/(1-?a2*?a3)›(is ‹_=?P›)
using j2 j3 by blast
have n1: ‹1-?a2*?a3 = (?a1 - root3)/?a1›
by (smt (verit, ccfv_threshold) cis_divide cis_times_cis_opposite cis_zero
diff_divide_distrib eq_j minus_real_def mult_1 times_divide_eq_left)
then have P_last:‹P = ?a1*(?a2*?b3 + ?b2)/(?a1-root3)›
using P_def jjj by (simp add: )
then have Q_def:‹Q = (?a3*?b1 + ?b3)/(1-?a3*?a1)› (is ‹_=?Q›)
using f21' j4 Q_inv by(auto simp:field_simps)
have n2: ‹1-?a3*?a1 = (?a2 - root3)/?a2›
by (smt (verit, ccfv_threshold) cis_divide cis_times_cis_opposite cis_zero
diff_divide_distrib eq_j minus_real_def mult_1 times_divide_eq_left)
then have Q_last:‹Q = ?a2*(?a3*?b1 + ?b3)/(?a2-root3)›
using Q_def jjj by simp
then have R_def:‹R = (?a1*?b2 + ?b1)/(1-?a1*?a2)› (is ‹_=?R›)
using f21'' j5 R_inv by(auto simp:field_simps)
have n3:‹1-?a1*?a2 = (?a3 - root3)/?a3›
by (smt (verit, ccfv_threshold) cis_divide cis_times_cis_opposite cis_zero
diff_divide_distrib eq_j minus_real_def mult_1 times_divide_eq_left)
then have R_last:‹R = ?a3*(?a1*?b2 + ?b1)/(?a3-root3)›
using R_def jjj by simp
have ‹?a1 - root3 ≠ 0 ∧ ?a2-root3≠0 ∧ ?a3-root3 ≠ 0›
using eq_j j3 j4 j5 by auto
have rule_s:‹c ≠ 0 ⟹ a/c + b/c = (a+b)/c› for a b c::real
by argo
define j' where
defs: ‹j'≡root3›
have simp_rules_for_eq:‹P = (?a2*?b3 + ?b2)/(1-?a2*?a3)› ‹R = (?a1*?b2 + ?b1)/(1-?a1*?a2)›
‹Q = (?a3*?b1 + ?b3)/(1-?a1*?a3)› ‹1-?a1*?a2 ≠ 0 ∧ 1-?a2*?a3≠0 ∧ 1-?a1*?a3 ≠ 0›
‹?a1*?a2*?a3 = j' ›
‹1 + j' +j'^2 = 0› ‹((1 - ?a1 * ?a3) * ((1 - ?a1 * ?a2) * (1 - ?a2 * ?a3)))≠0›
‹j'^3 = 1› ‹j'*j'*j' = 1› ‹?a1≠0› ‹?a2≠0› ‹?a3≠0›
‹(1-?a1*?a2)*?a3 = (?a3-j')› ‹(1-?a2*?a3)*?a1 = (?a1-j')› ‹(1-?a1*?a3)*?a2 = (?a2-j')›
using Q_def P_def R_def eq_j j3 jjj j4 j5 root3_eq_0 root_unity_3 n1 n2 n3
by(auto simp add:mult.commute power3_eq_cube defs root3_def)
have graal:‹(?a1^2+?a1+1)*?b1 + ?a1^3*(?a2^2+?a2+1)*?b2 +?a1^3*?a2^3*(?a3^2+?a3+1)*?b3 =
-j'*?a1^2*?a2*(?a1-j')*(?a2-j')*(?a3-j')*(?R +j'*?P +j'^2*?Q)›
using root_unity_carac[of ?a1 ?a2 ?a3 j' ?R ?b2 ?b1 ?P ?b3 ?Q]
using simp_rules_for_eq defs by(auto simp:)
then have ‹(?a1^2+?a1+1)*?b1 + ?a1^3*(?a2^2+?a2+1)*?b2 +?a1^3*?a2^3*(?a3^2+?a3+1)*?b3 = 0›
unfolding defs using very_imp by auto
then have ‹(?R +j'*?P +j'^2*?Q) = 0›
using graal simp_rules_for_eq(13) simp_rules_for_eq(14)
simp_rules_for_eq(15) simp_rules_for_eq(11) simp_rules_for_eq(12) simp_rules_for_eq(4) by force
then have impp:‹R +j'*P +j'^2*Q = 0›
using R_def P_def Q_def
by (metis simp_rules_for_eq(1) simp_rules_for_eq(2) )
have neq_all:‹A≠B ∧ B≠C ∧ C≠A›
using ‹A ≠ B ∧ R ∉ line A B› ‹A ≠ C ∧ Q ∉ line A C› f2 by argo
have ‹R ≠ Q›
proof (rule ccontr)
assume ‹¬ R ≠ Q›
then have q1:‹angle_c A B R = angle_c A B Q›
‹angle_c B A R = angle_c B A Q› ‹angle_c C A Q = angle_c C A R›
‹angle_c A C Q = angle_c A C R›
using assms by auto
then have ‹angle_c B A R = ?α› using assms by auto
then have ‹angle_c B A Q = ?α›
using q1 by auto
then have ‹angle_c A B Q = angle_c A B R + angle_c R B Q›
using ‹¬ R ≠ Q› angle_c_neq0 by auto
have ‹angle_c C A B = - 3*?α› using assms
using ‹angle_c C A Q = - (angle_c B A C / 3)› by argo
then have ‹angle_c (axial_symmetry B A R) A B = ?α›
by (metis ‹angle_c (axial_symmetry A B R) A B = angle_c B A C / 3› axial_symmetry_eq)
have ‹C - A ≠ 0 ∧ Q - A ≠ 0 ∧A - R ≠ 0 ∧ A - B ≠ 0›
using ‹A ≠ C ∧ Q ∉ line A C› ‹angle_c A B Q = angle_c A B R + angle_c R B Q›
‹angle_c R B A = angle_c C B A / 3› neq_0 q1(1) neq_all by fastforce
then have ‹angle_c C A B = angle_c C A Q + angle_c Q A R + angle_c R A B›
using angle_c_sum[of C A Q R] angle_c_sum[of C A R B]
by (smt (verit) ‹¬ R ≠ Q› ‹angle_c C A B = - 3 * (angle_c B A C / 3)›
‹angle_c C A Q = - (angle_c B A C / 3)› ‹angle_c R A B = - (angle_c B A C / 3)›
angle_c_neq0 canon_ang(1) canon_ang(2) canon_ang_id)
then show False
using ‹¬ R ≠ Q›
by (smt (verit, best) ‹angle_c C A B = - 3 * (angle_c B A C / 3)›
‹angle_c C A Q = - (angle_c B A C / 3)› ‹angle_c R A B = - (angle_c B A C / 3)›
angle_c_neq0 neq_0 zero_canonical)
qed
then have ‹cdist R P = cdist R Q ∧ cdist R Q = cdist Q P›
using equilateral_caracterization_neg[of R Q P] impp unfolding defs
by (metis cdist_commute)
then have ?thesis
using cdist_commute by auto
}note case_pi3=this
then show ?thesis using hhh by auto
qed
theorem Morley_neg:
assumes‹¬collinear A B C›
‹angle_c A B R = angle_c A B C / 3› (is ‹?abr = ?abc›)
"angle_c B A R = angle_c B A C / 3" (is ‹?bar = ?α›)
"angle_c B C P = angle_c B C A / 3" (is ‹?bcp = ?bca›)
"angle_c C B P = angle_c C B A / 3" (is ‹?cbp = ?β›)
"angle_c C A Q = angle_c C A B / 3" (is ‹?caq = ?cab›)
"angle_c A C Q = angle_c A C B / 3" (is ‹?acq = ?γ›)
and hhh:‹⇂angle_c B A C / 3+angle_c C B A / 3+angle_c A C B / 3⇃ = -pi/3›
shows ‹cdist R P = cdist P Q ∧ cdist Q R = cdist P Q›
proof -
have ‹⇂-angle_c B A C / 3+-angle_c C B A / 3+-angle_c A C B / 3⇃ = pi/3›
using hhh
by (metis (no_types, opaque_lifting) canon_ang(1) canon_ang_uminus less_eq_real_def
linorder_not_le minus_add_distrib minus_divide_left mult_le_0_iff
nonzero_mult_div_cancel_left not_numeral_le_zero pi_gt_zero times_divide_eq_right verit_minus_simplify(4) zero_canonical)
then show ?thesis using Morley_pos[of C B A P Q R]
by (smt (verit, best) Morley_pos angle_c_commute assms(1) assms(2) assms(3) assms(4) assms(5)
assms(6) assms(7) cdist_commute collinear_sin_neq_0 collinear_sym1 collinear_sym2 sin_pi)
qed
theorem Morley:
assumes‹¬collinear A B C›
‹angle_c A B R = angle_c A B C / 3› (is ‹?abr = ?abc›)
"angle_c B A R = angle_c B A C / 3" (is ‹?bar = ?α›)
"angle_c B C P = angle_c B C A / 3" (is ‹?bcp = ?bca›)
"angle_c C B P = angle_c C B A / 3" (is ‹?cbp = ?β›)
"angle_c C A Q = angle_c C A B / 3" (is ‹?caq = ?cab›)
"angle_c A C Q = angle_c A C B / 3" (is ‹?acq = ?γ›)
shows ‹cdist R P = cdist P Q ∧ cdist Q R = cdist P Q›
proof -
{fix A B C γ
assume ABC_nline:‹A ∉ line B C›
and eq_3c:‹angle_c A C B = 3*γ›
then have neq_PI:‹abs γ < pi/3›
proof -
have ‹angle_c A C B ≠ pi› using ABC_nline(1) unfolding line_def
by (metis angle_c_commute_pi collinear_iff mem_Collect_eq non_collinear_independant)
then have ‹angle_c A C B ∈ {-pi<..<pi}›
using ang_c_in less_eq_real_def by auto
then show ‹abs γ < pi/3›
using eq_3c by force
qed}note ang_inf_pi3=this
have ‹⇂angle_c B A C + angle_c C B A + angle_c A C B⇃ = pi›
by (metis Elementary_Complex_Geometry.collinear_def add.commute
angle_sum_triangle_c assms(1) collinear_sym1 collinear_sym2')
have eq_pi:‹⇂3*?α + 3*?β + 3*?γ⇃ = pi›
using ‹⇂angle_c B A C + angle_c C B A + angle_c A C B⇃ = pi› by force
have ‹A∉line B C ∧ B∉ line A C ∧ C ∉ line A B›
using assms(1) unfolding line_def using collinear_sym1 collinear_sym2' by(auto)
then have f2:‹abs ?α < pi/3 ∧ abs ?β < pi/3 ∧ abs ?γ < pi/3›
using ang_inf_pi3
by (smt (verit, ccfv_SIG) ang_vec_bounded angle_c_def assms(1) collinear_sin_neq_0
collinear_sym1 collinear_sym2 divide_less_cancel minus_divide_left sin_pi)
have possi_abc:‹⇂?α+?β+?γ⇃ =pi/3 ∨ ⇂?α+?β+?γ⇃ = -pi/3›
proof -
have ‹?α+?β+?γ ≤ pi›
using f2 by(auto simp:field_simps)
then have ‹⇂?α+?β+?γ⇃ = ?α+?β+?γ›
using canon_ang_id f2 by fastforce
then have ‹⇂3*⇂?α+?β+?γ⇃⇃ = pi›
using eq_pi by force
then show ?thesis
by (smt (verit) add_divide_distrib 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
eq_pi f2 field_sum_of_halves)
qed
then show ?thesis
using Morley_neg Morley_pos assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7)
by meson
qed
end