matita/contribs/CoRN-Decl/complex/NRootCC.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/complex/NRootCC".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: NRootCC.v,v 1.9 2004/04/23 10:00:55 lcf Exp $ *)
  22
  23 (*#* printing sqrt_Half %\ensuremath{\sqrt{\frac12}}% *)
  24
  25 (*#* printing sqrt_I %\ensuremath{\sqrt{\imath}}% *)
  26
  27 (*#* printing nroot_I %\ensuremath{\sqrt[n]{\imath}}% *)
  28
  29 (*#* printing nroot_minus_I %\ensuremath{\sqrt[n]{-\imath}}% *)
  30
  31 include "complex/CComplex.ma".
  32
  33 (*#* * Roots of Complex Numbers
  34
  35 Properties of non-zero complex numbers
  36 *)
  37
  38 (* UNEXPORTED
  39 Section CC_ap_zero
  40 *)
  41
  42 inline "cic:/CoRN/complex/NRootCC/cc_ap_zero.con".
  43
  44 inline "cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con".
  45
  46 (* UNEXPORTED
  47 End CC_ap_zero
  48 *)
  49
  50 (*#* Weird lemma. *)
  51
  52 (* UNEXPORTED
  53 Section Imag_to_Real
  54 *)
  55
  56 inline "cic:/CoRN/complex/NRootCC/imag_to_real.con".
  57
  58 (* UNEXPORTED
  59 End Imag_to_Real
  60 *)
  61
  62 (*#* ** Roots of the imaginary unit *)
  63
  64 (* UNEXPORTED
  65 Section NRootI
  66 *)
  67
  68 inline "cic:/CoRN/complex/NRootCC/sqrt_Half.con".
  69
  70 inline "cic:/CoRN/complex/NRootCC/sqrt_I.con".
  71
  72 inline "cic:/CoRN/complex/NRootCC/sqrt_I_nexp.con".
  73
  74 inline "cic:/CoRN/complex/NRootCC/nroot_I_nexp_aux.con".
  75
  76 inline "cic:/CoRN/complex/NRootCC/nroot_I.con".
  77
  78 inline "cic:/CoRN/complex/NRootCC/nroot_I_nexp.con".
  79
  80 (* UNEXPORTED
  81 Hint Resolve nroot_I_nexp: algebra.
  82 *)
  83
  84 inline "cic:/CoRN/complex/NRootCC/nroot_minus_I.con".
  85
  86 inline "cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con".
  87
  88 (* UNEXPORTED
  89 End NRootI
  90 *)
  91
  92 (*#* ** Roots of complex numbers *)
  93
  94 (* UNEXPORTED
  95 Section NRootCC_1
  96 *)
  97
  98 (*#* We define the nth root of a complex number with a non zero imaginary part.
  99 *)
 100
 101 (* UNEXPORTED
 102 Section NRootCC_1_ap_real
 103 *)
 104
 105 (*#*
 106 %\begin{convention}% Let [a,b : IR] and [b_ : (b [#] Zero)].
 107 Define [c2 := a[^]2[+]b[^]2], [c := sqrt c2], [a'2 := (c[+]a) [*]Half],
 108 [a' := sqrt a'2], [b'2 := (c[-]a) [*]Half] and [b' := sqrt b'2].
 109 %\end{convention}%
 110 *)
 111
 112 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a.var".
 113
 114 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b.var".
 115
 116 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b_.var".
 117
 118 (* begin hide *)
 119
 120 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c2.con" "NRootCC_1__NRootCC_1_ap_real__".
 121
 122 (* end hide *)
 123
 124 inline "cic:/CoRN/complex/NRootCC/nrCC1_c2pos.con".
 125
 126 (* begin hide *)
 127
 128 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c.con" "NRootCC_1__NRootCC_1_ap_real__".
 129
 130 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'2.con" "NRootCC_1__NRootCC_1_ap_real__".
 131
 132 (* end hide *)
 133
 134 inline "cic:/CoRN/complex/NRootCC/nrCC1_a'2pos.con".
 135
 136 (* begin hide *)
 137
 138 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'.con" "NRootCC_1__NRootCC_1_ap_real__".
 139
 140 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'2.con" "NRootCC_1__NRootCC_1_ap_real__".
 141
 142 (* end hide *)
 143
 144 inline "cic:/CoRN/complex/NRootCC/nrCC1_b'2pos.con".
 145
 146 (* begin hide *)
 147
 148 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'.con" "NRootCC_1__NRootCC_1_ap_real__".
 149
 150 (* end hide *)
 151
 152 inline "cic:/CoRN/complex/NRootCC/nrCC1_a3.con".
 153
 154 inline "cic:/CoRN/complex/NRootCC/nrCC1_a4.con".
 155
 156 (* UNEXPORTED
 157 Hint Resolve nrCC1_a4: algebra.
 158 *)
 159
 160 inline "cic:/CoRN/complex/NRootCC/nrCC1_a5.con".
 161
 162 inline "cic:/CoRN/complex/NRootCC/nrCC1_a6.con".
 163
 164 inline "cic:/CoRN/complex/NRootCC/nrCC1_a6'.con".
 165
 166 (* UNEXPORTED
 167 Hint Resolve nrCC1_a5: algebra.
 168 *)
 169
 170 inline "cic:/CoRN/complex/NRootCC/nrCC1_a7_upper.con".
 171
 172 inline "cic:/CoRN/complex/NRootCC/nrCC1_a7_lower.con".
 173
 174 (* UNEXPORTED
 175 Hint Resolve nrCC1_a3 nrCC1_a7_upper nrCC1_a7_lower: algebra.
 176 *)
 177
 178 inline "cic:/CoRN/complex/NRootCC/nrootCC_1_upper.con".
 179
 180 inline "cic:/CoRN/complex/NRootCC/nrootCC_1_lower.con".
 181
 182 inline "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con".
 183
 184 (* UNEXPORTED
 185 End NRootCC_1_ap_real
 186 *)
 187
 188 (*#* We now define the nth root of a complex number with a non zero real part.
 189 *)
 190
 191 (* UNEXPORTED
 192 Section NRootCC_1_ap_imag
 193 *)
 194
 195 (*#*
 196 %\begin{convention}% Let [a,b : IR] and [a_ : (a [#] Zero)] and define
 197 [c' := (a[+I*]b) [*][--]II := a'[+I*]b'].
 198 %\end{convention}%
 199 *)
 200
 201 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a.var".
 202
 203 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b.var".
 204
 205 alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a_.var".
 206
 207 (* begin hide *)
 208
 209 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/c'.con" "NRootCC_1__NRootCC_1_ap_imag__".
 210
 211 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a'.con" "NRootCC_1__NRootCC_1_ap_imag__".
 212
 213 inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b'.con" "NRootCC_1__NRootCC_1_ap_imag__".
 214
 215 (* end hide *)
 216
 217 (* UNEXPORTED
 218 Hint Resolve sqrt_I_nexp: algebra.
 219 *)
 220
 221 inline "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con".
 222
 223 (* UNEXPORTED
 224 End NRootCC_1_ap_imag
 225 *)
 226
 227 (*#* We now define the roots of arbitrary non zero complex numbers. *)
 228
 229 inline "cic:/CoRN/complex/NRootCC/nrootCC_1.con".
 230
 231 (* UNEXPORTED
 232 End NRootCC_1
 233 *)
 234
 235 (* UNEXPORTED
 236 Section NRootCC_2
 237 *)
 238
 239 (*#*
 240 %\begin{convention}% Let [n : nat] and [c,z : CC] and [c_:(c [#] Zero)].
 241 %\end{convention}%
 242 *)
 243
 244 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_2/n.var".
 245
 246 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c.var".
 247
 248 alias id "z" = "cic:/CoRN/complex/NRootCC/NRootCC_2/z.var".
 249
 250 alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c_.var".
 251
 252 inline "cic:/CoRN/complex/NRootCC/nrootCC_2'.con".
 253
 254 inline "cic:/CoRN/complex/NRootCC/nrootCC_2.con".
 255
 256 (* UNEXPORTED
 257 End NRootCC_2
 258 *)
 259
 260 (* UNEXPORTED
 261 Section NRootCC_3
 262 *)
 263
 264 inline "cic:/CoRN/complex/NRootCC/Im_poly.con".
 265
 266 inline "cic:/CoRN/complex/NRootCC/nrCC3_a1.con".
 267
 268 inline "cic:/CoRN/complex/NRootCC/nrCC3_a2.con".
 269
 270 (*#*
 271 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)] and [n : nat].
 272 %\end{convention}%
 273 *)
 274
 275 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_3/a.var".
 276
 277 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b.var".
 278
 279 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b_.var".
 280
 281 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3/n.var".
 282
 283 inline "cic:/CoRN/complex/NRootCC/nrCC3_poly''.con".
 284
 285 inline "cic:/CoRN/complex/NRootCC/nrCC3_a3.con".
 286
 287 inline "cic:/CoRN/complex/NRootCC/nrCC3_a4.con".
 288
 289 inline "cic:/CoRN/complex/NRootCC/nrCC3_a5.con".
 290
 291 inline "cic:/CoRN/complex/NRootCC/nrCC3_a6.con".
 292
 293 inline "cic:/CoRN/complex/NRootCC/nrCC3_poly'.con".
 294
 295 (* UNEXPORTED
 296 Hint Resolve nrCC3_a3: algebra.
 297 *)
 298
 299 inline "cic:/CoRN/complex/NRootCC/nrCC3_a7.con".
 300
 301 inline "cic:/CoRN/complex/NRootCC/nrCC3_a8.con".
 302
 303 (* UNEXPORTED
 304 Hint Resolve nth_coeff_p_mult_c_: algebra.
 305 *)
 306
 307 (* UNEXPORTED
 308 Hint Resolve nrCC3_a6: algebra.
 309 *)
 310
 311 inline "cic:/CoRN/complex/NRootCC/nrCC3_a9.con".
 312
 313 inline "cic:/CoRN/complex/NRootCC/nrootCC_3_poly.con".
 314
 315 (* UNEXPORTED
 316 Hint Resolve nrCC3_a1 nrCC3_a7: algebra.
 317 *)
 318
 319 inline "cic:/CoRN/complex/NRootCC/nrootCC_3_.con".
 320
 321 (* UNEXPORTED
 322 Hint Resolve nrootCC_3_: algebra.
 323 *)
 324
 325 (* UNEXPORTED
 326 Hint Resolve calculate_Im: algebra.
 327 *)
 328
 329 inline "cic:/CoRN/complex/NRootCC/nrootCC_3.con".
 330
 331 (* UNEXPORTED
 332 Hint Resolve nrCC3_a2: algebra.
 333 *)
 334
 335 (* UNEXPORTED
 336 Hint Resolve nrCC3_a9: algebra.
 337 *)
 338
 339 inline "cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con".
 340
 341 (* UNEXPORTED
 342 End NRootCC_3
 343 *)
 344
 345 (* UNEXPORTED
 346 Section NRootCC_3'
 347 *)
 348
 349 (*#*
 350 %\begin{convention}% Let [c:IR], [n:nat] and [n_:(lt (0) n)].
 351 %\end{convention}%
 352 *)
 353
 354 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/c.var".
 355
 356 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n.var".
 357
 358 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n_.var".
 359
 360 inline "cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con".
 361
 362 inline "cic:/CoRN/complex/NRootCC/nrootCC_3'.con".
 363
 364 inline "cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con".
 365
 366 (* UNEXPORTED
 367 End NRootCC_3'
 368 *)
 369
 370 (* UNEXPORTED
 371 Section NRootCC_4
 372 *)
 373
 374 (* UNEXPORTED
 375 Section NRootCC_4_ap_real
 376 *)
 377
 378 (*#*
 379 %\begin{convention}% Let [a,b : IR], [b_ : (b [#] Zero)], [n : nat] and
 380 [n_:(odd n)]; define [c := a[+I*]b].
 381 %\end{convention}%
 382 *)
 383
 384 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/a.var".
 385
 386 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b.var".
 387
 388 alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b_.var".
 389
 390 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n.var".
 391
 392 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n_.var".
 393
 394 (* begin hide *)
 395
 396 inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/c.con" "NRootCC_4__NRootCC_4_ap_real__".
 397
 398 (* end hide *)
 399
 400 (* UNEXPORTED
 401 Section NRootCC_4_solutions
 402 *)
 403
 404 (* UNEXPORTED
 405 Hint Resolve nrootCC_3: algebra.
 406 *)
 407
 408 inline "cic:/CoRN/complex/NRootCC/nrCC4_a1.con".
 409
 410 (*#*
 411 %\begin{convention}% Let [r2',c2 : IR] and [r2'_ : (r2' [#] Zero)].
 412 %\end{convention}%
 413 *)
 414
 415 alias id "r2'" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'.var".
 416
 417 alias id "c2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/c2.var".
 418
 419 alias id "r2'_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'_.var".
 420
 421 (* UNEXPORTED
 422 Hint Resolve nrootCC_3': algebra.
 423 *)
 424
 425 inline "cic:/CoRN/complex/NRootCC/nrCC4_a1'.con".
 426
 427 (* UNEXPORTED
 428 End NRootCC_4_solutions
 429 *)
 430
 431 (* UNEXPORTED
 432 Section NRootCC_4_equations
 433 *)
 434
 435 (*#*
 436 %\begin{convention}% Let [r,y2 : IR] be such that
 437 [(r[+I*]One) [^]n[*] (CC_conj c) [-] (r[+I*][--]One) [^]n[*]c [=] Zero]
 438 and [(y2[*] (r[^] (2) [+]One)) [^]n [=] a[^] (2) [+]b[^] (2)].
 439 %\end{convention}%
 440 *)
 441
 442 alias id "r" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r.var".
 443
 444 alias id "r_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r_property.var".
 445
 446 alias id "y2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2.var".
 447
 448 alias id "y2_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2_property.var".
 449
 450 inline "cic:/CoRN/complex/NRootCC/nrCC4_a2.con".
 451
 452 inline "cic:/CoRN/complex/NRootCC/nrCC4_a3.con".
 453
 454 inline "cic:/CoRN/complex/NRootCC/nrCC4_a4.con".
 455
 456 inline "cic:/CoRN/complex/NRootCC/nrCC4_y.con".
 457
 458 inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
 459
 460 inline "cic:/CoRN/complex/NRootCC/nrCC4_x.con".
 461
 462 inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/x.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
 463
 464 inline "cic:/CoRN/complex/NRootCC/nrCC4_a5.con".
 465
 466 inline "cic:/CoRN/complex/NRootCC/nrCC4_a6.con".
 467
 468 inline "cic:/CoRN/complex/NRootCC/nrCC4_z.con".
 469
 470 inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/z.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
 471
 472 inline "cic:/CoRN/complex/NRootCC/nrCC4_a7.con".
 473
 474 (* UNEXPORTED
 475 Hint Resolve nrCC4_a6: algebra.
 476 *)
 477
 478 inline "cic:/CoRN/complex/NRootCC/nrCC4_a8.con".
 479
 480 inline "cic:/CoRN/complex/NRootCC/nrCC4_a9.con".
 481
 482 (* UNEXPORTED
 483 End NRootCC_4_equations
 484 *)
 485
 486 inline "cic:/CoRN/complex/NRootCC/nrCC4_a10.con".
 487
 488 inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con".
 489
 490 (* UNEXPORTED
 491 End NRootCC_4_ap_real
 492 *)
 493
 494 (* UNEXPORTED
 495 Section NRootCC_4_ap_imag
 496 *)
 497
 498 (*#*
 499 %\begin{convention}% Let [a,b : IR] and [n : nat] with [a [#] Zero]
 500 and [(odd n)]; define [c' := (a[+I*]b) [*]II := a'[+I*]b'].
 501 %\end{convention}%
 502 *)
 503
 504 alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a.var".
 505
 506 alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b.var".
 507
 508 alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a_.var".
 509
 510 alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n.var".
 511
 512 alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n_.var".
 513
 514 (* begin hide *)
 515
 516 inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/c'.con" "NRootCC_4__NRootCC_4_ap_imag__".
 517
 518 inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a'.con" "NRootCC_4__NRootCC_4_ap_imag__".
 519
 520 inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b'.con" "NRootCC_4__NRootCC_4_ap_imag__".
 521
 522 (* end hide *)
 523
 524 inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real'.con".
 525
 526 (* UNEXPORTED
 527 Hint Resolve nroot_minus_I_nexp: algebra.
 528 *)
 529
 530 inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con".
 531
 532 (* UNEXPORTED
 533 End NRootCC_4_ap_imag
 534 *)
 535
 536 inline "cic:/CoRN/complex/NRootCC/nrootCC_4.con".
 537
 538 (* UNEXPORTED
 539 End NRootCC_4
 540 *)
 541
 542 (*#* Finally, the general definition of nth root. *)
 543
 544 (* UNEXPORTED
 545 Section NRootCC_5
 546 *)
 547
 548 inline "cic:/CoRN/complex/NRootCC/nrCC_5a2.con".
 549
 550 inline "cic:/CoRN/complex/NRootCC/nrCC_5a3.con".
 551
 552 (* UNEXPORTED
 553 Hint Resolve nrCC_5a3: algebra.
 554 *)
 555
 556 (*#*
 557 %\begin{convention}% Let [c : CC] with [c [#] Zero].
 558 %\end{convention}%
 559 *)
 560
 561 alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c.var".
 562
 563 alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c_.var".
 564
 565 inline "cic:/CoRN/complex/NRootCC/nrCC_5a4.con".
 566
 567 inline "cic:/CoRN/complex/NRootCC/nrootCC_5.con".
 568
 569 (* UNEXPORTED
 570 End NRootCC_5
 571 *)
 572
 573 (*#* Final definition *)
 574
 575 inline "cic:/CoRN/complex/NRootCC/CnrootCC.con".
 576