definition prim: nat \to nat \def
\lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
+(* This is chebishev psi funcion *)
definition A: nat \to nat \def
\lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
]
qed.
+(* an equivalent formulation for psi *)
definition A': nat \to nat \def
\lambda n. pi_p (S n) primeb
(\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
]
]
qed.
-
+
+(* factorization of n into primes *)
theorem pi_p_primeb_divides_b: \forall n. O < n \to
n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
intros.
]
qed.
+(* the factorial function *)
theorem eq_fact_pi_p:\forall n. fact n =
pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
intro.elim n
]
qed.
+(* still another characterization of the factorial *)
theorem fact_pi_p: \forall n. fact n =
pi_p (S n) primeb
(\lambda p.(pi_p (log p n)
assumption
|cut (i\sup(S i1)≤(S(S O))*n)
[apply div_mod_spec_intro
- [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
- apply lt_plus_to_lt_minus
+ [apply lt_plus_to_lt_minus
[assumption
|simplify in ⊢ (? % ?).
rewrite < plus_n_O.