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