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 (**************************************************************************)
16 include "nat/pi_p.ma".
17 include "nat/factorization.ma".
18 include "nat/factorial2.ma".
20 definition prim: nat \to nat \def
21 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
23 (* This is chebishev psi function *)
24 definition A: nat \to nat \def
25 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
27 theorem le_Al1: \forall n.
28 A n \le pi_p (S n) primeb (\lambda p.n).
39 theorem le_Al: \forall n.
40 A n \le exp n (prim n).
42 rewrite < exp_sigma_p.
46 theorem leA_r2: \forall n.
47 exp n (prim n) \le A n * A n.
49 elim (le_to_or_lt_eq ? ? (le_O_n n))
50 [rewrite < (exp_sigma_p (S n) n primeb).
55 rewrite < exp_plus_times.
56 apply (trans_le ? (exp i (S(log i n))))
60 apply primeb_true_to_prime.
64 apply primeb_true_to_prime.
77 |rewrite < H. apply le_n
81 (* an equivalent formulation for psi *)
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 (* factorization of n into primes *)
332 theorem pi_p_primeb_divides_b: \forall n. O < n \to
333 n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
335 apply lt_max_to_pi_p_primeb
342 theorem pi_p_primeb: \forall n. O < n \to
343 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
345 rewrite < eq_pi_p_primeb_divides_b.
346 apply pi_p_primeb_divides_b.
350 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
353 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
357 |apply lt_O_ord_rem;assumption
364 theorem sigma_p_divides_b:
365 \forall m,n,p. O < n \to prime p \to \lnot divides p n \to
366 m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
369 |simplify in ⊢ (? ? ? (? % ? ?)).
370 rewrite > true_to_sigma_p_Sn
371 [rewrite > sym_plus.rewrite < plus_n_SO.
373 rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
376 apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
378 apply divides_to_divides_b_true
382 |apply (witness ? ? ((exp p (n - x))*n1)).
383 rewrite < assoc_times.
384 rewrite < exp_plus_times.
386 [apply eq_f.simplify.
389 apply plus_minus_m_m.
390 apply lt_to_le.assumption
396 apply (divides_b_false_to_not_divides ? ? H5).
397 apply (witness ? ? ((exp p (n - S x))*n1)).
398 rewrite < assoc_times.
399 rewrite < exp_plus_times.
403 apply plus_minus_m_m.
410 |apply divides_to_divides_b_true
412 apply prime_to_lt_O.assumption
413 |apply (witness ? ? n1).reflexivity
419 theorem sigma_p_divides_b1:
420 \forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
421 m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
423 lapply (prime_to_lt_SO ? H1) as H4.
424 lapply (prime_to_lt_O ? H1) as H5.
425 rewrite > (false_to_eq_sigma_p m k)
426 [apply sigma_p_divides_b;assumption
429 apply not_divides_to_divides_b_false
430 [apply lt_O_exp.assumption
431 |intro.apply (le_to_not_lt ? ? H6).
433 rewrite < (ord_exp p)
434 [rewrite > (plus_n_O m).
435 rewrite < (not_divides_to_ord_O ? ? H1 H2).
436 rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
438 [apply divides_to_le_ord
439 [apply lt_O_exp.assumption
440 |rewrite > (times_n_O O).
442 [apply lt_O_exp.assumption
448 |apply lt_O_exp.assumption
458 theorem eq_ord_sigma_p:
459 \forall n,m,x. O < n \to prime x \to
460 exp x m \le n \to n < exp x (S m) \to
461 ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
463 lapply (prime_to_lt_SO ? H1).
464 rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
465 [apply sigma_p_divides_b1
466 [apply lt_O_ord_rem;assumption
468 |apply not_divides_ord_rem;assumption
470 apply (le_to_lt_to_lt ? (log x n))
471 [apply le_ord_log;assumption
472 |apply (lt_exp_to_lt x)
474 |apply (le_to_lt_to_lt ? n ? ? H3).
485 theorem pi_p_primeb1: \forall n. O < n \to
486 n = pi_p (S n) primeb
487 (\lambda p.(pi_p (log p n)
488 (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
490 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
494 rewrite > exp_sigma_p.
498 |apply primeb_true_to_prime.
500 |apply le_exp_log.assumption
502 apply prime_to_lt_SO.
503 apply primeb_true_to_prime.
509 (* the factorial function *)
510 theorem eq_fact_pi_p:\forall n. fact n =
511 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
514 |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
515 rewrite > true_to_pi_p_Sn
516 [apply eq_f.assumption
522 theorem eq_sigma_p_div: \forall n,q.O < q \to
523 sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
526 apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
527 [apply div_mod_spec_intro
528 [apply lt_mod_m_m.assumption
530 [simplify.elim q;reflexivity
531 |elim (or_div_mod1 n1 q)
533 rewrite > divides_to_mod_O
535 rewrite > true_to_sigma_p_Sn
536 [rewrite > H4 in ⊢ (? ? % ?).
541 apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
542 [apply div_mod_spec_div_mod.
544 |apply div_mod_spec_intro
545 [apply lt_mod_m_m.assumption
551 |apply true_to_true_to_andb_true
553 |apply divides_to_divides_b_true;assumption
560 rewrite > false_to_sigma_p_Sn
562 [rewrite < plus_n_Sm.
566 |elim (le_to_or_lt_eq (S (mod n1 q)) q)
570 apply (witness ? ? (S(div n1 q))).
571 rewrite < times_n_Sm.
573 rewrite < H2 in ⊢ (? ? ? (? ? %)).
580 |rewrite > not_divides_to_divides_b_false
581 [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
590 |apply div_mod_spec_div_mod.
595 (* still another characterization of the factorial *)
596 theorem fact_pi_p: \forall n. fact n =
598 (\lambda p.(pi_p (log p n)
599 (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
601 rewrite > eq_fact_pi_p.
603 (pi_p (S n) (λi:nat.leb (S O) i)
604 (λn.pi_p (S n) primeb
605 (\lambda p.(pi_p (log p n)
606 (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
607 [apply eq_pi_p1;intros
610 apply leb_true_to_le.assumption
613 (pi_p (S n) (λi:nat.leb (S O) i)
615 .pi_p (S n) (\lambda p.primeb p\land leb p n)
616 (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
619 |intros.apply eq_pi_p1
620 [intros.elim (primeb x1)
621 [simplify.apply sym_eq.
622 apply le_to_leb_true.
631 (pi_p (S n) (λi:nat.leb (S O) i)
633 .pi_p (S n) (λp:nat.primeb p∧leb p m)
634 (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
639 apply false_to_eq_pi_p
641 |intros.rewrite > lt_to_leb_false
642 [elim primeb;reflexivity|assumption]
645 |(* make a general theorem *)
649 .pi_p (S n) (λm.leb p m)
650 (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
654 apply (bool_elim ? (primeb y \land leb y x));intros
655 [rewrite > (le_to_leb_true (S O) x)
657 |apply (trans_le ? y)
658 [apply prime_to_lt_O.
659 apply primeb_true_to_prime.
660 apply (andb_true_true ? ? H2)
661 |apply leb_true_to_le.
662 apply (andb_true_true_r ? ? H2)
665 |elim (leb (S O) x);reflexivity
671 (pi_p (S n) (λm:nat.leb x m)
672 (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
677 apply false_to_eq_pi_p
679 [apply prime_to_lt_SO.
680 apply primeb_true_to_prime.
686 apply not_divides_to_divides_b_false
689 apply primeb_true_to_prime.
692 apply (lt_to_not_le x1 (exp x (S i)))
693 [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
695 apply prime_to_lt_SO.
696 apply primeb_true_to_prime.
699 [apply prime_to_lt_O.
700 apply primeb_true_to_prime.
707 [apply (lt_to_le_to_lt ? x)
708 [apply prime_to_lt_O.
709 apply primeb_true_to_prime.
711 |apply leb_true_to_le.
722 (pi_p (log x n) (λi:nat.true)
723 (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
724 [apply (pi_p_pi_p1 (\lambda m,i.x)).
730 rewrite > exp_sigma_p.
733 (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
736 apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
737 [apply (bool_elim ? (leb x x2));intro
738 [rewrite > le_to_leb_true
740 |apply (trans_le ? x)
741 [apply prime_to_lt_O.
742 apply primeb_true_to_prime.
744 |apply leb_true_to_le.
748 |rewrite > lt_to_leb_false
750 |apply not_le_to_lt.intro.
751 apply (leb_false_to_not_le ? ? H6).
752 apply (trans_le ? (exp x (S x1)))
753 [rewrite > times_n_SO in ⊢ (? % ?).
754 change with (exp x (S O) \le exp x (S x1)).
756 [apply prime_to_lt_O.
757 apply primeb_true_to_prime.
759 |apply le_S_S.apply le_O_n.
763 |apply divides_b_true_to_divides.
770 rewrite < andb_sym in ⊢ (? ? ? %).
775 |apply eq_sigma_p_div.
778 apply primeb_true_to_prime.
791 (* odd n is just mod n (S(S O))
795 | S m \Rightarrow (S O) - odd m
798 theorem le_odd_SO: \forall n. odd n \le S O.
801 |simplify.cases (odd n1)
802 [simplify.apply le_n.
808 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
810 [apply (lt_O_n_elim ? H).
811 intro.simplify.reflexivity
815 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
816 pi_p (S ((S(S O))*n)) primeb
817 (\lambda p.(pi_p (log p ((S(S O))*n))
818 (\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)))))))).
819 intros.rewrite > fact_pi_p.
822 |intros.apply eq_pi_p
825 rewrite < exp_plus_times.
827 rewrite > sym_times in ⊢ (? ? ? (? % ?)).
831 apply primeb_true_to_prime.
837 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
838 pi_p (S ((S(S O))*n)) primeb
839 (\lambda p.(pi_p (log p ((S(S O))*n))
840 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
841 pi_p (S ((S(S O))*n)) primeb
842 (\lambda p.(pi_p (log p ((S(S O))*n))
843 (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
845 rewrite < times_pi_p.
846 rewrite > fact_pi_p2.
853 theorem pi_p_primeb4: \forall n. S O < n \to
854 pi_p (S ((S(S O))*n)) primeb
855 (\lambda p.(pi_p (log p ((S(S O))*n))
856 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
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)))))))).
862 apply or_false_eq_SO_to_eq_pi_p
869 [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
870 rewrite < times_n_SO.
873 |simplify.rewrite < times_n_SO.assumption
877 |apply le_S_S_to_le.assumption
882 theorem pi_p_primeb5: \forall n. S O < n \to
883 pi_p (S ((S(S O))*n)) primeb
884 (\lambda p.(pi_p (log p ((S(S O))*n))
885 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
888 (\lambda p.(pi_p (log p n)
889 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
891 rewrite > (pi_p_primeb4 ? H).
892 apply eq_pi_p1;intros
894 |apply or_false_eq_SO_to_eq_pi_p
896 [apply prime_to_lt_SO.
897 apply primeb_true_to_prime.
904 [simplify.reflexivity
905 |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
907 apply prime_to_lt_SO.
908 apply primeb_true_to_prime.
911 [apply prime_to_lt_O.
912 apply primeb_true_to_prime.
923 theorem exp_fact_SSO: \forall n.
924 exp (fact n) (S(S O))
927 (\lambda p.(pi_p (log p n)
928 (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
942 (\lambda p.(pi_p (log p n)
943 (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
945 theorem B_SSSO: B 3 = 6.
949 theorem B_SSSSO: B 4 = 6.
953 theorem B_SSSSSO: B 5 = 30.
957 theorem B_SSSSSSO: B 6 = 20.
961 theorem B_SSSSSSSO: B 7 = 140.
965 theorem B_SSSSSSSSO: B 8 = 70.
969 theorem eq_fact_B:\forall n.S O < n \to
970 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
972 rewrite > fact_pi_p3.
975 rewrite > pi_p_primeb5
983 theorem le_B_A: \forall n. B n \le A n.
987 apply le_pi_p.intros.
988 apply le_pi_p.intros.
989 rewrite > exp_n_SO in ⊢ (? ? %).
991 [apply prime_to_lt_O.
992 apply primeb_true_to_prime.
1000 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).
1004 cut ((S(S O)) < (S ((S(S(S(S O))))*n)))
1005 [cut (O<log (S(S O)) ((S(S(S(S O))))*n))
1006 [rewrite > (pi_p_gi ? ? (S(S O)))
1007 [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %)
1008 [rewrite < assoc_times.
1010 [rewrite > (pi_p_gi ? ? O)
1011 [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %)
1012 [rewrite < assoc_times.
1014 [rewrite < exp_n_SO.
1015 change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?)
1016 with ((S(S O))*(S(S O))).
1017 rewrite > assoc_times.
1018 rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?).
1019 rewrite > lt_O_to_div_times
1020 [rewrite > divides_to_mod_O
1023 |apply (witness ? ? n).reflexivity
1027 |apply le_pi_p.intros.
1028 rewrite > exp_n_SO in ⊢ (? ? %).
1031 |apply le_S_S_to_le.
1042 |apply le_pi_p.intros.
1043 apply le_pi_p.intros.
1044 rewrite > exp_n_SO in ⊢ (? ? %).
1046 [apply prime_to_lt_O.
1047 apply primeb_true_to_prime.
1048 apply (andb_true_true ? ? H2)
1049 |apply le_S_S_to_le.
1061 [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?).
1066 |rewrite > times_n_SO in ⊢ (? % ?).
1068 [apply le_S.apply le_S.apply le_n
1074 rewrite > times_n_SO in ⊢ (? % ?).
1076 [apply le_S.apply le_n_Sn
1082 theorem le_fact_A:\forall n.S O < n \to
1083 fact (2*n) \le exp (fact n) 2 * A (2*n).
1092 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
1093 B (2*n) \le exp 2 (pred (2*n)).
1095 apply (le_times_to_le (exp (fact n) (S(S O))))
1098 |rewrite < eq_fact_B
1099 [rewrite < sym_times in ⊢ (? ? %).
1101 rewrite < assoc_times.
1108 theorem le_B_exp: \forall n.
1109 B (2*n) \le exp 2 (pred (2*n)).
1113 [simplify.apply le_n
1114 |apply lt_SO_to_le_B_exp.
1115 apply le_S_S.apply lt_O_S.
1120 theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to
1121 B (2*n) \le exp 2 ((2*n)-2).
1123 apply (le_times_to_le (exp (fact n) (S(S O))))
1126 |rewrite < eq_fact_B
1127 [rewrite < sym_times in ⊢ (? ? %).
1129 rewrite < assoc_times.
1130 apply lt_SSSSO_to_fact.assumption
1131 |apply lt_to_le.apply lt_to_le.
1132 apply lt_to_le.assumption
1137 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1138 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1140 apply (le_times_to_le (exp (fact n) (S(S O))))
1143 |rewrite < assoc_times in ⊢ (? ? %).
1144 rewrite > sym_times in ⊢ (? ? (? % ?)).
1145 rewrite > assoc_times in ⊢ (? ? %).
1147 [rewrite < sym_times.
1149 apply lt_to_le.assumption
1155 theorem le_exp_B: \forall n. O < n \to
1156 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1160 |apply lt_SO_to_le_exp_B.
1161 apply le_S_S.assumption
1165 theorem eq_A_SSO_n: \forall n.O < n \to
1167 pi_p (S ((S(S O))*n)) primeb
1168 (\lambda p.(pi_p (log p ((S(S O))*n) )
1169 (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1172 rewrite > eq_A_A'.rewrite > eq_A_A'.
1175 pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1176 = pi_p (S ((S(S O))*n)) primeb
1177 (λ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))))))))
1179 rewrite < times_pi_p.
1180 apply eq_pi_p1;intros
1182 |rewrite < times_pi_p.
1183 apply eq_pi_p;intros
1185 |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1186 [simplify.rewrite < times_n_SO.apply times_n_SO
1187 |simplify.rewrite < plus_n_O.apply times_n_SO
1191 |apply (trans_eq ? ? (pi_p (S n) primeb
1192 (\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))))))))
1193 [apply eq_pi_p1;intros
1195 |apply eq_pi_p1;intros
1197 |rewrite > lt_to_leb_false
1198 [simplify.apply times_n_SO
1200 apply (trans_le ? (exp x (log x n)))
1202 [apply prime_to_lt_O.
1203 apply primeb_true_to_prime.
1213 |apply (trans_eq ? ?
1214 (pi_p (S ((S(S O))*n)) primeb
1215 (λp:nat.pi_p (log p n) (λi:nat.true)
1216 (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1218 apply or_false_eq_SO_to_eq_pi_p
1223 rewrite > lt_to_log_O
1229 |apply eq_pi_p1;intros
1232 apply or_false_eq_SO_to_eq_pi_p
1234 [apply prime_to_lt_SO.
1235 apply primeb_true_to_prime.
1241 rewrite > le_to_leb_true
1242 [simplify.reflexivity
1243 |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1245 apply prime_to_lt_SO.
1246 apply primeb_true_to_prime.
1249 [apply prime_to_lt_O.
1250 apply primeb_true_to_prime.
1252 |apply le_S_S.assumption
1263 theorem le_A_BA1: \forall n. O < n \to
1264 A((S(S O))*n) \le B((S(S O))*n)*A n.
1266 rewrite > eq_A_SSO_n
1269 apply le_pi_p.intros.
1270 apply le_pi_p.intros.
1272 [apply prime_to_lt_O.
1273 apply primeb_true_to_prime.
1275 |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1276 [simplify in ⊢ (? % ?).
1277 cut ((S(S O))*n/i\sup(S i1) = S O)
1278 [rewrite > Hcut.apply le_n
1279 |apply (div_mod_spec_to_eq
1280 ((S(S O))*n) (exp i (S i1))
1281 ? (mod ((S(S O))*n) (exp i (S i1)))
1282 ? (minus ((S(S O))*n) (exp i (S i1))) )
1283 [apply div_mod_spec_div_mod.
1285 apply prime_to_lt_O.
1286 apply primeb_true_to_prime.
1288 |cut (i\sup(S i1)≤(S(S O))*n)
1289 [apply div_mod_spec_intro
1290 [apply lt_plus_to_lt_minus
1292 |simplify in ⊢ (? % ?).
1295 [apply leb_true_to_le.assumption
1296 |apply leb_true_to_le.assumption
1299 |rewrite > sym_plus.
1300 rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1301 rewrite < times_n_SO.
1302 apply plus_minus_m_m.
1305 |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1307 [apply prime_to_lt_O.
1308 apply primeb_true_to_prime.
1313 rewrite > (times_n_O O) in ⊢ (? % ?).
1329 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1332 |apply le_A_BA1.apply lt_O_S
1336 theorem le_A_exp: \forall n.
1337 A(2*n) \le (exp 2 (pred (2*n)))*A n.
1339 apply (trans_le ? (B(2*n)*A n))
1346 theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to
1347 A(2*n) \le exp 2 ((2*n)-2)*A n.
1349 apply (trans_le ? (B(2*n)*A n))
1352 apply lt_SSSSO_to_le_B_exp.assumption
1356 theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n).
1359 |simplify.apply le_plus_r.
1364 theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n.
1368 |rewrite > times_SSO.
1370 apply (trans_le ? (2*n1))
1377 theorem le_A_exp1: \forall n.
1378 A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))).
1380 [simplify.apply le_n
1381 |change in ⊢ (? % ?) with (A(2*(exp 2 n1))).
1382 apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1384 |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1))))
1387 |rewrite < exp_plus_times.
1390 |cut (S(S n1) \le 2*(exp 2 n1))
1391 [apply le_S_S_to_le.
1392 change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))).
1394 [rewrite > eq_minus_S_pred in ⊢ (? ? %).
1396 [rewrite < eq_minus_plus_plus_minus
1397 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1401 |apply lt_to_lt_O_minus.
1402 apply (lt_to_le_to_lt ? (2*(S(S n1))))
1403 [rewrite > times_n_SO in ⊢ (? % ?).
1404 rewrite > sym_times.
1413 |unfold.rewrite > times_n_SO in ⊢ (? % ?).
1422 |apply (trans_le ? (2*(S(S n2))))
1423 [apply le_S_times_SSO.
1436 theorem monotonic_A: monotonic nat le A.
1440 |apply (trans_le ? (A n1))
1443 cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1444 ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1445 [apply (bool_elim ? (primeb (S n1)));intro
1446 [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1447 rewrite > times_n_SO in ⊢ (? % ?).
1448 rewrite > sym_times.
1450 [apply lt_O_exp.apply lt_O_S
1453 |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1456 |apply le_pi_p.intros.
1458 [apply prime_to_lt_O.
1459 apply primeb_true_to_prime.
1462 [apply prime_to_lt_SO.
1463 apply primeb_true_to_prime.
1465 |apply le_S.apply le_n
1474 theorem le_A_exp2: \forall n. O < n \to
1475 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1477 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1482 |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1486 |rewrite > assoc_times.apply le_times_r.
1487 change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1498 theorem A_SO: A (S O) = S O.
1502 theorem A_SSO: A (S(S O)) = S (S O).
1506 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1510 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1515 theorem or_eq_eq_S: \forall n.\exists m.
1516 n = (S(S O))*m \lor n = S ((S(S O))*m).
1518 [apply (ex_intro ? ? O).
1521 [apply (ex_intro ? ? a).
1522 right.apply eq_f.assumption
1523 |apply (ex_intro ? ? (S a)).
1532 (* a better result *)
1533 theorem le_A_exp3: \forall n. S O < n \to
1534 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
1536 apply (nat_elim1 n).
1538 elim (or_eq_eq_S m).
1540 [elim (le_to_or_lt_eq (S O) a)
1541 [rewrite > H3 in ⊢ (? % ?).
1542 apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1544 |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1545 ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1549 rewrite > times_n_SO in ⊢ (? % ?).
1550 rewrite > sym_times.
1552 [apply lt_to_le.assumption
1557 |rewrite > sym_times.
1558 rewrite > assoc_times.
1559 rewrite < exp_plus_times.
1561 (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1562 [rewrite > assoc_times.
1564 rewrite < exp_plus_times.
1570 apply le_S.apply le_S.
1574 rewrite > times_exp.
1575 apply monotonic_exp1.
1577 rewrite > sym_times.
1581 rewrite < plus_n_Sm.
1588 |rewrite < H4 in H3.
1592 apply le_S_S.apply le_S_S.apply le_O_n
1593 |apply not_lt_to_le.intro.
1594 apply (lt_to_not_le ? ? H1).
1596 apply (le_n_O_elim a)
1597 [apply le_S_S_to_le.assumption
1601 |elim (le_to_or_lt_eq O a (le_O_n ?))
1602 [apply (trans_le ? (A ((S(S O))*(S a))))
1605 rewrite > times_SSO.
1607 |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1609 |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1610 (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1616 rewrite > plus_n_SO.
1620 |apply le_S_S.assumption
1622 |rewrite > sym_times.
1623 rewrite > assoc_times.
1624 rewrite < exp_plus_times.
1626 (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1627 [rewrite > assoc_times.
1629 rewrite < exp_plus_times.
1632 |rewrite > times_SSO.
1635 rewrite < plus_n_Sm.
1640 rewrite > times_exp.
1641 apply monotonic_exp1.
1643 rewrite > sym_times.
1649 |rewrite < H4 in H3.simplify in H3.
1651 apply (lt_to_not_le ? ? H1).
1659 theorem le_A_exp4: \forall n. S O < n \to
1660 A(n) \le (pred n)*exp 2 ((2 * n) -3).
1662 apply (nat_elim1 n).
1664 elim (or_eq_eq_S m).
1666 [elim (le_to_or_lt_eq (S O) a)
1667 [rewrite > H3 in ⊢ (? % ?).
1668 apply (trans_le ? (exp 2 (pred(2*a))*A a))
1670 |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
1674 rewrite > times_n_SO in ⊢ (? % ?).
1675 rewrite > sym_times.
1677 [apply lt_to_le.assumption
1683 rewrite < assoc_times.
1684 rewrite > sym_times in ⊢ (? (? % ?) ?).
1685 rewrite > assoc_times.
1688 elim a[apply le_n|simplify.apply le_plus_n_r]
1689 |rewrite < exp_plus_times.
1692 |apply (trans_le ? (m+(m-3)))
1694 cases m[apply le_n|apply le_n_Sn]
1695 |simplify.rewrite < plus_n_O.
1696 rewrite > eq_minus_plus_plus_minus
1699 apply (trans_le ? (2*2))
1700 [simplify.apply (le_n_Sn 3)
1701 |apply le_times_r.assumption
1709 |rewrite > H3.rewrite < H4.simplify.
1710 apply le_S_S.apply lt_O_S
1711 |apply not_lt_to_le.intro.
1712 apply (lt_to_not_le ? ? H1).
1714 apply (le_n_O_elim a)
1715 [apply le_S_S_to_le.assumption
1719 |elim (le_to_or_lt_eq O a (le_O_n ?))
1720 [apply (trans_le ? (A ((S(S O))*(S a))))
1723 rewrite > times_SSO.
1725 |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a)))
1727 |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
1732 apply le_S_times_SSO.
1734 |apply le_S_S.assumption
1737 change in ⊢ (? ? (? % ?)) with (2*a).
1738 rewrite > times_SSO.
1739 change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)).
1740 rewrite > minus_Sn_m
1741 [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))).
1742 rewrite < assoc_times in ⊢ (? (? ? %) ?).
1743 rewrite < assoc_times.
1744 rewrite > sym_times in ⊢ (? (? % ?) ?).
1745 rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
1746 rewrite > assoc_times.
1748 rewrite < exp_plus_times.
1751 |rewrite < eq_minus_plus_plus_minus
1752 [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?).
1755 apply O_lt_const_to_le_times_const.
1760 apply O_lt_const_to_le_times_const.
1766 |rewrite < H4 in H3.simplify in H3.
1768 apply (lt_to_not_le ? ? H1).
1775 theorem le_n_SSSSSSSSO_to_le_A_exp:
1776 \forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3).
1784 [intro.apply leb_true_to_le.reflexivity
1786 [intro.apply leb_true_to_le.reflexivity
1788 [intro.apply leb_true_to_le.reflexivity
1790 [intro.apply leb_true_to_le.reflexivity
1792 [intro.apply leb_true_to_le.reflexivity
1794 [intro.apply leb_true_to_le.reflexivity
1795 |intro.apply False_ind.
1796 apply (lt_to_not_le ? ? H).
1797 apply leb_true_to_le.reflexivity
1809 theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3).
1811 apply (nat_elim1 n).
1813 elim (decidable_le 9 m)
1814 [elim (or_eq_eq_S m).
1816 [rewrite > H3 in ⊢ (? % ?).
1817 apply (trans_le ? (exp 2 (pred(2*a))*A a))
1819 |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
1824 [apply (trans_lt ? 4)
1826 |apply (lt_times_to_lt 2)
1828 |rewrite < H3.assumption
1834 rewrite < exp_plus_times.
1837 |simplify.rewrite < plus_n_O.
1838 rewrite > eq_minus_plus_plus_minus
1841 |apply (trans_le ? 9)
1842 [apply leb_true_to_le. reflexivity
1849 |apply (trans_le ? (A (2*(S a))))
1852 rewrite > times_SSO.
1854 |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
1855 [apply lt_SSSSO_to_le_A_exp.
1857 apply (le_times_to_le 2)
1859 |apply le_S_S_to_le.rewrite < H3.assumption
1861 |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
1867 [apply (lt_to_le_to_lt ? 4)
1869 |apply (le_times_to_le 2)
1871 |apply le_S_S_to_le.
1872 rewrite < H3.assumption
1877 |rewrite > times_SSO.
1879 rewrite < exp_plus_times.
1887 rewrite < minus_n_O.
1889 rewrite < plus_n_Sm.
1890 simplify.rewrite < minus_n_O.
1891 rewrite < plus_n_Sm.
1900 |apply le_n_SSSSSSSSO_to_le_A_exp.
1907 theorem eq_sigma_pi_SO_n: \forall n.
1908 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1911 |rewrite > true_to_sigma_p_Sn
1912 [rewrite > H.reflexivity
1918 theorem leA_prim: \forall n.
1919 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1922 rewrite < (exp_sigma_p (S n) n primeb).
1924 rewrite < times_pi_p.
1927 rewrite > sym_times.
1928 change in ⊢ (? ? %) with (exp i (S (log i n))).
1931 apply prime_to_lt_SO.
1932 apply primeb_true_to_prime.
1937 theorem le_prim_log : \forall n,b.S O < b \to
1938 log b (A n) \leq prim n * (S (log b n)).
1939 intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?))
1947 (* the inequalities *)
1948 theorem le_exp_priml: \forall n. O < n \to
1949 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1951 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1952 [apply le_exp_B.assumption
1953 |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1955 apply (trans_le ? (A ((S(S O))*n)))
1962 theorem le_exp_prim4l: \forall n. O < n \to
1963 exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))).
1965 apply (trans_le ? (2*(4*n*(B (4*n)))))
1966 [change in ⊢ (? % ?) with (2*(exp 2 (4*n))).
1971 apply lt_to_le.unfold.
1972 rewrite > times_n_SO in ⊢ (? % ?).
1973 apply le_times_r.assumption
1974 |rewrite < assoc_times.
1977 |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))).
1978 rewrite < assoc_times.
1979 rewrite > sym_times in ⊢ (? (? % ?) ?).
1980 rewrite > assoc_times.
1982 apply (trans_le ? (A (4*n)))
1983 [apply le_B_A4.assumption
1989 theorem le_priml: \forall n. O < n \to
1990 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1992 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1993 [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1996 |apply le_exp_priml.assumption
1998 |rewrite > sym_times in ⊢ (? ? %).
2006 theorem le_exp_primr: \forall n.
2007 exp n (prim n) \le exp 2 (2*(2*n-3)).
2009 apply (trans_le ? (exp (A n) 2))
2010 [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
2011 rewrite < times_n_SO.
2013 |rewrite > sym_times.
2014 rewrite < exp_exp_times.
2015 apply monotonic_exp1.