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 set "baseuri" "cic:/matita/nat/chebishev".
18 include "nat/pi_p.ma".
19 include "nat/factorization.ma".
20 include "nat/factorial2.ma".
22 definition prim: nat \to nat \def
23 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
25 definition A: nat \to nat \def
26 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
28 theorem le_Al1: \forall n.
29 A n \le pi_p (S n) primeb (\lambda p.n).
40 theorem le_Al: \forall n.
41 A n \le exp n (prim n).
43 rewrite < exp_sigma_p.
47 theorem leA_r2: \forall n.
48 exp n (prim n) \le A n * A n.
50 elim (le_to_or_lt_eq ? ? (le_O_n n))
51 [rewrite < (exp_sigma_p (S n) n primeb).
56 rewrite < exp_plus_times.
57 apply (trans_le ? (exp i (S(log i n))))
61 apply primeb_true_to_prime.
65 apply primeb_true_to_prime.
78 |rewrite < H. apply le_n
82 definition A': nat \to nat \def
83 \lambda n. pi_p (S n) primeb
84 (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
86 theorem eq_A_A': \forall n.A n = A' n.
87 intro.unfold A.unfold A'.
91 apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
92 [apply eq_f.apply sym_eq.apply sigma_p_true
93 |apply sym_eq.apply exp_sigma_p
98 theorem eq_pi_p_primeb_divides_b: \forall n,m.
99 pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
100 = pi_p n primeb (\lambda p.exp p (ord m p)).
104 |apply (bool_elim ? (primeb n1));intro
105 [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
106 [apply (bool_elim ? (divides_b n1 m));intro
107 [rewrite > true_to_pi_p_Sn
110 |apply true_to_true_to_andb_true;assumption
112 |rewrite > false_to_pi_p_Sn
113 [rewrite > not_divides_to_ord_O
114 [simplify in ⊢ (? ? ? (? % ?)).
116 rewrite < times_n_SO.
118 |apply primeb_true_to_prime.assumption
119 |apply divides_b_false_to_not_divides.
122 |rewrite > H1.rewrite > H2.reflexivity
127 |rewrite > false_to_pi_p_Sn
128 [rewrite > false_to_pi_p_Sn
132 |rewrite > H1.reflexivity
138 theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to
139 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
142 apply (not_le_Sn_O ? H1)
143 |apply (bool_elim ? (primeb n∧divides_b n m));intro
144 [rewrite > true_to_pi_p_Sn
145 [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
147 rewrite > (H (ord_rem m n))
150 apply (bool_elim ? (primeb x));intro
152 apply (bool_elim ? (divides_b x (ord_rem m n)));intro
154 apply divides_to_divides_b_true
155 [apply prime_to_lt_O.
156 apply primeb_true_to_prime.
158 |apply (trans_divides ? (ord_rem m n))
159 [apply divides_b_true_to_divides.
161 |apply divides_ord_rem
162 [apply (trans_lt ? x)
163 [apply prime_to_lt_SO.
164 apply primeb_true_to_prime.
173 apply not_divides_to_divides_b_false
174 [apply prime_to_lt_O.
175 apply primeb_true_to_prime.
177 |apply ord_O_to_not_divides
179 |apply primeb_true_to_prime.
181 |rewrite < (ord_ord_rem n)
182 [apply not_divides_to_ord_O
183 [apply primeb_true_to_prime.
185 |apply divides_b_false_to_not_divides.
189 |apply primeb_true_to_prime.
190 apply (andb_true_true ? ? H3)
191 |apply primeb_true_to_prime.
204 |apply primeb_true_to_prime.
205 apply (andb_true_true ? ? H3)
206 |apply primeb_true_to_prime.
207 apply (andb_true_true ? ? H5)
212 [apply prime_to_lt_SO.
213 apply primeb_true_to_prime.
214 apply (andb_true_true ? ? H3)
217 |apply not_eq_to_le_to_lt
218 [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
220 intro.rewrite > H7 in H6.simplify in H6.
221 apply (not_divides_ord_rem m n)
223 |apply prime_to_lt_SO.
224 apply primeb_true_to_prime.
225 apply (andb_true_true ? ? H3)
226 |apply divides_b_true_to_divides.
227 apply (andb_true_true_r ? ? H6)
229 |elim H4.rewrite > H6.
232 apply primeb_true_to_prime.
233 apply (andb_true_true ? ? H3)
235 |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
239 |apply divides_ord_rem
240 [apply prime_to_lt_SO.
241 apply primeb_true_to_prime.
242 apply (andb_true_true ? ? H3)
246 |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
247 [apply le_max_f_max_g.
249 apply (bool_elim ? (primeb i));intro
251 apply divides_to_divides_b_true
252 [apply prime_to_lt_O.
253 apply primeb_true_to_prime.
255 |apply (trans_divides ? (ord_rem m n))
256 [apply divides_b_true_to_divides.
257 apply (andb_true_true_r ? ? H5)
258 |apply divides_ord_rem
259 [apply prime_to_lt_SO.
260 apply primeb_true_to_prime.
261 apply (andb_true_true ? ? H3)
275 |apply prime_to_lt_SO.
276 apply primeb_true_to_prime.
277 apply (andb_true_true ? ? H3)
282 |elim (le_to_or_lt_eq ? ? H1)
283 [rewrite > false_to_pi_p_Sn
286 |apply false_to_lt_max
287 [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
289 apply lt_SO_max_prime.
302 rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
305 apply (bool_elim ? (primeb x));intro
307 change with (divides_b x (S O) =false).
308 apply not_divides_to_divides_b_false
309 [apply prime_to_lt_O.
310 apply primeb_true_to_prime.
313 apply (le_to_not_lt x (S O))
315 [apply lt_O_S.assumption
318 |elim (primeb_true_to_prime ? H6).
331 theorem pi_p_primeb_divides_b: \forall n. O < n \to
332 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
334 apply lt_max_to_pi_p_primeb
341 theorem pi_p_primeb: \forall n. O < n \to
342 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
344 rewrite < eq_pi_p_primeb_divides_b.
345 apply pi_p_primeb_divides_b.
349 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
352 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
356 |apply lt_O_ord_rem;assumption
363 theorem sigma_p_divides_b:
364 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
365 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
368 |simplify in ⊢ (? ? ? (? % ? ?)).
369 rewrite > true_to_sigma_p_Sn
370 [rewrite > sym_plus.rewrite < plus_n_SO.
372 rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
375 apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
377 apply divides_to_divides_b_true
381 |apply (witness ? ? ((exp p (n - x))*n1)).
382 rewrite < assoc_times.
383 rewrite < exp_plus_times.
385 [apply eq_f.simplify.
388 apply plus_minus_m_m.
389 apply lt_to_le.assumption
395 apply (divides_b_false_to_not_divides ? ? H5).
396 apply (witness ? ? ((exp p (n - S x))*n1)).
397 rewrite < assoc_times.
398 rewrite < exp_plus_times.
402 apply plus_minus_m_m.
409 |apply divides_to_divides_b_true
411 apply prime_to_lt_O.assumption
412 |apply (witness ? ? n1).reflexivity
418 theorem sigma_p_divides_b1:
419 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
420 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
422 lapply (prime_to_lt_SO ? H1) as H4.
423 lapply (prime_to_lt_O ? H1) as H5.
424 rewrite > (false_to_eq_sigma_p m k)
425 [apply sigma_p_divides_b;assumption
428 apply not_divides_to_divides_b_false
429 [apply lt_O_exp.assumption
430 |intro.apply (le_to_not_lt ? ? H6).
432 rewrite < (ord_exp p)
433 [rewrite > (plus_n_O m).
434 rewrite < (not_divides_to_ord_O ? ? H1 H2).
435 rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
437 [apply divides_to_le_ord
438 [apply lt_O_exp.assumption
439 |rewrite > (times_n_O O).
441 [apply lt_O_exp.assumption
447 |apply lt_O_exp.assumption
457 theorem eq_ord_sigma_p:
458 \forall n,m,x. O < n \to prime x \to
459 exp x m \le n \to n < exp x (S m) \to
460 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
462 lapply (prime_to_lt_SO ? H1).
463 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
464 [apply sigma_p_divides_b1
465 [apply lt_O_ord_rem;assumption
467 |apply not_divides_ord_rem;assumption
469 apply (le_to_lt_to_lt ? (log x n))
470 [apply le_ord_log;assumption
471 |apply (lt_exp_to_lt x)
473 |apply (le_to_lt_to_lt ? n ? ? H3).
484 theorem pi_p_primeb1: \forall n. O < n \to
485 n = pi_p (S n) primeb
486 (\lambda p.(pi_p (log p n)
487 (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
489 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
493 rewrite > exp_sigma_p.
497 |apply primeb_true_to_prime.
499 |apply le_exp_log.assumption
501 apply prime_to_lt_SO.
502 apply primeb_true_to_prime.
508 theorem eq_fact_pi_p:\forall n. fact n =
509 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
512 |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
513 rewrite > true_to_pi_p_Sn
514 [apply eq_f.assumption
520 theorem eq_sigma_p_div: \forall n,q.O < q \to
521 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
524 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
525 [apply div_mod_spec_intro
526 [apply lt_mod_m_m.assumption
528 [simplify.elim q;reflexivity
529 |elim (or_div_mod1 n1 q)
531 rewrite > divides_to_mod_O
533 rewrite > true_to_sigma_p_Sn
534 [rewrite > H4 in ⊢ (? ? % ?).
539 apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
540 [apply div_mod_spec_div_mod.
542 |apply div_mod_spec_intro
543 [apply lt_mod_m_m.assumption
549 |apply true_to_true_to_andb_true
551 |apply divides_to_divides_b_true;assumption
558 rewrite > false_to_sigma_p_Sn
560 [rewrite < plus_n_Sm.
564 |elim (le_to_or_lt_eq (S (mod n1 q)) q)
568 apply (witness ? ? (S(div n1 q))).
569 rewrite < times_n_Sm.
571 rewrite < H2 in ⊢ (? ? ? (? ? %)).
578 |rewrite > not_divides_to_divides_b_false
579 [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
588 |apply div_mod_spec_div_mod.
593 theorem fact_pi_p: \forall n. fact n =
595 (\lambda p.(pi_p (log p n)
596 (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
598 rewrite > eq_fact_pi_p.
600 (pi_p (S n) (λi:nat.leb (S O) i)
601 (λn.pi_p (S n) primeb
602 (\lambda p.(pi_p (log p n)
603 (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
604 [apply eq_pi_p1;intros
607 apply leb_true_to_le.assumption
610 (pi_p (S n) (λi:nat.leb (S O) i)
612 .pi_p (S n) (\lambda p.primeb p\land leb p n)
613 (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
616 |intros.apply eq_pi_p1
617 [intros.elim (primeb x1)
618 [simplify.apply sym_eq.
619 apply le_to_leb_true.
628 (pi_p (S n) (λi:nat.leb (S O) i)
630 .pi_p (S n) (λp:nat.primeb p∧leb p m)
631 (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
636 apply false_to_eq_pi_p
638 |intros.rewrite > lt_to_leb_false
639 [elim primeb;reflexivity|assumption]
642 |(* make a general theorem *)
646 .pi_p (S n) (λm.leb p m)
647 (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
651 apply (bool_elim ? (primeb y \land leb y x));intros
652 [rewrite > (le_to_leb_true (S O) x)
654 |apply (trans_le ? y)
655 [apply prime_to_lt_O.
656 apply primeb_true_to_prime.
657 apply (andb_true_true ? ? H2)
658 |apply leb_true_to_le.
659 apply (andb_true_true_r ? ? H2)
662 |elim (leb (S O) x);reflexivity
668 (pi_p (S n) (λm:nat.leb x m)
669 (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
674 apply false_to_eq_pi_p
676 [apply prime_to_lt_SO.
677 apply primeb_true_to_prime.
679 |apply (lt_to_le_to_lt ? x)
680 [apply prime_to_lt_O.
681 apply primeb_true_to_prime.
683 |apply leb_true_to_le.
690 apply not_divides_to_divides_b_false
693 apply primeb_true_to_prime.
696 apply (lt_to_not_le x1 (exp x (S i)))
697 [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
699 apply prime_to_lt_SO.
700 apply primeb_true_to_prime.
703 [apply prime_to_lt_O.
704 apply primeb_true_to_prime.
711 [apply (lt_to_le_to_lt ? x)
712 [apply prime_to_lt_O.
713 apply primeb_true_to_prime.
715 |apply leb_true_to_le.
726 (pi_p (log x n) (λi:nat.true)
727 (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
728 [apply (pi_p_pi_p1 (\lambda m,i.x)).
734 rewrite > exp_sigma_p.
737 (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
740 apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
741 [apply (bool_elim ? (leb x x2));intro
742 [rewrite > le_to_leb_true
744 |apply (trans_le ? x)
745 [apply prime_to_lt_O.
746 apply primeb_true_to_prime.
748 |apply leb_true_to_le.
752 |rewrite > lt_to_leb_false
754 |apply not_le_to_lt.intro.
755 apply (leb_false_to_not_le ? ? H6).
756 apply (trans_le ? (exp x (S x1)))
757 [rewrite > times_n_SO in ⊢ (? % ?).
758 change with (exp x (S O) \le exp x (S x1)).
760 [apply prime_to_lt_O.
761 apply primeb_true_to_prime.
763 |apply le_S_S.apply le_O_n.
767 |apply divides_b_true_to_divides.
774 rewrite < andb_sym in ⊢ (? ? ? %).
779 |apply eq_sigma_p_div.
782 apply primeb_true_to_prime.
795 (* odd n is just mod n (S(S O))
799 | S m \Rightarrow (S O) - odd m
802 theorem le_odd_SO: \forall n. odd n \le S O.
805 |simplify.cases (odd n1)
806 [simplify.apply le_n.
812 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
814 [apply (lt_O_n_elim ? H).
815 intro.simplify.reflexivity
819 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
820 pi_p (S ((S(S O))*n)) primeb
821 (\lambda p.(pi_p (log p ((S(S O))*n))
822 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))).
823 intros.rewrite > fact_pi_p.
826 |intros.apply eq_pi_p
829 rewrite < exp_plus_times.
831 rewrite > sym_times in ⊢ (? ? ? (? % ?)).
835 apply primeb_true_to_prime.
841 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
842 pi_p (S ((S(S O))*n)) primeb
843 (\lambda p.(pi_p (log p ((S(S O))*n))
844 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
845 pi_p (S ((S(S O))*n)) primeb
846 (\lambda p.(pi_p (log p ((S(S O))*n))
847 (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
849 rewrite < times_pi_p.
850 rewrite > fact_pi_p2.
857 theorem pi_p_primeb4: \forall n. S O < n \to
858 pi_p (S ((S(S O))*n)) primeb
859 (\lambda p.(pi_p (log p ((S(S O))*n))
860 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
863 (\lambda p.(pi_p (log p (S(S O)*n))
864 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
866 apply or_false_eq_SO_to_eq_pi_p
873 [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
874 rewrite < times_n_SO.
877 |simplify.rewrite < times_n_SO.assumption
881 |apply le_S_S_to_le.assumption
886 theorem pi_p_primeb5: \forall n. S O < n \to
887 pi_p (S ((S(S O))*n)) primeb
888 (\lambda p.(pi_p (log p ((S(S O))*n))
889 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
892 (\lambda p.(pi_p (log p n)
893 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
895 rewrite > (pi_p_primeb4 ? H).
896 apply eq_pi_p1;intros
898 |apply or_false_eq_SO_to_eq_pi_p
900 [apply prime_to_lt_SO.
901 apply primeb_true_to_prime.
903 |apply lt_to_le.assumption
909 [simplify.reflexivity
910 |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
912 apply prime_to_lt_SO.
913 apply primeb_true_to_prime.
916 [apply prime_to_lt_O.
917 apply primeb_true_to_prime.
928 theorem exp_fact_SSO: \forall n.
929 exp (fact n) (S(S O))
932 (\lambda p.(pi_p (log p n)
933 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
947 (\lambda p.(pi_p (log p n)
948 (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
950 theorem eq_fact_B:\forall n.S O < n \to
951 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
953 rewrite > fact_pi_p3.
956 rewrite > pi_p_primeb5
964 theorem le_B_A: \forall n. B n \le A n.
968 apply le_pi_p.intros.
969 apply le_pi_p.intros.
970 rewrite > exp_n_SO in ⊢ (? ? %).
972 [apply prime_to_lt_O.
973 apply primeb_true_to_prime.
981 theorem le_fact_A:\forall n.S O < n \to
982 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
991 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
992 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
994 apply (le_times_to_le (exp (fact n) (S(S O))))
998 [rewrite < sym_times in ⊢ (? ? %).
1000 rewrite < assoc_times.
1007 theorem le_B_exp: \forall n.
1008 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1012 [simplify.apply le_S.apply le_S.apply le_n
1013 |apply lt_SO_to_le_B_exp.
1014 apply le_S_S.apply lt_O_S.
1019 theorem eq_A_SSO_n: \forall n.O < n \to
1021 pi_p (S ((S(S O))*n)) primeb
1022 (\lambda p.(pi_p (log p ((S(S O))*n) )
1023 (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1026 rewrite > eq_A_A'.rewrite > eq_A_A'.
1029 pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1030 = pi_p (S ((S(S O))*n)) primeb
1031 (λp:nat.pi_p (log p ((S(S O))*n)) (λi:nat.true) (λi:nat.(p)\sup(bool_to_nat (\lnot (leb (S n) (exp p (S i))))))))
1033 rewrite < times_pi_p.
1034 apply eq_pi_p1;intros
1036 |rewrite < times_pi_p.
1037 apply eq_pi_p;intros
1039 |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1040 [simplify.rewrite < times_n_SO.apply times_n_SO
1041 |simplify.rewrite < plus_n_O.apply times_n_SO
1045 |apply (trans_eq ? ? (pi_p (S n) primeb
1046 (\lambda p:nat.pi_p (log p n) (\lambda i:nat.true) (\lambda i:nat.(p)\sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
1047 [apply eq_pi_p1;intros
1049 |apply eq_pi_p1;intros
1051 |rewrite > lt_to_leb_false
1052 [simplify.apply times_n_SO
1054 apply (trans_le ? (exp x (log x n)))
1056 [apply prime_to_lt_O.
1057 apply primeb_true_to_prime.
1067 |apply (trans_eq ? ?
1068 (pi_p (S ((S(S O))*n)) primeb
1069 (λp:nat.pi_p (log p n) (λi:nat.true)
1070 (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1072 apply or_false_eq_SO_to_eq_pi_p
1077 rewrite > lt_to_log_O
1083 |apply eq_pi_p1;intros
1086 apply or_false_eq_SO_to_eq_pi_p
1088 [apply prime_to_lt_SO.
1089 apply primeb_true_to_prime.
1096 rewrite > le_to_leb_true
1097 [simplify.reflexivity
1098 |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1100 apply prime_to_lt_SO.
1101 apply primeb_true_to_prime.
1104 [apply prime_to_lt_O.
1105 apply primeb_true_to_prime.
1107 |apply le_S_S.assumption
1118 theorem le_A_BA1: \forall n. O < n \to
1119 A((S(S O))*n) \le B((S(S O))*n)*A n.
1121 rewrite > eq_A_SSO_n
1124 apply le_pi_p.intros.
1125 apply le_pi_p.intros.
1127 [apply prime_to_lt_O.
1128 apply primeb_true_to_prime.
1130 |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1131 [simplify in ⊢ (? % ?).
1132 cut ((S(S O))*n/i\sup(S i1) = S O)
1133 [rewrite > Hcut.apply le_n
1134 |apply (div_mod_spec_to_eq
1135 ((S(S O))*n) (exp i (S i1))
1136 ? (mod ((S(S O))*n) (exp i (S i1)))
1137 ? (minus ((S(S O))*n) (exp i (S i1))) )
1138 [apply div_mod_spec_div_mod.
1140 apply prime_to_lt_O.
1141 apply primeb_true_to_prime.
1143 |cut (i\sup(S i1)≤(S(S O))*n)
1144 [apply div_mod_spec_intro
1145 [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
1146 apply lt_plus_to_lt_minus
1148 |simplify in ⊢ (? % ?).
1151 [apply leb_true_to_le.assumption
1152 |apply leb_true_to_le.assumption
1155 |rewrite > sym_plus.
1156 rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1157 rewrite < times_n_SO.
1158 apply plus_minus_m_m.
1161 |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1163 [apply prime_to_lt_O.
1164 apply primeb_true_to_prime.
1169 rewrite > (times_n_O O) in ⊢ (? % ?).
1185 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1188 |apply le_A_BA1.apply lt_O_S
1192 theorem le_A_exp: \forall n.
1193 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1195 apply (trans_le ? (B((S(S O))*n)*A n))
1203 theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
1210 theorem le_exp_log: \forall p,n. O < n \to
1214 apply leb_true_to_le.
1216 apply (f_max_true (\lambda x.leb (exp p x) n)).
1217 apply (ex_intro ? ? O).
1220 |apply le_to_leb_true.simplify.assumption
1224 theorem lt_log_n_n: \forall n. O < n \to log n < n.
1227 [elim (le_to_or_lt_eq ? ? Hcut)
1229 |absurd (exp (S(S O)) n \le n)
1230 [rewrite < H1 in ⊢ (? (? ? %) ?).
1233 |apply lt_to_not_le.
1238 |unfold log.apply le_max_n
1242 theorem le_log_n_n: \forall n. log n \le n.
1252 theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
1254 [simplify.apply le_S.apply le_n
1255 |apply not_le_to_lt.
1256 apply leb_false_to_not_le.
1257 apply (lt_max_to_false ? (S n1) (S (log (S n1))))
1258 [apply le_S_S.apply le_n
1259 |apply lt_log_n_n.apply lt_O_S
1264 theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
1265 (\forall m. p < m \to f m = false)
1268 apply not_lt_to_le.intro.
1269 apply not_eq_true_false.
1270 rewrite < (H1 ? H2).
1276 theorem log_times1: \forall n,m. O < n \to O < m \to
1277 log (n*m) \le S(log n+log m).
1279 unfold in ⊢ (? (% ?) ?).
1280 apply f_false_to_le_max
1281 [apply (ex_intro ? ? O).
1284 |apply le_to_leb_true.
1286 rewrite > times_n_SO.
1287 apply le_times;assumption
1290 apply lt_to_leb_false.
1291 apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
1292 [apply lt_times;apply lt_exp_log
1293 |rewrite < exp_plus_times.
1297 rewrite < plus_n_Sm.
1304 theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
1309 [rewrite < times_n_O.
1311 |apply log_times1;apply lt_O_S
1316 theorem log_exp: \forall n,m.O < m \to
1317 log ((exp (S(S O)) n)*m)=n+log m.
1319 unfold log in ⊢ (? ? (% ?) ?).
1320 apply max_spec_to_max.
1330 rewrite > times_plus_l.
1331 apply (trans_le ? (S((S(S O))\sup(n1)*m)))
1332 [apply le_S_S.assumption
1333 |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
1334 [rewrite > (times_n_O O) in ⊢ (? % ?).
1340 |intro.simplify.apply le_S_S.
1346 apply le_to_leb_true.
1347 rewrite > exp_plus_times.
1354 apply lt_to_leb_false.
1355 apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
1357 [apply lt_O_exp.apply lt_O_S
1360 |rewrite < exp_plus_times.
1363 |rewrite < plus_n_Sm.
1370 theorem log_SSO: \forall n. O < n \to
1371 log ((S(S O))*n) = S (log n).
1373 change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
1374 rewrite > log_exp.reflexivity.assumption.
1377 theorem or_eq_S: \forall n.\exists m.
1378 (n = (S(S O))*m) \lor (n = S((S(S O))*m)).
1381 [apply (ex_intro ? ? O).left.apply times_n_O
1383 [apply (ex_intro ? ? a).right.apply eq_f.assumption
1384 |apply (ex_intro ? ? (S a)).left.
1385 rewrite > H2.simplify.
1387 rewrite < plus_n_Sm.
1393 theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land
1394 ((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
1398 [apply (ex_intro ? ? a).split
1400 rewrite > times_n_SO in ⊢ (? % ?).
1401 rewrite > sym_times.
1403 [apply (divides_to_lt_O a n ? ?)
1405 |apply (witness a n (S (S O))).
1406 rewrite > sym_times.
1413 |apply (ex_intro ? ? a).split
1415 apply (le_to_lt_to_lt ? ((S(S O))*a))
1416 [rewrite > times_n_SO in ⊢ (? % ?).
1417 rewrite > sym_times.
1427 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
1428 intro.simplify.reflexivity.
1431 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
1435 lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
1436 intro.simplify.rewrite < plus_n_Sm.reflexivity.
1439 theorem fact1: \forall n.
1440 fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
1442 [rewrite < times_n_O.apply le_n
1443 |rewrite > times_SSO.
1446 rewrite < assoc_times.
1448 apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
1450 rewrite > times_SSO.
1453 |rewrite > assoc_times.
1454 rewrite > assoc_times.
1455 rewrite > assoc_times in ⊢ (? ? %).
1457 rewrite > assoc_times in ⊢ (? ? %).
1459 rewrite < assoc_times.
1460 rewrite < assoc_times.
1461 rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
1462 rewrite > assoc_times.
1463 rewrite > assoc_times.
1465 rewrite > assoc_times in ⊢ (? ? %).
1467 rewrite > sym_times in ⊢ (? ? %).
1468 rewrite > assoc_times in ⊢ (? ? %).
1469 rewrite > assoc_times in ⊢ (? ? %).
1471 rewrite < assoc_times in ⊢ (? ? %).
1472 rewrite < assoc_times in ⊢ (? ? %).
1473 rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
1474 rewrite > assoc_times in ⊢ (? ? %).
1475 rewrite > assoc_times in ⊢ (? ? %).
1477 rewrite > sym_times in ⊢ (? ? (? ? %)).
1478 rewrite > sym_times in ⊢ (? ? %).
1484 theorem monotonic_log: monotonic nat le log.
1485 unfold monotonic.intros.
1486 elim (le_to_or_lt_eq ? ? H) 0
1490 apply (lt_exp_to_lt (S(S O)))
1492 |apply (le_to_lt_to_lt ? (S n))
1495 |apply (trans_lt ? y)
1502 |intro.rewrite < H1.apply le_n
1506 theorem lt_O_fact: \forall n. O < fact n.
1508 [simplify.apply lt_O_S
1510 rewrite > (times_n_O O).
1518 theorem fact2: \forall n.O < n \to
1519 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
1521 [simplify.apply le_S.apply le_n
1522 |rewrite > times_SSO.
1525 rewrite < assoc_times.
1527 rewrite < times_SSO in ⊢ (? ? %).
1528 apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
1529 [rewrite > assoc_times in ⊢ (? ? %).
1531 rewrite > assoc_times.
1532 rewrite > assoc_times.
1533 rewrite > assoc_times.
1536 rewrite > assoc_times.
1537 rewrite > sym_times in ⊢ (? ? %).
1538 rewrite > assoc_times in ⊢ (? ? %).
1539 rewrite > assoc_times in ⊢ (? ? %).
1541 rewrite > sym_times.
1542 rewrite > assoc_times.
1543 rewrite > assoc_times.
1545 rewrite < assoc_times.
1546 rewrite < assoc_times.
1547 rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1548 rewrite > assoc_times.
1549 rewrite > assoc_times.
1550 rewrite > sym_times in ⊢ (? ? %).
1552 rewrite < assoc_times.
1553 rewrite < sym_times.
1554 rewrite < assoc_times.
1557 [rewrite > (times_n_O O) in ⊢ (? % ?).
1559 [rewrite > (times_n_O O) in ⊢ (? % ?).
1572 theorem lt_O_log: \forall n. S O < n \to O < log n.
1574 [simplify.apply lt_O_S
1575 |apply (lt_to_le_to_lt ? (log n1))
1577 |apply monotonic_log.
1583 theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
1587 lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
1591 theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
1595 theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
1599 theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to
1600 n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
1603 [rewrite > factS in ⊢ (? (? %) ?).
1604 rewrite > factS in ⊢ (? (? (? ? %)) ?).
1605 rewrite < assoc_times in ⊢ (? (? %) ?).
1606 rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
1607 rewrite > assoc_times in ⊢ (? (? %) ?).
1608 change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
1610 theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
1611 intro.apply (nat_elim1 n).
1613 elim (lt_O_to_or_eq_S m)
1617 apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
1618 [apply monotonic_log.
1620 |rewrite > assoc_times in ⊢ (? (? %) ?).
1622 apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
1625 |rewrite > plus_n_Sm.
1627 rewrite < times_n_Sm.
1628 apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
1632 |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
1637 |rewrite > times_SSO_n.
1638 rewrite > distr_times_minus.
1640 rewrite > plus_minus
1641 [rewrite > sym_plus.
1642 rewrite < assoc_times.
1644 |rewrite < assoc_times.
1645 rewrite > times_n_SO in ⊢ (? % ?).
1649 apply (lt_times_n_to_lt_r (S(S O)))
1651 |rewrite < times_n_SO.
1662 rewrite < eq_plus_minus_minus_plus.
1664 rewrite > assoc_plus.
1666 rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
1668 (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
1669 apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
1677 theorem stirling: \forall n,k.k \le n \to
1678 log (fact n) < n*log n - n + k*log n.
1680 apply (nat_elim1 n).
1682 elim (lt_O_to_or_eq_S m)
1686 apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
1687 [apply monotonic_log.
1689 |rewrite > assoc_times in ⊢ (? (? %) ?).
1691 apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
1694 |rewrite < plus_n_Sm.
1695 rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
1697 (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
1698 apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))