proposition: Theorem Cardan_Tartaglia : forall a1 a2 a3 :C, let u1:=(Cardan_Tartaglia_formula a1 a2 a3 0) in let u2:=(Cardan_Tartaglia_formula a1 a2 a3 1) in let u3:=(Cardan_Tartaglia_formula a1 a2 a3 2) in forall u:C, (u-u1)*(u-u2)*(u-u3)=Cpow u 3+a1*Cpow u 2+a2*u+a3.
proof: Proof. intros. pose (-a1/3) as s. pose (a2+2*s*a1+3*Cpow s 2) as p. pose (a3+a2*s+a1*Cpow s 2+Cpow s 3) as q. pose ((Cpow (q/2) 2)+(Cpow (p/3) 3)) as Delta. pose (if(Ceq_dec p 0) then (RtoC 0) else (cubicroot (-(q/2)+Csqrt Delta)))%C as alpha. pose (if(Ceq_dec p 0) then -cubicroot q else -(p/3)/alpha) as beta. pose (alpha+beta) as z1. pose (alpha*CJ+beta*Cpow CJ 2) as z2. pose (alpha*Cpow CJ 2+beta*CJ) as z3. assert(u1=s+z1 /\ u2=s+z2 /\ u3=s+z3) as uv. unfold u1,z1,u2,z2,u3,z3,Cardan_Tartaglia_formula. fold s p q Delta alpha beta. unfold Nat.add,Cpow. repeat rewrite Cmult_1_r. pose proof CJ3 as CJ3b. rewrite<-Cmult_assoc in CJ3b. rewrite CJ3b. rewrite Cmult_1_r. repeat split;reflexivity. destruct uv as [uv1 uv2]. destruct uv2 as [uv2 uv3]. rewrite uv1. rewrite uv2. rewrite uv3. assert(RtoC 1<>RtoC 0) as neq0_1 by nneq0. assert(RtoC 2<>RtoC 0) as neq0_2 by nneq0. assert(RtoC 3<>RtoC 0) as neq0_3 by nneq0. assert(forall z0:C, z0<>0 -> /z0 <> 0) as invnot0. intros z0 z0neq0. pose proof (Cinv_r z0 z0neq0) as prodz0. intro z0eq0. rewrite z0eq0 in prodz0. rewrite Cmult_0_r in prodz0. apply neq0_1. rewrite prodz0. reflexivity. assert(forall f g h:C, f+g-(g+h)=f-h) as mincancel. intros. field. intros. pose (z:=u-s). assert(u=z+s) as Hszu. unfold z. field. rewrite Hszu. rewrite (shiftdeg3 s). fold p. fold q. unfold s at 7. rewrite (Cmult_comm 3). unfold Cdiv. rewrite<-(Cmult_assoc _ _ 3). rewrite (Cinv_l _ neq0_3). Csimpl. repeat rewrite mincancel. rewrite factorisationdeg3. destruct (Ceq_dec p 0) as [peq0|pneq0]. unfold Cpow in z2,z3. unfold z1,z2,z3,alpha. Csimpl. f_equal. f_equal. rewrite CJ2. field. f_equal. rewrite peq0. developall. rewrite CJ3. rewrite CJ2. field. developall. rewrite CJ3. rewrite<-(cubicroot3 q). unfold beta. unfold Cpow. field. assert((Cpow alpha 3)<>0) as alpha3neq0. unfold alpha. rewrite cubicroot3. apply( (f_notequal _ _ (fun z => (q/2)+z) )). rewrite Cplus_assoc. Csimpl. apply( (f_notequal _ _ (fun z => Cpow z 2) )). unfold Cpow at 1. rewrite Cmult_1_r. rewrite Csqrt_Cpow2. unfold Delta. rewrite Cplus_comm. apply( (f_notequal _ _ (fun z => (z+-Cpow (q/2) 2)) )). rewrite<-Cplus_assoc. Csimpl. unfold Cpow. repeat apply Cmult_neq_0; try apply invnot0; try assumption. assert (alpha<>0) as alphaneq0. apply( (f_notequal _ _ (fun z => Cpow z 3))). unfold Cpow at 2. repeat rewrite Cmult_0_l. assumption. f_equal. f_equal. f_equal. replace (z1+z2+z3) with (RtoC 0). Csimpl. reflexivity. unfold z1,z2,z3. unfold Cpow. developall. rewrite CJ2. field. f_equal. unfold z1,z2,z3. unfold Cpow. developall. rewrite CJ3. repeat rewrite Cmult_1_l. rewrite CJ2. unfold Cminus. developall. transitivity(-(3*alpha*beta)). rewrite Cval3. field. unfold beta. field; try (split; [ nneq0 | ]). assumption. unfold z1,z2,z3. developall. rewrite CJ3. rewrite CJ2. developall. transitivity(-(Cpow alpha 3+Cpow beta 3)). unfold Cpow. field. transitivity(--q). f_equal. rewrite<-Cmult_1_r at 1. rewrite<-Cmult_1_r. rewrite<-(Cinv_r (Cpow alpha 3)). repeat rewrite Cmult_assoc. f_equal. rewrite Cmult_plus_distr_r. rewrite<-(comCpow _ beta alpha). unfold beta. unfold Cdiv. rewrite<-Cmult_assoc. rewrite Cinv_l. fold (Cdiv p 3). unfold alpha. rewrite cubicroot3. developall. rewrite Csqrt_Cpow2. generalize (Csqrt Delta). intro. unfold Delta,Cpow. rewrite Cval2. field; split; nneq0. assumption. assumption. field. Qed.
imports: Reals Coq.Reals.Rtrigo_def Coquelicot.Coquelicot Coquelicot.ElemFct Lra