matita/matita/lib/arithmetics/chebyshev/chebyshev.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "arithmetics/log.ma".
  13 include "arithmetics/sigma_pi.ma".
  14 include "arithmetics/ord.ma".
  15
  16 (* (prim n) counts the number of prime numbers up to n included *)
  17 definition prim ≝ λn. ∑_{i < S n | primeb i} 1.
  18
  19 lemma le_prim_n: ∀n. prim n ≤ n.
  20 #n elim n // -n #n #H
  21 whd in ⊢ (?%?); cases (primeb (S n)) whd in ⊢ (?%?);
  22   [@le_S_S @H |@le_S @H]
  23 qed.
  24
  25 lemma not_prime_times_2: ∀n. 1 < n → ¬prime (2*n).
  26 #n #ltn % * #H #H1 @(absurd (2 = 2*n))
  27   [@H1 // %{n} //
  28   |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r //
  29   ]
  30 qed.
  31
  32 theorem eq_prim_prim_pred: ∀n. 1 < n →
  33   prim (2*n) = prim (pred (2*n)).
  34 #n #ltn
  35 lapply (S_pred (2*n) ?) [>(times_n_1 0) in ⊢ (?%?); @lt_times //] #H2n
  36 lapply (not_prime_times_2 n ltn) #notp2n
  37 whd in ⊢ (??%?); >(not_prime_to_primeb_false … notp2n) whd in ⊢ (??%?);
  38 <H2n in ⊢ (??%?); %
  39 qed.
  40
  41 theorem le_prim_n1: ∀n. 4 ≤ n →
  42   prim (S(2*n)) ≤ n.
  43 #n #le4 elim le4 -le4
  44   [@le_n
  45   |#m #le4 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
  46    <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le4) //]
  47    #H whd in ⊢ (?%?); cases (primeb (S (2*S m)))
  48     [@le_S_S @H |@le_S @H]
  49   ]
  50 qed.
  51
  52 (* usefull to kill a successor in bertrand *)
  53 theorem le_prim_n2: ∀n. 7 ≤ n → prim (S(2*n)) ≤ pred n.
  54 #n #le7 elim le7 -le7
  55   [@le_n
  56   |#m #le7 cut (S (2*m) = pred (2*(S m))) [normalize //] #Heq >Heq
  57    <eq_prim_prim_pred [2: @le_S_S @(transitive_le … le7) //]
  58    #H whd in ⊢ (?%?);
  59    whd in ⊢ (??%); <(S_pred m) in ⊢ (??%); [2: @(transitive_le … le7) //]
  60    cases (primeb (S (2*S m))) [@le_S_S @H |@le_S @H]
  61   ]
  62 qed.
  63
  64 lemma even_or_odd: ∀n.∃a.n=2*a ∨ n = S(2*a).
  65 #n elim n -n
  66   [%{0} %1 %
  67   |#n * #a * #Hn [%{a} %2 @eq_f @Hn | %{(S a)} %1 >Hn normalize //
  68   ]
  69 qed.
  70
  71 (* la prova potrebbe essere migliorata *)
  72 theorem le_prim_n3: ∀n. 15 ≤ n →
  73   prim n ≤ pred (n/2).
  74 #n #len cases (even_or_odd (pred n)) #a * #Hpredn
  75   [cut (n = S (2*a)) [<Hpredn @sym_eq @S_pred @(transitive_le … len) //] #Hn
  76    >Hn @(transitive_le ? (pred a))
  77     [@le_prim_n2 @(le_times_to_le 2) [//|@le_S_S_to_le <Hn @len]
  78     |@monotonic_pred @le_times_to_le_div //
  79     ]
  80   |cut (n = (2*S a))
  81     [normalize normalize in Hpredn:(???%); <plus_n_Sm <Hpredn @sym_eq @S_pred
  82      @(transitive_le … len) //] #Hn
  83    >Hn @(transitive_le ? (pred a))
  84     [>eq_prim_prim_pred
  85       [2:@(lt_times_n_to_lt_r 2) <Hn @(transitive_le … len) //]
  86      <Hn >Hpredn @le_prim_n2 @le_S_S_to_le @(lt_times_n_to_lt_r 2) <Hn @len
  87     |@monotonic_pred @le_times_to_le_div //
  88     ]
  89   ]
  90 qed.
  91
  92 (* This is chebishev psi function *)
  93 definition Psi: nat → nat ≝
  94   λn.∏_{p < S n | primeb p} (exp p (log p n)).
  95
  96 definition psi_def : ∀n.
  97   Psi n = ∏_{p < S n | primeb p} (exp p (log p n)).
  98 // qed.
  99
 100 theorem le_Psil1: ∀n.
 101   Psi n ≤ ∏_{p < S n | primeb p} n.
 102 #n cases n [@le_n |#m @le_pi #i #_ #_ @le_exp_log //]
 103 qed.
 104
 105 theorem le_Psil: ∀n. Psi n ≤ exp n (prim n).
 106 #n <exp_sigma @le_Psil1
 107 qed.
 108
 109 theorem lePsi_r2: ∀n.
 110   exp n (prim n) ≤ Psi n * Psi n.
 111 #n elim (le_to_or_lt_eq ?? (le_O_n n)) #Hn
 112   [<(exp_sigma (S n) n primeb) <times_pi
 113    @le_pi #i #lti #primei
 114    cut (1<n)
 115      [@(lt_to_le_to_lt … (le_S_S_to_le … lti)) @prime_to_lt_SO
 116       @primeb_true_to_prime //] #lt1n
 117    <exp_plus_times
 118    @(transitive_le ? (exp i (S(log i n))))
 119     [@lt_to_le @lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 120     |@le_exp
 121       [@prime_to_lt_O @primeb_true_to_prime //
 122       |>(plus_n_O (log i n)) in ⊢ (?%?); >plus_n_Sm
 123        @monotonic_le_plus_r @lt_O_log //
 124        @le_S_S_to_le //
 125       ]
 126     ]
 127   |<Hn @le_n
 128   ]
 129 qed.
 130
 131 (* an equivalent formulation for psi *)
 132 definition Psi': nat → nat ≝
 133 λn. ∏_{p < S n | primeb p} (∏_{i < log p n} p).
 134
 135 lemma Psidef: ∀n. Psi' n = ∏_{p < S n | primeb p} (∏_{i < log p n} p).
 136 // qed-.
 137
 138 theorem eq_Psi_Psi': ∀n.Psi n = Psi' n.
 139 #n @same_bigop // #i #lti #primebi
 140 @(trans_eq ? ? (exp i (∑_{x < log i n} 1)))
 141   [@eq_f @sym_eq @sigma_const
 142   |@sym_eq @exp_sigma
 143   ]
 144 qed.
 145
 146 theorem eq_pi_p_primeb_divides_b: ∀n,m.
 147 ∏_{p<n | primeb p ∧ dividesb p m} (exp p (ord m p))
 148   = ∏_{p<n | primeb p} (exp p (ord m p)).
 149 #n #m elim n // #n1 #Hind cases (true_or_false (primeb n1)) #Hprime
 150   [>bigop_Strue in ⊢ (???%); //
 151    cases (true_or_false (dividesb n1 m)) #Hdivides
 152     [>bigop_Strue [@eq_f @Hind| @true_to_andb_true //]
 153   |>bigop_Sfalse
 154     [>not_divides_to_ord_O
 155       [whd in ⊢ (???(?%?)); //
 156       |@dividesb_false_to_not_divides //
 157       |@primeb_true_to_prime //
 158       ]
 159     |>Hprime >Hdivides %
 160     ]
 161   ]
 162 |>bigop_Sfalse [>bigop_Sfalse // |>Hprime %]
 163 ]
 164 qed.
 165
 166 (* integrations to minimization *)
 167 theorem false_to_lt_max: ∀f,n,m.O < n →
 168   f n = false → max m f ≤ n → max m f < n.
 169 #f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax
 170   [//
 171   |cases (exists_max_forall_false f m)
 172     [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) //
 173     |* //
 174     ]
 175   ]
 176 qed.
 177
 178 (* integrations to minimization *)
 179 lemma lt_1_max_prime: ∀n. 1 <  n →
 180   1 < max (S n) (λi:nat.primeb i∧dividesb i n).
 181 #n #lt1n
 182 @(lt_to_le_to_lt ? (smallest_factor n))
 183   [@lt_SO_smallest_factor //
 184   |@true_to_le_max
 185     [@le_S_S @le_smallest_factor_n
 186     |@true_to_andb_true
 187       [@prime_to_primeb_true @prime_smallest_factor_n //
 188       |@divides_to_dividesb_true
 189         [@lt_O_smallest_factor @lt_to_le //
 190         |@divides_smallest_factor_n @lt_to_le //
 191         ]
 192       ]
 193     ]
 194   ]
 195 qed.
 196
 197 theorem lt_max_to_pi_p_primeb: ∀q,m. O<m → max (S m) (λi.primeb i ∧ dividesb i m)<q →
 198   m = ∏_{p < q | primeb p ∧ dividesb p m} (exp p (ord m p)).
 199 #q elim q
 200   [#m #posm #Hmax normalize @False_ind @(absurd … Hmax (not_le_Sn_O ?))
 201   |#n #Hind #m #posm #Hmax
 202    cases (true_or_false (primeb n∧dividesb n m)) #Hcase
 203     [>bigop_Strue
 204       [>(exp_ord n m … posm) in ⊢ (??%?);
 205         [@eq_f >(Hind (ord_rem m n))
 206           [@same_bigop
 207             [#x #ltxn cases (true_or_false (primeb x)) #Hx >Hx
 208               [cases (true_or_false (dividesb x (ord_rem m n))) #Hx1 >Hx1
 209                 [@sym_eq @divides_to_dividesb_true
 210                   [@prime_to_lt_O @primeb_true_to_prime //
 211                   |@(transitive_divides ? (ord_rem m n))
 212                     [@dividesb_true_to_divides //
 213                     |@(divides_ord_rem … posm) @(transitive_lt … ltxn)
 214                      @prime_to_lt_SO @primeb_true_to_prime //
 215                     ]
 216                   ]
 217                 |@sym_eq @not_divides_to_dividesb_false
 218                   [@prime_to_lt_O @primeb_true_to_prime //
 219                   |@(ord_O_to_not_divides … posm)
 220                     [@primeb_true_to_prime //
 221                     |<(ord_ord_rem n … posm … ltxn)
 222                       [@not_divides_to_ord_O
 223                         [@primeb_true_to_prime //
 224                         |@dividesb_false_to_not_divides //
 225                         ]
 226                       |@primeb_true_to_prime //
 227                       |@primeb_true_to_prime @(andb_true_l ?? Hcase)
 228                       ]
 229                     ]
 230                   ]
 231                 ]
 232               |//
 233               ]
 234             |#x #ltxn #Hx @eq_f @ord_ord_rem //
 235               [@primeb_true_to_prime @(andb_true_l ? ? Hcase)
 236               |@primeb_true_to_prime @(andb_true_l ? ? Hx)
 237               ]
 238             ]
 239           |@not_eq_to_le_to_lt
 240             [elim (exists_max_forall_false (λi:nat.primeb i∧dividesb i (ord_rem m n)) (S(ord_rem m n)))
 241               [* #Hex #Hord_rem cases Hex #x * #H6 #H7 % #H
 242                >H in Hord_rem; #Hn @(absurd ?? (not_divides_ord_rem m n posm ?))
 243                 [@dividesb_true_to_divides @(andb_true_r ?? Hn)
 244                 |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hn)
 245                 ]
 246               |* #Hall #Hmax >Hmax @lt_to_not_eq @prime_to_lt_O
 247                @primeb_true_to_prime @(andb_true_l ?? Hcase)
 248               ]
 249             |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i (ord_rem m n))))
 250               [@le_to_le_max @le_S_S @(divides_to_le … posm) @(divides_ord_rem … posm)
 251                @prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase)
 252               |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i m)))
 253                 [@le_max_f_max_g #i #ltim #Hi
 254                  cases (true_or_false (primeb i)) #Hprimei >Hprimei
 255                   [@divides_to_dividesb_true
 256                     [@prime_to_lt_O @primeb_true_to_prime //
 257                     |@(transitive_divides ? (ord_rem m n))
 258                       [@dividesb_true_to_divides @(andb_true_r ?? Hi)
 259                       |@(divides_ord_rem … posm)
 260                        @prime_to_lt_SO @primeb_true_to_prime
 261                        @(andb_true_l ?? Hcase)
 262                       ]
 263                     ]
 264                   |>Hprimei in Hi; #Hi @Hi
 265                   ]
 266                 |@le_S_S_to_le //
 267                 ]
 268               ]
 269             ]
 270           |@(lt_O_ord_rem … posm) @prime_to_lt_SO
 271            @primeb_true_to_prime @(andb_true_l ?? Hcase)
 272           ]
 273         |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase)
 274         ]
 275       |//
 276       ]
 277     |cases (le_to_or_lt_eq ?? posm) #Hm
 278       [>bigop_Sfalse
 279         [@(Hind … posm) @false_to_lt_max
 280           [@(lt_to_le_to_lt ? (max (S m) (λi:nat.primeb i∧dividesb i m)))
 281             [@lt_to_le @lt_1_max_prime //
 282             |@le_S_S_to_le //
 283             ]
 284           |//
 285           |@le_S_S_to_le //
 286           ]
 287         |@Hcase
 288         ]
 289       |<Hm
 290        <(bigop_false (S n) ? 1 times (λp:nat.p\sup(ord 1 p))) in ⊢ (??%?);
 291        @same_bigop
 292         [#i #lein cases (true_or_false (primeb i)) #primei >primei //
 293          @sym_eq @not_divides_to_dividesb_false
 294           [@prime_to_lt_O @primeb_true_to_prime //
 295           |% #divi @(absurd ?? (le_to_not_lt i 1 ?))
 296             [@prime_to_lt_SO @(primeb_true_to_prime ? primei)
 297             |@divides_to_le //
 298             ]
 299           ]
 300         |//
 301         ]
 302       ]
 303     ]
 304   ]
 305 qed.
 306
 307 (* factorization of n into primes *)
 308 theorem pi_p_primeb_dividesb: ∀n. O < n →
 309   n = ∏_{ p < S n | primeb p ∧ dividesb p n} (exp p (ord n p)).
 310 #n #posn @lt_max_to_pi_p_primeb // @lt_max_n @le_S @posn
 311 qed.
 312
 313 theorem pi_p_primeb: ∀n. O < n →
 314   n = ∏_{ p < (S n) | primeb p}(exp p (ord n p)).
 315 #n #posn <eq_pi_p_primeb_divides_b @pi_p_primeb_dividesb //
 316 qed.
 317
 318 (* more result on order functions *)
 319 theorem le_ord_log: ∀n,p. O < n → 1 < p →
 320   ord n p ≤ log p n.
 321 #n #p #posn #lt1p >(exp_ord p ? lt1p posn) in ⊢ (??(??%));
 322 >log_exp // @lt_O_ord_rem //
 323 qed.
 324
 325 theorem sigma_p_dividesb:
 326 ∀m,n,p. O < n → prime p → p ∤ n →
 327 m = ∑_{ i < m | dividesb (p\sup (S i)) ((exp p m)*n)} 1.
 328 #m elim m // -m #m #Hind #n #p #posn #primep #ndivp
 329 >bigop_Strue
 330   [>commutative_plus <plus_n_Sm @eq_f <plus_n_O
 331    >(Hind n p posn primep ndivp) in ⊢ (? ? % ?);
 332    @same_bigop
 333     [#i #ltim cases (true_or_false (dividesb (p\sup(S i)) (p\sup m*n))) #Hc >Hc
 334       [@sym_eq @divides_to_dividesb_true
 335         [@lt_O_exp @prime_to_lt_O //
 336         |%{((exp p (m - i))*n)} <associative_times
 337          <exp_plus_times @eq_f2 // @eq_f normalize @eq_f >commutative_plus
 338          @plus_minus_m_m @lt_to_le //
 339         ]
 340       |@False_ind @(absurd ?? (dividesb_false_to_not_divides ? ? Hc))
 341        %{((exp p (m - S i))*n)} <associative_times <exp_plus_times @eq_f2
 342         [@eq_f >commutative_plus @plus_minus_m_m //
 343            assumption
 344         |%
 345         ]
 346       ]
 347     |//
 348     ]
 349   |@divides_to_dividesb_true
 350     [@lt_O_exp @prime_to_lt_O // | %{n} //]
 351   ]
 352 qed.
 353
 354 theorem sigma_p_dividesb1:
 355 ∀m,n,p,k. O < n → prime p → p ∤ n → m ≤ k →
 356   m = ∑_{i < k | dividesb (p\sup (S i)) ((exp p m)*n)} 1.
 357 #m #n #p #k #posn #primep #ndivp #lemk
 358 lapply (prime_to_lt_SO ? primep) #lt1p
 359 lapply (prime_to_lt_O ? primep) #posp
 360 >(sigma_p_dividesb m n p posn primep ndivp) in ⊢ (??%?);
 361 >(pad_bigop k m) // @same_bigop
 362   [#i #ltik cases (true_or_false (leb m i)) #Him > Him
 363     [whd in ⊢(??%?); @sym_eq
 364      @not_divides_to_dividesb_false
 365       [@lt_O_exp //
 366       |lapply (leb_true_to_le … Him) -Him #Him
 367        % #Hdiv @(absurd ?? (le_to_not_lt ?? Him))
 368        (* <(ord_exp p m lt1p) *) >(plus_n_O m)
 369        <(not_divides_to_ord_O ?? primep ndivp)
 370        <(ord_exp p m lt1p)
 371        <ord_times //
 372         [whd <(ord_exp p (S i) lt1p)
 373          @divides_to_le_ord //
 374           [@lt_O_exp //
 375           |>(times_n_O O) @lt_times // @lt_O_exp //
 376           ]
 377         |@lt_O_exp //
 378         ]
 379       ]
 380     |%
 381     ]
 382   |//
 383   ]
 384 qed.
 385
 386 theorem eq_ord_sigma_p:
 387 ∀n,m,x. O < n → prime x →
 388 exp x m ≤ n → n < exp x (S m) →
 389 ord n x= ∑_{i < m | dividesb (x\sup (S i)) n} 1.
 390 #n #m #x #posn #primex #Hexp #ltn
 391 lapply (prime_to_lt_SO ? primex) #lt1x
 392 >(exp_ord x n) in ⊢ (???%); // @sigma_p_dividesb1
 393   [@lt_O_ord_rem //
 394   |//
 395   |@not_divides_ord_rem //
 396   |@le_S_S_to_le @(le_to_lt_to_lt ? (log x n))
 397     [@le_ord_log //
 398     |@(lt_exp_to_lt x)
 399       [@lt_to_le //
 400       |@(le_to_lt_to_lt ? n ? ? ltn) @le_exp_log //
 401       ]
 402     ]
 403   ]
 404 qed.
 405
 406 theorem pi_p_primeb1: ∀n. O < n →
 407 n = ∏_{p < S n| primeb p}
 408   (∏_{i < log p n| dividesb (exp p (S i)) n} p).
 409 #n #posn >(pi_p_primeb n posn) in ⊢ (??%?);
 410 @same_bigop
 411   [//
 412   |#p #ltp #primep >exp_sigma @eq_f @eq_ord_sigma_p
 413     [//
 414     |@primeb_true_to_prime //
 415     |@le_exp_log //
 416     |@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 417     ]
 418   ]
 419 qed.
 420
 421 (* the factorial function *)
 422 theorem eq_fact_pi_p:∀n.
 423   fact n = ∏_{i < S n | leb 1 i} i.
 424 #n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue
 425   [@eq_f // | % ]
 426 qed.
 427
 428 theorem eq_sigma_p_div: ∀n,q.O < q →
 429   ∑_{ m < S n | leb (S O) m ∧ dividesb q m} 1 =n/q.
 430 #n #q #posq
 431 @(div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
 432   [@div_mod_spec_intro
 433     [@lt_mod_m_m //
 434     |elim n
 435       [normalize cases q //
 436       |#n1 #Hind cases (or_div_mod1 n1 q posq)
 437         [* #divq #eqn1  >divides_to_mod_O //
 438          <plus_n_O >bigop_Strue
 439           [>eqn1 in ⊢ (??%?); @eq_f2
 440             [<commutative_plus <plus_n_Sm <plus_n_O @eq_f
 441              @(div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
 442               [@div_mod_spec_div_mod //
 443               |@div_mod_spec_intro [@lt_mod_m_m // | //]
 444               ]
 445             |%
 446             ]
 447           |@true_to_andb_true [//|@divides_to_dividesb_true //]
 448           ]
 449         |* #ndiv #eqn1 >bigop_Sfalse
 450           [>(mod_S … posq)
 451             [< plus_n_Sm @eq_f //
 452             |cases (le_to_or_lt_eq (S (mod n1 q)) q ?)
 453               [//
 454               |#eqq @False_ind cases ndiv #Hdiv @Hdiv
 455                %{(S(div n1 q))} <times_n_Sm <commutative_plus //
 456               |@lt_mod_m_m //
 457               ]
 458             ]
 459           |>not_divides_to_dividesb_false //
 460           ]
 461         ]
 462       ]
 463     ]
 464   |@div_mod_spec_div_mod //
 465   ]
 466 qed.
 467
 468 lemma timesACdef: ∀n,m. timesAC n m = n * m.
 469 // qed-.
 470
 471 (* still another characterization of the factorial *)
 472 theorem fact_pi_p: ∀n.
 473 fact n = ∏_{ p < S n | primeb p}
 474            (∏_{i < log p n} (exp p (n /(exp p (S i))))).
 475 #n >eq_fact_pi_p
 476 @(trans_eq ??
 477   (∏_{m < S n | leb 1 m}
 478    (∏_{p < S m | primeb p}
 479     (∏_{i < log p m | dividesb (exp p (S i)) m} p))))
 480   [@same_bigop [// |#x #Hx1 #Hx2  @pi_p_primeb1 @leb_true_to_le //]
 481   |@(trans_eq ??
 482     (∏_{m < S n | leb 1 m}
 483       (∏_{p < S m | primeb p ∧ leb p m}
 484        (∏_{ i < log p m | dividesb ((p)\sup(S i)) m} p))))
 485     [@same_bigop
 486       [//
 487       |#x #Hx1 #Hx2 @same_bigop
 488         [#p #ltp >(le_to_leb_true … (le_S_S_to_le …ltp))
 489          cases (primeb p) //
 490         |//
 491         ]
 492       ]
 493     |@(trans_eq ??
 494       (∏_{m < S n | leb 1 m}
 495        (∏_{p < S n | primeb p ∧ leb p m}
 496          (∏_{i < log p m |dividesb ((p)\sup(S i)) m} p))))
 497       [@same_bigop
 498         [//
 499         |#p #Hp1 #Hp2 @pad_bigop1
 500           [@Hp1
 501           |#i #lti #upi >lt_to_leb_false
 502             [cases (primeb i) //|@lti]
 503           ]
 504         ]
 505       |(* make a general theorem *)
 506        @(trans_eq ??
 507         (∏_{p < S n | primeb p}
 508           (∏_{m < S n | leb p m}
 509            (∏_{i < log p m | dividesb (p^(S i)) m} p))))
 510         [@(bigop_commute … timesAC … (lt_O_S n) (lt_O_S n))
 511          #i #j #lti #ltj
 512          cases (true_or_false (primeb j ∧ leb j i)) #Hc >Hc
 513           [>(le_to_leb_true 1 i)
 514             [//
 515             |@(transitive_le ? j)
 516               [@prime_to_lt_O @primeb_true_to_prime @(andb_true_l ? ? Hc)
 517               |@leb_true_to_le @(andb_true_r ?? Hc)
 518               ]
 519             ]
 520           |cases(leb 1 i) //
 521           ]
 522         |@same_bigop
 523           [//
 524           |#p #Hp1 #Hp2
 525            @(trans_eq ??
 526             (∏_{m < S n | leb p m}
 527              (∏_{i < log p n | dividesb (p\sup(S i)) m} p)))
 528             [@same_bigop
 529               [//
 530               |#x #Hx1 #Hx2 @sym_eq
 531                @sym_eq @pad_bigop1
 532                 [@le_log
 533                   [@prime_to_lt_SO @primeb_true_to_prime //
 534                   |@le_S_S_to_le //
 535                   ]
 536                 |#i #Hi1 #Hi2 @not_divides_to_dividesb_false
 537                   [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //
 538                   |@(not_to_not … (lt_to_not_le x (exp p (S i)) ?))
 539                     [#H @divides_to_le // @(lt_to_le_to_lt ? p)
 540                       [@prime_to_lt_O @primeb_true_to_prime //
 541                       |@leb_true_to_le //
 542                       ]
 543                     |@(lt_to_le_to_lt ? (exp p (S(log p x))))
 544                       [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 545                       |@le_exp
 546                         [@ prime_to_lt_O @primeb_true_to_prime //
 547                         |@le_S_S //
 548                         ]
 549                       ]
 550                     ]
 551                   ]
 552                 ]
 553               ]
 554             |@
 555              (trans_eq ? ?
 556               (∏_{i < log p n}
 557                 (∏_{m < S n | leb p m ∧ dividesb (p\sup(S i)) m} p)))
 558               [@(bigop_commute ?????? nat 1 timesAC (λm,i.p) ???) //
 559                cut (p ≤ n) [@le_S_S_to_le //] #lepn
 560                @(lt_O_log … lepn) @(lt_to_le_to_lt … lepn) @prime_to_lt_SO
 561                @primeb_true_to_prime //
 562               |@same_bigop
 563                 [//
 564                 |#m #ltm #_ >exp_sigma @eq_f
 565                  @(trans_eq ??
 566                   (∑_{i < S n |leb 1 i∧dividesb (p\sup(S m)) i} 1))
 567                   [@same_bigop
 568                     [#i #lti
 569                      cases (true_or_false (dividesb (p\sup(S m)) i)) #Hc >Hc
 570                       [cases (true_or_false (leb p i)) #Hp3 >Hp3
 571                         [>le_to_leb_true
 572                           [//
 573                           |@(transitive_le ? p)
 574                             [@prime_to_lt_O @primeb_true_to_prime //
 575                             |@leb_true_to_le //
 576                             ]
 577                           ]
 578                         |>lt_to_leb_false
 579                           [//
 580                           |@not_le_to_lt
 581                            @(not_to_not ??? (leb_false_to_not_le ?? Hp3)) #posi
 582                            @(transitive_le ? (exp p (S m)))
 583                             [>(exp_n_1 p) in ⊢ (?%?);
 584                              @le_exp
 585                               [@prime_to_lt_O @primeb_true_to_prime //
 586                               |@le_S_S @le_O_n
 587                               ]
 588                             |@(divides_to_le … posi)
 589                              @dividesb_true_to_divides //
 590                             ]
 591                           ]
 592                         ]
 593                       |cases (leb p i) cases (leb 1 i) //
 594                       ]
 595                     |//
 596                     ]
 597                   |@eq_sigma_p_div @lt_O_exp
 598                    @prime_to_lt_O @primeb_true_to_prime //
 599                   ]
 600                 ]
 601               ]
 602             ]
 603           ]
 604         ]
 605       ]
 606     ]
 607   ]
 608 qed.
 609
 610 theorem fact_pi_p2: ∀n. fact (2*n) =
 611 ∏_{p < S (2*n) | primeb p}
 612   (∏_{i < log p (2*n)}
 613     (exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))).
 614 #n >fact_pi_p @same_bigop
 615   [//
 616   |#p #ltp #primep @same_bigop
 617     [//
 618     |#i #lti #_ <exp_plus_times @eq_f
 619      >commutative_times in ⊢ (???(?%?));
 620      cut (0 < p ^ (S i))
 621        [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //]
 622      generalize in match (p ^(S i)); #a #posa
 623      >(div_times_times n a 2) // >(commutative_times n 2)
 624      <eq_div_div_div_times //
 625     ]
 626   ]
 627 qed.
 628
 629 theorem fact_pi_p3: ∀n. fact (2*n) =
 630 ∏_{p < S (2*n) | primeb p}
 631   (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))) *
 632 ∏_{p < S (2*n) | primeb p}
 633   (∏_{i < log p (2*n)}(exp p (mod (2*n /(exp p (S i))) 2))).
 634 #n <times_pi >fact_pi_p2 @same_bigop
 635   [//
 636   |#p #ltp #primep @times_pi
 637   ]
 638 qed.
 639
 640 theorem pi_p_primeb4: ∀n. 1 < n →
 641 ∏_{p < S (2*n) | primeb p}
 642   (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i))))))
 643 =
 644 ∏_{p < S n | primeb p}
 645   (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))).
 646 #n #lt1n
 647 @sym_eq @(pad_bigop_nil … timesAC)
 648   [@le_S_S /2 by /
 649   |#i #ltn #lti %2
 650    >log_i_2n //
 651     [>bigop_Strue // whd in ⊢ (??(??%)?); <times_n_1
 652      <exp_n_1 >eq_div_O //
 653     |@le_S_S_to_le //
 654     ]
 655   ]
 656 qed.
 657
 658 theorem pi_p_primeb5: ∀n. 1 < n →
 659 ∏_{p < S (2*n) | primeb p}
 660   (∏_{i < log p (2*n)} (exp p (2*(n /(exp p (S i))))))
 661 =
 662 ∏_{p < S n | primeb p}
 663   (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))).
 664 #n #lt1n >(pi_p_primeb4 ? lt1n) @same_bigop
 665   [//
 666   |#p #lepn #primebp @sym_eq @(pad_bigop_nil … timesAC)
 667     [@le_log
 668       [@prime_to_lt_SO @primeb_true_to_prime //
 669       |//
 670       ]
 671     |#i #lelog #lti %2 >eq_div_O //
 672      @(lt_to_le_to_lt ? (exp p (S(log p n))))
 673       [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
 674       |@le_exp
 675         [@prime_to_lt_O @primeb_true_to_prime // |@le_S_S //]
 676       ]
 677     ]
 678   ]
 679 qed.
 680
 681 theorem exp_fact_2: ∀n.
 682 exp (fact n) 2 =
 683   ∏_{p < S n| primeb p}
 684     (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))).
 685 #n >fact_pi_p <exp_pi @same_bigop
 686   [//
 687   |#p #ltp #primebp @sym_eq
 688    @(trans_eq ?? (∏_{x < log p n} (exp (exp p (n/(exp p (S x)))) 2)))
 689   [@same_bigop
 690     [//
 691     |#x #ltx #_ @sym_eq >commutative_times @exp_exp_times
 692     ]
 693   |@exp_pi
 694   ]
 695 qed.
 696