# Library HighSchoolGeometry.formes_complexes

Require Export complexes.
Set Implicit Arguments.
Unset Strict Implicit.
Parameter partie_reelle : C R.
Parameter partie_imaginaire : C R.

Axiom
partie_reelle_def :
(z : C) (a b : R), z = cons_cart a b a = partie_reelle z.

Axiom
partie_imaginaire_def :
(z : C) (a b : R), z = cons_cart a b b = partie_imaginaire z.

Axiom
forme_algebrique_def :
(z : C) (a b : R),
a = partie_reelle z b = partie_imaginaire z z = cons_cart a b.

Lemma car_image_forme_algebrique :
(z : C) (M : PO),
M = image z
partie_reelle z = abscisse M partie_imaginaire z = ordonnee M.
intros.
elim existence_coordonnees with (O := O) (I := I) (J := J) (M := M);
[ intros x H2; elim H2; intros y H3 | auto with geo ].
cut (z = cons_cart x y); intros.
rewrite <- (partie_reelle_def H0).
rewrite <- (partie_imaginaire_def H0).
split; eauto with geo.
eauto with geo.
Qed.

Lemma coordonnees_affixe :
M : PO, cons_cart (abscisse M) (ordonnee M) = affixe M :>C.
intros.
elim existence_affixe_point with (M := M); intros z H;
try clear existence_affixe_point; try exact H.
elim car_image_forme_algebrique with (z := z) (M := M);
[ intros; try exact H1 | eauto with geo ].
rewrite <- H1; rewrite <- H0; rewrite <- H.
symmetry in |- *; eauto with geo.
Qed.
Hint Resolve coordonnees_affixe: geo.

Lemma absvec_ordvec_affixe :
(a b : R) (A B : PO),
a = absvec (vec A B)
b = ordvec (vec A B) cons_cart a b = affixe_vec (vec A B).
intros a b A B.
elim existence_representant_vecteur with (A := O) (B := A) (C := B);
intros D H1; try exact H1.
rewrite <- H1; intros.
apply affixe_point_vecteur.
rewrite H0; rewrite H; rewrite (ordvec_ordonnee (O:=O) (I:=I) (J:=J) D);
auto with geo.
rewrite (absvec_abscisse (O:=O) (I:=I) (J:=J) D); auto with geo.
Qed.
Parameter module : C R.
Parameter argument : C AV.

Axiom
module_def :
(z : C) (M : PO), M = image z module z = distance O M.

Axiom
argument_def :
(M : PO) (z : C),
O M M = image z argument z = cons_AV (vec O I) (vec O M).
Hint Resolve module_def argument_def: geo.

Lemma module_def2 :
(z : C) (M : PO), z = affixe M module z = distance O M.
intros; eauto with geo.
Qed.

Lemma argument_def2 :
(M : PO) (z : C),
O M z = affixe M argument z = cons_AV (vec O I) (vec O M).
intros; eauto with geo.
Qed.

Lemma existence_module : z : C, r : R, module z = r.
intros.
elim existence_image_complexe with (z := z); intros M H1;
try clear existence_image_complexe; try exact H1.
(distance O M); eauto with geo.
Qed.

Definition zeroC := cons_cart 0 0.

Lemma image_zeroC : image zeroC = O.
elim existence_image_complexe with (z := zeroC); unfold zeroC in |- *;
intros M H1; try exact H1.
cut (vec O M = add_PP (mult_PP 0 (vec O I)) (mult_PP 0 (vec O J))); intros;
eauto with geo.
rewrite <- H1.
symmetry in |- ×.
apply vecteur_nul_conf.
rewrite H.
Ringvec.
Qed.
Hint Resolve image_zeroC: geo.

Lemma affixe_origine : zeroC = affixe O.
eauto with geo.
Qed.
Hint Resolve affixe_origine: geo.

Lemma module_zeroC : module zeroC = 0.
rewrite (module_def (z:=zeroC) (M:=O)); auto with geo.
Qed.

Lemma module_nul_zeroC : z : C, module z = 0 z = zeroC.
intros.
elim existence_image_complexe with (z := z); intros M H1;
try clear existence_image_complexe; try exact H1.
cut (O = M); intros.
rewrite (affixe_image H1).
rewrite <- H0; auto with geo.
apply distance_refl1.
rewrite <- H; symmetry in |- *; auto with geo.
Qed.
Hint Resolve module_zeroC module_nul_zeroC: geo.

Lemma module_non_zero : z : C, z zeroC module z 0.
red in |- *; intros.
apply H; auto with geo.
Qed.

Lemma nonzero_module : z : C, module z 0 z zeroC.
red in |- *; intros.
apply H; rewrite H0; auto with geo.
Qed.
Hint Resolve module_non_zero nonzero_module: geo.

Lemma image_nonzero_nonorigine :
(M : PO) (z : C), z zeroC :>C M = image z O M.
intros.
red in |- *; intros; apply H.
replace z with (affixe M).
rewrite <- H1; auto with geo.
symmetry in |- *; auto with geo.
Qed.
Hint Resolve image_nonzero_nonorigine: geo.

Lemma nonorigine_image_nonzero :
(M : PO) (z : C), O M M = image z z zeroC :>C.
intros.
red in |- *; intros; apply H.
rewrite H0; rewrite H1.
symmetry in |- *; auto with geo.
Qed.
Hint Resolve nonorigine_image_nonzero: geo.

Lemma existence_argument :
z : C, z zeroC a : R, argument z = image_angle a.
intros.
elim existence_image_complexe with (z := z); intros M H1;
try clear existence_image_complexe; try exact H1.
cut (O M); intros; eauto with geo.
mesure O I O M.
x.
rewrite H2; eauto with geo.
Qed.

Lemma existence_forme_polaire :
z : C,
z zeroC
r : R, ( a : R, module z = r argument z = image_angle a).
intros.
elim existence_module with (z := z); intros r H0; try clear existence_module;
try exact H0.
elim existence_argument with (z := z);
[ intros a H1; try clear existence_argument; try exact H1 | auto ].
r; a; auto.
Qed.
Parameter cons_pol : R R C.

Axiom
forme_polaire_def :
(z : C) (r a : R),
z zeroC
module z = r argument z = image_angle a z = cons_pol r a.

Axiom complexe_polaire_module : r a : R, module (cons_pol r a) = r.

Axiom
complexe_polaire_argument :
r a : R, r 0 argument (cons_pol r a) = image_angle a.

Lemma polaire_non_nul : r a : R, r 0 cons_pol r a zeroC.
intros.
apply nonzero_module.
rewrite complexe_polaire_module; auto.
Qed.

Lemma complexe_pol_module :
(z : C) (r a : R), z zeroC z = cons_pol r a module z = r.
intros.
rewrite H0; rewrite complexe_polaire_module; auto.
Qed.

Lemma complexe_pol_argument :
(z : C) (r a : R),
z zeroC z = cons_pol r a argument z = image_angle a.
intros.
rewrite H0; rewrite complexe_polaire_argument; auto.
rewrite <- (complexe_pol_module (z:=z) (r:=r) (a:=a)); auto with geo.
Qed.
Hint Resolve forme_polaire_def complexe_pol_module complexe_pol_argument
polaire_non_nul complexe_polaire_module complexe_polaire_module: geo.

Lemma pol_complexe_module :
(z : C) (r a : R) (M : PO),
z zeroC z = cons_pol r a M = image z distance O M = r.
intros.
rewrite <- (module_def H1); eauto with geo.
Qed.

Lemma pol_complexe_argument :
(z : C) (r a : R) (M : PO),
z zeroC
z = cons_pol r a
M = image z cons_AV (vec O I) (vec O M) = image_angle a.
intros.
rewrite <- (argument_def (M:=M) (z:=z)); eauto with geo.
Qed.
Hint Resolve pol_complexe_argument pol_complexe_module: geo.

Lemma image_forme_polaire :
(z : C) (M : PO),
O M
M = image z
module z = distance O M argument z = cons_AV (vec O I) (vec O M).
intros.
split; eauto with geo.
Qed.

Lemma unicite_forme_polaire_nonzero :
(z : C) (r a r' a' : R),
z zeroC
z = cons_pol r a
z = cons_pol r' a' r = r' image_angle a = image_angle a'.
intros.
split.
rewrite <- (complexe_pol_module (z:=z) (r:=r) (a:=a)); eauto with geo.
rewrite <- (complexe_pol_argument (z:=z) (r:=r) (a:=a)); eauto with geo.
Qed.
Hint Resolve unicite_forme_polaire_nonzero image_forme_polaire: geo.

Lemma passage_polaire_algebrique :
(z : C) (r a x y : R),
z zeroC
z = cons_cart x y z = cons_pol r a x = r × cos a y = r × sin a.
intros.
elim existence_image_complexe with (z := z); intros M H2;
try clear existence_image_complexe; try exact H2.
elim
coordonnees_polaires_cartesiennes
with
(x := x)
(y := y)
(a := a)
(r := r)
(O := O)
(I := I)
(J := J)
(M := M);
[ intros; eauto with geo
| eauto with geo
| eauto with geo
| eauto with geo
| eauto with geo
| eauto with geo ].
symmetry in |- *; eauto with geo.
symmetry in |- *; eauto with geo.
Qed.

Lemma passage_algebrique_module :
(z : C) (x y : R),
z = cons_cart x y module z = sqrt (Rsqr x + Rsqr y).
intros.
elim existence_image_complexe with (z := z); intros M H2;
try clear existence_image_complexe; try exact H2.
replace (module z) with (distance O M); auto.
rewrite (distance_coordonnees (O:=O) (I:=I) (J:=J) (M:=M) (x:=x) (y:=y));
eauto with geo.
symmetry in |- *; eauto with geo.
Qed.

Lemma passage_algebrique_argument :
(z : C) (r x y a : R),
z zeroC
z = cons_cart x y z = cons_pol r a cos a = / r × x sin a = / r × y.
intros.
elim
passage_polaire_algebrique with (z := z) (r := r) (a := a) (x := x) (y := y);
[ intros | eauto with geo | eauto with geo | eauto with geo ].
cut (r 0); intros.
split; [ try assumption | idtac ].
rewrite H2.
field; auto.
rewrite H3.
field; auto.
replace r with (module z); eauto with geo.
Qed.

Lemma egalite_forme_polaire :
z z' : C,
z zeroC
z' zeroC module z = module z' argument z = argument z' z = z'.
intros.
elim existence_forme_polaire with (z := z);
[ intros r H3; elim H3; intros a H4; elim H4; intros H5 H6;
try clear H4 H3 existence_forme_polaire; try exact H6
| auto ].
elim existence_forme_polaire with (z := z');
[ intros r0 H7; elim H7; intros a0 H8; elim H8; intros H9 H10;
try clear H8 H7 existence_forme_polaire; try exact H10
| auto ].
rewrite (forme_polaire_def (z:=z) (r:=r) (a:=a)); auto.
rewrite (forme_polaire_def (z:=z') (r:=r) (a:=a)); auto.
rewrite <- H5; auto.
rewrite <- H6; auto.
Qed.
Hint Resolve passage_algebrique_module passage_algebrique_argument
egalite_forme_polaire: geo.

Lemma algebrique_zeroC :
a b : R, cons_cart a b = zeroC :>C a = 0 b = 0.
intros.
apply unicite_parties_relles_imaginaires with zeroC; auto.
Qed.

Lemma polaire_calcul_algebrique :
(z : C) (r a : R),
z zeroC :>C
z = cons_pol r a :>C z = cons_cart (r × cos a) (r × sin a) :>C.
intros.
elim existence_parties_relles_imaginaires with (z := z); intros a0 H1;
elim H1; intros b H2; try clear H1 existence_parties_relles_imaginaires;
try exact H2.
elim
passage_polaire_algebrique
with (z := z) (r := r) (a := a) (x := a0) (y := b);
[ intros; try exact H4 | auto | auto | auto ].
rewrite H2; rewrite H3; rewrite H4; auto.
Qed.
Hint Resolve polaire_calcul_algebrique: geo.

Definition Rinj (x : R) := cons_cart x 0.

Definition oneC := cons_cart 1 0.
Hint Unfold oneC zeroC Rinj: geo.

Lemma Rinj_zero : Rinj 0 = zeroC.
unfold Rinj, zeroC in |- *; auto.
Qed.

Lemma Rinj_un : Rinj 1 = oneC.
unfold Rinj, oneC in |- *; auto.
Qed.

Lemma module_oneC : module oneC = 1.
intros.
rewrite (passage_algebrique_module (z:=oneC) (x:=1) (y:=0)).
replace (Rsqr 1 + Rsqr 0) with 1 by (unfold Rsqr; ring).
exact sqrt_1.
unfold oneC in |- *; auto.
Qed.

Lemma oneC_nonzero : oneC zeroC.
apply nonzero_module.
rewrite module_oneC; auto with real.
Qed.
Hint Resolve module_oneC oneC_nonzero: geo.

Lemma argument_oneC : argument oneC = image_angle 0.
elim existence_forme_polaire with (z := oneC);
[ intros r H; elim H; intros a H0; elim H0; intros H1 H2;
try clear H0 H existence_forme_polaire; try exact H2
| auto with geo ].
rewrite module_oneC in H1.
rewrite H2.
elim
passage_algebrique_argument
with (z := oneC) (r := 1) (x := 1) (y := 0) (a := a);
[ intros | auto with geo | auto with geo | auto with geo ].
apply egalite_angle_trigo.
rewrite sin_zero; rewrite H4; ring.
rewrite H3; rewrite cos_zero; field.
Qed.
Hint Resolve argument_oneC: geo.

Definition i := cons_cart 0 1.
Hint Unfold i: geo.

Lemma module_i : module i = 1.
intros.
rewrite (passage_algebrique_module (z:=i) (x:=0) (y:=1)).
replace (Rsqr 0 + Rsqr 1) with 1 by (unfold Rsqr; ring).
exact sqrt_1.
unfold i in |- *; auto.
Qed.

Lemma i_nonzero : i zeroC.
apply nonzero_module.
rewrite module_i; auto with real.
Qed.
Hint Resolve module_i i_nonzero: geo.

Lemma argument_i : argument i = image_angle pisurdeux.
elim existence_forme_polaire with (z := i);
[ intros r H; elim H; intros a H0; elim H0; intros H1 H2;
try clear H0 H existence_forme_polaire; try exact H2
| auto with geo ].
elim
passage_algebrique_argument
with (z := i) (r := 1) (x := 0) (y := 1) (a := a);
[ intros | auto with geo | auto with geo | auto with geo ].
rewrite module_i in H1.
rewrite H2.
elim
passage_algebrique_argument
with (z := i) (r := 1) (x := 0) (y := 1) (a := a);
[ intros | auto with geo | auto with geo | auto with geo ].
apply egalite_angle_trigo.
rewrite sin_pisurdeux; rewrite H4; field.
rewrite H3; rewrite cos_pisurdeux; ring.
Qed.
Hint Resolve argument_i: geo.

Lemma forme_polaire_oneC : oneC = cons_pol 1 0.
apply forme_polaire_def; auto with geo.
Qed.

Lemma forme_polaire_i : i = cons_pol 1 pisurdeux.
apply forme_polaire_def; auto with geo.
Qed.
Hint Resolve forme_polaire_oneC forme_polaire_i: geo.

Lemma egalite_cart_pol :
x y r a : R,
r 0
module (cons_cart x y) = r
argument (cons_cart x y) = image_angle a :>AV
cons_cart x y = cons_pol r a :>C.
intros.
rewrite <- (forme_polaire_def (z:=cons_cart x y) (r:=r) (a:=a));
auto with geo.
apply nonzero_module.
rewrite H0; auto.
Qed.

Lemma module_opp_un : module (Rinj (-1)) = 1.
unfold Rinj in |- ×.
rewrite (passage_algebrique_module (z:=cons_cart (-1) 0) (x:=-1) (y:=0));
auto with geo.
replace (Rsqr (-1) + Rsqr 0) with 1 by (unfold Rsqr; ring).
exact sqrt_1.
Qed.

Lemma opp_un_nonzero : Rinj (-1) zeroC :>C.
apply nonzero_module.
rewrite module_opp_un; auto with real.
Qed.
Hint Resolve opp_un_nonzero module_opp_un: geo.

Lemma argument_opp_un : argument (Rinj (-1)) = image_angle pi.
elim existence_forme_polaire with (z := Rinj (-1));
[ intros r H1; elim H1; intros a H2; elim H2; intros H3 H4; try clear H2 H1;
try exact H4
| auto with geo ].
rewrite module_opp_un in H3.
elim
passage_algebrique_argument
with (z := Rinj (-1)) (r := 1) (x := -1) (y := 0) (a := a);
[ intros | auto with geo | auto with geo | auto with geo ].
rewrite H4.
apply egalite_angle_trigo.
rewrite sin_pi; rewrite H0; ring.
rewrite H; rewrite cos_pi; field.
Qed.
Hint Resolve argument_opp_un: geo.

Lemma forme_polaire_opp_un : Rinj (-1) = cons_pol 1 pi.
apply forme_polaire_def; auto with geo.
Qed.

Lemma module_reel : x : R, module (Rinj x) = Rabs x.
unfold Rinj in |- *; intros.
rewrite (passage_algebrique_module (z:=cons_cart x 0) (x:=x) (y:=0));
auto with geo.
replace (Rsqr x + Rsqr 0) with (Rsqr x) by (unfold Rsqr; ring).
rewrite sqrt_Rsqr_abs; auto.
Qed.

Lemma module_reel_pos : x : R, 0 x module (Rinj x) = x.
unfold Rinj in |- *; intros.
rewrite (passage_algebrique_module (z:=cons_cart x 0) (x:=x) (y:=0));
auto with geo.
replace (Rsqr x + Rsqr 0) with (Rsqr x) by (unfold Rsqr in |- *; ring).
rewrite sqrt_Rsqr; auto.
Qed.

Lemma reel_non_nul : x : R, x 0 Rinj x zeroC.
intros.
apply nonzero_module.
rewrite module_reel.
apply Rabs_no_R0; auto.
Qed.
Hint Resolve reel_non_nul module_reel_pos module_reel: geo.

Lemma argument_reel_pos :
x : R, 0 < x argument (Rinj x) = image_angle 0.
intros.
cut (x 0); intros.
elim existence_forme_polaire with (z := Rinj x);
[ intros r H1; elim H1; intros a H2; elim H2; intros H3 H4; try clear H2 H1;
try exact H4
| auto with geo ].
cut (x = r); intros.
elim
passage_algebrique_argument
with (z := Rinj x) (r := r) (x := x) (y := 0) (a := a);
[ intros | auto with geo | auto with geo | auto with geo ].
rewrite H4.
apply egalite_angle_trigo.
rewrite sin_zero; rewrite H5; ring.
rewrite H2; rewrite <- H1; rewrite cos_zero; field; trivial.
rewrite module_reel_pos in H3; auto.
fourier.
auto with real.
Qed.
Hint Resolve argument_reel_pos: geo.

Lemma forme_pol_reel_pos : x : R, 0 < x Rinj x = cons_pol x 0 :>C.
intros.
apply forme_polaire_def; auto with geo.
apply reel_non_nul; auto with real.
apply module_reel_pos; auto with real.
Qed.

Lemma module_reel_neg : x : R, 0 > x module (Rinj x) = - x.
intros.
rewrite module_reel; auto.
apply Rabs_left1; auto with real.
Qed.
Hint Resolve module_reel_neg: geo.

Lemma argument_reel_neg :
x : R, 0 > x argument (Rinj x) = image_angle pi.
intros.
cut (x 0); intros.
elim existence_forme_polaire with (z := Rinj x);
[ intros r H1; elim H1; intros a H2; elim H2; intros H3 H4; try clear H2 H1;
try exact H4
| auto with geo ].
elim
passage_algebrique_argument
with (z := Rinj x) (r := r) (x := x) (y := 0) (a := a);
[ intros | auto with geo | auto with geo | auto with geo ].
rewrite H4.
apply egalite_angle_trigo.
rewrite sin_pi; rewrite H2; ring.
cut (r = - x); intros.
rewrite H1; rewrite H5; rewrite cos_pi; field; trivial.
rewrite <- H3.
rewrite module_reel_neg in |- *; [ ring | auto with geo ].
auto with real.
Qed.
Hint Resolve argument_reel_neg: geo.

Lemma forme_pol_reel_neg :
x : R, 0 > x Rinj x = cons_pol (- x) pi :>C.
intros.
apply forme_polaire_def; auto with geo.
apply reel_non_nul; auto with real.
Qed.

Lemma module_pos : z : C, module z 0.
intros.
elim existence_image_complexe with (z := z); intros M H;
try clear existence_image_complexe; try exact H.
rewrite (module_def H); auto with geo.
Qed.
Hint Resolve module_pos: geo.

Lemma module_stric_pos : z : C, z zeroC :>C module z > 0.
intros.
cut (module z 0); intros; auto with geo.
elim H0; intros; auto.
absurd (module z = 0); auto with geo.
Qed.
Hint Resolve module_stric_pos: geo.

Lemma abs_module : z : C, module z = Rabs (module z).
intros.
cut (module z 0); intros; auto with geo.
rewrite Rabs_right; auto.
Qed.
Hint Resolve abs_module: geo.