proposition: Theorem Bertrand : forall n : nat, 2 <= n -> exists p : nat, prime p /\ n < p /\ p < 2 * n.
proof: Proof. intros n H. case (Nat.le_gt_cases n (power 2 7)); intros H1. apply postulate_correct_128; auto. case (postulate_dec n); auto. intros n0; absurd (power 4 n < power (2 * n) (div (sqr (2 * n)) 2) * power 4 (div (2 * n) 3)). 2: apply no_prime_imp_spec_inegality; auto. 2: apply Nat.lt_le_incl; auto. apply Nat.le_ngt. apply INR_le. repeat rewrite INR_power; rewrite mult_INR; repeat rewrite INR_power. repeat rewrite <- Rpower_pow. apply Rle_trans with (Rpower (INR (2 * n)) (sqrt (INR (2 * n)) / INR 2) * Rpower (INR 4) (INR (2 * n) / INR 3))%R. apply Rmult_le_compat; auto with real. unfold Rpower in |- *; apply Rlt_le; auto with real. unfold Rpower in |- *; apply Rlt_le; auto with real. apply Rle_Rpower; simpl in |- *; auto with real. replace 1%R with (INR 1); auto with real arith. apply Rle_trans with (INR (sqr (n + (n + 0))) / 2)%R. apply div_Rdiv with (m := 2); auto with real arith. unfold Rdiv in |- *; apply Rmult_le_compat; auto with real arith. apply sqr_Rsqrt. apply Rle_Rpower. unfold IZR; rewrite <- INR_IPR; auto with real. apply div_Rdiv; auto with real arith. rewrite Rmult_comm. apply Rmult_le_reg_l with (r := (/ Rpower (INR 4) (INR (2 * n) / INR 3))%R); auto with real. apply Rinv_0_lt_compat; unfold Rpower in |- *; auto with real. rewrite <- Rmult_assoc; rewrite Rinv_l. rewrite Rmult_1_l. rewrite <- Rpower_Ropp. rewrite <- Rpower_plus. replace (- (INR (2 * n) / INR 3) + INR n)%R with (INR n / INR 3)%R. repeat rewrite mult_INR. simpl in |- *. repeat rewrite Rplus_assoc. apply Rlt_le. apply spec_fun_bound. replace (1 + (1 + (1 + (1 + 3))))%R with (INR 7); [ idtac | simpl in |- * ]; auto. replace 2%R with (INR 2); [ idtac | simpl in |- * ]; auto. rewrite Rpower_pow. rewrite <- INR_power; auto with real. replace 0%R with (INR 0); auto with real arith. ring. rewrite mult_INR; simpl in |- *; field. unfold Rpower in |- *; apply Compare.not_eq_sym; auto with real. replace 0%R with (INR 0); auto with real arith. replace 0%R with (INR 0); auto with real arith. replace 0%R with (INR 0); auto with real arith. Qed.
imports: Coq(Wf_nat Ranalysis Rtrigo ArithRing Lra)