1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "nat/sqrt.ma".
16 include "nat/chebyshev_teta.ma".
17 include "nat/chebyshev.ma".
18 include "list/list.ma".
21 let rec list_divides l n \def
24 | cons (m:nat) (tl:list nat) ⇒ orb (divides_b m n) (list_divides tl n) ].
26 definition lprim : nat \to list nat \def
27 \lambda n.let rec aux m acc \def
30 | S m1 => match (list_divides acc (n-m1)) with
32 | false => aux m1 (n-m1::acc)]]
35 let rec filter A l p on l \def
38 | cons (a:A) (tl:list A) => match (p a) with
39 [ true => a::(filter A tl p)
40 | false => filter A tl p ]].
42 let rec length A (l:list A) on l \def
45 | cons (a:A) (tl:list A) => S (length A tl) ].
47 definition list_n : nat \to list nat \def
48 \lambda n.let rec aux n k \def
51 | S n1 => k::aux n1 (S k) ]
54 let rec sieve_aux l1 l2 t on t \def
57 | S t1 => match l2 with
59 | cons n tl => sieve_aux (n::l1) (filter nat tl (\lambda x.notb (divides_b n x))) t1]].
61 definition sieve : nat \to list nat \def
62 \lambda m.sieve_aux [] (list_n m) m.
64 definition ord_list \def
66 \forall a,b,l1,l2.l = l1@(a::b::l2) \to b \leq a.
68 definition in_list \def
69 \lambda A.\lambda a:A.\lambda l:list A.
70 \exists l1,l2.l = l1@(a::l2).
72 lemma in_list_filter_to_p_true : \forall l,x,p.in_list nat x (filter nat l p) \to p x = true.
73 intros;elim H;elim H1;clear H H1;generalize in match H2;generalize in match a;elim l 0
74 [simplify;intro;elim l1
75 [simplify in H;destruct H
76 |simplify in H1;destruct H1]
77 |intros;simplify in H1;apply (bool_elim ? (p t));intro;
78 rewrite > H3 in H1;simplify in H1
79 [generalize in match H1;elim l2
80 [simplify in H4;destruct H4;assumption
81 |simplify in H5;destruct H5;apply (H l3);assumption]
82 |apply (H l2);assumption]]
85 lemma in_list_cons : \forall l,x,y.in_list nat x l \to in_list nat x (y::l).
86 intros;unfold in H;unfold;elim H;elim H1;apply (ex_intro ? ? (y::a));
87 apply (ex_intro ? ? a1);simplify;rewrite < H2;reflexivity.
90 lemma in_list_tail : \forall l,x,y.in_list nat x (y::l) \to x \neq y \to in_list nat x l.
91 intros;elim H;elim H2;generalize in match H3;elim a
92 [simplify in H4;destruct H4;elim H1;reflexivity
93 |simplify in H5;destruct H5;apply (ex_intro ? ? l1);apply (ex_intro ? ? a1);
97 lemma in_list_filter : \forall l,p,x.in_list nat x (filter nat l p) \to in_list nat x l.
98 intros;elim H;elim H1;generalize in match H2;generalize in match a;elim l 0
99 [simplify;intro;elim l1
100 [simplify in H3;destruct H3
101 |simplify in H4;destruct H4]
102 |intros;simplify in H4;apply (bool_elim ? (p t));intro
103 [rewrite > H5 in H4;simplify in H4;generalize in match H4;elim l2
104 [simplify in H6;destruct H6;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
106 |simplify in H7;destruct H7;apply in_list_cons;apply (H3 ? Hcut1);]
107 |rewrite > H5 in H4;simplify in H4;apply in_list_cons;apply (H3 ? H4);]]
110 lemma in_list_filter_r : \forall l,p,x.in_list nat x l \to p x = true \to in_list nat x (filter nat l p).
111 intros;elim H;elim H2;rewrite > H3;elim a
112 [simplify;rewrite > H1;simplify;apply (ex_intro ? ? []);apply (ex_intro ? ? (filter nat a1 p));
114 |simplify;elim (p t);simplify
115 [apply in_list_cons;assumption
119 axiom sieve_monotonic : \forall n.sieve (S n) = sieve n \lor sieve (S n) = (S n)::sieve n.
121 axiom daemon : False.
123 axiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
124 x = a \lor in_list A x l.
126 lemma divides_to_prime_divides : \forall n,m.1 < m \to m < n \to m \divides n \to
127 \exists p.p \leq m \land prime p \land p \divides n.
128 intros;apply (ex_intro ? ? (nth_prime (max_prime_factor m)));split
131 [apply lt_to_le;assumption
132 |apply divides_max_prime_factor_n;assumption]
133 |apply prime_nth_prime;]
134 |apply (transitive_divides ? ? ? ? H2);apply divides_max_prime_factor_n;
138 lemma in_list_head : \forall x,l.in_list nat x (x::l).
139 intros;apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity;
142 lemma le_length_filter : \forall A,l,p.length A (filter A l p) \leq length A l.
145 |simplify;apply (bool_elim ? (p t));intro
146 [simplify;apply le_S_S;assumption
147 |simplify;apply le_S;assumption]]
150 lemma sieve_prime : \forall t,k,l2,l1.
151 (\forall p.(in_list ? p l1 \to prime p \land p \leq k \land \forall x.in_list ? x l2 \to p < x) \land
152 (prime p \to p \leq k \to (\forall x.in_list ? x l2 \to p < x) \to in_list ? p l1)) \to
153 (\forall x.(in_list ? x l2 \to x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \land
154 ((x \leq k \land \forall p.in_list ? p l1 \to \lnot p \divides x) \to
156 length ? l2 \leq t \to
157 \forall p.(in_list ? p (sieve_aux l1 l2 t) \to prime p \land p \leq k) \land
158 (prime p \to p \leq k \to in_list ? p (sieve_aux l1 l2 t)).
160 [intros;cut (l2 = [])
161 [|generalize in match H2;elim l2
163 |simplify in H4;elim (not_le_Sn_O ? H4)]]
164 simplify;split;intros;
165 [elim (H p);elim (H4 H3);assumption
166 |elim (H p);apply (H6 H3 H4);rewrite > Hcut;intros;unfold in H7;
167 elim H7;elim H8;clear H7 H8;generalize in match H9;elim a
168 [simplify in H7;destruct H7
169 |simplify in H8;destruct H8]]
171 [simplify;split;intros
172 [elim (H1 p);elim (H5 H4);assumption
173 |elim (H1 p);apply (H7 H4 H5);intros;unfold in H8;
174 elim H8;elim H9;clear H8 H9;generalize in match H10;elim a
175 [simplify in H8;destruct H8
176 |simplify in H9;destruct H9]]
177 |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b t1 x))) (t1::l1) ? ? ? p)
180 |apply H6;assumption]
182 [elim (in_list_cons_case ? ? ? ? H5);
186 [elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *)
187 |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H7))
188 [elim (divides_to_prime_divides ? ? H8 H9 H7);elim H10;
189 elim H11;clear H10 H11;elim (H3 t1);elim H10
190 [clear H10 H11;elim (H16 ? ? H12);elim (H2 a);clear H10;
193 |apply (trans_le ? ? ? ? H15);
194 apply (trans_le ? ? ? H13);
195 apply lt_to_le;assumption
197 (* sfruttare il fatto che a < t1
198 e t1 è il minimo di t1::l *)
200 |unfold;apply (ex_intro ? ? []);
201 apply (ex_intro ? ? l);
203 |elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *)
205 |elim (H3 t1);elim H7
207 |apply (ex_intro ? ? []);apply (ex_intro ? ? l);reflexivity]]
208 |intros;elim (le_to_or_lt_eq t1 x)
210 |rewrite > H8 in H7;lapply (in_list_filter_to_p_true ? ? ? H7);
211 lapply (divides_n_n x);
212 rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin
213 [simplify in Hletin;destruct Hletin
214 |elim daemon (* aggiungere hp: ogni elemento di l2 è >= 2 *)]
215 |(* sfruttare il fatto che t1 è il minimo di t1::l *)
217 |elim (H2 p1);elim (H7 H6);split
219 |intros;apply H10;apply in_list_cons;apply (in_list_filter ? ? ? H11);]]
220 |elim (decidable_eq_nat p1 t1)
221 [rewrite > H8;apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
223 |apply in_list_cons;elim (H2 p1);apply (H10 H5 H6);intros;
224 apply (trans_le ? t1)
225 [elim (decidable_lt p1 t1)
227 |lapply (not_lt_to_le ? ? H12);
228 lapply (decidable_divides t1 p1)
230 [elim H5;lapply (H15 ? H13)
231 [elim H8;symmetry;assumption
232 |(* per il solito discorso l2 >= 2 *)
234 |elim (Not_lt_n_n p1);apply H7;apply in_list_filter_r
235 [elim (H3 p1);apply (in_list_tail ? ? t1)
238 |intros;elim H5;intro;lapply (H18 ? H19)
239 [rewrite > Hletin2 in H16;elim (H9 H16);
241 [elim (lt_to_not_le ? ? Hletin3 Hletin)
242 |apply (ex_intro ? ? []);apply (ex_intro ? ? l);
244 |apply prime_to_lt_SO;elim (H2 p2);elim (H20 H16);
245 elim H22;assumption]]
246 |unfold;intro;apply H13;rewrite > H16;apply divides_n_n;]
247 |rewrite > (not_divides_to_divides_b_false ? ? ? H13);
249 |elim daemon (* usare il solito >= 2 *)]]]
250 |elim daemon (* come sopra *)]]
251 |elim daemon (* t1::l è ordinata *)]]]
252 |intro;elim (H3 x);split;intros;
256 |apply in_list_cons;apply (in_list_filter ? ? ? H7)]
257 |intros;elim (in_list_cons_case ? ? ? ? H8)
258 [rewrite > H9;intro;lapply (in_list_filter_to_p_true ? ? ? H7);
259 rewrite > (divides_to_divides_b_true ? ? ? H10) in Hletin
260 [simplify in Hletin;destruct Hletin
261 |elim daemon (* dal fatto che ogni elemento di t1::l è >= 2 *)]
263 [apply H11;assumption
264 |apply in_list_cons;apply (in_list_filter ? ? ? H7)]]]
265 |elim H7;elim (in_list_cons_case ? ? ? ? (H6 ?))
267 [rewrite > H10;unfold;
268 apply (ex_intro ? ? []);apply (ex_intro ? ? l1);
273 |intros;apply H9;apply in_list_cons;assumption]
274 |apply in_list_filter_r;
277 [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin);
281 |apply in_list_head]]]]
282 |apply (trans_le ? ? ? (le_length_filter ? ? ?));apply le_S_S_to_le;
286 lemma sieve_soundness : \forall n.\forall p.
287 in_list ? p (sieve n) \to
288 p \leq n \land prime p.
289 intros;unfold sieve in H;lapply (sieve_prime n (S n) (list_n n) [] ? ? ? p)
290 [intros;split;intros;
291 [elim daemon (* H1 is absurd *)
292 |elim daemon (* da sistemare, bisognerebbe raggiungere l'assurdo sapendo che p1 è primo e < 2 *)]
295 [elim daemon (* vero, dalla H1 *)
296 |intros;elim daemon (* H2 è assurda *)]
298 (* vera supponendo x >= 2, il che in effetti è doveroso sistemare nel teoremone di prima *)
300 |elim daemon (* sempre vero, da dimostrare *)
301 |elim Hletin;elim (H1 H);split
302 [elim daemon (* si può ottenere da H *)
306 definition bertrand \def \lambda n.
307 \exists p.n < p \land p \le 2*n \land (prime p).
309 definition not_bertrand \def \lambda n.
310 \forall p.n < p \to p \le 2*n \to \not (prime p).
312 lemma not_not_bertrand_to_bertrand1: \forall n.
313 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
314 (\forall p.x < p \to p \le 2*n \to \not (prime p))
315 \to \exists p.n < p \land p \le x \land (prime p).
317 [apply False_ind.apply H.assumption
318 |apply (bool_elim ? (primeb (S n1)));intro
319 [apply (ex_intro ? ? (S n1)).
322 [apply le_S_S.assumption
325 |apply primeb_true_to_prime.assumption
330 apply (ex_intro ? ? a).
334 |apply le_S.assumption
338 |apply lt_to_le.assumption
339 |elim (le_to_or_lt_eq ? ? H7)
342 apply primeb_false_to_not_prime.
350 theorem not_not_bertrand_to_bertrand: \forall n.
351 \lnot (not_bertrand n) \to bertrand n.
352 unfold bertrand.intros.
353 apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
355 |apply le_times_n.apply le_n_Sn
357 |intros.apply False_ind.
358 apply (lt_to_not_le ? ? H1 H2)
363 theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to
364 divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
369 apply (le_to_not_lt p 1)
376 |apply (bool_elim ? (b n1));intro
377 [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2.
378 elim (divides_times_to_divides ? ? ? H1 H2)
379 [apply (ex_intro ? ? n1).
386 apply (ex_intro ? ? a).
388 [apply lt_to_le.apply le_S_S.assumption
392 |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2.
395 apply (ex_intro ? ? a).
397 [apply lt_to_le.apply le_S_S.assumption
404 theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to
405 p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O.
408 elim (divides_pi_p_to_divides ? ? ? ? H H1).
411 elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5.
416 [rewrite > Hcut.apply le_S_S_to_le.assumption
417 |apply (ex_intro ? ? a1).
420 change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)).
424 [apply divides_to_le[apply lt_O_S|assumption]
425 |apply lt_to_not_le.elim H.assumption
428 |apply (divides_exp_to_eq ? ? ? H ? H7).
429 apply primeb_true_to_prime.
435 definition k \def \lambda n,p.
436 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
438 theorem le_k: \forall n,p. k n p \le log p n.
439 intros.unfold k.elim (log p n)
441 |rewrite > true_to_sigma_p_Sn
442 [rewrite > plus_n_SO.
443 rewrite > sym_plus in ⊢ (? ? %).
456 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
458 theorem eq_B_B1: \forall n. B n = B1 n.
459 intros.unfold B.unfold B1.
467 definition B_split1 \def \lambda n.
468 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
470 definition B_split2 \def \lambda n.
471 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
473 theorem eq_B1_times_B_split1_B_split2: \forall n.
474 B1 n = B_split1 n * B_split2 n.
475 intro.unfold B1.unfold B_split1.unfold B_split2.
476 rewrite < times_pi_p.
479 |intros.apply (bool_elim ? (leb (k n x) 1));intro
480 [rewrite > (lt_to_leb_false 2 (k n x))
481 [simplify.rewrite < plus_n_O.
482 rewrite < times_n_SO.reflexivity
483 |apply le_S_S.apply leb_true_to_le.assumption
485 |rewrite > (le_to_leb_true 2 (k n x))
486 [simplify.rewrite < plus_n_O.
487 rewrite < plus_n_O.reflexivity
488 |apply not_le_to_lt.apply leb_false_to_not_le.assumption
494 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
498 intro.apply (lt_to_not_le ? ? H1).
499 apply le_times_to_le_div;assumption
500 |apply (ltn_to_ltO ? ? H1)
504 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
506 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
507 [apply div_mod_spec_div_mod.
508 apply (ltn_to_ltO ? ? H)
509 |apply div_mod_spec_intro
516 (* the value of n could be smaller *)
517 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
521 |rewrite > true_to_sigma_p_Sn
526 cut (2*n/p = 2) as H4
527 [rewrite > H4.reflexivity
528 |apply lt_to_le_times_to_lt_S_to_div
529 [apply (ltn_to_ltO ? ? H2)
530 |rewrite < sym_times.
533 |rewrite > sym_times in ⊢ (? ? %).
534 apply lt_div_to_times
540 |cut (2*n/(p)\sup(S (S n2)) = O) as H4
541 [rewrite > H4.reflexivity
543 apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
544 [apply (le_times_to_le (exp 3 2))
545 [apply leb_true_to_le.reflexivity
546 |rewrite > sym_times in ⊢ (? ? %).
548 apply (trans_le ? (exp n 2))
549 [rewrite < assoc_times.
550 rewrite > exp_SSO in ⊢ (? ? %).
553 |apply monotonic_exp1.
554 apply (le_plus_to_le 3).
555 change in ⊢ (? ? %) with ((S(2*n/3))*3).
556 apply (trans_le ? (2*n))
557 [simplify in ⊢ (? ? %).
560 apply (trans_le ? 18 ? ? H).
561 apply leb_true_to_le.reflexivity
568 |apply (lt_to_le_to_lt ? (exp p 2))
574 [apply (ltn_to_ltO ? ? H2)
575 |apply le_S_S.apply le_S_S.apply le_O_n
586 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
587 B_split1 (2*n) \le teta (2 * n / 3).
588 intros.unfold B_split1.unfold teta.
589 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
590 [apply le_pi_p.intros.
592 [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
593 |apply (bool_elim ? (leb (k (2*n) i) 1));intro
594 [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
595 [lapply (le_S_S_to_le ? ? H5) as H6.
596 apply (le_n_O_elim ? H6).
599 |rewrite > (eq_to_eqb_true ? ? H5).
600 rewrite > H5.apply le_n
605 |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
606 [apply (eq_ind ? ? ? (le_n ?)).
607 apply or_false_eq_SO_to_eq_pi_p
609 apply le_times_to_le_div2
611 |rewrite > sym_times in ⊢ (? ? %).
613 apply leb_true_to_le.reflexivity
616 unfold not_bertrand in H1.
617 elim (decidable_le (S n) i)
619 apply not_prime_to_primeb_false.
622 |apply le_S_S_to_le.assumption
629 apply not_le_to_lt.assumption
634 |apply le_pi_p.intros.
635 elim (eqb (k (2*n) i) 1)
636 [rewrite < exp_n_SO.apply le_n
637 |simplify.apply prime_to_lt_O.
638 apply primeb_true_to_prime.
645 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
646 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
647 intros.unfold B_split2.
649 [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
650 (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
651 [apply (eq_ind ? ? ? (le_n ?)).
652 apply or_false_eq_SO_to_eq_pi_p
656 apply (bool_elim ? (leb 2 (k (2*n) i)));intro
658 apply (lt_to_not_le ? ? H1).unfold sqrt.
660 [apply le_S_S_to_le.assumption
661 |apply le_to_leb_true.
663 apply not_lt_to_le.intro.
664 apply (le_to_not_lt 2 (log i (2*n)))
665 [apply (trans_le ? (k (2*n) i))
666 [apply leb_true_to_le.assumption
669 |apply le_S_S.unfold log.apply f_false_to_le_max
670 [apply (ex_intro ? ? O).split
672 |apply le_to_leb_true.simplify.
678 |intros.apply lt_to_leb_false.
679 apply (lt_to_le_to_lt ? (exp i 2))
682 [apply (ltn_to_ltO ? ? H1)
692 |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
693 [apply le_pi_p.intros.
694 apply (trans_le ? (exp i (log i (2*n))))
696 [apply prime_to_lt_O.
697 apply primeb_true_to_prime.
699 |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
700 [simplify in ⊢ (? (? % ?) ?).
702 rewrite < times_n_SO.
708 rewrite > (times_n_O O) in ⊢ (? % ?).
714 |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
716 apply (eq_ind ? ? ? (le_n ?)).
719 [rewrite > (times_n_O O) in ⊢ (? % ?).
727 [apply (trans_le ? (2*(exp 2 7)))
728 [apply leb_true_to_le.reflexivity
729 |apply le_times_r.assumption
731 |apply le_to_leb_true.
732 apply (trans_le ? (2*(exp 2 7)))
733 [apply leb_true_to_le.reflexivity
734 |apply le_times_r.assumption
741 |apply (lt_to_le_to_lt ? ? ? ? H).
742 apply leb_true_to_le.reflexivity
746 theorem not_bertrand_to_le_B:
747 \forall n.exp 2 7 \le n \to not_bertrand n \to
748 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
751 rewrite > eq_B1_times_B_split1_B_split2.
753 [apply (trans_le ? (teta ((2*n)/3)))
754 [apply le_B_split1_teta
755 [apply (trans_le ? ? ? ? H).
756 apply leb_true_to_le.reflexivity
761 |apply le_B_split2_exp.
767 theorem not_bertrand_to_le1:
768 \forall n.18 \le n \to not_bertrand n \to
769 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
772 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
774 rewrite > (div_mod n m) in ⊢ (? ? %)
780 theorem not_bertrand_to_le1:
781 \forall n.exp 2 7 \le n \to not_bertrand n \to
782 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
784 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
785 [apply lt_O_exp.apply lt_O_S
786 |rewrite < exp_plus_times.
787 apply (trans_le ? (exp 2 (2*n)))
791 change in ⊢ (? % ?) with (3*(2*n/3)).
793 apply le_times_div_m_m.
797 rewrite < distr_times_plus.
799 apply (trans_le ? ((2*n + n)/3))
800 [apply le_plus_div.apply lt_O_S
802 change in ⊢ (? (? % ?) ?) with (3*n).
804 rewrite > lt_O_to_div_times
810 |apply (trans_le ? (2*n*B(2*n)))
812 apply (trans_le ? ? ? ? H).
813 apply leb_true_to_le.reflexivity
814 |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
816 rewrite < assoc_times.
817 rewrite < sym_times in ⊢ (? ? (? % ?)).
818 rewrite > assoc_times in ⊢ (? ? %).
820 apply not_bertrand_to_le_B;assumption
821 |apply le_times_to_le_div
823 |apply (trans_le ? (sqrt (exp 2 8)))
824 [apply leb_true_to_le.reflexivity
825 |apply monotonic_sqrt.
826 change in ⊢ (? % ?) with (2*(exp 2 7)).
837 theorem not_bertrand_to_le2:
838 \forall n.exp 2 7 \le n \to not_bertrand n \to
839 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
841 rewrite < (eq_log_exp 2)
842 [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
845 |apply not_bertrand_to_le1;assumption
854 theorem tech1: \forall a,b,c,d.O < b \to O < d \to
855 (a/b)*(c/d) \le (a*c)/(b*d).
857 apply le_times_to_le_div
858 [rewrite > (times_n_O O).
859 apply lt_times;assumption
860 |rewrite > assoc_times.
861 rewrite < assoc_times in ⊢ (? (? ? %) ?).
862 rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
863 rewrite > assoc_times.
864 rewrite < assoc_times.
866 rewrite > sym_times;apply le_times_div_m_m;assumption
870 theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
871 (sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
873 cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
874 [rewrite > sym_times.
875 apply le_times_to_le_div
877 |rewrite < assoc_times.
878 apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
879 [apply le_times_l.assumption
880 |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
881 [apply le_times_div_div_times.
883 |rewrite > assoc_times.
885 rewrite > lt_O_to_div_times.
891 |change in ⊢ (? (? % ?) ?) with (2*2).
892 rewrite > assoc_times.
898 theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to
901 apply lt_times_to_lt_div.
902 apply (lt_to_le_to_lt ? (S(n/m)*m))
903 [apply lt_div_S.assumption
904 |rewrite > sym_times in ⊢ (? ? %). simplify.
905 rewrite > sym_times in ⊢ (? ? (? ? %)).
907 apply le_times_to_le_div
915 theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
918 rewrite > distr_times_plus.
919 rewrite > times_plus_l.
921 rewrite > assoc_plus.
922 rewrite > assoc_plus.
924 rewrite > times_plus_l.
926 rewrite < assoc_plus.
928 rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
929 rewrite > assoc_times.
930 apply eq_f2;reflexivity.
933 theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
935 lapply (le_log 2 ? ? (le_n ?) H) as H1.
936 rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
943 apply (trans_le ? (2*log 2 n))
944 [rewrite < times_SSO_n.
947 [apply leb_true_to_le.reflexivity
948 |rewrite < (eq_log_exp 2)
953 |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
954 apply le_times_SSO_n_exp_SSO_n.
955 apply (lt_to_le_to_lt ? ? ? ? H).
956 apply leb_true_to_le.reflexivity
958 |apply le_to_leb_true.
959 rewrite > assoc_times.
962 rewrite > assoc_times.
964 rewrite > exp_plus_SSO.
965 rewrite > distr_times_plus.
966 rewrite > distr_times_plus.
967 rewrite > assoc_plus.
968 apply (trans_le ? (4*exp (log 2 n) 2))
969 [change in ⊢ (? ? (? % ?)) with (2*2).
970 rewrite > assoc_times in ⊢ (? ? %).
971 rewrite < times_SSO_n in ⊢ (? ? %).
973 rewrite < times_SSO_n in ⊢ (? ? %).
975 [rewrite > sym_times in ⊢ (? (? ? %) ?).
976 rewrite < assoc_times.
977 rewrite < assoc_times.
978 change in ⊢ (? (? % ?) ?) with 8.
981 (* strange things here *)
982 rewrite < (eq_log_exp 2)
986 |apply (trans_le ? (log 2 n))
987 [change in ⊢ (? % ?) with 8.
988 rewrite < (eq_log_exp 2)
992 |rewrite > exp_n_SO in ⊢ (? % ?).
995 [apply (lt_to_le_to_lt ? ? ? ? H).
996 apply leb_true_to_le.reflexivity
997 |apply (lt_to_le_to_lt ? ? ? ? H).
998 apply leb_true_to_le.reflexivity
1004 |change in ⊢ (? (? % ?) ?) with (exp 2 2).
1005 apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
1006 [apply le_times_exp_n_SSO_exp_SSO_n
1008 |change in ⊢ (? % ?) with 8.
1009 rewrite < (eq_log_exp 2)
1014 |apply (lt_to_le_to_lt ? ? ? ? H).
1015 apply leb_true_to_le.reflexivity
1020 |apply (lt_to_le_to_lt ? ? ? ? H).
1021 apply leb_true_to_le.reflexivity
1025 theorem le_to_bertrand:
1026 \forall n. (exp 2 8) \le n \to bertrand n.
1028 apply not_not_bertrand_to_bertrand.unfold.intro.
1029 absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
1030 [apply not_bertrand_to_le2
1031 [apply (trans_le ? ? ? ? H).
1038 |apply lt_to_not_le.
1039 apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
1040 [apply tech.apply tech3.assumption
1042 |apply (trans_le ? (2*exp 2 8))
1043 [apply leb_true_to_le.reflexivity
1044 |apply le_times_r.assumption
1051 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.