From fd12cbee622c58bc45089d62c3e6f131c238beb5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 3 Jan 2013 16:49:01 +0000 Subject: [PATCH] refactoring --- .../lib/arithmetics/chebyshev/bertrand256.ma | 2 +- .../lib/arithmetics/chebyshev/chebyshev.ma | 696 ------------------ .../arithmetics/chebyshev/chebyshev_teta.ma | 214 ------ 3 files changed, 1 insertion(+), 911 deletions(-) delete mode 100644 matita/matita/lib/arithmetics/chebyshev/chebyshev.ma delete mode 100644 matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma diff --git a/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma index 163125b81..c65e62381 100644 --- a/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma +++ b/matita/matita/lib/arithmetics/chebyshev/bertrand256.ma @@ -236,6 +236,6 @@ theorem bertrand : ∀n. O < n → bertrand n. #n #posn elim (decidable_le n 256) [@bertrand_down // - |#len @le_to_bertrand2 @lt_to_le @not_le_to_lt @len] + |#len @bertrand_up @lt_to_le @not_le_to_lt @len] qed. diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma deleted file mode 100644 index 50fb09fd7..000000000 --- a/matita/matita/lib/arithmetics/chebyshev/chebyshev.ma +++ /dev/null @@ -1,696 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| - \ / This file is distributed under the terms of the - \ / GNU General Public License Version 2 - V_____________________________________________________________*) - -include "arithmetics/log.ma". -include "arithmetics/sigma_pi.ma". -include "arithmetics/ord.ma". - -(* (prim n) counts the number of prime numbers up to n included *) -definition prim ≝ λn. ∑_{i < S n | primeb i} 1. - -lemma le_prim_n: ∀n. prim n ≤ n. -#n elim n // -n #n #H -whd in ⊢ (?%?); cases (primeb (S n)) whd in ⊢ (?%?); - [@le_S_S @H |@le_S @H] -qed. - -lemma not_prime_times_2: ∀n. 1 < n → ¬prime (2*n). -#n #ltn % * #H #H1 @(absurd (2 = 2*n)) - [@H1 // %{n} // - |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r // - ] -qed. - -theorem eq_prim_prim_pred: ∀n. 1 < n → - prim (2*n) = prim (pred (2*n)). -#n #ltn -lapply (S_pred (2*n) ?) [>(times_n_1 0) in ⊢ (?%?); @lt_times //] #H2n -lapply (not_prime_times_2 n ltn) #notp2n -whd in ⊢ (??%?); >(not_prime_to_primeb_false … notp2n) whd in ⊢ (??%?); -Heq - Heq - Hn normalize // - ] -qed. - -(* la prova potrebbe essere migliorata *) -theorem le_prim_n3: ∀n. 15 ≤ n → - prim n ≤ pred (n/2). -#n #len cases (even_or_odd (pred n)) #a * #Hpredn - [cut (n = S (2*a)) [Hn @(transitive_le ? (pred a)) - [@le_prim_n2 @(le_times_to_le 2) [//|@le_S_S_to_le Hn @(transitive_le ? (pred a)) - [>eq_prim_prim_pred - [2:@(lt_times_n_to_lt_r 2) Hpredn @le_prim_n2 @le_S_S_to_le @(lt_times_n_to_lt_r 2) (plus_n_O (log i n)) in ⊢ (?%?); >plus_n_Sm - @monotonic_le_plus_r @lt_O_log // - @le_S_S_to_le // - ] - ] - |bigop_Strue in ⊢ (???%); // - cases (true_or_false (dividesb n1 m)) #Hdivides - [>bigop_Strue [@eq_f @Hind| @true_to_andb_true //] - |>bigop_Sfalse - [>not_divides_to_ord_O - [whd in ⊢ (???(?%?)); // - |@dividesb_false_to_not_divides // - |@primeb_true_to_prime // - ] - |>Hprime >Hdivides % - ] - ] -|>bigop_Sfalse [>bigop_Sfalse // |>Hprime %] -] -qed. - -(* integrations to minimization *) -theorem false_to_lt_max: ∀f,n,m.O < n → - f n = false → max m f ≤ n → max m f < n. -#f #n #m #posn #Hfn #Hmax cases (le_to_or_lt_eq ?? Hmax) -Hmax #Hmax - [// - |cases (exists_max_forall_false f m) - [* #_ #Hfmax @False_ind @(absurd ?? not_eq_true_false) // - |* // - ] - ] -qed. - -(* integrations to minimization *) -lemma lt_1_max_prime: ∀n. 1 < n → - 1 < max (S n) (λi:nat.primeb i∧dividesb i n). -#n #lt1n -@(lt_to_le_to_lt ? (smallest_factor n)) - [@lt_SO_smallest_factor // - |@true_to_le_max - [@le_S_S @le_smallest_factor_n - |@true_to_andb_true - [@prime_to_primeb_true @prime_smallest_factor_n // - |@divides_to_dividesb_true - [@lt_O_smallest_factor @lt_to_le // - |@divides_smallest_factor_n @lt_to_le // - ] - ] - ] - ] -qed. - -theorem lt_max_to_pi_p_primeb: ∀q,m. Obigop_Strue - [>(exp_ord n m … posm) in ⊢ (??%?); - [@eq_f >(Hind (ord_rem m n)) - [@same_bigop - [#x #ltxn cases (true_or_false (primeb x)) #Hx >Hx - [cases (true_or_false (dividesb x (ord_rem m n))) #Hx1 >Hx1 - [@sym_eq @divides_to_dividesb_true - [@prime_to_lt_O @primeb_true_to_prime // - |@(transitive_divides ? (ord_rem m n)) - [@dividesb_true_to_divides // - |@(divides_ord_rem … posm) @(transitive_lt … ltxn) - @prime_to_lt_SO @primeb_true_to_prime // - ] - ] - |@sym_eq @not_divides_to_dividesb_false - [@prime_to_lt_O @primeb_true_to_prime // - |@(ord_O_to_not_divides … posm) - [@primeb_true_to_prime // - |<(ord_ord_rem n … posm … ltxn) - [@not_divides_to_ord_O - [@primeb_true_to_prime // - |@dividesb_false_to_not_divides // - ] - |@primeb_true_to_prime // - |@primeb_true_to_prime @(andb_true_l ?? Hcase) - ] - ] - ] - ] - |// - ] - |#x #ltxn #Hx @eq_f @ord_ord_rem // - [@primeb_true_to_prime @(andb_true_l ? ? Hcase) - |@primeb_true_to_prime @(andb_true_l ? ? Hx) - ] - ] - |@not_eq_to_le_to_lt - [elim (exists_max_forall_false (λi:nat.primeb i∧dividesb i (ord_rem m n)) (S(ord_rem m n))) - [* #Hex #Hord_rem cases Hex #x * #H6 #H7 % #H - >H in Hord_rem; #Hn @(absurd ?? (not_divides_ord_rem m n posm ?)) - [@dividesb_true_to_divides @(andb_true_r ?? Hn) - |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hn) - ] - |* #Hall #Hmax >Hmax @lt_to_not_eq @prime_to_lt_O - @primeb_true_to_prime @(andb_true_l ?? Hcase) - ] - |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i (ord_rem m n)))) - [@le_to_le_max @le_S_S @(divides_to_le … posm) @(divides_ord_rem … posm) - @prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase) - |@(transitive_le ? (max (S m) (λi:nat.primeb i∧dividesb i m))) - [@le_max_f_max_g #i #ltim #Hi - cases (true_or_false (primeb i)) #Hprimei >Hprimei - [@divides_to_dividesb_true - [@prime_to_lt_O @primeb_true_to_prime // - |@(transitive_divides ? (ord_rem m n)) - [@dividesb_true_to_divides @(andb_true_r ?? Hi) - |@(divides_ord_rem … posm) - @prime_to_lt_SO @primeb_true_to_prime - @(andb_true_l ?? Hcase) - ] - ] - |>Hprimei in Hi; #Hi @Hi - ] - |@le_S_S_to_le // - ] - ] - ] - |@(lt_O_ord_rem … posm) @prime_to_lt_SO - @primeb_true_to_prime @(andb_true_l ?? Hcase) - ] - |@prime_to_lt_SO @primeb_true_to_prime @(andb_true_l ?? Hcase) - ] - |// - ] - |cases (le_to_or_lt_eq ?? posm) #Hm - [>bigop_Sfalse - [@(Hind … posm) @false_to_lt_max - [@(lt_to_le_to_lt ? (max (S m) (λi:nat.primeb i∧dividesb i m))) - [@lt_to_le @lt_1_max_prime // - |@le_S_S_to_le // - ] - |// - |@le_S_S_to_le // - ] - |@Hcase - ] - |primei // - @sym_eq @not_divides_to_dividesb_false - [@prime_to_lt_O @primeb_true_to_prime // - |% #divi @(absurd ?? (le_to_not_lt i 1 ?)) - [@prime_to_lt_SO @(primeb_true_to_prime ? primei) - |@divides_to_le // - ] - ] - |// - ] - ] - ] - ] -qed. - -(* factorization of n into primes *) -theorem pi_p_primeb_dividesb: ∀n. O < n → - n = ∏_{ p < S n | primeb p ∧ dividesb p n} (exp p (ord n p)). -#n #posn @lt_max_to_pi_p_primeb // @lt_max_n @le_S @posn -qed. - -theorem pi_p_primeb: ∀n. O < n → - n = ∏_{ p < (S n) | primeb p}(exp p (ord n p)). -#n #posn (exp_ord p ? lt1p posn) in ⊢ (??(??%)); ->log_exp // @lt_O_ord_rem // -qed. - -theorem sigma_p_dividesb: -∀m,n,p. O < n → prime p → p ∤ n → -m = ∑_{ i < m | dividesb (p\sup (S i)) ((exp p m)*n)} 1. -#m elim m // -m #m #Hind #n #p #posn #primep #ndivp ->bigop_Strue - [>commutative_plus (Hind n p posn primep ndivp) in ⊢ (? ? % ?); - @same_bigop - [#i #ltim cases (true_or_false (dividesb (p\sup(S i)) (p\sup m*n))) #Hc >Hc - [@sym_eq @divides_to_dividesb_true - [@lt_O_exp @prime_to_lt_O // - |%{((exp p (m - i))*n)} commutative_plus - @plus_minus_m_m @lt_to_le // - ] - |@False_ind @(absurd ?? (dividesb_false_to_not_divides ? ? Hc)) - %{((exp p (m - S i))*n)} commutative_plus @plus_minus_m_m // - assumption - |% - ] - ] - |// - ] - |@divides_to_dividesb_true - [@lt_O_exp @prime_to_lt_O // | %{n} //] - ] -qed. - -theorem sigma_p_dividesb1: -∀m,n,p,k. O < n → prime p → p ∤ n → m ≤ k → - m = ∑_{i < k | dividesb (p\sup (S i)) ((exp p m)*n)} 1. -#m #n #p #k #posn #primep #ndivp #lemk -lapply (prime_to_lt_SO ? primep) #lt1p -lapply (prime_to_lt_O ? primep) #posp ->(sigma_p_dividesb m n p posn primep ndivp) in ⊢ (??%?); ->(pad_bigop k m) // @same_bigop - [#i #ltik cases (true_or_false (leb m i)) #Him > Him - [whd in ⊢(??%?); @sym_eq - @not_divides_to_dividesb_false - [@lt_O_exp // - |lapply (leb_true_to_le … Him) -Him #Him - % #Hdiv @(absurd ?? (le_to_not_lt ?? Him)) - (* <(ord_exp p m lt1p) *) >(plus_n_O m) - <(not_divides_to_ord_O ?? primep ndivp) - <(ord_exp p m lt1p) - (times_n_O O) @lt_times // @lt_O_exp // - ] - |@lt_O_exp // - ] - ] - |% - ] - |// - ] -qed. - -theorem eq_ord_sigma_p: -∀n,m,x. O < n → prime x → -exp x m ≤ n → n < exp x (S m) → -ord n x= ∑_{i < m | dividesb (x\sup (S i)) n} 1. -#n #m #x #posn #primex #Hexp #ltn -lapply (prime_to_lt_SO ? primex) #lt1x ->(exp_ord x n) in ⊢ (???%); // @sigma_p_dividesb1 - [@lt_O_ord_rem // - |// - |@not_divides_ord_rem // - |@le_S_S_to_le @(le_to_lt_to_lt ? (log x n)) - [@le_ord_log // - |@(lt_exp_to_lt x) - [@lt_to_le // - |@(le_to_lt_to_lt ? n ? ? ltn) @le_exp_log // - ] - ] - ] -qed. - -theorem pi_p_primeb1: ∀n. O < n → -n = ∏_{p < S n| primeb p} - (∏_{i < log p n| dividesb (exp p (S i)) n} p). -#n #posn >(pi_p_primeb n posn) in ⊢ (??%?); -@same_bigop - [// - |#p #ltp #primep >exp_sigma @eq_f @eq_ord_sigma_p - [// - |@primeb_true_to_prime // - |@le_exp_log // - |@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // - ] - ] -qed. - -(* the factorial function *) -theorem eq_fact_pi_p:∀n. - fact n = ∏_{i < S n | leb 1 i} i. -#n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue - [@eq_f // | % ] -qed. - -theorem eq_sigma_p_div: ∀n,q.O < q → - ∑_{ m < S n | leb (S O) m ∧ dividesb q m} 1 =n/q. -#n #q #posq -@(div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q)) - [@div_mod_spec_intro - [@lt_mod_m_m // - |elim n - [normalize cases q // - |#n1 #Hind cases (or_div_mod1 n1 q posq) - [* #divq #eqn1 >divides_to_mod_O // - bigop_Strue - [>eqn1 in ⊢ (??%?); @eq_f2 - [bigop_Sfalse - [>(mod_S … posq) - [< plus_n_Sm @eq_f // - |cases (le_to_or_lt_eq (S (mod n1 q)) q ?) - [// - |#eqq @False_ind cases ndiv #Hdiv @Hdiv - %{(S(div n1 q))} not_divides_to_dividesb_false // - ] - ] - ] - ] - |@div_mod_spec_div_mod // - ] -qed. - -lemma timesACdef: ∀n,m. timesAC n m = n * m. -// qed-. - -(* still another characterization of the factorial *) -theorem fact_pi_p: ∀n. -fact n = ∏_{ p < S n | primeb p} - (∏_{i < log p n} (exp p (n /(exp p (S i))))). -#n >eq_fact_pi_p -@(trans_eq ?? - (∏_{m < S n | leb 1 m} - (∏_{p < S m | primeb p} - (∏_{i < log p m | dividesb (exp p (S i)) m} p)))) - [@same_bigop [// |#x #Hx1 #Hx2 @pi_p_primeb1 @leb_true_to_le //] - |@(trans_eq ?? - (∏_{m < S n | leb 1 m} - (∏_{p < S m | primeb p ∧ leb p m} - (∏_{ i < log p m | dividesb ((p)\sup(S i)) m} p)))) - [@same_bigop - [// - |#x #Hx1 #Hx2 @same_bigop - [#p #ltp >(le_to_leb_true … (le_S_S_to_le …ltp)) - cases (primeb p) // - |// - ] - ] - |@(trans_eq ?? - (∏_{m < S n | leb 1 m} - (∏_{p < S n | primeb p ∧ leb p m} - (∏_{i < log p m |dividesb ((p)\sup(S i)) m} p)))) - [@same_bigop - [// - |#p #Hp1 #Hp2 @pad_bigop1 - [@Hp1 - |#i #lti #upi >lt_to_leb_false - [cases (primeb i) //|@lti] - ] - ] - |(* make a general theorem *) - @(trans_eq ?? - (∏_{p < S n | primeb p} - (∏_{m < S n | leb p m} - (∏_{i < log p m | dividesb (p^(S i)) m} p)))) - [@(bigop_commute … timesAC … (lt_O_S n) (lt_O_S n)) - #i #j #lti #ltj - cases (true_or_false (primeb j ∧ leb j i)) #Hc >Hc - [>(le_to_leb_true 1 i) - [// - |@(transitive_le ? j) - [@prime_to_lt_O @primeb_true_to_prime @(andb_true_l ? ? Hc) - |@leb_true_to_le @(andb_true_r ?? Hc) - ] - ] - |cases(leb 1 i) // - ] - |@same_bigop - [// - |#p #Hp1 #Hp2 - @(trans_eq ?? - (∏_{m < S n | leb p m} - (∏_{i < log p n | dividesb (p\sup(S i)) m} p))) - [@same_bigop - [// - |#x #Hx1 #Hx2 @sym_eq - @sym_eq @pad_bigop1 - [@le_log - [@prime_to_lt_SO @primeb_true_to_prime // - |@le_S_S_to_le // - ] - |#i #Hi1 #Hi2 @not_divides_to_dividesb_false - [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime // - |@(not_to_not … (lt_to_not_le x (exp p (S i)) ?)) - [#H @divides_to_le // @(lt_to_le_to_lt ? p) - [@prime_to_lt_O @primeb_true_to_prime // - |@leb_true_to_le // - ] - |@(lt_to_le_to_lt ? (exp p (S(log p x)))) - [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // - |@le_exp - [@ prime_to_lt_O @primeb_true_to_prime // - |@le_S_S // - ] - ] - ] - ] - ] - ] - |@ - (trans_eq ? ? - (∏_{i < log p n} - (∏_{m < S n | leb p m ∧ dividesb (p\sup(S i)) m} p))) - [@(bigop_commute ?????? nat 1 timesAC (λm,i.p) ???) // - cut (p ≤ n) [@le_S_S_to_le //] #lepn - @(lt_O_log … lepn) @(lt_to_le_to_lt … lepn) @prime_to_lt_SO - @primeb_true_to_prime // - |@same_bigop - [// - |#m #ltm #_ >exp_sigma @eq_f - @(trans_eq ?? - (∑_{i < S n |leb 1 i∧dividesb (p\sup(S m)) i} 1)) - [@same_bigop - [#i #lti - cases (true_or_false (dividesb (p\sup(S m)) i)) #Hc >Hc - [cases (true_or_false (leb p i)) #Hp3 >Hp3 - [>le_to_leb_true - [// - |@(transitive_le ? p) - [@prime_to_lt_O @primeb_true_to_prime // - |@leb_true_to_le // - ] - ] - |>lt_to_leb_false - [// - |@not_le_to_lt - @(not_to_not ??? (leb_false_to_not_le ?? Hp3)) #posi - @(transitive_le ? (exp p (S m))) - [>(exp_n_1 p) in ⊢ (?%?); - @le_exp - [@prime_to_lt_O @primeb_true_to_prime // - |@le_S_S @le_O_n - ] - |@(divides_to_le … posi) - @dividesb_true_to_divides // - ] - ] - ] - |cases (leb p i) cases (leb 1 i) // - ] - |// - ] - |@eq_sigma_p_div @lt_O_exp - @prime_to_lt_O @primeb_true_to_prime // - ] - ] - ] - ] - ] - ] - ] - ] - ] -qed. - -theorem fact_pi_p2: ∀n. fact (2*n) = -∏_{p < S (2*n) | primeb p} - (∏_{i < log p (2*n)} - (exp p (2*(n /(exp p (S i))))*(exp p (mod (2*n /(exp p (S i))) 2)))). -#n >fact_pi_p @same_bigop - [// - |#p #ltp #primep @same_bigop - [// - |#i #lti #_ commutative_times in ⊢ (???(?%?)); - cut (0 < p ^ (S i)) - [@lt_O_exp @prime_to_lt_O @primeb_true_to_prime //] - generalize in match (p ^(S i)); #a #posa - >(div_times_times n a 2) // >(commutative_times n 2) - fact_pi_p2 @same_bigop - [// - |#p #ltp #primep @times_pi - ] -qed. - -theorem pi_p_primeb4: ∀n. 1 < n → -∏_{p < S (2*n) | primeb p} - (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))) -= -∏_{p < S n | primeb p} - (∏_{i < log p (2*n)}(exp p (2*(n /(exp p (S i)))))). -#n #lt1n -@sym_eq @(pad_bigop_nil … timesAC) - [@le_S_S /2 by / - |#i #ltn #lti %2 - >log_i_2n // - [>bigop_Strue // whd in ⊢ (??(??%)?); eq_div_O // - |@le_S_S_to_le // - ] - ] -qed. - -theorem pi_p_primeb5: ∀n. 1 < n → -∏_{p < S (2*n) | primeb p} - (∏_{i < log p (2*n)} (exp p (2*(n /(exp p (S i)))))) -= -∏_{p < S n | primeb p} - (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))). -#n #lt1n >(pi_p_primeb4 ? lt1n) @same_bigop - [// - |#p #lepn #primebp @sym_eq @(pad_bigop_nil … timesAC) - [@le_log - [@prime_to_lt_SO @primeb_true_to_prime // - |// - ] - |#i #lelog #lti %2 >eq_div_O // - @(lt_to_le_to_lt ? (exp p (S(log p n)))) - [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime // - |@le_exp - [@prime_to_lt_O @primeb_true_to_prime // |@le_S_S //] - ] - ] - ] -qed. - -theorem exp_fact_2: ∀n. -exp (fact n) 2 = - ∏_{p < S n| primeb p} - (∏_{i < log p n} (exp p (2*(n /(exp p (S i)))))). -#n >fact_pi_p commutative_times @exp_exp_times - ] - |@exp_pi - ] -qed. - diff --git a/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma b/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma deleted file mode 100644 index d2fb6bbd4..000000000 --- a/matita/matita/lib/arithmetics/chebyshev/chebyshev_teta.ma +++ /dev/null @@ -1,214 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "arithmetics/binomial.ma". -include "arithmetics/gcd.ma". -include "arithmetics/chebyshev/chebyshev_psi.ma". - -(* This is chebishev theta function *) - -definition theta: nat → nat ≝ λn. - ∏_{p < S n| primeb p} p. - -lemma theta_def: ∀n.theta n = ∏_{p < S n| primeb p} p. -// qed. - -theorem lt_O_theta: ∀n. O < theta n. -#n elim n - [@le_n - |#n1 #Hind cases (true_or_false (primeb (S n1))) #Hc - [>theta_def >bigop_Strue - [>(times_n_O O) @lt_times // | //] - |>theta_def >bigop_Sfalse // - ] - ] -qed. - -theorem divides_fact_to_divides: ∀p,n. prime p → divides p n! → - ∃m.O < m ∧ m \le n ∧ divides p m. -#p #n #primep elim n - [normalize in ⊢ (%→?); #H @False_ind @(absurd (p ≤1)) - [@divides_to_le //|@lt_to_not_le @prime_to_lt_SO @primep] - |#n1 #Hind >factS #Hdiv - cases (divides_times_to_divides ??? primep Hdiv) #Hcase - [%{(S n1)} %[ % [@lt_O_S |@le_n] |@Hcase] - |cases(Hind Hcase) #a * * #posa #lea #diva - %{a} % [% [// |@le_S //] |//] - ] - ] -qed. - -theorem divides_fact_to_le: ∀p,n. prime p → divides p n! → p ≤ n. -#p #n #primep #divp cases (divides_fact_to_divides p n primep divp) -#a * * #posa #lea #diva @(transitive_le ? a) [@divides_to_le // | //] -qed. - -theorem prime_to_divides_M: ∀m,p. - prime p → S m < p → p ≤ S(2*m) → divides p (M m). -#m #p #primep #lemp #lep >Mdef >bceq -cases (bc2 (S(2*m)) m ?) - [#q #Hq >Hq >commutative_times >div_times - [cases (divides_times_to_divides p (m!*(S (2*m)-m)!) q primep ?) - [#Hdiv @False_ind - cases (divides_times_to_divides p (m!) (S (2*m)-m)! primep ?) - [-Hdiv #Hdiv @(absurd (p ≤ m)) - [@divides_fact_to_le // - |@(lt_to_not_le ?? (lt_to_le ?? lemp)) - ] - |-Hdiv #Hdiv @(absurd (p ≤S m)) - [@(divides_fact_to_le … primep) - cut (S m = S(2*m)-m) - [normalize in ⊢ (???(?%?)); plus_n_Sm >commutative_plus @minus_plus_m_m - ] #HSm - >HSm // - |@lt_to_not_le // - ] - |// - ] - |// - |(times_n_O O) in ⊢ (?%?); @lt_times // - ] - |normalize in ⊢ (??(?%)); commutative_times @times_n_1 - |#n #Hind #len - cases (true_or_false (leb (S (S m)) n ∧ primeb n)) #Hc - [>bigop_Strue - [@divides_to_divides_times - [@primeb_true_to_prime @(andb_true_r ?? Hc) - |cut (∀p.prime p → n ≤ p → ¬p∣∏_{p < n | leb (S (S m)) p∧primeb p} p) - [2: #Hcut @(Hcut … (le_n ?)) @primeb_true_to_prime @(andb_true_r ?? Hc)] - #p #primep elim n - [#_ normalize @(not_to_not ? (p ≤ 1)) - [@divides_to_le @lt_O_S|@lt_to_not_le @prime_to_lt_SO //] - |#n1 #Hind1 #Hn1 cases (true_or_false (leb (S (S m)) n1∧primeb n1)) #Hc1 - [>bigop_Strue - [% #Habs cases(divides_times_to_divides ??? primep Habs) - [-Habs #Habs @(absurd … Hn1) @le_to_not_lt - @(divides_to_le … Habs) @prime_to_lt_O - @primeb_true_to_prime @(andb_true_r ?? Hc1) - |-Habs #Habs @(absurd … Habs) @Hind1 @lt_to_le // - ] - |@Hc1 - ] - |>bigop_Sfalse // @Hind1 @lt_to_le // - ] - ] - |@prime_to_divides_M - [@primeb_true_to_prime @(andb_true_r ?? Hc) - |@leb_true_to_le @(andb_true_l ?? Hc) - |@le_S_S_to_le // - ] - |@Hind @lt_to_le // - ] - |@Hc - ] - |>bigop_Sfalse // @Hind @lt_to_le @len - ] - ] -qed. - -theorem divides_pi_p_M:∀m. - ∏_{p < S(S(2*m)) | leb (S(S m)) p ∧ primeb p} p ∣ (M m). -#m @divides_pi_p_M1 @le_n -qed. - -theorem theta_pi_p_theta: ∀m. theta (S (2*m)) -= (∏_{p < S (S (2*m)) | leb (S (S m)) p∧primeb p} p)*theta (S m). -#m >theta_def >theta_def -<(bigop_I ???? timesA) ->(bigop_sumI 0 (S(S m)) (S(S(2*m))) (λp.primeb p) … timesA (λp.p)) - [2:@le_S_S @le_S_S // |3:@le_O_n] -@eq_f2 - [>bigop_I_gen // |@(bigop_I … timesA)] -qed. - -theorem div_theta_theta: ∀m. - theta (S(2*m))/theta (S m) = - ∏_{p < S(S(2*m)) | leb (S(S m)) p ∧ primeb p} p. -#m @(div_mod_spec_to_eq ????? 0 (div_mod_spec_div_mod …)) - [@lt_O_theta - |@div_mod_spec_intro [@lt_O_theta |theta_pi_p_theta @le_times [2://] @divides_to_le - [@lt_O_bc @lt_to_le @le_S_S // | @divides_pi_p_M - ] -qed. - -theorem lt_O_to_le_theta_exp_theta: ∀m. O < m→ - theta (S(2*m)) < exp 2 (2*m)*theta (S m). -#m #posm @(le_to_lt_to_lt ? (M m*theta (S m))) - [@le_theta_M_theta - |@monotonic_lt_times_l [@lt_O_theta|@lt_M //] - ] -qed. - -theorem theta_pred: ∀n. 1 < n → theta (2*n) = theta (pred (2*n)). -#n #lt1n >theta_def >theta_def >bigop_Sfalse - [>S_pred - [// - |>(times_n_O 2) in ⊢ (?%?); @monotonic_lt_times_r @lt_to_le // - ] - |@not_prime_to_primeb_false % * #lt2n #Hprime - @(absurd (2=2*n)) - [@(Hprime … (le_n ?)) %{n} // - |@lt_to_not_eq >(times_n_1 2) in ⊢ (?%?); @monotonic_lt_times_r // - ] - ] -qed. - -theorem le_theta: ∀m.theta m ≤ exp 2 (2*m). -#m @(nat_elim1 m) #m1 #Hind -cut (∀a. 2 *a = a+a) [//] #times2 -cases (even_or_odd m1) #a * #Ha >Ha - [lapply Ha cases a - [#_ @le_n - |#n cases n - [#_ @leb_true_to_le // - |#n1 #Hn1 >theta_pred - [cut (pred (2*S(S n1)) = (S (2*S n1))) - [normalize >plus_n_Sm in ⊢ (???%); //] #Hcut >Hcut - @(transitive_le ? (exp 2 (2*(S n1))*theta (S (S n1)))) - [@lt_to_le @lt_O_to_le_theta_exp_theta @lt_O_S - |>times2 in ⊢ (??%);>exp_plus_times in ⊢ (??%); @le_times - [@le_exp [@lt_O_S |@monotonic_le_times_r @le_n_Sn] - |@Hind >Hn1 >times2 // - ] - ] - |@le_S_S @lt_O_S - ] - ] - ] - |lapply Ha cases a - [#_ @leb_true_to_le // - |#n #Hn @(transitive_le ? (exp 2 (2*(S n))*theta (S (S n)))) - [@lt_to_le @lt_O_to_le_theta_exp_theta @lt_O_S - |>times2 in ⊢ (??%); plus_n_Sm - >exp_plus_times in ⊢ (??%); @monotonic_le_times_r - cut (∀a. 2*(S a) = S(S(2*a))) [#a normalize Hn @le_S_S >times2 // - ] - ] - ] -qed. - -- 2.39.2