790 next |
793 next |
791 case False |
794 case False |
792 have "x \<noteq> y" |
795 have "x \<noteq> y" |
793 proof (rule ccontr) |
796 proof (rule ccontr) |
794 assume "\<not> x \<noteq> y" hence "x = y" by auto |
797 assume "\<not> x \<noteq> y" hence "x = y" by auto |
795 have "?X mod y = 0" unfolding `x = y` using zmod_zmult_self2 by auto |
798 have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto |
796 thus False using False by auto |
799 thus False using False by auto |
797 qed |
800 qed |
798 hence "x < y" using `x \<le> y` by auto |
801 hence "x < y" using `x \<le> y` by auto |
799 hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto |
802 hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto |
800 |
803 |
1088 also |
1091 also |
1089 let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))" |
1092 let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))" |
1090 { have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono, auto) |
1093 { have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono, auto) |
1091 also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" unfolding pow_split zpower_zadd_distrib by auto |
1094 also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" unfolding pow_split zpower_zadd_distrib by auto |
1092 finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m" using `0 < m` by (rule zdiv_mono1) |
1095 finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m" using `0 < m` by (rule zdiv_mono1) |
1093 hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding zdiv_zmult_self1[OF `m \<noteq> 0`] . |
1096 hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] . |
1094 hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d" |
1097 hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d" |
1095 unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto } |
1098 unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto } |
1096 from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib real_mult_assoc[symmetric] right_inverse[OF pow_not0] real_mult_1], of "2^?e"] |
1099 from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib real_mult_assoc[symmetric] right_inverse[OF pow_not0] real_mult_1], of "2^?e"] |
1097 have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto |
1100 have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto |
1098 finally have "1 \<le> 2^?e * ?d" . |
1101 finally have "1 \<le> 2^?e * ?d" . |