helm/software/matita/library/nat/chebyshev.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/chebishev".
  16
  17 include "nat/log.ma".
  18 include "nat/pi_p.ma".
  19 include "nat/factorization.ma".
  20 include "nat/factorial2.ma".
  21
  22 definition prim: nat \to nat \def
  23 \lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
  24
  25 definition A: nat \to nat \def
  26 \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
  27
  28 theorem le_Al1: \forall n.
  29 A n \le pi_p (S n) primeb (\lambda p.n).
  30 intro.unfold A.
  31 cases n
  32   [simplify.apply le_n
  33   |apply le_pi_p.
  34    intros.
  35    apply le_exp_log.
  36    apply lt_O_S
  37   ]
  38 qed.
  39
  40 theorem le_Al: \forall n.
  41 A n \le exp n (prim n).
  42 intro.unfold prim.
  43 rewrite < exp_sigma_p.
  44 apply le_Al1.
  45 qed.
  46
  47 theorem leA_r2: \forall n.
  48 exp n (prim n) \le A n * A n.
  49 intro.unfold prim.
  50 elim (le_to_or_lt_eq ? ? (le_O_n n))
  51   [rewrite < (exp_sigma_p (S n) n primeb).
  52    unfold A.
  53    rewrite < times_pi_p.
  54    apply le_pi_p.
  55    intros.
  56    rewrite < exp_plus_times.
  57    apply (trans_le ? (exp i (S(log i n))))
  58     [apply lt_to_le.
  59      apply lt_exp_log.
  60      apply prime_to_lt_SO.
  61      apply primeb_true_to_prime.
  62      assumption
  63     |apply le_exp
  64       [apply prime_to_lt_O.
  65        apply primeb_true_to_prime.
  66        assumption
  67       |rewrite > plus_n_O.
  68        simplify.
  69        rewrite > plus_n_Sm.
  70        apply le_plus_r.
  71        apply lt_O_log
  72         [assumption
  73         |apply le_S_S_to_le.
  74          apply H1
  75         ]
  76       ]
  77     ]
  78   |rewrite < H. apply le_n
  79   ]
  80 qed.
  81
  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))).
  85
  86 theorem eq_A_A': \forall n.A n = A' n.
  87 intro.unfold A.unfold A'.
  88 apply eq_pi_p
  89   [intros.reflexivity
  90   |intros.
  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
  94     ]
  95   ]
  96 qed.
  97
  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)).
 101 intro.
 102 elim n
 103   [reflexivity
 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
 108           [apply eq_f.
 109            apply H
 110           |apply true_to_true_to_andb_true;assumption
 111           ]
 112         |rewrite > false_to_pi_p_Sn
 113           [rewrite > not_divides_to_ord_O
 114             [simplify in ⊢ (? ? ? (? % ?)).
 115              rewrite > sym_times.
 116              rewrite < times_n_SO.
 117              apply H
 118             |apply primeb_true_to_prime.assumption
 119             |apply divides_b_false_to_not_divides.
 120              assumption
 121             ]
 122           |rewrite > H1.rewrite > H2.reflexivity
 123           ]
 124         ]
 125       |assumption
 126       ]
 127     |rewrite > false_to_pi_p_Sn
 128       [rewrite > false_to_pi_p_Sn
 129         [apply H
 130         |assumption
 131         ]
 132       |rewrite > H1.reflexivity
 133       ]
 134     ]
 135   ]
 136 qed.
 137
 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)).
 140 intro.elim q
 141   [apply False_ind.
 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 ⊢ (? ? % ?)
 146         [apply eq_f.
 147          rewrite > (H (ord_rem m n))
 148           [apply eq_pi_p1
 149             [intros.
 150              apply (bool_elim ? (primeb x));intro
 151               [simplify.
 152                apply (bool_elim ? (divides_b x (ord_rem m n)));intro
 153                 [apply sym_eq.
 154                  apply divides_to_divides_b_true
 155                   [apply prime_to_lt_O.
 156                    apply primeb_true_to_prime.
 157                    assumption
 158                   |apply (trans_divides ? (ord_rem m n))
 159                     [apply divides_b_true_to_divides.
 160                      assumption
 161                     |apply divides_ord_rem
 162                       [apply (trans_lt ? x)
 163                         [apply prime_to_lt_SO.
 164                          apply primeb_true_to_prime.
 165                          assumption
 166                         |assumption
 167                         ]
 168                       |assumption
 169                       ]
 170                     ]
 171                   ]
 172                 |apply sym_eq.
 173                  apply not_divides_to_divides_b_false
 174                   [apply prime_to_lt_O.
 175                    apply primeb_true_to_prime.
 176                    assumption
 177                   |apply ord_O_to_not_divides
 178                     [assumption
 179                     |apply primeb_true_to_prime.
 180                      assumption
 181                     |rewrite < (ord_ord_rem n)
 182                       [apply not_divides_to_ord_O
 183                         [apply primeb_true_to_prime.
 184                          assumption
 185                         |apply divides_b_false_to_not_divides.
 186                          assumption
 187                         ]
 188                       |assumption
 189                       |apply primeb_true_to_prime.
 190                        apply (andb_true_true ? ? H3)
 191                       |apply primeb_true_to_prime.
 192                        assumption
 193                       |assumption
 194                       ]
 195                     ]
 196                   ]
 197                 ]
 198               |reflexivity
 199               ]
 200             |intros.
 201              apply eq_f.
 202              apply ord_ord_rem
 203               [assumption
 204               |apply primeb_true_to_prime.
 205                apply (andb_true_true ? ? H3)
 206               |apply primeb_true_to_prime.
 207                apply (andb_true_true ? ? H5)
 208               |assumption
 209               ]
 210             ]
 211           |apply lt_O_ord_rem
 212             [apply prime_to_lt_SO.
 213              apply primeb_true_to_prime.
 214              apply (andb_true_true ? ? H3)
 215             |assumption
 216             ]
 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))
 219               [elim H4.
 220                intro.rewrite > H7 in H6.simplify in H6.
 221                apply (not_divides_ord_rem m n)
 222                 [assumption
 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)
 228                 ]
 229               |elim H4.rewrite > H6.
 230                apply lt_to_not_eq.
 231                apply prime_to_lt_O.
 232                apply primeb_true_to_prime.
 233                apply (andb_true_true ? ? H3)
 234               ]
 235             |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
 236               [apply le_to_le_max.
 237                apply divides_to_le
 238                 [assumption
 239                 |apply divides_ord_rem
 240                   [apply prime_to_lt_SO.
 241                    apply primeb_true_to_prime.
 242                    apply (andb_true_true ? ? H3)
 243                   |assumption
 244                   ]
 245                 ]
 246               |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
 247                 [apply le_max_f_max_g.
 248                  intros.
 249                  apply (bool_elim ? (primeb i));intro
 250                   [simplify.
 251                    apply divides_to_divides_b_true
 252                     [apply prime_to_lt_O.
 253                      apply primeb_true_to_prime.
 254                      assumption
 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)
 262                         |assumption
 263                         ]
 264                       ]
 265                     ]
 266                   |rewrite > H6 in H5.
 267                    assumption
 268                   ]
 269                 |apply le_S_S_to_le.
 270                  assumption
 271                 ]
 272               ]
 273             ]
 274           ]
 275         |apply prime_to_lt_SO.
 276          apply primeb_true_to_prime.
 277          apply (andb_true_true ? ? H3)
 278         |assumption
 279         ]
 280       |assumption
 281       ]
 282     |elim (le_to_or_lt_eq ? ? H1)
 283       [rewrite > false_to_pi_p_Sn
 284         [apply H
 285           [assumption
 286           |apply false_to_lt_max
 287             [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
 288               [apply lt_to_le.
 289                apply lt_SO_max_prime.
 290                assumption
 291               |apply le_S_S_to_le.
 292                assumption
 293               ]
 294             |assumption
 295             |apply le_S_S_to_le.
 296              assumption
 297             ]
 298           ]
 299         |assumption
 300         ]
 301       |rewrite < H4.
 302        rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
 303        apply eq_pi_p
 304         [intros.
 305          apply (bool_elim ? (primeb x));intro
 306           [apply sym_eq.
 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.
 311              assumption
 312             |intro.
 313              apply (le_to_not_lt x (S O))
 314               [apply divides_to_le
 315                 [apply lt_O_S.assumption
 316                 |assumption
 317                 ]
 318               |elim (primeb_true_to_prime ? H6).
 319                assumption
 320               ]
 321             ]
 322           |reflexivity
 323           ]
 324         |intros.reflexivity
 325         ]
 326       ]
 327     ]
 328   ]
 329 qed.
 330
 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)).
 333 intros.
 334 apply lt_max_to_pi_p_primeb
 335   [assumption
 336   |apply le_S_S.
 337    apply le_max_n
 338   ]
 339 qed.
 340
 341 theorem pi_p_primeb: \forall n. O < n \to
 342 n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
 343 intros.
 344 rewrite < eq_pi_p_primeb_divides_b.
 345 apply pi_p_primeb_divides_b.
 346 assumption.
 347 qed.
 348
 349 theorem le_ord_log: \forall n,p. O < n \to S O < p \to
 350 ord n p \le log p n.
 351 intros.
 352 rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
 353   [rewrite > log_exp
 354     [apply le_plus_n_r
 355     |assumption
 356     |apply lt_O_ord_rem;assumption
 357     ]
 358   |assumption
 359   |assumption
 360   ]
 361 qed.
 362
 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).
 366 intro.elim m
 367   [reflexivity
 368   |simplify in ⊢ (? ? ? (? % ? ?)).
 369    rewrite > true_to_sigma_p_Sn
 370     [rewrite > sym_plus.rewrite < plus_n_SO.
 371      apply eq_f.
 372      rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
 373      apply eq_sigma_p1
 374       [intros.
 375        apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
 376         [apply sym_eq.
 377          apply divides_to_divides_b_true
 378           [apply lt_O_exp.
 379            apply prime_to_lt_O.
 380            assumption
 381           |apply (witness ? ? ((exp p (n - x))*n1)).
 382            rewrite < assoc_times.
 383            rewrite < exp_plus_times.
 384            apply eq_f2
 385             [apply eq_f.simplify.
 386              apply eq_f.
 387              rewrite > sym_plus.
 388              apply plus_minus_m_m.
 389              apply lt_to_le.assumption
 390             |reflexivity
 391             ]
 392           ]
 393         |apply sym_eq.
 394          apply False_ind.
 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.
 399          apply eq_f2
 400           [apply eq_f.
 401            rewrite > sym_plus.
 402            apply plus_minus_m_m.
 403            assumption
 404           |reflexivity
 405           ]
 406         ]
 407       |intros.reflexivity
 408       ]
 409     |apply divides_to_divides_b_true
 410       [apply lt_O_exp.
 411        apply prime_to_lt_O.assumption
 412       |apply (witness ? ? n1).reflexivity
 413       ]
 414     ]
 415   ]
 416 qed.
 417
 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).
 421 intros.
 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
 426   |assumption
 427   |intros.
 428    apply not_divides_to_divides_b_false
 429     [apply lt_O_exp.assumption
 430     |intro.apply (le_to_not_lt ? ? H6).
 431      unfold lt.
 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 ⊢ (? ? (? % ?)).
 436        rewrite < ord_times
 437         [apply divides_to_le_ord
 438           [apply lt_O_exp.assumption
 439           |rewrite > (times_n_O O).
 440            apply lt_times
 441             [apply lt_O_exp.assumption
 442             |assumption
 443             ]
 444           |assumption
 445           |assumption
 446           ]
 447         |apply lt_O_exp.assumption
 448         |assumption
 449         |assumption
 450         ]
 451       |assumption
 452       ]
 453     ]
 454   ]
 455 qed.
 456
 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).
 461 intros.
 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
 466     |assumption
 467     |apply not_divides_ord_rem;assumption
 468     |apply lt_S_to_le.
 469      apply (le_to_lt_to_lt ? (log x n))
 470       [apply le_ord_log;assumption
 471       |apply (lt_exp_to_lt x)
 472         [assumption
 473         |apply (le_to_lt_to_lt ? n ? ? H3).
 474          apply le_exp_log.
 475          assumption
 476         ]
 477       ]
 478     ]
 479   |assumption
 480   |assumption
 481   ]
 482 qed.
 483
 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))).
 488 intros.
 489 rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
 490 apply eq_pi_p1
 491   [intros.reflexivity
 492   |intros.
 493    rewrite > exp_sigma_p.
 494    apply eq_f.
 495    apply eq_ord_sigma_p
 496     [assumption
 497     |apply primeb_true_to_prime.
 498      assumption
 499     |apply le_exp_log.assumption
 500     |apply lt_exp_log.
 501      apply prime_to_lt_SO.
 502      apply primeb_true_to_prime.
 503      assumption
 504     ]
 505   ]
 506 qed.
 507
 508 theorem eq_fact_pi_p:\forall n. fact n =
 509 pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
 510 intro.elim n
 511   [reflexivity
 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
 515     |reflexivity
 516     ]
 517   ]
 518 qed.
 519
 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)
 522 =n/q.
 523 intros.
 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
 527     |elim n
 528       [simplify.elim q;reflexivity
 529       |elim (or_div_mod1 n1 q)
 530         [elim H2.clear H2.
 531          rewrite > divides_to_mod_O
 532           [rewrite < plus_n_O.
 533            rewrite > true_to_sigma_p_Sn
 534             [rewrite > H4 in ⊢ (? ? % ?).
 535              apply eq_f2
 536               [rewrite < sym_plus.
 537                rewrite < plus_n_SO.
 538                apply eq_f.
 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.
 541                  assumption
 542                 |apply div_mod_spec_intro
 543                   [apply lt_mod_m_m.assumption
 544                   |assumption
 545                   ]
 546                 ]
 547               |reflexivity
 548               ]
 549             |apply true_to_true_to_andb_true
 550               [reflexivity
 551               |apply divides_to_divides_b_true;assumption
 552               ]
 553             ]
 554           |assumption
 555           |assumption
 556           ]
 557         |elim H2.clear H2.
 558          rewrite > false_to_sigma_p_Sn
 559           [rewrite > mod_S
 560             [rewrite < plus_n_Sm.
 561              apply eq_f.
 562              assumption
 563             |assumption
 564             |elim (le_to_or_lt_eq (S (mod n1 q)) q)
 565               [assumption
 566               |apply False_ind.
 567                apply H3.
 568                apply (witness ? ? (S(div n1 q))).
 569                rewrite < times_n_Sm.
 570                rewrite < sym_plus.
 571                rewrite < H2 in ⊢ (? ? ? (? ? %)).
 572                rewrite > sym_times.
 573                assumption
 574               |apply lt_mod_m_m.
 575                assumption
 576               ]
 577             ]
 578           |rewrite > not_divides_to_divides_b_false
 579             [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
 580             |assumption
 581             |assumption
 582             ]
 583           ]
 584         |assumption
 585         ]
 586       ]
 587     ]
 588   |apply div_mod_spec_div_mod.
 589    assumption
 590   ]
 591 qed.
 592
 593 theorem fact_pi_p: \forall n. fact n =
 594 pi_p (S n) primeb
 595   (\lambda p.(pi_p (log p n)
 596     (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
 597 intros.
 598 rewrite > eq_fact_pi_p.
 599 apply (trans_eq ? ?
 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
 605     [reflexivity
 606     |apply pi_p_primeb1.
 607      apply leb_true_to_le.assumption
 608     ]
 609   |apply (trans_eq ? ?
 610     (pi_p (S n) (λi:nat.leb (S O) i)
 611      (λn:nat
 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)))))
 614     [apply eq_pi_p1
 615       [intros.reflexivity
 616       |intros.apply eq_pi_p1
 617         [intros.elim (primeb x1)
 618           [simplify.apply sym_eq.
 619            apply le_to_leb_true.
 620            apply le_S_S_to_le.
 621            assumption
 622           |reflexivity
 623           ]
 624         |intros.reflexivity
 625         ]
 626       ]
 627     |apply (trans_eq ? ?
 628       (pi_p (S n) (λi:nat.leb (S O) i)
 629        (λm:nat
 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)))))
 632       [apply eq_pi_p1
 633         [intros.reflexivity
 634         |intros.
 635          apply sym_eq.
 636          apply false_to_eq_pi_p
 637           [assumption
 638           |intros.rewrite > lt_to_leb_false
 639             [elim primeb;reflexivity|assumption]
 640           ]
 641         ]
 642       |(* make a general theorem *)
 643        apply (trans_eq ? ?
 644         (pi_p (S n) primeb
 645          (λp:nat
 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)))
 648         ))
 649         [apply pi_p_pi_p1.
 650          intros.
 651          apply (bool_elim ? (primeb y \land leb y x));intros
 652           [rewrite > (le_to_leb_true (S O) x)
 653             [reflexivity
 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)
 660               ]
 661             ]
 662           |elim (leb (S O) x);reflexivity
 663           ]
 664         |apply eq_pi_p1
 665           [intros.reflexivity
 666           |intros.
 667            apply (trans_eq ? ?
 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))))
 670             [apply eq_pi_p1
 671               [intros.reflexivity
 672               |intros.
 673                apply sym_eq.
 674                apply false_to_eq_pi_p
 675                 [apply le_log
 676                   [apply prime_to_lt_SO.
 677                    apply primeb_true_to_prime.
 678                    assumption
 679                   |apply le_S_S_to_le.
 680                    assumption
 681                   ]
 682                 |intros.
 683                  apply not_divides_to_divides_b_false
 684                   [apply lt_O_exp.
 685                    apply prime_to_lt_O.
 686                    apply primeb_true_to_prime.
 687                    assumption
 688                   |intro.
 689                    apply (lt_to_not_le x1 (exp x (S i)))
 690                     [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
 691                       [apply lt_exp_log.
 692                        apply prime_to_lt_SO.
 693                        apply primeb_true_to_prime.
 694                        assumption
 695                       |apply le_exp
 696                         [apply prime_to_lt_O.
 697                          apply primeb_true_to_prime.
 698                          assumption
 699                         |apply le_S_S.
 700                          assumption
 701                         ]
 702                       ]
 703                     |apply divides_to_le
 704                       [apply (lt_to_le_to_lt ? x)
 705                         [apply prime_to_lt_O.
 706                          apply primeb_true_to_prime.
 707                          assumption
 708                         |apply leb_true_to_le.
 709                          assumption
 710                         ]
 711                       |assumption
 712                       ]
 713                     ]
 714                   ]
 715                 ]
 716               ]
 717             |apply
 718              (trans_eq ? ?
 719               (pi_p (log x n) (λi:nat.true)
 720                (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
 721               [apply (pi_p_pi_p1 (\lambda m,i.x)).
 722                intros.
 723                reflexivity
 724               |apply eq_pi_p1
 725                 [intros.reflexivity
 726                 |intros.
 727                  rewrite > exp_sigma_p.
 728                  apply eq_f.
 729                  apply (trans_eq ? ?
 730                   (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
 731                   [apply eq_sigma_p1
 732                     [intros.
 733                      apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
 734                       [apply (bool_elim ? (leb x x2));intro
 735                         [rewrite > le_to_leb_true
 736                           [reflexivity
 737                           |apply (trans_le ? x)
 738                             [apply prime_to_lt_O.
 739                              apply primeb_true_to_prime.
 740                              assumption
 741                             |apply leb_true_to_le.
 742                              assumption
 743                             ]
 744                           ]
 745                         |rewrite > lt_to_leb_false
 746                           [reflexivity
 747                           |apply not_le_to_lt.intro.
 748                            apply (leb_false_to_not_le ? ? H6).
 749                            apply (trans_le ? (exp x (S x1)))
 750                             [rewrite > times_n_SO in ⊢ (? % ?).
 751                              change with (exp x (S O) \le exp x (S x1)).
 752                              apply le_exp
 753                               [apply prime_to_lt_O.
 754                                apply primeb_true_to_prime.
 755                                assumption
 756                               |apply le_S_S.apply le_O_n.
 757                               ]
 758                             |apply divides_to_le
 759                               [assumption
 760                               |apply divides_b_true_to_divides.
 761                                assumption
 762                               ]
 763                             ]
 764                           ]
 765                         ]
 766                       |rewrite < andb_sym.
 767                        rewrite < andb_sym in ⊢ (? ? ? %).
 768                        reflexivity
 769                       ]
 770                     |intros.reflexivity
 771                     ]
 772                   |apply eq_sigma_p_div.
 773                    apply lt_O_exp.
 774                    apply prime_to_lt_O.
 775                    apply primeb_true_to_prime.
 776                    assumption
 777                   ]
 778                 ]
 779               ]
 780             ]
 781           ]
 782         ]
 783       ]
 784     ]
 785   ]
 786 qed.
 787
 788 (* odd n is just mod n (S(S O))
 789 let rec odd n \def
 790   match n with
 791   [ O \Rightarrow O
 792   | S m \Rightarrow (S O) - odd m
 793   ].
 794
 795 theorem le_odd_SO: \forall n. odd n \le S O.
 796 intro.elim n
 797   [apply le_O_n
 798   |simplify.cases (odd n1)
 799     [simplify.apply le_n.
 800     |apply le_O_n
 801     ]
 802   ]
 803 qed.
 804
 805 theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
 806 intro.elim n
 807   [apply (lt_O_n_elim ? H).
 808    intro.simplify.reflexivity
 809   |
 810 *)
 811
 812 theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
 813 pi_p (S ((S(S O))*n)) primeb
 814   (\lambda p.(pi_p (log p ((S(S O))*n))
 815     (\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)))))))).
 816 intros.rewrite > fact_pi_p.
 817 apply eq_pi_p1
 818   [intros.reflexivity
 819   |intros.apply eq_pi_p
 820     [intros.reflexivity
 821     |intros.
 822      rewrite < exp_plus_times.
 823      apply eq_f.
 824      rewrite > sym_times in ⊢ (? ? ? (? % ?)).
 825      apply SSO_mod.
 826      apply lt_O_exp.
 827      apply prime_to_lt_O.
 828      apply primeb_true_to_prime.
 829      assumption
 830     ]
 831   ]
 832 qed.
 833
 834 theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
 835 pi_p (S ((S(S O))*n)) primeb
 836   (\lambda p.(pi_p (log p ((S(S O))*n))
 837     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
 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 (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
 841 intros.
 842 rewrite < times_pi_p.
 843 rewrite > fact_pi_p2.
 844 apply eq_pi_p;intros
 845   [reflexivity
 846   |apply times_pi_p
 847   ]
 848 qed.
 849
 850 theorem pi_p_primeb4: \forall n. S O < n \to
 851 pi_p (S ((S(S O))*n)) primeb
 852   (\lambda p.(pi_p (log p ((S(S O))*n))
 853     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 854 =
 855 pi_p (S n) primeb
 856   (\lambda p.(pi_p (log p (S(S O)*n))
 857     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 858 intros.
 859 apply or_false_eq_SO_to_eq_pi_p
 860   [apply le_S_S.
 861    apply le_times_n.
 862    apply lt_O_S
 863   |intros.
 864    right.
 865    rewrite > log_i_SSOn
 866     [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
 867      rewrite < times_n_SO.
 868      rewrite > eq_div_O
 869       [reflexivity
 870       |simplify.rewrite < times_n_SO.assumption
 871       ]
 872     |assumption
 873     |assumption
 874     |apply le_S_S_to_le.assumption
 875     ]
 876   ]
 877 qed.
 878
 879 theorem pi_p_primeb5: \forall n. S O < n \to
 880 pi_p (S ((S(S O))*n)) primeb
 881   (\lambda p.(pi_p (log p ((S(S O))*n))
 882     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
 883 =
 884 pi_p (S n) primeb
 885   (\lambda p.(pi_p (log p n)
 886     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 887 intros.
 888 rewrite > (pi_p_primeb4 ? H).
 889 apply eq_pi_p1;intros
 890   [reflexivity
 891   |apply or_false_eq_SO_to_eq_pi_p
 892     [apply le_log
 893       [apply prime_to_lt_SO.
 894        apply primeb_true_to_prime.
 895        assumption
 896       |apply le_times_n.
 897        apply lt_O_S
 898       ]
 899     |intros.right.
 900      rewrite > eq_div_O
 901       [simplify.reflexivity
 902       |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
 903         [apply lt_exp_log.
 904          apply prime_to_lt_SO.
 905          apply primeb_true_to_prime.
 906          assumption
 907         |apply le_exp
 908           [apply prime_to_lt_O.
 909            apply primeb_true_to_prime.
 910            assumption
 911           |apply le_S_S.
 912            assumption
 913           ]
 914         ]
 915       ]
 916     ]
 917   ]
 918 qed.
 919
 920 theorem exp_fact_SSO: \forall n.
 921 exp (fact n) (S(S O))
 922 =
 923 pi_p (S n) primeb
 924   (\lambda p.(pi_p (log p n)
 925     (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
 926 intros.
 927 rewrite > fact_pi_p.
 928 rewrite < exp_pi_p.
 929 apply eq_pi_p;intros
 930   [reflexivity
 931   |apply sym_eq.
 932    apply exp_times_pi_p
 933   ]
 934 qed.
 935
 936 definition B \def
 937 \lambda n.
 938 pi_p (S n) primeb
 939   (\lambda p.(pi_p (log p n)
 940     (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
 941
 942 theorem eq_fact_B:\forall n.S O < n \to
 943 fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
 944 intros. unfold B.
 945 rewrite > fact_pi_p3.
 946 apply eq_f2
 947   [apply sym_eq.
 948    rewrite > pi_p_primeb5
 949     [apply exp_fact_SSO
 950     |assumption
 951     ]
 952   |reflexivity
 953   ]
 954 qed.
 955
 956 theorem le_B_A: \forall n. B n \le A n.
 957 intro.unfold B.
 958 rewrite > eq_A_A'.
 959 unfold A'.
 960 apply le_pi_p.intros.
 961 apply le_pi_p.intros.
 962 rewrite > exp_n_SO in ⊢ (? ? %).
 963 apply le_exp
 964   [apply prime_to_lt_O.
 965    apply primeb_true_to_prime.
 966    assumption
 967   |apply le_S_S_to_le.
 968    apply lt_mod_m_m.
 969    apply lt_O_S
 970   ]
 971 qed.
 972
 973 theorem le_fact_A:\forall n.S O < n \to
 974 fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
 975 intros.
 976 rewrite > eq_fact_B
 977   [apply le_times_r.
 978    apply le_B_A
 979   |assumption
 980   ]
 981 qed.
 982
 983 theorem lt_SO_to_le_B_exp: \forall n.S O < n \to
 984 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
 985 intros.
 986 apply (le_times_to_le (exp (fact n) (S(S O))))
 987   [apply lt_O_exp.
 988    apply lt_O_fact
 989   |rewrite < eq_fact_B
 990     [rewrite < sym_times in ⊢ (? ? %).
 991      rewrite > exp_SSO.
 992      rewrite < assoc_times.
 993      apply fact1
 994     |assumption
 995     ]
 996   ]
 997 qed.
 998
 999 theorem le_B_exp: \forall n.
1000 B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
1001 intro.cases n
1002   [apply le_n
1003   |cases n1
1004     [simplify.apply le_S.apply le_S.apply le_n
1005     |apply lt_SO_to_le_B_exp.
1006      apply le_S_S.apply lt_O_S.
1007     ]
1008   ]
1009 qed.
1010
1011 theorem lt_SO_to_le_exp_B: \forall n. S O < n \to
1012 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1013 intros.
1014 apply (le_times_to_le (exp (fact n) (S(S O))))
1015   [apply lt_O_exp.
1016    apply lt_O_fact
1017   |rewrite < assoc_times in ⊢ (? ? %).
1018    rewrite > sym_times in ⊢ (? ? (? % ?)).
1019    rewrite > assoc_times in ⊢ (? ? %).
1020    rewrite < eq_fact_B
1021     [rewrite < sym_times.
1022      apply fact3.
1023      apply lt_to_le.assumption
1024     |assumption
1025     ]
1026   ]
1027 qed.
1028
1029 theorem le_exp_B: \forall n. O < n \to
1030 exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n).
1031 intros.
1032 elim H
1033   [apply le_n
1034   |apply lt_SO_to_le_exp_B.
1035    apply le_S_S.assumption
1036   ]
1037 qed.
1038
1039 theorem eq_A_SSO_n: \forall n.O < n \to
1040 A((S(S O))*n) =
1041  pi_p (S ((S(S O))*n)) primeb
1042   (\lambda p.(pi_p (log p ((S(S O))*n) )
1043     (\lambda i.true) (\lambda i.(exp p (bool_to_nat (leb (S n) (exp p (S i))))))))
1044  *A n.
1045 intro.
1046 rewrite > eq_A_A'.rewrite > eq_A_A'.
1047 unfold A'.intros.
1048 cut (
1049  pi_p (S n) primeb (λp:nat.pi_p (log p n) (λi:nat.true) (λi:nat.p))
1050  = pi_p (S ((S(S O))*n)) primeb
1051     (λ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))))))))
1052   [rewrite > Hcut.
1053    rewrite < times_pi_p.
1054    apply eq_pi_p1;intros
1055     [reflexivity
1056     |rewrite < times_pi_p.
1057      apply eq_pi_p;intros
1058       [reflexivity
1059       |apply (bool_elim ? (leb (S n) (exp x (S x1))));intro
1060         [simplify.rewrite < times_n_SO.apply times_n_SO
1061         |simplify.rewrite < plus_n_O.apply times_n_SO
1062         ]
1063       ]
1064     ]
1065   |apply (trans_eq ? ? (pi_p (S n) primeb
1066     (\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))))))))
1067     [apply eq_pi_p1;intros
1068       [reflexivity
1069       |apply eq_pi_p1;intros
1070         [reflexivity
1071         |rewrite > lt_to_leb_false
1072           [simplify.apply times_n_SO
1073           |apply le_S_S.
1074            apply (trans_le ? (exp x (log x n)))
1075             [apply le_exp
1076               [apply prime_to_lt_O.
1077                apply primeb_true_to_prime.
1078                assumption
1079               |assumption
1080               ]
1081             |apply le_exp_log.
1082              assumption
1083             ]
1084           ]
1085         ]
1086       ]
1087     |apply (trans_eq ? ?
1088       (pi_p (S ((S(S O))*n)) primeb
1089        (λp:nat.pi_p (log p n) (λi:nat.true)
1090         (λi:nat.(p)\sup(bool_to_nat (¬leb (S n) ((p)\sup(S i))))))))
1091       [apply sym_eq.
1092        apply or_false_eq_SO_to_eq_pi_p
1093         [apply le_S_S.
1094          simplify.
1095          apply le_plus_n_r
1096         |intros.right.
1097          rewrite > lt_to_log_O
1098           [reflexivity
1099           |assumption
1100           |assumption
1101           ]
1102         ]
1103       |apply eq_pi_p1;intros
1104         [reflexivity
1105         |apply sym_eq.
1106          apply or_false_eq_SO_to_eq_pi_p
1107           [apply le_log
1108             [apply prime_to_lt_SO.
1109              apply primeb_true_to_prime.
1110              assumption
1111             |simplify.
1112              apply le_plus_n_r
1113             ]
1114           |intros.right.
1115            rewrite > le_to_leb_true
1116             [simplify.reflexivity
1117             |apply (lt_to_le_to_lt ? (exp x (S (log x n))))
1118               [apply lt_exp_log.
1119                apply prime_to_lt_SO.
1120                apply primeb_true_to_prime.
1121                assumption
1122               |apply le_exp
1123                 [apply prime_to_lt_O.
1124                  apply primeb_true_to_prime.
1125                  assumption
1126                 |apply le_S_S.assumption
1127                 ]
1128               ]
1129             ]
1130           ]
1131         ]
1132       ]
1133     ]
1134   ]
1135 qed.
1136
1137 theorem le_A_BA1: \forall n. O < n \to
1138 A((S(S O))*n) \le B((S(S O))*n)*A n.
1139 intros.
1140 rewrite > eq_A_SSO_n
1141   [apply le_times_l.
1142    unfold B.
1143    apply le_pi_p.intros.
1144    apply le_pi_p.intros.
1145    apply le_exp
1146     [apply prime_to_lt_O.
1147      apply primeb_true_to_prime.
1148      assumption
1149     |apply (bool_elim ? (leb (S n) (exp i (S i1))));intro
1150       [simplify in ⊢ (? % ?).
1151        cut ((S(S O))*n/i\sup(S i1) = S O)
1152         [rewrite > Hcut.apply le_n
1153         |apply (div_mod_spec_to_eq
1154           ((S(S O))*n) (exp i (S i1))
1155            ? (mod ((S(S O))*n) (exp i (S i1)))
1156            ? (minus ((S(S O))*n) (exp i (S i1))) )
1157           [apply div_mod_spec_div_mod.
1158            apply lt_O_exp.
1159            apply prime_to_lt_O.
1160            apply primeb_true_to_prime.
1161            assumption
1162           |cut (i\sup(S i1)≤(S(S O))*n)
1163             [apply div_mod_spec_intro
1164               [alias id "lt_plus_to_lt_minus" = "cic:/matita/nat/map_iter_p.ma/lt_plus_to_lt_minus.con".
1165                apply lt_plus_to_lt_minus
1166                 [assumption
1167                 |simplify in ⊢ (? % ?).
1168                  rewrite < plus_n_O.
1169                  apply lt_plus
1170                   [apply leb_true_to_le.assumption
1171                   |apply leb_true_to_le.assumption
1172                   ]
1173                 ]
1174               |rewrite > sym_plus.
1175                rewrite > sym_times in ⊢ (? ? ? (? ? %)).
1176                rewrite < times_n_SO.
1177                apply plus_minus_m_m.
1178                assumption
1179               ]
1180             |apply (trans_le ? (exp i (log i ((S(S O))*n))))
1181               [apply le_exp
1182                 [apply prime_to_lt_O.
1183                  apply primeb_true_to_prime.
1184                  assumption
1185                 |assumption
1186                 ]
1187               |apply le_exp_log.
1188                rewrite > (times_n_O O) in ⊢ (? % ?).
1189                apply lt_times
1190                 [apply lt_O_S
1191                 |assumption
1192                 ]
1193               ]
1194             ]
1195           ]
1196         ]
1197       |apply le_O_n
1198       ]
1199     ]
1200   |assumption
1201   ]
1202 qed.
1203
1204 theorem le_A_BA: \forall n. A((S(S O))*n) \le B((S(S O))*n)*A n.
1205 intros.cases n
1206   [apply le_n
1207   |apply le_A_BA1.apply lt_O_S
1208   ]
1209 qed.
1210
1211 theorem le_A_exp: \forall n.
1212 A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n.
1213 intro.
1214 apply (trans_le ? (B((S(S O))*n)*A n))
1215   [apply le_A_BA
1216   |apply le_times_l.
1217    apply le_B_exp
1218   ]
1219 qed.
1220
1221 theorem le_A_exp1: \forall n.
1222 A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))).
1223 intro.elim n
1224   [simplify.apply le_S_S.apply le_O_n
1225   |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))).
1226    apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1)))
1227     [apply le_A_exp
1228     |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))))
1229       [apply le_times_r.
1230        assumption
1231       |rewrite < exp_plus_times.
1232        simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))).
1233        apply le_n
1234       ]
1235     ]
1236   ]
1237 qed.
1238
1239 theorem monotonic_A: monotonic nat le A.
1240 unfold.intros.
1241 elim H
1242   [apply le_n
1243   |apply (trans_le ? (A n1))
1244     [assumption
1245     |unfold A.
1246      cut (pi_p (S n1) primeb (λp:nat.(p)\sup(log p n1))
1247           ≤pi_p (S n1) primeb (λp:nat.(p)\sup(log p (S n1))))
1248       [apply (bool_elim ? (primeb (S n1)));intro
1249         [rewrite > (true_to_pi_p_Sn ? ? ? H3).
1250          rewrite > times_n_SO in ⊢ (? % ?).
1251          rewrite > sym_times.
1252          apply le_times
1253           [apply lt_O_exp.apply lt_O_S
1254           |assumption
1255           ]
1256         |rewrite > (false_to_pi_p_Sn ? ? ? H3).
1257          assumption
1258         ]
1259       |apply le_pi_p.intros.
1260        apply le_exp
1261         [apply prime_to_lt_O.
1262          apply primeb_true_to_prime.
1263          assumption
1264         |apply le_log
1265           [apply prime_to_lt_SO.
1266            apply primeb_true_to_prime.
1267            assumption
1268           |apply le_S.apply le_n
1269           ]
1270         ]
1271       ]
1272     ]
1273   ]
1274 qed.
1275
1276 theorem le_A_exp2: \forall n. O < n \to
1277 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
1278 intros.
1279 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
1280   [apply monotonic_A.
1281    apply lt_to_le.
1282    apply lt_exp_log.
1283    apply le_n
1284   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
1285     [apply le_A_exp1
1286     |apply le_exp
1287       [apply lt_O_S
1288       |rewrite > assoc_times.apply le_times_r.
1289        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
1290        apply le_times_r.
1291        apply le_exp_log.
1292        assumption
1293       ]
1294     ]
1295   ]
1296 qed.
1297
1298 (* example *)
1299 theorem A_SO: A (S O) = S O.
1300 reflexivity.
1301 qed.
1302
1303 theorem A_SSO: A (S(S O)) = S (S O).
1304 reflexivity.
1305 qed.
1306
1307 theorem A_SSSO: A (S(S(S O))) = S(S(S(S(S(S O))))).
1308 reflexivity.
1309 qed.
1310
1311 theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))).
1312 reflexivity.
1313 qed.
1314
1315 (* da spostare *)
1316 theorem or_eq_eq_S: \forall n.\exists m.
1317 n = (S(S O))*m \lor n = S ((S(S O))*m).
1318 intro.elim n
1319   [apply (ex_intro ? ? O).
1320    left.reflexivity
1321   |elim H.elim H1
1322     [apply (ex_intro ? ? a).
1323      right.apply eq_f.assumption
1324     |apply (ex_intro ? ? (S a)).
1325      left.rewrite > H2.
1326      apply sym_eq.
1327      apply times_SSO
1328     ]
1329   ]
1330 qed.
1331
1332 (* a better result *)
1333 theorem le_A_exp3: \forall n. S O < n \to
1334 A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)).
1335 intro.
1336 apply (nat_elim1 n).
1337 intros.
1338 elim (or_eq_eq_S m).
1339 elim H2
1340   [elim (le_to_or_lt_eq (S O) a)
1341     [rewrite > H3 in ⊢ (? % ?).
1342      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
1343       [apply le_A_exp
1344       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
1345          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
1346         [apply le_times_r.
1347          apply H
1348           [rewrite > H3.
1349            rewrite > times_n_SO in ⊢ (? % ?).
1350            rewrite > sym_times.
1351            apply lt_times_l1
1352             [apply lt_to_le.assumption
1353             |apply le_n
1354             ]
1355           |assumption
1356           ]
1357         |rewrite > sym_times.
1358          rewrite > assoc_times.
1359          rewrite < exp_plus_times.
1360          apply (trans_le ?
1361           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1362           [rewrite > assoc_times.
1363            apply le_times_r.
1364            rewrite < exp_plus_times.
1365            apply le_exp
1366             [apply lt_O_S
1367             |rewrite < H3.
1368              simplify.
1369              rewrite < plus_n_O.
1370              apply le_S.apply le_S.
1371              apply le_n
1372             ]
1373           |apply le_times_l.
1374            rewrite > times_exp.
1375            apply monotonic_exp1.
1376            rewrite > H3.
1377            rewrite > sym_times.
1378            cases a
1379             [apply le_n
1380             |simplify.
1381              rewrite < plus_n_Sm.
1382              apply le_S.
1383              apply le_n
1384             ]
1385           ]
1386         ]
1387       ]
1388     |rewrite < H4 in H3.
1389      simplify in H3.
1390      rewrite > H3.
1391      simplify.
1392      apply le_S_S.apply le_S_S.apply le_O_n
1393     |apply not_lt_to_le.intro.
1394      apply (lt_to_not_le ? ? H1).
1395      rewrite > H3.
1396      apply (le_n_O_elim a)
1397       [apply le_S_S_to_le.assumption
1398       |apply le_O_n
1399       ]
1400     ]
1401   |elim (le_to_or_lt_eq O a (le_O_n ?))
1402     [apply (trans_le ? (A ((S(S O))*(S a))))
1403       [apply monotonic_A.
1404        rewrite > H3.
1405        rewrite > times_SSO.
1406        apply le_n_Sn
1407       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
1408         [apply le_A_exp
1409         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
1410            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
1411           [apply le_times_r.
1412            apply H
1413             [rewrite > H3.
1414              apply le_S_S.
1415              simplify.
1416              rewrite > plus_n_SO.
1417              apply le_plus_r.
1418              rewrite < plus_n_O.
1419              assumption
1420             |apply le_S_S.assumption
1421             ]
1422           |rewrite > sym_times.
1423            rewrite > assoc_times.
1424            rewrite < exp_plus_times.
1425            apply (trans_le ?
1426             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
1427             [rewrite > assoc_times.
1428              apply le_times_r.
1429              rewrite < exp_plus_times.
1430              apply le_exp
1431               [apply lt_O_S
1432               |rewrite > times_SSO.
1433                rewrite < H3.
1434                simplify.
1435                rewrite < plus_n_Sm.
1436                rewrite < plus_n_O.
1437                apply le_n
1438               ]
1439             |apply le_times_l.
1440              rewrite > times_exp.
1441              apply monotonic_exp1.
1442              rewrite > H3.
1443              rewrite > sym_times.
1444              apply le_n
1445             ]
1446           ]
1447         ]
1448       ]
1449     |rewrite < H4 in H3.simplify in H3.
1450      apply False_ind.
1451      apply (lt_to_not_le ? ? H1).
1452      rewrite > H3.
1453      apply le_n
1454     ]
1455   ]
1456 qed.
1457
1458 theorem eq_sigma_pi_SO_n: \forall n.
1459 sigma_p n (\lambda i.true) (\lambda i.S O) = n.
1460 intro.elim n
1461   [reflexivity
1462   |rewrite > true_to_sigma_p_Sn
1463     [rewrite > H.reflexivity
1464     |reflexivity
1465     ]
1466   ]
1467 qed.
1468
1469 theorem leA_prim: \forall n.
1470 exp n (prim n) \le A n * pi_p (S n) primeb (λp:nat.p).
1471 intro.
1472 unfold prim.
1473 rewrite < (exp_sigma_p (S n) n primeb).
1474 unfold A.
1475 rewrite < times_pi_p.
1476 apply le_pi_p.
1477 intros.
1478 rewrite > sym_times.
1479 change in ⊢ (? ? %) with (exp i (S (log i n))).
1480 apply lt_to_le.
1481 apply lt_exp_log.
1482 apply prime_to_lt_SO.
1483 apply primeb_true_to_prime.
1484 assumption.
1485 qed.
1486
1487
1488 (* the inequalities *)
1489 theorem le_exp_priml: \forall n. O < n \to
1490 exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))).
1491 intros.
1492 apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n))))))
1493   [apply le_exp_B.assumption
1494   |change in ⊢ (? ? %) with ((((S(S O))*n))*(((S(S O))*n))\sup (prim ((S(S O))*n))).
1495    apply le_times_r.
1496    apply (trans_le ? (A ((S(S O))*n)))
1497     [apply le_B_A
1498     |apply le_Al
1499     ]
1500   ]
1501 qed.
1502
1503 theorem le_priml: \forall n. O < n \to
1504 (S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)).
1505 intros.
1506 rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?)
1507   [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n)))))))
1508     [apply le_log
1509       [apply le_n
1510       |apply le_exp_priml.assumption
1511       ]
1512     |rewrite > sym_times in ⊢ (? ? %).
1513      apply log_exp1.
1514      apply le_n
1515     ]
1516   |apply le_n
1517   ]
1518 qed.
1519
1520 theorem le_exp_primr: \forall n. S O < n \to
1521 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)).
1522 intros.
1523 apply (trans_le ? (exp (A n) (S(S O))))
1524   [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))).
1525    rewrite < times_n_SO.
1526    apply leA_r2
1527   |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O))))
1528     [apply monotonic_exp1.
1529      apply le_A_exp3.
1530      assumption
1531     |rewrite < times_exp.
1532      rewrite > exp_exp_times.
1533      rewrite > exp_exp_times.
1534      rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?).
1535      rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?).
1536      apply le_n
1537     ]
1538   ]
1539 qed.
1540