Section CC_ap_zero.
Lemma cc_ap_zero : forall P : C -> Prop,
(forall a b, a [#] 0 -> P (a[+I*]b)) -> (forall a b, b [#] 0 -> P (a[+I*]b)) -> forall c, c [#] 0 -> P c.
Lemma C_cc_ap_zero : forall P : C -> CProp,
(forall a b, a [#] 0 -> P (a[+I*]b)) -> (forall a b, b [#] 0 -> P (a[+I*]b)) -> forall c, c [#] 0 -> P c.
End CC_ap_zero.
Weird lemma.
Section Imag_to_Real.
Lemma imag_to_real : forall a b a' b', a'[+I*]b' [=] (a[+I*]b) [*]i -> a [#] 0 -> b' [#] 0.
End Imag_to_Real.
Section NRootI.
Definition sqrt_Half := sqrt ½ (less_leEq _ _ _ (pos_half IR)).
Definition sqrt_I := sqrt_Half[+I*]sqrt_Half.
Lemma sqrt_I_nexp : sqrt_I[^]2 [=] i.
Lemma nroot_I_nexp_aux : forall n, odd n -> {m : N | n * n = 4 * m + 1}.
Definition nroot_I (n : N) (n_ : odd n) : C := i[^]n.
Lemma nroot_I_nexp : forall n n_, nroot_I n n_[^]n [=] i.
Definition nroot_minus_I (n : N) (n_ : odd n) : C := [--] (nroot_I n n_).
Lemma nroot_minus_I_nexp : forall n n_, nroot_minus_I n n_[^]n [=] [--]i.
End NRootI.
We define the nth root of a complex number with a non zero imaginary part.
Let a,b : IR and b_ : (b [#] 0).
Define c2 := a^2+b^2, c := sqrt c2, a'2 := (c+a) ×½,
a' := sqrt a'2, b'2 := (c−a) ×½ and b' := sqrt b'2.
Variables a b : IR.
Hypothesis b_ : b [#] 0.
Lemma nrCC1_c2pos : 0 [<] c2.
Lemma nrCC1_a'2pos : 0 [<] a'2.
Lemma nrCC1_b'2pos : 0 [<] b'2.
Lemma nrCC1_a3 : a'[^]2[-]b'[^]2 [=] a.
Lemma nrCC1_a4 : (c[+]a) [*] (c[-]a) [=] b[^]2.
Lemma nrCC1_a5 : a'2[*]b'2 [=] (b[*]½) [^]2.
Lemma nrCC1_a6 : 0 [<] a'2[*]b'2.
Lemma nrCC1_a6' : 0 [<] (b[*]½) [^]2.
Lemma nrCC1_a7_upper : 0 [<] b -> a'[*]b' [=] b[*]½.
Lemma nrCC1_a7_lower : b [<] 0 -> a'[*][--]b' [=] b[*]½.
Lemma nrootCC_1_upper : 0 [<] b -> (a'[+I*]b') [^]2 [=] a[+I*]b.
Lemma nrootCC_1_lower : b [<] 0 -> (a'[+I*][--]b') [^]2 [=] a[+I*]b.
Lemma nrootCC_1_ap_real : {z : C | z[^]2 [=] a[+I*]b}.
End NRootCC_1_ap_real.
Hypothesis b_ : b [#] 0.
Lemma nrCC1_c2pos : 0 [<] c2.
Lemma nrCC1_a'2pos : 0 [<] a'2.
Lemma nrCC1_b'2pos : 0 [<] b'2.
Lemma nrCC1_a3 : a'[^]2[-]b'[^]2 [=] a.
Lemma nrCC1_a4 : (c[+]a) [*] (c[-]a) [=] b[^]2.
Lemma nrCC1_a5 : a'2[*]b'2 [=] (b[*]½) [^]2.
Lemma nrCC1_a6 : 0 [<] a'2[*]b'2.
Lemma nrCC1_a6' : 0 [<] (b[*]½) [^]2.
Lemma nrCC1_a7_upper : 0 [<] b -> a'[*]b' [=] b[*]½.
Lemma nrCC1_a7_lower : b [<] 0 -> a'[*][--]b' [=] b[*]½.
Lemma nrootCC_1_upper : 0 [<] b -> (a'[+I*]b') [^]2 [=] a[+I*]b.
Lemma nrootCC_1_lower : b [<] 0 -> (a'[+I*][--]b') [^]2 [=] a[+I*]b.
Lemma nrootCC_1_ap_real : {z : C | z[^]2 [=] a[+I*]b}.
End NRootCC_1_ap_real.
We now define the nth root of a complex number with a non zero real part.
Let a,b : IR and a_ : (a [#] 0) and define
c' := (a[+I*]b) [*][--]i := a'[+I*]b'.
Variables a b : IR.
Hypothesis a_ : a [#] 0.
Lemma nrootCC_1_ap_imag : {z : C | z[^]2 [=] a[+I*]b}.
End NRootCC_1_ap_imag.
Hypothesis a_ : a [#] 0.
Lemma nrootCC_1_ap_imag : {z : C | z[^]2 [=] a[+I*]b}.
End NRootCC_1_ap_imag.
We now define the roots of arbitrary non zero complex numbers.
Let n : N and c,z : C and c_:(c [#] 0).
Variable n : N.
Variables c z : C.
Hypothesis c_ : c [#] 0.
Lemma nrootCC_2' : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c ->
z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] 0 -> (z[^]n) [^]2 [=] c[^]2.
Lemma nrootCC_2 : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c ->
z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] 0 -> z[^]n [=] c or z[^]n [=] [--]c.
End NRootCC_2.
Section NRootCC_3.
Fixpoint Im_poly (p : cpoly C) : cpoly IR :=
match p with
| cpoly_zero => cpoly_zero IR
| cpoly_linear c p1 => cpoly_linear IR (ℑ c) (Im_poly p1)
end.
Lemma nrCC3_a1 : forall p r, (Im_poly p) ! r [=] ℑ p ! (cc_IR r).
Lemma nrCC3_a2 : forall p n, nth_coeff n (Im_poly p) [=] ℑ (nth_coeff n p).
Variables c z : C.
Hypothesis c_ : c [#] 0.
Lemma nrootCC_2' : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c ->
z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] 0 -> (z[^]n) [^]2 [=] c[^]2.
Lemma nrootCC_2 : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c ->
z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] 0 -> z[^]n [=] c or z[^]n [=] [--]c.
End NRootCC_2.
Section NRootCC_3.
Fixpoint Im_poly (p : cpoly C) : cpoly IR :=
match p with
| cpoly_zero => cpoly_zero IR
| cpoly_linear c p1 => cpoly_linear IR (ℑ c) (Im_poly p1)
end.
Lemma nrCC3_a1 : forall p r, (Im_poly p) ! r [=] ℑ p ! (cc_IR r).
Lemma nrCC3_a2 : forall p n, nth_coeff n (Im_poly p) [=] ℑ (nth_coeff n p).
Let a,b : IR, b_ : (b [#] 0) and n : N.
Variables a b : IR.
Hypothesis b_ : b [#] 0.
Variable n : N.
Definition nrCC3_poly'' := (_X_[+]_C_ i) [^]n.
Lemma nrCC3_a3 : forall r : IR, nrCC3_poly'' ! (cc_IR r) [=] (r[+I*]1) [^]n.
Lemma nrCC3_a4 : degree_le 1 (_X_[+]_C_ i).
Lemma nrCC3_a5 : degree_le n nrCC3_poly''.
Lemma nrCC3_a6 : nth_coeff n nrCC3_poly'' [=] 1.
Definition nrCC3_poly' := nrCC3_poly''[*]_C_ (a[+I*][--]b).
Lemma nrCC3_a7 : forall r : IR, nrCC3_poly' ! (cc_IR r) [=] (r[+I*]1) [^]n[*] (a[+I*][--]b).
Lemma nrCC3_a8 : degree_le n nrCC3_poly'.
Lemma nrCC3_a9 : nth_coeff n nrCC3_poly' [=] a[+I*][--]b.
Definition nrootCC_3_poly := Im_poly nrCC3_poly'.
Lemma nrootCC_3_ : forall r : IR, nrootCC_3_poly ! r [=] ℑ ((r[+I*]1) [^]n[*] (a[+I*][--]b)).
Lemma nrootCC_3 : forall r : IR,
cc_IR nrootCC_3_poly ! r[*] (2[*]i) [=] (r[+I*]1) [^]n[*] (a[+I*][--]b) [-] (r[+I*][--]1) [^]n[*] (a[+I*]b).
Lemma nrootCC_3_degree : degree n nrootCC_3_poly.
End NRootCC_3.
Section NRootCC_3'.
Let c:IR, n:nat and n_:(lt (0) n).
Variable c : IR.
Variable n : N.
Hypothesis n_ : 0 < n.
Definition nrootCC_3'_poly := _X_[^]n[-]_C_ c.
Lemma nrootCC_3' : forall x : IR, nrootCC_3'_poly ! x [=] x[^]n[-]c.
Lemma nrootCC_3'_degree : degree n nrootCC_3'_poly.
End NRootCC_3'.
Section NRootCC_4.
Section NRootCC_4_ap_real.
Let a,b : IR, b_ : (b [#] 0), n : N and
n_:(odd n); define c := a[+I*]b.
Variables a b : IR.
Hypothesis b_ : b [#] 0.
Variable n : N.
Hypothesis n_ : odd n.
Section NRootCC_4_solutions.
Lemma nrCC4_a1 : {r : IR | (r[+I*]1) [^]n[*]CC_conj c[-] (r[+I*][--]1) [^]n[*]c [=] 0}.
Let r2',c2 : IR and r2'_ : (r2' [#] 0).
Variables r2' c2 : IR.
Hypothesis r2'_ : r2' [#] 0.
Lemma nrCC4_a1' : {y2 : IR | (y2[*]r2') [^]n [=] c2}.
End NRootCC_4_solutions.
Section NRootCC_4_equations.
Let r,y2 : IR be such that
(r[+I*]1) ^n× (CC_conj c) − (r[+I*][--]1) ^n×c = 0
and (y2× (r^ (2) +1)) ^n = a^ (2) +b^ (2).
Variable r : IR.
Hypothesis r_property : (r[+I*]1) [^]n[*]CC_conj c[-] (r[+I*][--]1) [^]n[*]c [=] 0.
Variable y2 : IR.
Hypothesis y2_property : (y2[*] (r[^]2[+]1)) [^]n [=] a[^]2[+]b[^]2.
Lemma nrCC4_a2 : 0 [<] a[^]2[+]b[^]2.
Lemma nrCC4_a3 : 0 [<] r[^]2[+]1.
Lemma nrCC4_a4 : 0 [<] y2.
Definition nrCC4_y := sqrt y2 (less_leEq _ _ _ nrCC4_a4).
Let y := nrCC4_y.
Definition nrCC4_x := y[*]r.
Let x := nrCC4_x.
Lemma nrCC4_a5 : x [=] y[*]r.
Lemma nrCC4_a6 : (x[^]2[+]y[^]2) [^]n [=] a[^]2[+]b[^]2.
Definition nrCC4_z := x[+I*]y.
Let z := nrCC4_z.
Lemma nrCC4_a7 : z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] 0.
Lemma nrCC4_a8 : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c.
Lemma nrCC4_a9 : z[^]n [=] c or z[^]n [=] [--]c.
End NRootCC_4_equations.
Lemma nrCC4_a10 : forall c, {z : C | z[^]n [=] c or z[^]n [=] [--]c} -> {z : C | z[^]n [=] c}.
Lemma nrootCC_4_ap_real : {z : C | z[^]n [=] c}.
End NRootCC_4_ap_real.
Section NRootCC_4_ap_imag.
Hypothesis r_property : (r[+I*]1) [^]n[*]CC_conj c[-] (r[+I*][--]1) [^]n[*]c [=] 0.
Variable y2 : IR.
Hypothesis y2_property : (y2[*] (r[^]2[+]1)) [^]n [=] a[^]2[+]b[^]2.
Lemma nrCC4_a2 : 0 [<] a[^]2[+]b[^]2.
Lemma nrCC4_a3 : 0 [<] r[^]2[+]1.
Lemma nrCC4_a4 : 0 [<] y2.
Definition nrCC4_y := sqrt y2 (less_leEq _ _ _ nrCC4_a4).
Let y := nrCC4_y.
Definition nrCC4_x := y[*]r.
Let x := nrCC4_x.
Lemma nrCC4_a5 : x [=] y[*]r.
Lemma nrCC4_a6 : (x[^]2[+]y[^]2) [^]n [=] a[^]2[+]b[^]2.
Definition nrCC4_z := x[+I*]y.
Let z := nrCC4_z.
Lemma nrCC4_a7 : z[^]n[*]CC_conj c[-]CC_conj z[^]n[*]c [=] 0.
Lemma nrCC4_a8 : (z[*]CC_conj z) [^]n [=] c[*]CC_conj c.
Lemma nrCC4_a9 : z[^]n [=] c or z[^]n [=] [--]c.
End NRootCC_4_equations.
Lemma nrCC4_a10 : forall c, {z : C | z[^]n [=] c or z[^]n [=] [--]c} -> {z : C | z[^]n [=] c}.
Lemma nrootCC_4_ap_real : {z : C | z[^]n [=] c}.
End NRootCC_4_ap_real.
Section NRootCC_4_ap_imag.
Let a,b : IR and n : N with a [#] 0
and (odd n); define c' := (a[+I*]b) ×i := a'[+I*]b'.
Variables a b : IR.
Hypothesis a_ : a [#] 0.
Variable n : N.
Hypothesis n_ : odd n.
Lemma nrootCC_4_ap_real' : {z' : C | z'[^]n [=] a'[+I*]b'}.
Lemma nrootCC_4_ap_imag : {z : C | z[^]n [=] a[+I*]b}.
End NRootCC_4_ap_imag.
Lemma nrootCC_4 : forall c, c [#] 0 -> forall n, odd n -> {z : C | z[^]n [=] c}.
End NRootCC_4.
Hypothesis a_ : a [#] 0.
Variable n : N.
Hypothesis n_ : odd n.
Lemma nrootCC_4_ap_real' : {z' : C | z'[^]n [=] a'[+I*]b'}.
Lemma nrootCC_4_ap_imag : {z : C | z[^]n [=] a[+I*]b}.
End NRootCC_4_ap_imag.
Lemma nrootCC_4 : forall c, c [#] 0 -> forall n, odd n -> {z : C | z[^]n [=] c}.
End NRootCC_4.
Finally, the general definition of nth root.
Section NRootCC_5.
Lemma nrCC_5a2 : forall n : N, double n = 2 * n.
Lemma nrCC_5a3 : forall (n : N) (z : C), (z[^]2) [^]n [=] z[^]double n.
Let c : C with c [#] 0.
Variable c : C.
Hypothesis c_ : c [#] 0.
Lemma nrCC_5a4 : forall n, 0 < n -> {z : C | z[^]n [=] c} -> {z : C | z[^]double n [=] c}.
Lemma nrootCC_5 : forall n : N, 0 < n -> {z : C | z[^]n [=] c}.
End NRootCC_5.
Hypothesis c_ : c [#] 0.
Lemma nrCC_5a4 : forall n, 0 < n -> {z : C | z[^]n [=] c} -> {z : C | z[^]double n [=] c}.
Lemma nrootCC_5 : forall n : N, 0 < n -> {z : C | z[^]n [=] c}.
End NRootCC_5.
Final definition