1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: NRootCC.v,v 1.9 2004/04/23 10:00:55 lcf Exp $ *)
21 (*#* printing sqrt_Half %\ensuremath{\sqrt{\frac12}}% *)
23 (*#* printing sqrt_I %\ensuremath{\sqrt{\imath}}% *)
25 (*#* printing nroot_I %\ensuremath{\sqrt[n]{\imath}}% *)
27 (*#* printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)
29 include "complex/CComplex.ma".
31 (*#* * Roots of Complex Numbers
33 Properties of non-zero complex numbers
40 inline procedural "cic:/CoRN/complex/NRootCC/cc_ap_zero.con" as lemma.
42 inline procedural "cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con" as lemma.
54 inline procedural "cic:/CoRN/complex/NRootCC/imag_to_real.con" as lemma.
60 (*#* ** Roots of the imaginary unit *)
66 inline procedural "cic:/CoRN/complex/NRootCC/sqrt_Half.con" as definition.
68 inline procedural "cic:/CoRN/complex/NRootCC/sqrt_I.con" as definition.
70 inline procedural "cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con" as lemma.
72 inline procedural "cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con" as lemma.
74 inline procedural "cic:/CoRN/complex/NRootCC/nroot_I.con" as definition.
76 inline procedural "cic:/CoRN/complex/NRootCC/nroot_I_nexp.con" as lemma.
79 Hint Resolve nroot_I_nexp: algebra.
82 inline procedural "cic:/CoRN/complex/NRootCC/nroot_minus_I.con" as definition.
84 inline procedural "cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con" as lemma.
90 (*#* ** Roots of complex numbers *)
96 (*#* We define the nth root of a complex number with a non zero imaginary part.
100 Section NRootCC_1_ap_real
104 %\begin{convention}% Let [a,b : IR] and [b_ : (b [#] Zero)].
105 Define [c2 := a[^]2[+]b[^]2], [c := sqrt c2], [a'2 := (c[+]a) [*]Half],
106 [a' := sqrt a'2], [b'2 := (c[-]a) [*]Half] and [b' := sqrt b'2].
110 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a.var".
112 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b.var".
114 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b_.var".
118 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c2.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
122 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con" as lemma.
126 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
128 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'2.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
132 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con" as lemma.
136 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
138 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'2.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
142 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con" as lemma.
146 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'.con" "NRootCC_1__NRootCC_1_ap_real__" as definition.
150 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a3.con" as lemma.
152 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a4.con" as lemma.
155 Hint Resolve nrCC1_a4: algebra.
158 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a5.con" as lemma.
160 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a6.con" as lemma.
162 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a6'.con" as lemma.
165 Hint Resolve nrCC1_a5: algebra.
168 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con" as lemma.
170 inline procedural "cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con" as lemma.
173 Hint Resolve nrCC1_a3 nrCC1_a7_upper nrCC1_a7_lower: algebra.
176 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con" as lemma.
178 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con" as lemma.
180 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con" as lemma.
183 End NRootCC_1_ap_real
186 (*#* We now define the nth root of a complex number with a non zero real part.
190 Section NRootCC_1_ap_imag
194 %\begin{convention}% Let [a,b : IR] and [a_ : (a [#] Zero)] and define
195 [c' := (a[+I*]b) [*][--]II := a'[+I*]b'].
199 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a.var".
201 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b.var".
203 alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a_.var".
207 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/c'.con" "NRootCC_1__NRootCC_1_ap_imag__" as definition.
209 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a'.con" "NRootCC_1__NRootCC_1_ap_imag__" as definition.
211 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b'.con" "NRootCC_1__NRootCC_1_ap_imag__" as definition.
216 Hint Resolve sqrt_I_nexp: algebra.
219 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con" as lemma.
222 End NRootCC_1_ap_imag
225 (*#* We now define the roots of arbitrary non zero complex numbers. *)
227 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_1.con" as lemma.
238 %\begin{convention}% Let [n : nat] and [c,z : CC] and [c_:(c [#] Zero)].
242 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_2/n.var".
244 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c.var".
246 alias id "z" = "cic:/CoRN/complex/NRootCC/NRootCC_2/z.var".
248 alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c_.var".
250 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_2'.con" as lemma.
252 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_2.con" as lemma.
262 inline procedural "cic:/CoRN/complex/NRootCC/Im_poly.con" as definition.
264 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a1.con" as lemma.
266 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a2.con" as lemma.
269 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)] and [n : nat].
273 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_3/a.var".
275 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b.var".
277 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b_.var".
279 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3/n.var".
281 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_poly''.con" as definition.
283 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a3.con" as lemma.
285 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a4.con" as lemma.
287 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a5.con" as lemma.
289 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a6.con" as lemma.
291 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_poly'.con" as definition.
294 Hint Resolve nrCC3_a3: algebra.
297 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a7.con" as lemma.
299 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a8.con" as lemma.
302 Hint Resolve nth_coeff_p_mult_c_: algebra.
306 Hint Resolve nrCC3_a6: algebra.
309 inline procedural "cic:/CoRN/complex/NRootCC/nrCC3_a9.con" as lemma.
311 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con" as definition.
314 Hint Resolve nrCC3_a1 nrCC3_a7: algebra.
317 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_.con" as lemma.
320 Hint Resolve nrootCC_3_: algebra.
324 Hint Resolve calculate_Im: algebra.
327 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3.con" as lemma.
330 Hint Resolve nrCC3_a2: algebra.
334 Hint Resolve nrCC3_a9: algebra.
337 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con" as lemma.
348 %\begin{convention}% Let [c:IR], [n:nat] and [n_:(lt (0) n)].
352 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/c.var".
354 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n.var".
356 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n_.var".
358 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con" as definition.
360 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'.con" as lemma.
362 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con" as lemma.
373 Section NRootCC_4_ap_real
377 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)], [n : nat] and
378 [n_:(odd n)]; define [c := a[+I*]b].
382 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/a.var".
384 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b.var".
386 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b_.var".
388 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n.var".
390 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n_.var".
394 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/c.con" "NRootCC_4__NRootCC_4_ap_real__" as definition.
399 Section NRootCC_4_solutions
403 Hint Resolve nrootCC_3: algebra.
406 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a1.con" as lemma.
409 %\begin{convention}% Let [r2',c2 : IR] and [r2'_ : (r2' [#] Zero)].
413 alias id "r2'" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'.var".
415 alias id "c2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/c2.var".
417 alias id "r2'_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'_.var".
420 Hint Resolve nrootCC_3': algebra.
423 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a1'.con" as lemma.
426 End NRootCC_4_solutions
430 Section NRootCC_4_equations
434 %\begin{convention}% Let [r,y2 : IR] be such that
435 [(r[+I*]One) [^]n[*] (CC_conj c) [-] (r[+I*][--]One) [^]n[*]c [=] Zero]
436 and [(y2[*] (r[^] (2) [+]One)) [^]n [=] a[^] (2) [+]b[^] (2)].
440 alias id "r" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r.var".
442 alias id "r_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r_property.var".
444 alias id "y2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2.var".
446 alias id "y2_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2_property.var".
448 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a2.con" as lemma.
450 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a3.con" as lemma.
452 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a4.con" as lemma.
454 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_y.con" as definition.
456 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__" as definition.
458 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_x.con" as definition.
460 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/x.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__" as definition.
462 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a5.con" as lemma.
464 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a6.con" as lemma.
466 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_z.con" as definition.
468 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/z.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__" as definition.
470 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a7.con" as lemma.
473 Hint Resolve nrCC4_a6: algebra.
476 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a8.con" as lemma.
478 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a9.con" as lemma.
481 End NRootCC_4_equations
484 inline procedural "cic:/CoRN/complex/NRootCC/nrCC4_a10.con" as lemma.
486 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con" as lemma.
489 End NRootCC_4_ap_real
493 Section NRootCC_4_ap_imag
497 %\begin{convention}% Let [a,b : IR] and [n : nat] with [a [#] Zero]
498 and [(odd n)]; define [c' := (a[+I*]b) [*]II := a'[+I*]b'].
502 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a.var".
504 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b.var".
506 alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a_.var".
508 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n.var".
510 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n_.var".
514 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/c'.con" "NRootCC_4__NRootCC_4_ap_imag__" as definition.
516 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a'.con" "NRootCC_4__NRootCC_4_ap_imag__" as definition.
518 inline procedural "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b'.con" "NRootCC_4__NRootCC_4_ap_imag__" as definition.
522 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con" as lemma.
525 Hint Resolve nroot_minus_I_nexp: algebra.
528 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con" as lemma.
531 End NRootCC_4_ap_imag
534 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_4.con" as lemma.
540 (*#* Finally, the general definition of nth root. *)
546 inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a2.con" as lemma.
548 inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a3.con" as lemma.
551 Hint Resolve nrCC_5a3: algebra.
555 %\begin{convention}% Let [c : CC] with [c [#] Zero].
559 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c.var".
561 alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c_.var".
563 inline procedural "cic:/CoRN/complex/NRootCC/nrCC_5a4.con" as lemma.
565 inline procedural "cic:/CoRN/complex/NRootCC/nrootCC_5.con" as lemma.
571 (*#* Final definition *)
573 inline procedural "cic:/CoRN/complex/NRootCC/CnrootCC.con" as definition.