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 (* This is chebishev psi function *)
26 definition A: nat \to nat \def
27 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
29 theorem le_Al1: \forall n.
30 A n \le pi_p (S n) primeb (\lambda p.n).
41 theorem le_Al: \forall n.
42 A n \le exp n (prim n).
44 rewrite < exp_sigma_p.
48 theorem leA_r2: \forall n.
49 exp n (prim n) \le A n * A n.
51 elim (le_to_or_lt_eq ? ? (le_O_n n))
52 [rewrite < (exp_sigma_p (S n) n primeb).
57 rewrite < exp_plus_times.
58 apply (trans_le ? (exp i (S(log i n))))
62 apply primeb_true_to_prime.
66 apply primeb_true_to_prime.
79 |rewrite < H. apply le_n
83 (* an equivalent formulation for psi *)
84 definition A': nat \to nat \def
85 \lambda n. pi_p (S n) primeb
86 (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
88 theorem eq_A_A': \forall n.A n = A' n.
89 intro.unfold A.unfold A'.
93 apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
94 [apply eq_f.apply sym_eq.apply sigma_p_true
95 |apply sym_eq.apply exp_sigma_p
100 theorem eq_pi_p_primeb_divides_b: \forall n,m.
101 pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
102 = pi_p n primeb (\lambda p.exp p (ord m p)).
106 |apply (bool_elim ? (primeb n1));intro
107 [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
108 [apply (bool_elim ? (divides_b n1 m));intro
109 [rewrite > true_to_pi_p_Sn
112 |apply true_to_true_to_andb_true;assumption
114 |rewrite > false_to_pi_p_Sn
115 [rewrite > not_divides_to_ord_O
116 [simplify in ⊢ (? ? ? (? % ?)).
118 rewrite < times_n_SO.
120 |apply primeb_true_to_prime.assumption
121 |apply divides_b_false_to_not_divides.
124 |rewrite > H1.rewrite > H2.reflexivity
129 |rewrite > false_to_pi_p_Sn
130 [rewrite > false_to_pi_p_Sn
134 |rewrite > H1.reflexivity
140 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
141 m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
144 apply (not_le_Sn_O ? H1)
145 |apply (bool_elim ? (primeb n∧divides_b n m));intro
146 [rewrite > true_to_pi_p_Sn
147 [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
149 rewrite > (H (ord_rem m n))
152 apply (bool_elim ? (primeb x));intro
154 apply (bool_elim ? (divides_b x (ord_rem m n)));intro
156 apply divides_to_divides_b_true
157 [apply prime_to_lt_O.
158 apply primeb_true_to_prime.
160 |apply (trans_divides ? (ord_rem m n))
161 [apply divides_b_true_to_divides.
163 |apply divides_ord_rem
164 [apply (trans_lt ? x)
165 [apply prime_to_lt_SO.
166 apply primeb_true_to_prime.
175 apply not_divides_to_divides_b_false
176 [apply prime_to_lt_O.
177 apply primeb_true_to_prime.
179 |apply ord_O_to_not_divides
181 |apply primeb_true_to_prime.
183 |rewrite < (ord_ord_rem n)
184 [apply not_divides_to_ord_O
185 [apply primeb_true_to_prime.
187 |apply divides_b_false_to_not_divides.
191 |apply primeb_true_to_prime.
192 apply (andb_true_true ? ? H3)
193 |apply primeb_true_to_prime.
206 |apply primeb_true_to_prime.
207 apply (andb_true_true ? ? H3)
208 |apply primeb_true_to_prime.
209 apply (andb_true_true ? ? H5)
214 [apply prime_to_lt_SO.
215 apply primeb_true_to_prime.
216 apply (andb_true_true ? ? H3)
219 |apply not_eq_to_le_to_lt
220 [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
222 intro.rewrite > H7 in H6.simplify in H6.
223 apply (not_divides_ord_rem m n)
225 |apply prime_to_lt_SO.
226 apply primeb_true_to_prime.
227 apply (andb_true_true ? ? H3)
228 |apply divides_b_true_to_divides.
229 apply (andb_true_true_r ? ? H6)
231 |elim H4.rewrite > H6.
234 apply primeb_true_to_prime.
235 apply (andb_true_true ? ? H3)
237 |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
241 |apply divides_ord_rem
242 [apply prime_to_lt_SO.
243 apply primeb_true_to_prime.
244 apply (andb_true_true ? ? H3)
248 |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
249 [apply le_max_f_max_g.
251 apply (bool_elim ? (primeb i));intro
253 apply divides_to_divides_b_true
254 [apply prime_to_lt_O.
255 apply primeb_true_to_prime.
257 |apply (trans_divides ? (ord_rem m n))
258 [apply divides_b_true_to_divides.
259 apply (andb_true_true_r ? ? H5)
260 |apply divides_ord_rem
261 [apply prime_to_lt_SO.
262 apply primeb_true_to_prime.
263 apply (andb_true_true ? ? H3)
277 |apply prime_to_lt_SO.
278 apply primeb_true_to_prime.
279 apply (andb_true_true ? ? H3)
284 |elim (le_to_or_lt_eq ? ? H1)
285 [rewrite > false_to_pi_p_Sn
288 |apply false_to_lt_max
289 [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
291 apply lt_SO_max_prime.
304 rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
307 apply (bool_elim ? (primeb x));intro
309 change with (divides_b x (S O) =false).
310 apply not_divides_to_divides_b_false
311 [apply prime_to_lt_O.
312 apply primeb_true_to_prime.
315 apply (le_to_not_lt x (S O))
317 [apply lt_O_S.assumption
320 |elim (primeb_true_to_prime ? H6).
333 (* factorization of n into primes *)
334 theorem pi_p_primeb_divides_b: \forall n. O < n \to
335 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
337 apply lt_max_to_pi_p_primeb
344 theorem pi_p_primeb: \forall n. O < n \to
345 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
347 rewrite < eq_pi_p_primeb_divides_b.
348 apply pi_p_primeb_divides_b.
352 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
355 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
359 |apply lt_O_ord_rem;assumption
366 theorem sigma_p_divides_b:
367 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
368 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
371 |simplify in ⊢ (? ? ? (? % ? ?)).
372 rewrite > true_to_sigma_p_Sn
373 [rewrite > sym_plus.rewrite < plus_n_SO.
375 rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
378 apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
380 apply divides_to_divides_b_true
384 |apply (witness ? ? ((exp p (n - x))*n1)).
385 rewrite < assoc_times.
386 rewrite < exp_plus_times.
388 [apply eq_f.simplify.
391 apply plus_minus_m_m.
392 apply lt_to_le.assumption
398 apply (divides_b_false_to_not_divides ? ? H5).
399 apply (witness ? ? ((exp p (n - S x))*n1)).
400 rewrite < assoc_times.
401 rewrite < exp_plus_times.
405 apply plus_minus_m_m.
412 |apply divides_to_divides_b_true
414 apply prime_to_lt_O.assumption
415 |apply (witness ? ? n1).reflexivity
421 theorem sigma_p_divides_b1:
422 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
423 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
425 lapply (prime_to_lt_SO ? H1) as H4.
426 lapply (prime_to_lt_O ? H1) as H5.
427 rewrite > (false_to_eq_sigma_p m k)
428 [apply sigma_p_divides_b;assumption
431 apply not_divides_to_divides_b_false
432 [apply lt_O_exp.assumption
433 |intro.apply (le_to_not_lt ? ? H6).
435 rewrite < (ord_exp p)
436 [rewrite > (plus_n_O m).
437 rewrite < (not_divides_to_ord_O ? ? H1 H2).
438 rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
440 [apply divides_to_le_ord
441 [apply lt_O_exp.assumption
442 |rewrite > (times_n_O O).
444 [apply lt_O_exp.assumption
450 |apply lt_O_exp.assumption
460 theorem eq_ord_sigma_p:
461 \forall n,m,x. O < n \to prime x \to
462 exp x m \le n \to n < exp x (S m) \to
463 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
465 lapply (prime_to_lt_SO ? H1).
466 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
467 [apply sigma_p_divides_b1
468 [apply lt_O_ord_rem;assumption
470 |apply not_divides_ord_rem;assumption
472 apply (le_to_lt_to_lt ? (log x n))
473 [apply le_ord_log;assumption
474 |apply (lt_exp_to_lt x)
476 |apply (le_to_lt_to_lt ? n ? ? H3).
487 theorem pi_p_primeb1: \forall n. O < n \to
488 n = pi_p (S n) primeb
489 (\lambda p.(pi_p (log p n)
490 (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
492 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
496 rewrite > exp_sigma_p.
500 |apply primeb_true_to_prime.
502 |apply le_exp_log.assumption
504 apply prime_to_lt_SO.
505 apply primeb_true_to_prime.
511 (* the factorial function *)
512 theorem eq_fact_pi_p:\forall n. fact n =
513 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
516 |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
517 rewrite > true_to_pi_p_Sn
518 [apply eq_f.assumption
524 theorem eq_sigma_p_div: \forall n,q.O < q \to
525 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
528 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
529 [apply div_mod_spec_intro
530 [apply lt_mod_m_m.assumption
532 [simplify.elim q;reflexivity
533 |elim (or_div_mod1 n1 q)
535 rewrite > divides_to_mod_O
537 rewrite > true_to_sigma_p_Sn
538 [rewrite > H4 in ⊢ (? ? % ?).
543 apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
544 [apply div_mod_spec_div_mod.
546 |apply div_mod_spec_intro
547 [apply lt_mod_m_m.assumption
553 |apply true_to_true_to_andb_true
555 |apply divides_to_divides_b_true;assumption
562 rewrite > false_to_sigma_p_Sn
564 [rewrite < plus_n_Sm.
568 |elim (le_to_or_lt_eq (S (mod n1 q)) q)
572 apply (witness ? ? (S(div n1 q))).
573 rewrite < times_n_Sm.
575 rewrite < H2 in ⊢ (? ? ? (? ? %)).
582 |rewrite > not_divides_to_divides_b_false
583 [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
592 |apply div_mod_spec_div_mod.
597 (* still another characterization of the factorial *)
598 theorem fact_pi_p: \forall n. fact n =
600 (\lambda p.(pi_p (log p n)
601 (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
603 rewrite > eq_fact_pi_p.
605 (pi_p (S n) (λi:nat.leb (S O) i)
606 (λn.pi_p (S n) primeb
607 (\lambda p.(pi_p (log p n)
608 (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
609 [apply eq_pi_p1;intros
612 apply leb_true_to_le.assumption
615 (pi_p (S n) (λi:nat.leb (S O) i)
617 .pi_p (S n) (\lambda p.primeb p\land leb p n)
618 (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
621 |intros.apply eq_pi_p1
622 [intros.elim (primeb x1)
623 [simplify.apply sym_eq.
624 apply le_to_leb_true.
633 (pi_p (S n) (λi:nat.leb (S O) i)
635 .pi_p (S n) (λp:nat.primeb p∧leb p m)
636 (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
641 apply false_to_eq_pi_p
643 |intros.rewrite > lt_to_leb_false
644 [elim primeb;reflexivity|assumption]
647 |(* make a general theorem *)
651 .pi_p (S n) (λm.leb p m)
652 (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
656 apply (bool_elim ? (primeb y \land leb y x));intros
657 [rewrite > (le_to_leb_true (S O) x)
659 |apply (trans_le ? y)
660 [apply prime_to_lt_O.
661 apply primeb_true_to_prime.
662 apply (andb_true_true ? ? H2)
663 |apply leb_true_to_le.
664 apply (andb_true_true_r ? ? H2)
667 |elim (leb (S O) x);reflexivity
673 (pi_p (S n) (λm:nat.leb x m)
674 (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
679 apply false_to_eq_pi_p
681 [apply prime_to_lt_SO.
682 apply primeb_true_to_prime.
688 apply not_divides_to_divides_b_false
691 apply primeb_true_to_prime.
694 apply (lt_to_not_le x1 (exp x (S i)))
695 [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
697 apply prime_to_lt_SO.
698 apply primeb_true_to_prime.
701 [apply prime_to_lt_O.
702 apply primeb_true_to_prime.
709 [apply (lt_to_le_to_lt ? x)
710 [apply prime_to_lt_O.
711 apply primeb_true_to_prime.
713 |apply leb_true_to_le.
724 (pi_p (log x n) (λi:nat.true)
725 (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
726 [apply (pi_p_pi_p1 (\lambda m,i.x)).
732 rewrite > exp_sigma_p.
735 (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
738 apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
739 [apply (bool_elim ? (leb x x2));intro
740 [rewrite > le_to_leb_true
742 |apply (trans_le ? x)
743 [apply prime_to_lt_O.
744 apply primeb_true_to_prime.
746 |apply leb_true_to_le.
750 |rewrite > lt_to_leb_false
752 |apply not_le_to_lt.intro.
753 apply (leb_false_to_not_le ? ? H6).
754 apply (trans_le ? (exp x (S x1)))
755 [rewrite > times_n_SO in ⊢ (? % ?).
756 change with (exp x (S O) \le exp x (S x1)).
758 [apply prime_to_lt_O.
759 apply primeb_true_to_prime.
761 |apply le_S_S.apply le_O_n.
765 |apply divides_b_true_to_divides.
772 rewrite < andb_sym in ⊢ (? ? ? %).
777 |apply eq_sigma_p_div.
780 apply primeb_true_to_prime.
793 (* odd n is just mod n (S(S O))
797 | S m \Rightarrow (S O) - odd m
800 theorem le_odd_SO: \forall n. odd n \le S O.
803 |simplify.cases (odd n1)
804 [simplify.apply le_n.
810 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
812 [apply (lt_O_n_elim ? H).
813 intro.simplify.reflexivity
817 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
818 pi_p (S ((S(S O))*n)) primeb
819 (\lambda p.(pi_p (log p ((S(S O))*n))
820 (\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)))))))).
821 intros.rewrite > fact_pi_p.
824 |intros.apply eq_pi_p
827 rewrite < exp_plus_times.
829 rewrite > sym_times in ⊢ (? ? ? (? % ?)).
833 apply primeb_true_to_prime.
839 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
840 pi_p (S ((S(S O))*n)) primeb
841 (\lambda p.(pi_p (log p ((S(S O))*n))
842 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
843 pi_p (S ((S(S O))*n)) primeb
844 (\lambda p.(pi_p (log p ((S(S O))*n))
845 (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
847 rewrite < times_pi_p.
848 rewrite > fact_pi_p2.
855 theorem pi_p_primeb4: \forall n. S O < n \to
856 pi_p (S ((S(S O))*n)) primeb
857 (\lambda p.(pi_p (log p ((S(S O))*n))
858 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
861 (\lambda p.(pi_p (log p (S(S O)*n))
862 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
864 apply or_false_eq_SO_to_eq_pi_p
871 [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
872 rewrite < times_n_SO.
875 |simplify.rewrite < times_n_SO.assumption
879 |apply le_S_S_to_le.assumption
884 theorem pi_p_primeb5: \forall n. S O < n \to
885 pi_p (S ((S(S O))*n)) primeb
886 (\lambda p.(pi_p (log p ((S(S O))*n))
887 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
890 (\lambda p.(pi_p (log p n)
891 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
893 rewrite > (pi_p_primeb4 ? H).
894 apply eq_pi_p1;intros
896 |apply or_false_eq_SO_to_eq_pi_p
898 [apply prime_to_lt_SO.
899 apply primeb_true_to_prime.
906 [simplify.reflexivity
907 |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
909 apply prime_to_lt_SO.
910 apply primeb_true_to_prime.
913 [apply prime_to_lt_O.
914 apply primeb_true_to_prime.
925 theorem exp_fact_SSO: \forall n.
926 exp (fact n) (S(S O))
929 (\lambda p.(pi_p (log p n)
930 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
944 (\lambda p.(pi_p (log p n)
945 (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
947 theorem eq_fact_B:\forall n.S O < n \to
948 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
950 rewrite > fact_pi_p3.
953 rewrite > pi_p_primeb5
961 theorem le_B_A: \forall n. B n \le A n.
965 apply le_pi_p.intros.
966 apply le_pi_p.intros.
967 rewrite > exp_n_SO in ⊢ (? ? %).
969 [apply prime_to_lt_O.
970 apply primeb_true_to_prime.
978 theorem le_B_A4: \forall n. O < n \to (S(S O))* B ((S(S(S(S O))))*n) \le A ((S(S(S(S O))))*n).
982 cut ((S(S O)) < (S ((S(S(S(S O))))*n)))
983 [cut (O<log (S(S O)) ((S(S(S(S O))))*n))
984 [rewrite > (pi_p_gi ? ? (S(S O)))
985 [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %)
986 [rewrite < assoc_times.
988 [rewrite > (pi_p_gi ? ? O)
989 [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %)
990 [rewrite < assoc_times.
993 change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?)
994 with ((S(S O))*(S(S O))).
995 rewrite > assoc_times.
996 rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?).
997 rewrite > lt_O_to_div_times
998 [rewrite > divides_to_mod_O
1001 |apply (witness ? ? n).reflexivity
1005 |apply le_pi_p.intros.
1006 rewrite > exp_n_SO in ⊢ (? ? %).
1009 |apply le_S_S_to_le.
1020 |apply le_pi_p.intros.
1021 apply le_pi_p.intros.
1022 rewrite > exp_n_SO in ⊢ (? ? %).
1024 [apply prime_to_lt_O.
1025 apply primeb_true_to_prime.
1026 apply (andb_true_true ? ? H2)
1027 |apply le_S_S_to_le.
1039 [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?).
1044 |rewrite > times_n_SO in ⊢ (? % ?).
1046 [apply le_S.apply le_S.apply le_n
1052 rewrite > times_n_SO in ⊢ (? % ?).
1054 [apply le_S.apply le_n_Sn
1060 theorem le_fact_A:\forall n.S O < n \to
1061 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
1070 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
1071 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1073 apply (le_times_to_le (exp (fact n) (S(S O))))
1076 |rewrite < eq_fact_B
1077 [rewrite < sym_times in ⊢ (? ? %).
1079 rewrite < assoc_times.
1086 theorem le_B_exp: \forall n.
1087 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1091 [simplify.apply le_S.apply le_S.apply le_n
1092 |apply lt_SO_to_le_B_exp.
1093 apply le_S_S.apply lt_O_S.
1098 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1099 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1101 apply (le_times_to_le (exp (fact n) (S(S O))))
1104 |rewrite < assoc_times in ⊢ (? ? %).
1105 rewrite > sym_times in ⊢ (? ? (? % ?)).
1106 rewrite > assoc_times in ⊢ (? ? %).
1108 [rewrite < sym_times.
1110 apply lt_to_le.assumption
1116 theorem le_exp_B: \forall n. O < n \to
1117 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1121 |apply lt_SO_to_le_exp_B.
1122 apply le_S_S.assumption
1126 theorem eq_A_SSO_n: \forall n.O < n \to
1128 pi_p (S ((S(S O))*n)) primeb
1129 (\lambda p.(pi_p (log p ((S(S O))*n) )
1130 (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1133 rewrite > eq_A_A'.rewrite > eq_A_A'.
1136 pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1137 = pi_p (S ((S(S O))*n)) primeb
1138 (λ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))))))))
1140 rewrite < times_pi_p.
1141 apply eq_pi_p1;intros
1143 |rewrite < times_pi_p.
1144 apply eq_pi_p;intros
1146 |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1147 [simplify.rewrite < times_n_SO.apply times_n_SO
1148 |simplify.rewrite < plus_n_O.apply times_n_SO
1152 |apply (trans_eq ? ? (pi_p (S n) primeb
1153 (\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))))))))
1154 [apply eq_pi_p1;intros
1156 |apply eq_pi_p1;intros
1158 |rewrite > lt_to_leb_false
1159 [simplify.apply times_n_SO
1161 apply (trans_le ? (exp x (log x n)))
1163 [apply prime_to_lt_O.
1164 apply primeb_true_to_prime.
1174 |apply (trans_eq ? ?
1175 (pi_p (S ((S(S O))*n)) primeb
1176 (λp:nat.pi_p (log p n) (λi:nat.true)
1177 (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1179 apply or_false_eq_SO_to_eq_pi_p
1184 rewrite > lt_to_log_O
1190 |apply eq_pi_p1;intros
1193 apply or_false_eq_SO_to_eq_pi_p
1195 [apply prime_to_lt_SO.
1196 apply primeb_true_to_prime.
1202 rewrite > le_to_leb_true
1203 [simplify.reflexivity
1204 |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1206 apply prime_to_lt_SO.
1207 apply primeb_true_to_prime.
1210 [apply prime_to_lt_O.
1211 apply primeb_true_to_prime.
1213 |apply le_S_S.assumption
1224 theorem le_A_BA1: \forall n. O < n \to
1225 A((S(S O))*n) \le B((S(S O))*n)*A n.
1227 rewrite > eq_A_SSO_n
1230 apply le_pi_p.intros.
1231 apply le_pi_p.intros.
1233 [apply prime_to_lt_O.
1234 apply primeb_true_to_prime.
1236 |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1237 [simplify in ⊢ (? % ?).
1238 cut ((S(S O))*n/i\sup(S i1) = S O)
1239 [rewrite > Hcut.apply le_n
1240 |apply (div_mod_spec_to_eq
1241 ((S(S O))*n) (exp i (S i1))
1242 ? (mod ((S(S O))*n) (exp i (S i1)))
1243 ? (minus ((S(S O))*n) (exp i (S i1))) )
1244 [apply div_mod_spec_div_mod.
1246 apply prime_to_lt_O.
1247 apply primeb_true_to_prime.
1249 |cut (i\sup(S i1)≤(S(S O))*n)
1250 [apply div_mod_spec_intro
1251 [apply lt_plus_to_lt_minus
1253 |simplify in ⊢ (? % ?).
1256 [apply leb_true_to_le.assumption
1257 |apply leb_true_to_le.assumption
1260 |rewrite > sym_plus.
1261 rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1262 rewrite < times_n_SO.
1263 apply plus_minus_m_m.
1266 |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1268 [apply prime_to_lt_O.
1269 apply primeb_true_to_prime.
1274 rewrite > (times_n_O O) in ⊢ (? % ?).
1290 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1293 |apply le_A_BA1.apply lt_O_S
1297 theorem le_A_exp: \forall n.
1298 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1300 apply (trans_le ? (B((S(S O))*n)*A n))
1307 theorem le_A_exp1: \forall n.
1308 A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
1310 [simplify.apply le_S_S.apply le_O_n
1311 |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
1312 apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1314 |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1))))
1317 |rewrite < exp_plus_times.
1318 simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
1325 theorem monotonic_A: monotonic nat le A.
1329 |apply (trans_le ? (A n1))
1332 cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1333 ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1334 [apply (bool_elim ? (primeb (S n1)));intro
1335 [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1336 rewrite > times_n_SO in ⊢ (? % ?).
1337 rewrite > sym_times.
1339 [apply lt_O_exp.apply lt_O_S
1342 |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1345 |apply le_pi_p.intros.
1347 [apply prime_to_lt_O.
1348 apply primeb_true_to_prime.
1351 [apply prime_to_lt_SO.
1352 apply primeb_true_to_prime.
1354 |apply le_S.apply le_n
1362 theorem le_A_exp2: \forall n. O < n \to
1363 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1365 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1370 |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1374 |rewrite > assoc_times.apply le_times_r.
1375 change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1385 theorem A_SO: A (S O) = S O.
1389 theorem A_SSO: A (S(S O)) = S (S O).
1393 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1397 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1402 theorem or_eq_eq_S: \forall n.\exists m.
1403 n = (S(S O))*m \lor n = S ((S(S O))*m).
1405 [apply (ex_intro ? ? O).
1408 [apply (ex_intro ? ? a).
1409 right.apply eq_f.assumption
1410 |apply (ex_intro ? ? (S a)).
1418 (* a better result *)
1419 theorem le_A_exp3: \forall n. S O < n \to
1420 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
1422 apply (nat_elim1 n).
1424 elim (or_eq_eq_S m).
1426 [elim (le_to_or_lt_eq (S O) a)
1427 [rewrite > H3 in ⊢ (? % ?).
1428 apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1430 |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1431 ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1435 rewrite > times_n_SO in ⊢ (? % ?).
1436 rewrite > sym_times.
1438 [apply lt_to_le.assumption
1443 |rewrite > sym_times.
1444 rewrite > assoc_times.
1445 rewrite < exp_plus_times.
1447 (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1448 [rewrite > assoc_times.
1450 rewrite < exp_plus_times.
1456 apply le_S.apply le_S.
1460 rewrite > times_exp.
1461 apply monotonic_exp1.
1463 rewrite > sym_times.
1467 rewrite < plus_n_Sm.
1474 |rewrite < H4 in H3.
1478 apply le_S_S.apply le_S_S.apply le_O_n
1479 |apply not_lt_to_le.intro.
1480 apply (lt_to_not_le ? ? H1).
1482 apply (le_n_O_elim a)
1483 [apply le_S_S_to_le.assumption
1487 |elim (le_to_or_lt_eq O a (le_O_n ?))
1488 [apply (trans_le ? (A ((S(S O))*(S a))))
1491 rewrite > times_SSO.
1493 |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1495 |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1496 (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1502 rewrite > plus_n_SO.
1506 |apply le_S_S.assumption
1508 |rewrite > sym_times.
1509 rewrite > assoc_times.
1510 rewrite < exp_plus_times.
1512 (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1513 [rewrite > assoc_times.
1515 rewrite < exp_plus_times.
1518 |rewrite > times_SSO.
1521 rewrite < plus_n_Sm.
1526 rewrite > times_exp.
1527 apply monotonic_exp1.
1529 rewrite > sym_times.
1535 |rewrite < H4 in H3.simplify in H3.
1537 apply (lt_to_not_le ? ? H1).
1544 theorem le_A_exp4: \forall n. S O < n \to
1545 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n))).
1547 apply (nat_elim1 n).
1549 elim (or_eq_eq_S m).
1551 [elim (le_to_or_lt_eq (S O) a)
1552 [rewrite > H3 in ⊢ (? % ?).
1553 apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1555 |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1556 ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*(pred a)))))
1560 rewrite > times_n_SO in ⊢ (? % ?).
1561 rewrite > sym_times.
1563 [apply lt_to_le.assumption
1568 |rewrite > sym_times.
1569 rewrite > assoc_times.
1570 rewrite < exp_plus_times.
1572 (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*(pred m))))
1573 [rewrite > assoc_times.
1575 rewrite < exp_plus_times.
1581 apply le_S.apply le_S.
1584 rewrite > plus_n_Sm in \vdash (? ? %);
1586 [change in \vdash (? % ?) with ((S (pred a + pred a)) + m);
1590 [rewrite > plus_n_Sm;rewrite > sym_plus;
1591 rewrite > plus_n_Sm;
1592 rewrite > H3;simplify in \vdash (? ? %);
1593 rewrite < plus_n_O;rewrite < S_pred;
1595 |apply lt_to_le;assumption]
1596 |apply lt_to_le;assumption]
1597 |apply lt_to_le;assumption]]
1599 rewrite > times_exp.
1600 apply monotonic_exp1.
1602 rewrite > sym_times.
1606 rewrite < plus_n_Sm.
1613 |rewrite < H4 in H3.
1617 apply le_S_S.apply le_S_S.apply le_O_n
1618 |apply not_lt_to_le.intro.
1619 apply (lt_to_not_le ? ? H1).
1621 apply (le_n_O_elim a)
1622 [apply le_S_S_to_le.assumption
1626 |elim (le_to_or_lt_eq O a (le_O_n ?))
1627 [apply (trans_le ? (A ((S(S O))*(S a))))
1630 rewrite > times_SSO.
1632 |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1634 |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1635 (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1637 apply (trans_le ? ? ? (H (S a) ? ?));
1641 rewrite > plus_n_SO.
1645 |apply le_S_S.assumption
1646 |simplify in ⊢ (? (? (? % ?) ?) ?);
1647 apply le_times_r;apply le_exp;
1648 [apply le_S;apply le_n
1649 |apply le_times_r;simplify;apply le_n]
1651 |rewrite > sym_times.
1652 rewrite > assoc_times.
1653 rewrite < exp_plus_times.
1655 change in ⊢ (? ? (? (? % ?) ?)) with ((S (S O))*a);
1656 rewrite < times_exp;
1657 rewrite < sym_times in \vdash (? ? (? % ?));
1658 rewrite > assoc_times;
1660 rewrite < times_n_Sm in ⊢ (? (? ? (? ? %)) ?);
1661 rewrite > sym_plus in \vdash (? (? ? %) ?);
1662 rewrite > assoc_plus in \vdash (? (? ? %) ?);
1663 rewrite > exp_plus_times;apply le_times_r;
1664 rewrite < distr_times_plus in ⊢ (? (? ? %) ?);
1665 simplify in ⊢ (? ? (? ? (? ? %)));rewrite < plus_n_O;
1670 |rewrite < H4 in H3.simplify in H3.
1672 apply (lt_to_not_le ? ? H1).
1679 theorem eq_sigma_pi_SO_n: \forall n.
1680 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1683 |rewrite > true_to_sigma_p_Sn
1684 [rewrite > H.reflexivity
1690 theorem leA_prim: \forall n.
1691 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1694 rewrite < (exp_sigma_p (S n) n primeb).
1696 rewrite < times_pi_p.
1699 rewrite > sym_times.
1700 change in ⊢ (? ? %) with (exp i (S (log i n))).
1703 apply prime_to_lt_SO.
1704 apply primeb_true_to_prime.
1709 theorem le_prim_log : \forall n,b.S O < b \to
1710 log b (A n) \leq prim n * (S (log b n)).
1711 intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?))
1719 (* the inequalities *)
1720 theorem le_exp_priml: \forall n. O < n \to
1721 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1723 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1724 [apply le_exp_B.assumption
1725 |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1727 apply (trans_le ? (A ((S(S O))*n)))
1734 alias num (instance 0) = "natural number".
1736 theorem le_exp_prim4l: \forall n. O < n \to
1737 exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
1739 apply (trans_le ? (2*(4*n*(B (4*n)))))
1740 [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
1745 apply lt_to_le.unfold.
1746 rewrite > times_n_SO in ⊢ (? % ?).
1747 apply le_times_r.assumption
1748 |rewrite < assoc_times.
1751 |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
1752 rewrite < assoc_times.
1753 rewrite > sym_times in ⊢ (? (? % ?) ?).
1754 rewrite > assoc_times.
1756 apply (trans_le ? (A (4*n)))
1757 [apply le_B_A4.assumption
1763 theorem le_priml: \forall n. O < n \to
1764 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1766 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1767 [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1770 |apply le_exp_priml.assumption
1772 |rewrite > sym_times in ⊢ (? ? %).
1780 theorem le_exp_primr: \forall n. S O < n \to
1781 exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * (pred n))).
1783 apply (trans_le ? (exp (A n) (S(S O))))
1784 [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
1785 rewrite < times_n_SO.
1787 |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n)))) (S(S O))))
1788 [apply monotonic_exp1.
1791 |rewrite < times_exp.
1792 rewrite > exp_exp_times.
1793 rewrite > exp_exp_times.
1794 rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
1795 rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).