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 funcion *)
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_fact_A:\forall n.S O < n \to
979 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
988 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
989 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
991 apply (le_times_to_le (exp (fact n) (S(S O))))
995 [rewrite < sym_times in ⊢ (? ? %).
997 rewrite < assoc_times.
1004 theorem le_B_exp: \forall n.
1005 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1009 [simplify.apply le_S.apply le_S.apply le_n
1010 |apply lt_SO_to_le_B_exp.
1011 apply le_S_S.apply lt_O_S.
1016 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1017 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1019 apply (le_times_to_le (exp (fact n) (S(S O))))
1022 |rewrite < assoc_times in ⊢ (? ? %).
1023 rewrite > sym_times in ⊢ (? ? (? % ?)).
1024 rewrite > assoc_times in ⊢ (? ? %).
1026 [rewrite < sym_times.
1028 apply lt_to_le.assumption
1034 theorem le_exp_B: \forall n. O < n \to
1035 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1039 |apply lt_SO_to_le_exp_B.
1040 apply le_S_S.assumption
1044 theorem eq_A_SSO_n: \forall n.O < n \to
1046 pi_p (S ((S(S O))*n)) primeb
1047 (\lambda p.(pi_p (log p ((S(S O))*n) )
1048 (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1051 rewrite > eq_A_A'.rewrite > eq_A_A'.
1054 pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1055 = pi_p (S ((S(S O))*n)) primeb
1056 (λ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))))))))
1058 rewrite < times_pi_p.
1059 apply eq_pi_p1;intros
1061 |rewrite < times_pi_p.
1062 apply eq_pi_p;intros
1064 |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1065 [simplify.rewrite < times_n_SO.apply times_n_SO
1066 |simplify.rewrite < plus_n_O.apply times_n_SO
1070 |apply (trans_eq ? ? (pi_p (S n) primeb
1071 (\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))))))))
1072 [apply eq_pi_p1;intros
1074 |apply eq_pi_p1;intros
1076 |rewrite > lt_to_leb_false
1077 [simplify.apply times_n_SO
1079 apply (trans_le ? (exp x (log x n)))
1081 [apply prime_to_lt_O.
1082 apply primeb_true_to_prime.
1092 |apply (trans_eq ? ?
1093 (pi_p (S ((S(S O))*n)) primeb
1094 (λp:nat.pi_p (log p n) (λi:nat.true)
1095 (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1097 apply or_false_eq_SO_to_eq_pi_p
1102 rewrite > lt_to_log_O
1108 |apply eq_pi_p1;intros
1111 apply or_false_eq_SO_to_eq_pi_p
1113 [apply prime_to_lt_SO.
1114 apply primeb_true_to_prime.
1120 rewrite > le_to_leb_true
1121 [simplify.reflexivity
1122 |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1124 apply prime_to_lt_SO.
1125 apply primeb_true_to_prime.
1128 [apply prime_to_lt_O.
1129 apply primeb_true_to_prime.
1131 |apply le_S_S.assumption
1142 theorem le_A_BA1: \forall n. O < n \to
1143 A((S(S O))*n) \le B((S(S O))*n)*A n.
1145 rewrite > eq_A_SSO_n
1148 apply le_pi_p.intros.
1149 apply le_pi_p.intros.
1151 [apply prime_to_lt_O.
1152 apply primeb_true_to_prime.
1154 |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1155 [simplify in ⊢ (? % ?).
1156 cut ((S(S O))*n/i\sup(S i1) = S O)
1157 [rewrite > Hcut.apply le_n
1158 |apply (div_mod_spec_to_eq
1159 ((S(S O))*n) (exp i (S i1))
1160 ? (mod ((S(S O))*n) (exp i (S i1)))
1161 ? (minus ((S(S O))*n) (exp i (S i1))) )
1162 [apply div_mod_spec_div_mod.
1164 apply prime_to_lt_O.
1165 apply primeb_true_to_prime.
1167 |cut (i\sup(S i1)≤(S(S O))*n)
1168 [apply div_mod_spec_intro
1169 [apply lt_plus_to_lt_minus
1171 |simplify in ⊢ (? % ?).
1174 [apply leb_true_to_le.assumption
1175 |apply leb_true_to_le.assumption
1178 |rewrite > sym_plus.
1179 rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1180 rewrite < times_n_SO.
1181 apply plus_minus_m_m.
1184 |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1186 [apply prime_to_lt_O.
1187 apply primeb_true_to_prime.
1192 rewrite > (times_n_O O) in ⊢ (? % ?).
1208 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1211 |apply le_A_BA1.apply lt_O_S
1215 theorem le_A_exp: \forall n.
1216 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1218 apply (trans_le ? (B((S(S O))*n)*A n))
1225 theorem le_A_exp1: \forall n.
1226 A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
1228 [simplify.apply le_S_S.apply le_O_n
1229 |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
1230 apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1232 |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))))
1235 |rewrite < exp_plus_times.
1236 simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
1243 theorem monotonic_A: monotonic nat le A.
1247 |apply (trans_le ? (A n1))
1250 cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1251 ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1252 [apply (bool_elim ? (primeb (S n1)));intro
1253 [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1254 rewrite > times_n_SO in ⊢ (? % ?).
1255 rewrite > sym_times.
1257 [apply lt_O_exp.apply lt_O_S
1260 |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1263 |apply le_pi_p.intros.
1265 [apply prime_to_lt_O.
1266 apply primeb_true_to_prime.
1269 [apply prime_to_lt_SO.
1270 apply primeb_true_to_prime.
1272 |apply le_S.apply le_n
1280 theorem le_A_exp2: \forall n. O < n \to
1281 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1283 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1288 |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1292 |rewrite > assoc_times.apply le_times_r.
1293 change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1303 theorem A_SO: A (S O) = S O.
1307 theorem A_SSO: A (S(S O)) = S (S O).
1311 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1315 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1320 theorem or_eq_eq_S: \forall n.\exists m.
1321 n = (S(S O))*m \lor n = S ((S(S O))*m).
1323 [apply (ex_intro ? ? O).
1326 [apply (ex_intro ? ? a).
1327 right.apply eq_f.assumption
1328 |apply (ex_intro ? ? (S a)).
1336 (* a better result *)
1337 theorem le_A_exp3: \forall n. S O < n \to
1338 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
1340 apply (nat_elim1 n).
1342 elim (or_eq_eq_S m).
1344 [elim (le_to_or_lt_eq (S O) a)
1345 [rewrite > H3 in ⊢ (? % ?).
1346 apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1348 |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1349 ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1353 rewrite > times_n_SO in ⊢ (? % ?).
1354 rewrite > sym_times.
1356 [apply lt_to_le.assumption
1361 |rewrite > sym_times.
1362 rewrite > assoc_times.
1363 rewrite < exp_plus_times.
1365 (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1366 [rewrite > assoc_times.
1368 rewrite < exp_plus_times.
1374 apply le_S.apply le_S.
1378 rewrite > times_exp.
1379 apply monotonic_exp1.
1381 rewrite > sym_times.
1385 rewrite < plus_n_Sm.
1392 |rewrite < H4 in H3.
1396 apply le_S_S.apply le_S_S.apply le_O_n
1397 |apply not_lt_to_le.intro.
1398 apply (lt_to_not_le ? ? H1).
1400 apply (le_n_O_elim a)
1401 [apply le_S_S_to_le.assumption
1405 |elim (le_to_or_lt_eq O a (le_O_n ?))
1406 [apply (trans_le ? (A ((S(S O))*(S a))))
1409 rewrite > times_SSO.
1411 |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1413 |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1414 (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1420 rewrite > plus_n_SO.
1424 |apply le_S_S.assumption
1426 |rewrite > sym_times.
1427 rewrite > assoc_times.
1428 rewrite < exp_plus_times.
1430 (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1431 [rewrite > assoc_times.
1433 rewrite < exp_plus_times.
1436 |rewrite > times_SSO.
1439 rewrite < plus_n_Sm.
1444 rewrite > times_exp.
1445 apply monotonic_exp1.
1447 rewrite > sym_times.
1453 |rewrite < H4 in H3.simplify in H3.
1455 apply (lt_to_not_le ? ? H1).
1462 theorem eq_sigma_pi_SO_n: \forall n.
1463 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1466 |rewrite > true_to_sigma_p_Sn
1467 [rewrite > H.reflexivity
1473 theorem leA_prim: \forall n.
1474 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1477 rewrite < (exp_sigma_p (S n) n primeb).
1479 rewrite < times_pi_p.
1482 rewrite > sym_times.
1483 change in ⊢ (? ? %) with (exp i (S (log i n))).
1486 apply prime_to_lt_SO.
1487 apply primeb_true_to_prime.
1492 (* the inequalities *)
1493 theorem le_exp_priml: \forall n. O < n \to
1494 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1496 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1497 [apply le_exp_B.assumption
1498 |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1500 apply (trans_le ? (A ((S(S O))*n)))
1507 theorem le_priml: \forall n. O < n \to
1508 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1510 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1511 [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1514 |apply le_exp_priml.assumption
1516 |rewrite > sym_times in ⊢ (? ? %).
1524 theorem le_exp_primr: \forall n. S O < n \to
1525 exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * n)).
1527 apply (trans_le ? (exp (A n) (S(S O))))
1528 [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
1529 rewrite < times_n_SO.
1531 |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O))))
1532 [apply monotonic_exp1.
1535 |rewrite < times_exp.
1536 rewrite > exp_exp_times.
1537 rewrite > exp_exp_times.
1538 rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
1539 rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).