proposition: Theorem upper_bound : forall n : nat, power 2 7 <= n -> (forall p : nat, n < p -> p < 2 * n -> ~ prime p) -> binomial (2 * n) n < power (2 * n) (div (sqr (2 * n)) 2 - 1) * power 4 (div (2 * n) 3).
proof: Proof. intros n H H0. cut (0 < n); [ intros Hn | apply Nat.lt_le_trans with (2 := H); simpl in |- * ]; auto with arith. cut (0 < binomial (2 * n) n); [ intros Hc | replace (2 * n) with (n + n); try apply binomial_lt; auto with arith; ring ]. cut (sqr (2 * n) < div (2 * n) 3); [ intros Hd | idtac ]. rewrite (fun x y : nat => factorization (binomial x y) (div (2 * n) 3)); auto with arith. rewrite prod_nm_split with (r := sqr (2 * n)); auto with arith. apply Nat.lt_le_trans with (prod_nm 0 (sqr (2 * n)) (fun x : nat => power (prime_dirac x) (power_div (binomial (2 * n) n) x)) * power 4 (div (2 * n) 3)). apply mult_lt_bis. apply Nat.lt_le_trans with (power 1 (S (sqr (2 * n)))); auto with arith. rewrite SO_power; auto with arith. rewrite <- prod_nm_c with (p := 0); apply prod_nm_le; auto with arith. intros x H1 H2. apply Nat.le_succ_l; auto with arith. apply power_lt_O. case (prime_dec x); intros Hx; [ rewrite prime_prime_dirac | rewrite not_prime_prime_dirac ]; auto with arith. generalize Hx; case x; auto with arith; intros Hx1; Contradict Hx1; auto with arith. rewrite <- (fun x y f => Nat.mul_1_l (prod_nm x y f)). pattern 1 at 1 in |- *; rewrite <- (SO_power (S (sqr (2 * n)))). apply Nat.le_lt_trans with (prod_nm 0 (div (2 * n) 3) (fun x : nat => prime_dirac x)); auto with arith. rewrite prod_nm_split with (p := 0) (r := sqr (2 * n)); auto with arith. apply le_mult. rewrite <- prod_nm_c with (p := 0). apply prod_nm_le. intros x H7 H8; unfold prime_dirac in |- *; generalize (primeb_correct x); case (primeb x); auto with arith. case x; auto with arith. intros H9; Contradict H9; auto with arith. apply prod_nm_le. intros x H7 H8. unfold prime_dirac in |- *; generalize (primeb_correct x); case (primeb x); intros Hx. pattern x at 3 in |- *; rewrite <- power_SO. apply power_le_mono. generalize Hx; case x; auto with arith. intros H9; Contradict H9; auto with arith. apply power_div_binomial2; auto with arith. apply Nat.lt_le_trans with (1 := sqr_lt (2 * n)). replace (power x 2) with (x * x); [ apply le_mult | simpl in |- *; ring ]; auto with arith. rewrite SO_power; auto with arith. apply prod_prime_lt; auto with arith. apply Nat.lt_le_trans with (2 := Hd). apply Nat.lt_succ_r; auto with arith. apply (sqr_mono 1). apply Nat.le_trans with (2 * power 2 7); auto with arith; simpl in |- *; auto with arith. apply le_mult. apply prod_prime_le with (f := fun x : nat => power (prime_dirac x) (power_div (binomial (2 * n) n) x)); auto with arith. replace (power 2 4) with (sqr (2 * power 2 7)); [ idtac | auto ]. apply sqr_mono; auto with arith. intros x H7 H8. rewrite prime_prime_dirac; auto; apply power_div_binomial1; auto. intros x H7 H8. rewrite not_prime_prime_dirac; auto; apply SO_power; auto. auto with arith. intros x H7 H8. case (Nat.le_gt_cases x (2 * n)); intros Hp1. case (Nat.le_gt_cases x n); intros Hp2. replace x with (power x (1 + power_div (binomial (2 * n) n) x)). apply power_div_not_divides; auto with arith. generalize H8; case x; auto with arith. intros Ht; Contradict Ht; auto with arith. intros x1; case x1; auto with arith. intros Ht; Contradict Ht; auto with arith. rewrite power_div_binomial3; auto with arith. simpl in |- *; ring. apply Nat.lt_le_trans with (2 := H); simpl in |- *; auto with arith. apply Nat.lt_le_trans with (3 * (1 + div (2 * n) 3)); auto with arith. apply div_lt; auto with arith. case (proj1 (Nat.lt_eq_cases _ _) Hp1); intros Hp3; auto with arith. contradict H8; auto with arith. contradict H8; auto with arith. rewrite Hp3. red in |- *; intros (H9, H10). absurd (2 * n = 2). red in |- *; intros H11; contradict H. apply Nat.lt_nge. apply lt_mult_right_anti with (z := 2); rewrite H11; simpl in |- *; auto with arith. apply H10; auto with arith. exists n; auto with arith. red in |- *; intros H9; absurd (divides (power x (power_div (binomial (2 * n) n) x)) (binomial (2 * n) n)). red in |- *; intros H10; absurd (power x (power_div (binomial (2 * n) n) x) <= 2 * n). apply Nat.lt_nge; apply Nat.lt_le_trans with (1 := Hp1). generalize (power_div_not_divides (binomial (2 * n) n) x). case (power_div (binomial (2 * n) n) x); auto with arith. intros H11; case H11; auto with arith. generalize H8; case x; auto with arith. intros Ht; Contradict Ht; auto with arith. intros x1; case x1; auto with arith. intros Ht; Contradict Ht; auto with arith. rewrite <- plus_n_O; rewrite power_SO; auto. intros n0 H11; pattern x at 1 in |- *; rewrite <- power_SO; auto with arith. apply power_le_mono; auto with arith. apply Nat.lt_trans with (2 := H7); auto with arith. apply Nat.le_lt_trans with (2 := Hd); auto with arith. apply power_div_binomial1; auto with arith. apply power_div_divides; auto with arith. apply Nat.lt_trans with (2 := H7); auto with arith. apply Nat.le_lt_trans with (2 := Hd); auto with arith. change (sqr 1 <= sqr (2 * n)) in |- *. apply sqr_mono. apply Nat.le_trans with (2 * power 2 7); auto with arith; simpl in |- *; auto with arith. apply mult_id_lt_inv. apply Nat.le_lt_trans with (2 * n). apply sqr_le. apply Nat.lt_le_trans with (3 * (1 + div (2 * n) 3)); auto with arith. apply div_lt. auto with arith. cut (4 <= div (2 * n) 3); [ intros H1 | idtac ]. apply Nat.le_trans with (4 * div (2 * n) 3); auto with arith. replace 4 with (1 + 3); auto with arith. rewrite Nat.mul_add_distr_l; rewrite Nat.mul_add_distr_r. apply Nat.add_le_mono; auto with arith. apply Nat.le_trans with 4; auto with arith. rewrite Nat.mul_1_l; auto. apply le_mult; auto with arith. apply Nat.lt_succ_r. apply lt_mult_right_anti with (z := 3). apply Nat.le_lt_trans with (2 * n); auto with arith. apply Nat.le_trans with (2 * power 2 7); auto with arith. apply Nat.le_trans with (2 * power 2 3). simpl in |- *; auto with arith. apply le_mult; auto with arith. apply power_le_mono; auto with arith. apply (div_lt (2 * n) 3); auto with arith. Qed.
imports: Coq(Wf_nat Ranalysis Rtrigo ArithRing Lra)