proposition: Theorem Ferrari_formula: forall (a:C) (b:C) (c:C) (d:C), let s:=-a/4 in let p:= b+3*s*a+6*Cpow s 2 in let q:= c+2*b*s+3*a*Cpow s 2+4*Cpow s 3 in let r:= d+c*s+b*Cpow s 2+a*Cpow s 3+Cpow s 4 in let lambda:=Cardan_Tartaglia_formula (-p/2) (-r) (r*p/2-/8*Cpow q 2) 0 in let A:=Csqrt(2*lambda-p) in let cond:=(Ceq_dec (2*lambda) p) in let B:=if cond then (RtoC 0) else (-q/(2*A)) in let z1:=if cond then Csqrt (binom_solution p r 0) else binom_solution A (B+lambda) 0 in let z2:=if cond then -Csqrt (binom_solution p r 0) else binom_solution A (B+lambda) 1 in let z3:=if cond then Csqrt (binom_solution p r 1) else binom_solution (-A) (-B+lambda) 0 in let z4:=if cond then -Csqrt (binom_solution p r 1) else binom_solution (-A) (-B+lambda) 1 in let u1:=z1+s in let u2:=z2+s in let u3:=z3+s in let u4:=z4+s in forall u:C, (u-u1)*(u-u2)*(u-u3)*(u-u4)=Cpow u 4+a*Cpow u 3+b*Cpow u 2+c*u+d.
proof: Proof. assert(forall w x:C, (w+-x)=0 -> w=x) as cancelm. intros w x diff. rewrite<-(Cplus_0_l w). rewrite<-(Cplus_opp_r x). rewrite<-Cplus_assoc. rewrite (Cplus_comm _ w). rewrite diff. rewrite Cplus_0_r. reflexivity. intros. unfold u1,u2,u3,u4. pose (z:=u-s). assert(u=z+s) as Hszu. unfold z. field. rewrite Hszu. rewrite (shiftdeg4 s). fold p. fold q. fold r. assert(forall f g h:C, f+g-(h+g)=f-h) as mincancel. intros. field. repeat rewrite mincancel. unfold s. unfold Cdiv. rewrite (Cmult_comm _ (/4)). rewrite (Cmult_assoc 4). rewrite Cinv_r; [ | nneq0 ]. rewrite Cmult_1_l. rewrite Cplus_opp_r. rewrite Cmult_0_l. rewrite Cplus_0_r. pose proof (Cardan_Tartaglia (- p / 2) (- r) (r*p / 2 - / 8 * Cpow q 2) lambda) as Hlambda. fold lambda in Hlambda. unfold Cminus in Hlambda at 1. rewrite Cplus_opp_r in Hlambda. repeat rewrite Cmult_0_l in Hlambda. destruct cond as [cond|cond]. assert(forall f g:C,(f-g)*(f--g)=f*f-g*g) as diffsqr. intros. field. unfold z1,z2. rewrite diffsqr. rewrite<-Cmult_assoc. unfold z3,z4. rewrite diffsqr. repeat rewrite Csqrt_Cpow2. rewrite <-Binom_solution_proof. rewrite<-cond in Hlambda. assert(/8*Cpow q 2=0) as aux. rewrite<-Copp_0. rewrite Hlambda. unfold Cpow,Cdiv,Cminus. field; split; nneq0. unfold Cpow in aux. rewrite Cmult_1_r in aux. assert(q=0) as q0. destruct (Ceq_dec q 0) as [Hq | Hq]. assumption. exfalso. apply (Cmult_neq_0 (/8) (q*q)). nneq0. apply (Cmult_neq_0 q q); assumption. assumption. rewrite q0. unfold Cpow. field. assert(A<>0) as Aneq0. intro Aeq0. assert(A*A=0) as A2eq0. rewrite Aeq0. apply Cmult_0_r. unfold A in A2eq0. rewrite Csqrt_Cpow2 in A2eq0. apply cond. apply cancelm. apply A2eq0. unfold z1. unfold z2. rewrite<-Binom_solution_proof. rewrite<-Cmult_assoc. unfold z3. unfold z4. rewrite<-Binom_solution_proof. transitivity (Cpow z 4+(-(A*A)+2*lambda)*Cpow z 2 +(-((A*B)*2))*z+(lambda*lambda+-(B*B))). unfold Cpow. rewrite Cval2. field. replace (A*B) with (-q/2). replace (B*B) with (q*q/((A*A)*4)). unfold A. rewrite Csqrt_Cpow2. f_equal. f_equal. f_equal. field. field; nneq0. apply cancelm. rewrite<-(Cmult_0_r (/(lambda-p/2))). rewrite Hlambda. rewrite Cval8. rewrite Cval4. rewrite Cval2. unfold Cpow. field. try (split; [ nneq0 | ]; split; [ nneq0 | ]; split; [ | nneq0 ]). apply Cminus_eq_contra. intro hypabs. apply cond. rewrite<-hypabs. destruct lambda. unfold Cmult,RtoC,fst,snd. f_equal; field; nneq0. unfold B. unfold Cdiv. rewrite Cval2. rewrite Cval4. field; try (split; [ | split; nneq0 ]). assumption. unfold B,Cdiv. field; try (split; [ | nneq0 ]). assumption. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra