equal
deleted
inserted
replaced
842 have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"] |
842 have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"] |
843 by (auto simp: powr_minus field_simps inverse_eq_divide) |
843 by (auto simp: powr_minus field_simps inverse_eq_divide) |
844 hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"] |
844 hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"] |
845 by (auto simp: powr_minus) |
845 by (auto simp: powr_minus) |
846 hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto) |
846 hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto) |
847 hence "?S \<le> real m" unfolding mult_assoc by auto |
847 hence "?S \<le> real m" unfolding mult.assoc by auto |
848 hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto |
848 hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto |
849 from this bitlen_bounds[OF `0 < m`, THEN conjunct2] |
849 from this bitlen_bounds[OF `0 < m`, THEN conjunct2] |
850 have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans) |
850 have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans) |
851 hence "-e < bitlen m" using False by auto |
851 hence "-e < bitlen m" using False by auto |
852 thus ?thesis by auto |
852 thus ?thesis by auto |