(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/chebyshev_teta".
-
include "nat/binomial.ma".
include "nat/pi_p.ma".
]
qed.
-theorem lt_O_to_le_teta_M_teta: \forall m. O < m\to
+theorem lt_O_to_le_teta_exp_teta: \forall m. O < m\to
teta (S(2*m)) < exp 2 (2*m)*teta (S m).
intros.
apply (le_to_lt_to_lt ? (M m*teta (S m)))
]
qed.
+theorem teta_pred: \forall n. S O < n \to teta (2*n) = teta (pred (2*n)).
+intros.unfold teta.
+rewrite > false_to_pi_p_Sn
+ [rewrite < S_pred
+ [reflexivity
+ |rewrite > (times_n_O 2) in ⊢ (? % ?).
+ apply lt_times_r.
+ apply lt_to_le.assumption
+ ]
+ |apply not_prime_to_primeb_false.
+ intro.
+ elim H1.
+ apply (lt_to_not_eq ? ? H).
+ apply (injective_times_r 1).
+ rewrite < times_n_SO.
+ apply H3
+ [apply (witness ? ? n).reflexivity
+ |apply le_n
+ ]
+ ]
+qed.
+theorem le_teta: \forall m.teta m \le exp 2 (2*m).
+intro.apply (nat_elim1 m).intros.
+elim (or_eq_eq_S m1).
+elim H1
+ [rewrite > H2.
+ generalize in match H2.
+ cases a
+ [intro.apply le_n
+ |cases n;intros
+ [apply leb_true_to_le.reflexivity
+ |rewrite > teta_pred
+ [rewrite > times_SSO.
+ change in ⊢ (? (? %) ?) with (S (2*S n1)).
+ apply (trans_le ? (exp 2 (2*(S n1))*teta (S (S n1))))
+ [apply lt_to_le.
+ apply lt_O_to_le_teta_exp_teta.
+ apply lt_O_S
+ |rewrite < times_SSO.
+ change in ⊢ (? ? (? ? %)) with ((2*S (S n1))+((2*S (S n1)) + O)).
+ rewrite < plus_n_O.
+ rewrite > exp_plus_times.
+ apply le_times
+ [apply le_exp
+ [apply lt_O_S
+ |apply le_times_r.
+ apply le_n_Sn
+ ]
+ |apply H.
+ rewrite > H3.
+ apply lt_m_nm
+ [apply lt_O_S
+ |apply le_n
+ ]
+ ]
+ ]
+ |apply le_S_S.apply lt_O_S
+ ]
+ ]
+ ]
+ |rewrite > H2.
+ generalize in match H2.
+ cases a;intro
+ [apply leb_true_to_le.reflexivity
+ |apply (trans_le ? (exp 2 (2*(S n))*teta (S (S n))))
+ [apply lt_to_le.
+ apply lt_O_to_le_teta_exp_teta.
+ apply lt_O_S
+ |change in ⊢ (? ? (? ? %)) with (S (2*S n) + (S (2*S n) +O)).
+ rewrite < plus_n_O.
+ rewrite < plus_n_Sm.
+ rewrite < sym_plus.
+ rewrite > plus_n_Sm.
+ rewrite > exp_plus_times.
+ apply le_times_r.
+ rewrite < times_SSO.
+ apply H.
+ rewrite > H3.
+ apply le_S_S.
+ apply lt_m_nm
+ [apply lt_O_S
+ |apply le_n
+ ]
+ ]
+ ]
+ ]
+qed.
+
+(*
+alias id "sqrt" = "cic:/matita/nat/sqrt/sqrt.con".
+alias id "not" = "cic:/matita/logic/connectives/Not.con".
+theorem absurd_bound: \forall n. exp 2 7 \le n \to
+(\forall p. n < p \to p < 2*n \to not (prime p)) \to
+bc (2*n) n < exp (2*n) (div (sqrt (2*n)) 2 - 1)*exp 4 (div (2*n) 3).
+intros.
+cut (O < n)
+ [cut (sqrt (2*n) < div (2*n) 3)
+ [
+ |
+*)