(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/moebius".
-
include "nat/factorization.ma".
include "Z/sigma_p.ma".
qed.
*)
-theorem not_divides_to_p_ord_O: \forall n,i.
-Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
-pair nat nat O n.
-intros.
-apply p_ord_exp1
- [apply lt_O_nth_prime_n
- |assumption
- |autobatch
- ]
-qed.
-
-theorem p_ord_O_to_not_divides: \forall n,i,r.
-O < n \to
-p_ord n (nth_prime i) = pair nat nat O r
-\to Not (divides (nth_prime i) n).
-intros.
-lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
- [apply lt_SO_nth_prime_n
- |assumption
- |elim Hletin.
- simplify in H3.
- rewrite > H3.
- rewrite < plus_n_O.
- assumption
- ]
-qed.
-
theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
(\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
\to moebius_aux p n = moebius_aux p1 n.
]
qed.
-theorem p_ord_to_not_eq_O : \forall n,p,q,r.
- (S O) < n \to
- p_ord n (nth_prime p) = pair nat nat q r \to
- Not (r=O).
-intros.
-unfold.intro.
-cut (O < n)
- [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
- [apply lt_SO_nth_prime_n.
- |assumption
- |elim Hletin.
- apply (lt_to_not_eq ? ? Hcut).
- rewrite > H4.
- rewrite > H2.
- apply times_n_O
- ]
- |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
- ]
-qed.
-
-theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
- (S O) < n \to
- p = max_prime_factor n \to
- p_ord n (nth_prime p) \neq pair nat nat O r.
-intros.unfold Not.intro.
-apply (p_ord_O_to_not_divides ? ? ? ? H2)
- [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
- |rewrite > H1.
- apply divides_max_prime_factor_n.
- assumption
- ]
-qed.
-
theorem p_ord_SO_SO_to_moebius : \forall n,p.
(S O) < n \to
p = max_prime_factor n \to
reflexivity.
qed.
-lemma eq_p_max: \forall n,p,r:nat. O < n \to
-O < r \to
-r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
-p = max_prime_factor (r*(nth_prime p)\sup n).
-intros.
-apply sym_eq.
-unfold max_prime_factor.
-apply max_spec_to_max.
-split
- [split
- [rewrite > times_n_SO in \vdash (? % ?).
- rewrite > sym_times.
- apply le_times
- [assumption
- |apply lt_to_le.
- apply (lt_to_le_to_lt ? (nth_prime p))
- [apply lt_n_nth_prime_n
- |rewrite > exp_n_SO in \vdash (? % ?).
- apply le_exp
- [apply lt_O_nth_prime_n
- |assumption
- ]
- ]
- ]
- |apply eq_to_eqb_true.
- apply divides_to_mod_O
- [apply lt_O_nth_prime_n
- |apply (lt_O_n_elim ? H).
- intro.
- apply (witness ? ? (r*(nth_prime p \sup m))).
- rewrite < assoc_times.
- rewrite < sym_times in \vdash (? ? ? (? % ?)).
- rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
- rewrite > assoc_times.
- rewrite < exp_plus_times.
- reflexivity
- ]
- ]
- |intros.
- apply not_eq_to_eqb_false.
- unfold Not.intro.
- lapply (mod_O_to_divides ? ? ? H5)
- [apply lt_O_nth_prime_n
- |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
- [elim H2
- [rewrite > H6 in Hletin.
- simplify in Hletin.
- rewrite < plus_n_O in Hletin.
- apply Hcut.assumption
- |elim (divides_times_to_divides ? ? ? ? Hletin)
- [apply (lt_to_not_le ? ? H3).
- apply lt_to_le.
- apply (le_to_lt_to_lt ? ? ? ? H6).
- apply f_m_to_le_max
- [apply (trans_le ? (nth_prime i))
- [apply lt_to_le.
- apply lt_n_nth_prime_n
- |apply divides_to_le[assumption|assumption]
- ]
- |apply eq_to_eqb_true.
- apply divides_to_mod_O
- [apply lt_O_nth_prime_n|assumption]
- ]
- |apply prime_nth_prime
- |apply Hcut.assumption
- ]
- ]
- |unfold Not.intro.
- apply (lt_to_not_eq ? ? H3).
- apply sym_eq.
- elim (prime_nth_prime p).
- apply injective_nth_prime.
- apply H8
- [apply (divides_exp_to_divides ? ? ? ? H6).
- apply prime_nth_prime.
- |apply lt_SO_nth_prime_n
- ]
- ]
- ]
- ]
-qed.
-
-lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
-O < n \to n=S O \lor max_prime_factor n < p \to
-(nth_prime p \ndivides n).
-intros.unfold Not.intro.
-elim H1
- [rewrite > H3 in H2.
- apply (le_to_not_lt (nth_prime p) (S O))
- [apply divides_to_le[apply le_n|assumption]
- |apply lt_SO_nth_prime_n
- ]
- |apply (not_le_Sn_n p).
- change with (p < p).
- apply (le_to_lt_to_lt ? ? ? ? H3).
- unfold max_prime_factor.
- apply f_m_to_le_max
- [apply (trans_le ? (nth_prime p))
- [apply lt_to_le.
- apply lt_n_nth_prime_n
- |apply divides_to_le;assumption
- ]
- |apply eq_to_eqb_true.
- apply divides_to_mod_O
- [apply lt_O_nth_prime_n|assumption]
- ]
- ]
-qed.
-
theorem moebius_exp: \forall p,q,r:nat. O < r \to
r = (S O) \lor (max_prime_factor r) < p \to
(* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)