From 06873c26e897b423cf2ea4814246fc5c2c5d4346 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 10 Dec 2012 08:56:30 +0000 Subject: [PATCH] Porting chebyshev --- matita/matita/lib/arithmetics/big_pi.ma | 417 ++++++++++++++++++++++++ matita/matita/lib/arithmetics/ord.ma | 415 +++++++++++++++++++++++ 2 files changed, 832 insertions(+) create mode 100644 matita/matita/lib/arithmetics/big_pi.ma create mode 100644 matita/matita/lib/arithmetics/ord.ma diff --git a/matita/matita/lib/arithmetics/big_pi.ma b/matita/matita/lib/arithmetics/big_pi.ma new file mode 100644 index 000000000..94068a088 --- /dev/null +++ b/matita/matita/lib/arithmetics/big_pi.ma @@ -0,0 +1,417 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "arithmetics/primes.ma". +include "arithmetics/bigops.ma". + +theorem sigma_const: ∀n:nat. ∑_{ibigop_Strue // +qed. + +(* monotonicity; these roperty should be expressed at a more +genral level *) + +theorem le_pi: +∀n.∀p:nat → bool.∀g1,g2:nat → nat. + (∀i.ibigop_Strue // >bigop_Strue // @le_times + [@Hle // |@Hind #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]] + |>bigop_Sfalse // >bigop_Sfalse // @Hind + #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi] + ] + ] +qed. + +theorem exp_sigma: ∀n,a,p. + ∏_{i < n | p i} a = exp a (∑_{i < n | p i} 1). +#n #a #p elim n // #n1 cases (true_or_false (p n1)) #Hcase + [>bigop_Strue // >bigop_Strue // |>bigop_Sfalse // >bigop_Sfalse //] +qed. + +theorem times_pi: ∀n,p,f,g. + ∏_{ibigop_Strue // >bigop_Strue // >bigop_Strue // + |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse // + ] +qed. + +(* +theorem true_to_pi_p_Sn: ∀n,p,g. + p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g). +intros. +unfold pi_p. +apply true_to_iter_p_gen_Sn. +assumption. +qed. + +theorem false_to_pi_p_Sn: +\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat. +p n = false \to pi_p (S n) p g = pi_p n p g. +intros. +unfold pi_p. +apply false_to_iter_p_gen_Sn. +assumption. +qed. + +theorem eq_pi_p: \forall p1,p2:nat \to bool. +\forall g1,g2: nat \to nat.\forall n. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to g1 x = g2 x) \to +pi_p n p1 g1 = pi_p n p2 g2. +intros. +unfold pi_p. +apply eq_iter_p_gen; +assumption. +qed. + +theorem eq_pi_p1: \forall p1,p2:nat \to bool. +\forall g1,g2: nat \to nat.\forall n. +(\forall x. x < n \to p1 x = p2 x) \to +(\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to +pi_p n p1 g1 = pi_p n p2 g2. +intros. +unfold pi_p. +apply eq_iter_p_gen1; +assumption. +qed. + +theorem pi_p_false: +\forall g: nat \to nat.\forall n.pi_p n (\lambda x.false) g = S O. +intros. +unfold pi_p. +apply iter_p_gen_false. +qed. + +theorem pi_p_times: \forall n,k:nat.\forall p:nat \to bool. +\forall g: nat \to nat. +pi_p (k+n) p g += pi_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) * pi_p n p g. +intros. +unfold pi_p. +apply (iter_p_gen_plusA nat n k p g (S O) times) +[ apply sym_times. +| intros. + apply sym_eq. + apply times_n_SO +| apply associative_times +] +qed. + +theorem false_to_eq_pi_p: \forall n,m:nat.n \le m \to +\forall p:nat \to bool. +\forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to +p i = false) \to pi_p m p g = pi_p n p g. +intros. +unfold pi_p. +apply (false_to_eq_iter_p_gen); +assumption. +qed. + +theorem or_false_eq_SO_to_eq_pi_p: +\forall n,m:nat.\forall p:nat \to bool. +\forall g: nat \to nat. +n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = S O) +\to pi_p m p g = pi_p n p g. +intros. +unfold pi_p. +apply or_false_eq_baseA_to_eq_iter_p_gen + [intros.simplify.rewrite < plus_n_O.reflexivity + |assumption + |assumption + ] +qed. + +theorem pi_p2 : +\forall n,m:nat. +\forall p1,p2:nat \to bool. +\forall g: nat \to nat \to nat. +pi_p (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) + (\lambda x.g (div x m) (mod x m)) = +pi_p n p1 + (\lambda x.pi_p m p2 (g x)). +intros. +unfold pi_p. +apply (iter_p_gen2 n m p1 p2 nat g (S O) times) +[ apply sym_times +| apply associative_times +| intros. + apply sym_eq. + apply times_n_SO +] +qed. + +theorem pi_p2' : +\forall n,m:nat. +\forall p1:nat \to bool. +\forall p2:nat \to nat \to bool. +\forall g: nat \to nat \to nat. +pi_p (n*m) + (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m))) + (\lambda x.g (div x m) (mod x m)) = +pi_p n p1 + (\lambda x.pi_p m (p2 x) (g x)). +intros. +unfold pi_p. +apply (iter_p_gen2' n m p1 p2 nat g (S O) times) +[ apply sym_times +| apply associative_times +| intros. + apply sym_eq. + apply times_n_SO +] +qed. + +lemma pi_p_gi: \forall g: nat \to nat. +\forall n,i.\forall p:nat \to bool.i < n \to p i = true \to +pi_p n p g = g i * pi_p n (\lambda x. andb (p x) (notb (eqb x i))) g. +intros. +unfold pi_p. +apply (iter_p_gen_gi) +[ apply sym_times +| apply associative_times +| intros. + apply sym_eq. + apply times_n_SO +| assumption +| assumption +] +qed. + +theorem eq_pi_p_gh: +\forall g,h,h1: nat \to nat.\forall n,n1. +\forall p1,p2:nat \to bool. +(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to +(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to +(\forall i. i < n \to p1 i = true \to h i < n1) \to +(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to +(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to +(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to +pi_p n p1 (\lambda x.g(h x)) = pi_p n1 p2 g. +intros. +unfold pi_p. +apply (eq_iter_p_gen_gh nat (S O) times ? ? ? g h h1 n n1 p1 p2) +[ apply sym_times +| apply associative_times +| intros. + apply sym_eq. + apply times_n_SO +| assumption +| assumption +| assumption +| assumption +| assumption +| assumption +] +qed. + +theorem exp_sigma_p: \forall n,a,p. +pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))). +intros. +elim n + [reflexivity + |apply (bool_elim ? (p n1)) + [intro. + rewrite > true_to_pi_p_Sn + [rewrite > true_to_sigma_p_Sn + [simplify. + rewrite > H. + reflexivity. + |assumption + ] + |assumption + ] + |intro. + rewrite > false_to_pi_p_Sn + [rewrite > false_to_sigma_p_Sn + [simplify.assumption + |assumption + ] + |assumption + ] + ] + ] +qed. + +theorem exp_sigma_p1: \forall n,a,p,f. +pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)). +intros. +elim n + [reflexivity + |apply (bool_elim ? (p n1)) + [intro. + rewrite > true_to_pi_p_Sn + [rewrite > true_to_sigma_p_Sn + [simplify. + rewrite > H. + rewrite > exp_plus_times. + reflexivity. + |assumption + ] + |assumption + ] + |intro. + rewrite > false_to_pi_p_Sn + [rewrite > false_to_sigma_p_Sn + [simplify.assumption + |assumption + ] + |assumption + ] + ] + ] +qed. + +theorem times_pi_p: \forall n,p,f,g. +pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p g. +intros. +elim n + [simplify.reflexivity + |apply (bool_elim ? (p n1)) + [intro. + rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn + [rewrite > H.autobatch + |assumption + ] + |assumption + ] + |assumption + ] + |intro. + rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn;assumption + |assumption + ] + |assumption + ] + ] + ] +qed. + +theorem pi_p_SO: \forall n,p. +pi_p n p (\lambda i.S O) = S O. +intros.elim n + [reflexivity + |simplify.elim (p n1) + [simplify.rewrite < plus_n_O.assumption + |simplify.assumption + ] + ] +qed. + +theorem exp_pi_p: \forall n,m,p,f. +pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m. +intros. +elim m + [simplify.apply pi_p_SO + |simplify. + rewrite > times_pi_p. + rewrite < H. + reflexivity + ] +qed. + +theorem exp_times_pi_p: \forall n,m,k,p,f. +pi_p n p (\lambda x.exp k (m*(f x))) = +exp (pi_p n p (\lambda x.exp k (f x))) m. +intros. +apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m)))) + [apply eq_pi_p;intros + [reflexivity + |apply sym_eq.rewrite > sym_times. + apply exp_exp_times + ] + |apply exp_pi_p + ] +qed. + + +theorem pi_p_knm: +\forall g: nat \to nat. +\forall h2:nat \to nat \to nat. +\forall h11,h12:nat \to nat. +\forall k,n,m. +\forall p1,p21:nat \to bool. +\forall p22:nat \to nat \to bool. +(\forall x. x < k \to p1 x = true \to +p21 (h11 x) = true ∧ p22 (h11 x) (h12 x) = true +\land h2 (h11 x) (h12 x) = x +\land (h11 x) < n \land (h12 x) < m) \to +(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to +p1 (h2 i j) = true \land +h11 (h2 i j) = i \land h12 (h2 i j) = j +\land h2 i j < k) → +(* +Pi z < k | p1 z. g z = +Pi x < n | p21 x. Pi y < m | p22 x y.g (h2 x y). +*) +pi_p k p1 g = +pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))). +intros. +unfold pi_p.unfold pi_p. +apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12) + [intros.apply sym_eq.apply times_n_SO. + |assumption + |assumption + ] +qed. + +theorem pi_p_pi_p: +\forall g: nat \to nat \to nat. +\forall h11,h12,h21,h22: nat \to nat \to nat. +\forall n1,m1,n2,m2. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to +p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true +\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j +\land h11 i j < n1 \land h12 i j < m1) \to +(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to +p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true +\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j +\land (h21 i j) < n2 \land (h22 i j) < m2) \to +pi_p n1 p11 + (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) = +pi_p n2 p21 + (\lambda x:nat .pi_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))). +intros. +unfold pi_p.unfold pi_p. +apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22) + [intros.apply sym_eq.apply times_n_SO. + |assumption + |assumption + ] +qed. + +theorem pi_p_pi_p1: +\forall g: nat \to nat \to nat. +\forall n,m. +\forall p11,p21:nat \to bool. +\forall p12,p22:nat \to nat \to bool. +(\forall x,y. x < n \to y < m \to + (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to +pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) = +pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)). +intros. +unfold pi_p.unfold pi_p. +apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times) + [intros.apply sym_eq.apply times_n_SO. + |assumption + ] +qed. *) \ No newline at end of file diff --git a/matita/matita/lib/arithmetics/ord.ma b/matita/matita/lib/arithmetics/ord.ma new file mode 100644 index 000000000..452106f78 --- /dev/null +++ b/matita/matita/lib/arithmetics/ord.ma @@ -0,0 +1,415 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| + \ / This file is distributed under the terms of the + \ / GNU General Public License Version 2 + V_____________________________________________________________*) + +include "arithmetics/exp.ma". +include "basics/types.ma". +include "arithmetics/primes.ma". +include "arithmetics/gcd.ma". +(* +include "arithmetics/nth_prime.ma". +(* for some properties of divides *) +*) + +let rec p_ord_aux p n m ≝ + match n \mod m with + [ O ⇒ + match p with + [ O ⇒ 〈O,n〉 + | S p ⇒ let 〈q,r〉 ≝ p_ord_aux p (n / m) m in 〈S q,r〉] + | S a ⇒ 〈O,n〉]. + +(* p_ord n m = if m divides n q times, with remainder r *) +definition p_ord ≝ λn,m:nat.p_ord_aux n n m. + +lemma p_ord_aux_0: ∀n,m.p_ord_aux 0 n m = 〈0,n〉. +#n #m whd in match (p_ord_aux 0??); cases (n\mod m) normalize // +qed. + +lemma p_ord_aux_Strue: ∀n,m,p,q,r. + n\mod m = 0 → p_ord_aux p (n / m) m = 〈q,r〉 → + p_ord_aux (S p) n m = 〈S q,r〉. +#n #m #p #q #r whd in match (p_ord_aux (S p)??); #H >H +#Hord whd in ⊢(??%?); >Hord // +qed. + +lemma p_ord_aux_false: ∀p,n,m,a. + n\mod m = (S a) → p_ord_aux p n m = 〈0,n〉. +#p #n #m #a cases p whd in match (p_ord_aux ???); + [#H whd in match (p_ord_aux ???); >H // + |#p1 #H whd in match (p_ord_aux ???); >H // + ] +qed. + +(* the definition of p_ord_aux only makes sense for m>1. + In case m=1 we always end up with the pair 〈p,n〉 *) + +lemma p_ord_degenerate: ∀p,n. p_ord_aux p n 1 = 〈p,n〉. +#p elim p // #p1 #Hind #n +cut (mod n 1 = 0) [@divides_to_mod_O //] #Hmod +>(p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%); +>Hmod p_ord_aux_0 #Hqr destruct (Hqr) // + |#a #H #q #r #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) // + ] + |#p1 #Hind #n #m @(nat_case (n \mod m)) + [#Hmod #q #r #posm lapply (refl …(p_ord_aux p1 (n/m) m)); + cases (p_ord_aux p1 (n/m) m) in ⊢ (???%→?); #q1 #r1 #H1 + >(p_ord_aux_Strue … Hmod H1) #H destruct (H) whd in match (exp ??); + >(div_mod n m) >Hmod (Hind … H1) // + |#a #H #q #r #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) // + ] + ] +qed. + +(* questo va spostato in primes1.ma *) +theorem p_ord_exp: ∀n,m,i. O < m → n \mod m ≠ O → + ∀p. i ≤ p → p_ord_aux p (m \sup i * n) m = 〈i,n〉. +#n #m #i #posm #Hmod +cut (∃a.n\mod m = S a) + [@(nat_case (n\mod m)) [#H @False_ind /2/|#a #Hmod1 %{a} //]] * #mod1 #Hmod1 +elim i + [#p normalize #posp Hp #Habs @False_ind @(absurd … Habs) //] + #p1 #Hp1 #lep1 + cut (((m \sup (S i)*n) \mod m) = O) + [whd in match (exp ??); @divides_to_mod_O // %{(m^i*n)} //] #Hmod2 + @(p_ord_aux_Strue … Hmod2) <(Hind p1) [2: @le_S_S_to_le //] + @eq_f2 // whd in match (exp ??); >associative_times >(commutative_times m) + div_times // + ] +qed. + +theorem p_ord_aux_to_not_mod_O: ∀p,n,m,q,r. 1(p_ord_aux_Strue … Hmod H1) #H destruct (H) whd in match (exp ??); + @(Hind … lt1m … H1) + [@(pos_div … posn Hmod) @lt_to_le // + |@le_S_S_to_le @(transitive_le … len) @lt_times_to_lt_div + >(times_n_1 n) in ⊢ (?%?); @monotonic_lt_times_r // + ] + |#a #H #q #r #lt1m #posn #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) + >H @sym_not_eq // + ] + ] +qed. + +theorem p_ord_exp1: ∀p,n,q,r. O < p → p ∤ r → + n = p \sup q * r → p_ord n p = 〈q,r〉. +#p #n #q #r #posp #ndivpr #Hn >Hn -Hn -n @(p_ord_exp … posp) + [@(not_to_not … ndivpr) /2/ + |@(transitive_le ? (p \sup q)) + [cut (1(times_n_1 (S q1)) in ⊢ (?%?); @monotonic_lt_times_r // + |@le_times // + ] + |>(times_n_1 (p^q)) in ⊢ (?%?); @le_times // + lapply ndivpr -ndivpr cases r // #Habs @False_ind @(absurd ?? Habs) % // + ] + ] +qed. + +theorem p_ord_to_exp1: ∀p,n,q,r. 1

p_ord_degenerate #H destruct (H) + |#p2 lapply (refl …(p_ord_aux (S n1) (S n1) (S (S p2)))); + cases (p_ord_aux (S n1) (S n1) (S (S p2))) in ⊢ (???%→?); #qa #ra #H + lapply (p_ord_to_exp1 (S (S p2)) (S n1) … H) // + * #_ #H1 >H #H2 @False_ind destruct (H2) Ha >Hb -Ha -Hb (p_ord_times p a b (fst ?? (p_ord a p)) (snd ?? (p_ord a p)) + (fst ?? (p_ord b p)) (snd ? ? (p_ord b p)) primep posa posb) // +qed. + +theorem p_ord_p: ∀p:nat. 1 < p → p_ord p p = 〈1,1〉. +#p #ltp1 @p_ord_exp1 + [@lt_to_le // + |% #divp1 @(absurd … ltp1) @le_to_not_lt @divides_to_le // + |// + ] +qed. + +(* p_ord and divides *) +theorem divides_to_p_ord: ∀p,a,b,c,d,n,m:nat. O < n → O < m → prime p +→ divides n m → p_ord n p = 〈a,b〉 → + p_ord m p = 〈c,d〉 → divides b d ∧ a ≤ c. +#p #a #b #c #d #n #m #posn #posm #primep #divnm #ordn #ordm +cut (1commutative_gcd // + |#c0 #Hind @eq_gcd_times_1 + [@lt_O_exp @lt_to_le // + |@lt_to_le // + |@Hind + |>commutative_gcd @prime_to_gcd_1 // + ] + ] + |@(transitive_divides ? n) [%{(exp p a)} // |commutative_gcd @eq_gcd_times_1 + [@lt_O_exp @lt_to_le // + |@lt_to_le // + |>commutative_gcd // + |>commutative_gcd @prime_to_gcd_1 // + ] + ] + |@(transitive_divides ? n) // %{b} // + ] + ] + ] +qed. + +(* p_ord and primes *) +theorem not_divides_to_p_ord_O: ∀n,i. + (nth_prime i) ∤ n → p_ord n (nth_prime i) = 〈O,n〉. +#n #i #H @p_ord_exp1 // +qed. + +theorem p_ord_O_to_not_divides: ∀n,i,r. O < n → + p_ord n (nth_prime i) = 〈O,r〉 + → (nth_prime i) ∤ n. +#n #i #r #posn #Hord +lapply (p_ord_to_exp1 … Hord) // * #H +normalize eqr in H2; // + ] +qed. + +definition ord :nat → nat → nat ≝ + λn,p. fst ?? (p_ord n p). + +definition ord_rem :nat → nat → nat ≝ + λn,p. snd ?? (p_ord n p). + +lemma ord_eq: ∀n,p. ord n p = fst ?? (p_ord n p). // +qed. + +lemma ord_rem_eq: ∀n,p. ord_rem n p = snd ?? (p_ord n p). // +qed. + +theorem divides_to_ord: ∀p,n,m:nat. + O < n → O < m → prime p → divides n m + → divides (ord_rem n p) (ord_rem m p) ∧ (ord n p) ≤ (ord m p). +#p #n #m #H #H1 #H2 #H3 +@(divides_to_p_ord p ? ? ? ? n m H H1 H2 H3) + [@eq_pair_fst_snd|@eq_pair_fst_snd] +qed. + +theorem divides_to_divides_ord_rem: ∀p,n,m:nat. +O < n → O < m → prime p → divides n m → + divides (ord_rem n p) (ord_rem m p). +#p #n #m #H #H1 #H2 #H3 cases (divides_to_ord p n m H H1 H2 H3) // +qed. + +theorem divides_to_le_ord: ∀p,n,m:nat. +O < n → O < m → prime p → divides n m → + ord n p ≤ ord m p. +#p #n #m #H #H1 #H2 #H3 cases (divides_to_ord p n m H H1 H2 H3) // +qed. + +theorem exp_ord: \forall p,n. 1 < p → O < n → + n = p \sup (ord n p) * (ord_rem n p). +#p #n #H #H1 +cases (p_ord_to_exp1 p n (ord n p) (ord_rem n p) H H1 ?) + [// |@eq_pair_fst_snd] +qed. + +theorem divides_ord_rem: ∀p,n. 1 < p → O < n + → divides (ord_rem n p) n. +#p #n #H #H1 %{(p \sup (ord n p))} >commutative_times @exp_ord // +qed. + +theorem lt_O_ord_rem: ∀p,n. 1 < p → O < n → O < ord_rem n p. +#p #n #H #H1 +cases (le_to_or_lt_eq … (le_O_n (ord_rem n p))) // +#remO lapply(divides_ord_rem ?? H H1) ord_eq >(p_ord_exp1 p (exp p m) m (S O)) // + [@(not_to_not … (lt_to_not_le … H)) @divides_to_le // + |@lt_to_le // + ] +qed. + +theorem not_divides_to_ord_O: +∀p,m. prime p → p ∤ m → ord m p = O. +#p #m #H #H1 >ord_eq >(p_ord_exp1 p m O m) // @prime_to_lt_O // +qed. + +theorem ord_O_to_not_divides: ∀p,m. O < m → prime p → + ord m p = O → p ∤ m. +#p #m #H #H1 #H2 +lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p) … H … (eq_pair_fst_snd …)) + [@prime_to_lt_SO // + |* #H3 >H2 >commutative_times (exp_ord p m) in ⊢ (??%); + [@(transitive_divides ? (exp p (ord m p))) + [lapply H2 cases (ord m p) + [* #H3 @False_ind @H3 // + |#a #_ normalize % // + ] + |%{(ord_rem m p)} // + ] + |// + |@prime_to_lt_SO // + ] +qed. + +theorem not_divides_ord_rem: ∀m,p.O< m → 1 < p → + p ∤ (ord_rem m p). +#m #p #H #H1 +lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p) ?? (eq_pair_fst_snd …)) // * +#H2 #H3 @H2 +qed. + +theorem ord_ord_rem: ∀p,q,m. O < m → prime p → prime q →q < p → + ord (ord_rem m p) q = ord m q. +#p #q #m #H #H1 #H2 #H3 >(exp_ord p m) in ⊢ (???(?%?)); + [>(ord_times … H2) + [>not_divides_to_ord_O in ⊢ (???(?%?)); // + @(not_to_not … (lt_to_not_eq ? ? H3)) + @(divides_exp_to_eq ? ? ? H2 H1) + |@lt_O_ord_rem // @prime_to_lt_SO // + |@lt_O_exp @prime_to_lt_O // + ] + |// + |@prime_to_lt_SO // + ] +qed. + +theorem lt_ord_rem: ∀n,m. prime n → O < m → + divides n m → ord_rem m n < m. +#n #m #H #H1 #H2 +cases (le_to_or_lt_eq (ord_rem m n) m ?) + [// + |#Hm @False_ind eq_p_ord_inv @div_plus_times +qed. + +theorem mod_p_ord_inv: +∀p,m,x. ord x p < m → p_ord_inv p m x \mod m = ord x p. +#p #m #x >eq_p_ord_inv @mod_plus_times +qed. -- 2.39.2