Zm
Let m be a positive integer. We will look at the integers modulo m and prove that they form a ring. Eventually we will proof that Zp is even a field for p prime.Section zm_setoid.
Definition ZModeq (a b:Z) : Prop := (Zmodeq m a b).
Definition ZModap (a b:Z) : CProp := (~ (Zmodeq m a b)).
Lemma Zmodeq_wd : forall a b:Z, a=b -> a mod m = b mod m.
Lemma Zmodap_irreflexive: (irreflexive ZModap).
Lemma Zmodap_symmetric: (Csymmetric ZModap).
Lemma Zmodap_cotransitive: (cotransitive ZModap).
Lemma Zmodap_tight_apart: (tight_apart ZModeq ZModap).
Lemma Zm_is_CSetoid : (is_CSetoid _ ZModeq ZModap).
Definition Zm_csetoid :=
(Build_CSetoid Z ZModeq ZModap Zm_is_CSetoid).
End zm_setoid.
Section zm_group.
Definition Zm_plus (a b:Zm_csetoid) : Zm_csetoid := (a+b).
Lemma Zm_plus_strext : (bin_fun_strext _ _ _ Zm_plus).
Lemma Zm_plus_wd : (bin_fun_wd _ _ _ Zm_plus).
Definition Zm_plus_op :=
(Build_CSetoid_bin_op _ _ Zm_plus_strext).
Lemma Zm_plus_associative : (associative Zm_plus_op).
Definition Zm_csemi_grp :=
(Build_CSemiGroup Zm_csetoid Zm_plus_op Zm_plus_associative).
Lemma Zm_plus_zero_rht: (is_rht_unit Zm_plus_op 0).
Lemma Zm_plus_zero_lft: (is_lft_unit Zm_plus_op 0).
Lemma Zm_plus_commutes: (commutes Zm_plus_op).
Definition Zm_is_CMonoid :=
(Build_is_CMonoid Zm_csemi_grp 0 Zm_plus_zero_rht Zm_plus_zero_lft).
Definition Zm_cmonoid := (Build_CMonoid _ _ Zm_is_CMonoid).
Definition Zm_opp (x:Zm_cmonoid) : Zm_cmonoid := -x.
Lemma Zm_opp_strext : (un_op_strext _ Zm_opp).
Lemma Zm_opp_well_def : (un_op_wd _ Zm_opp).
Definition Zm_opp_op :=
(Build_CSetoid_un_op _ _ Zm_opp_strext).
Lemma Zm_is_CGroup : (is_CGroup _ Zm_opp_op).
Definition Zm_cgroup := (Build_CGroup _ _ Zm_is_CGroup).
Lemma Zm_is_CAbGroup : (is_CAbGroup Zm_cgroup).
Definition Zm_cabgroup := (Build_CAbGroup _ Zm_is_CAbGroup).
End zm_group.
Section zm_ring.
Hypothesis Hnontriv: ~(m=xH).
Lemma m_gt_1: m>1.
Section zm_def.
Definition Zm_mult (x y:Zm_cabgroup) : Zm_cabgroup := x*y.
Lemma Zm_mult_strext : (bin_fun_strext _ _ _ Zm_mult).
Lemma Zm_mult_wd : (bin_fun_wd _ _ _ Zm_mult).
Definition Zm_mult_op := (Build_CSetoid_bin_op _ _ Zm_mult_strext).
Lemma Zm_mult_assoc : (associative Zm_mult_op).
Lemma Zm_mult_commutative: forall x y:Zm_cabgroup,
(Zm_mult_op x y) [=] (Zm_mult_op y x).
Lemma Zm_mult_one : forall x:Zm_cabgroup, (Zm_mult_op x 1)[=]x.
Lemma Zm_mult_onel : forall x:Zm_cabgroup, (Zm_mult_op 1 x)[=]x.
Definition Zm_mult_semigroup := (Build_CSemiGroup Zm_csetoid Zm_mult_op Zm_mult_assoc).
Lemma Zm_mult_one_r : is_rht_unit Zm_mult_op 1.
Lemma Zm_mult_one_l : is_lft_unit Zm_mult_op 1.
Lemma Zm_mult_monoid: (is_CMonoid Zm_mult_semigroup 1).
Lemma Zm_mult_plus_dist : (distributive Zm_mult_op Zm_plus_op).
Lemma Zm_non_triv : (ZModap 1 0).
Lemma Zm_is_CRing : (is_CRing Zm_cabgroup 1 Zm_mult_op).
End zm_def.
Definition Zm_cring := (Build_CRing _ _ _ Zm_is_CRing) : CRing.
Definition Zm := Zm_cring.
Section zm_ring_basics.
Definition Zm_mult_ord (a:Zm)(h:nat) := (a[^]h[=]1) /\
forall k:nat, (lt k h)->~(a[^]k[=]1).
End zm_ring_basics.
End zm_ring.
Section zp_def.
Hypothesis Hprime: (Prime m).
Lemma p_not_1: ~m=xH.
Lemma p_gt_0: m>0.
Lemma p_gt_1: m>1.
Definition Zp := (Zm p_not_1).
The inverse element in Zp
Let x in Zp, such that x is apart from Zero. Then we will show that there is an inverse element y such that x*y = One in Zp.Section zp_nonzero.
Variable x: Zp.
Hypothesis Hx: x[#]0.
Lemma Zp_nonz_mod: 0<(Zmod x m)<m.
Lemma Zp_nonz_relprime: (Zrelprime x m).
End zp_nonzero.
Definition Zp_inv (x:Zp)(Hx:(x[#]0)) : Zp := (Zgcd_coeff_a x m).
Lemma Zp_inv_strext : forall (x y:Zp)(x_ y_:_), (((Zp_inv x x_)[#](Zp_inv y y_))->(x[#]y)).
Lemma Zp_is_CField: (is_CField Zp Zp_inv).
Definition Fp : CField := (Build_CField _ _ Zp_is_CField Zp_inv_strext).
Definition Fp_inv (x:Fp)(Hx:x[#]0) : Fp := (Zp_inv x Hx).
End zp_def.
Section zp_prop.
End zp_prop.
End zm.