equal
deleted
inserted
replaced
718 by (auto simp add: choose_two of_nat_div mod_eq_0_iff_dvd) |
718 by (auto simp add: choose_two of_nat_div mod_eq_0_iff_dvd) |
719 also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)" |
719 also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)" |
720 by (simp add: x_def) |
720 by (simp add: x_def) |
721 also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
721 also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
722 using \<open>2 < n\<close> |
722 using \<open>2 < n\<close> |
723 by (intro setsum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
723 by (intro sum_mono2) (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
724 also have "\<dots> = (x n + 1) ^ n" |
724 also have "\<dots> = (x n + 1) ^ n" |
725 by (simp add: binomial_ring) |
725 by (simp add: binomial_ring) |
726 also have "\<dots> = n" |
726 also have "\<dots> = n" |
727 using \<open>2 < n\<close> by (simp add: x_def) |
727 using \<open>2 < n\<close> by (simp add: x_def) |
728 finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1" |
728 finally have "real (n - 1) * (real n / 2 * (x n)\<^sup>2) \<le> real (n - 1) * 1" |
759 by (simp add: choose_one) |
759 by (simp add: choose_one) |
760 also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)" |
760 also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)" |
761 by (simp add: x_def) |
761 by (simp add: x_def) |
762 also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
762 also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)" |
763 using \<open>1 < n\<close> \<open>1 \<le> c\<close> |
763 using \<open>1 < n\<close> \<open>1 \<le> c\<close> |
764 by (intro setsum_mono2) |
764 by (intro sum_mono2) |
765 (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
765 (auto intro!: mult_nonneg_nonneg zero_le_power simp: x_def le_diff_eq) |
766 also have "\<dots> = (x n + 1) ^ n" |
766 also have "\<dots> = (x n + 1) ^ n" |
767 by (simp add: binomial_ring) |
767 by (simp add: binomial_ring) |
768 also have "\<dots> = c" |
768 also have "\<dots> = c" |
769 using \<open>1 < n\<close> \<open>1 \<le> c\<close> by (simp add: x_def) |
769 using \<open>1 < n\<close> \<open>1 \<le> c\<close> by (simp add: x_def) |