equal
deleted
inserted
replaced
1091 qed |
1091 qed |
1092 show ?thesis |
1092 show ?thesis |
1093 proof |
1093 proof |
1094 have "real j < 2 ^ n" |
1094 have "real j < 2 ^ n" |
1095 using j_le i k |
1095 using j_le i k |
1096 apply (auto simp: le_max_iff_disj simp del: real_of_nat_less_numeral_power_cancel_iff elim!: le_less_trans) |
1096 apply (auto simp: le_max_iff_disj simp del: of_nat_less_numeral_power_cancel_iff |
|
1097 elim!: le_less_trans) |
1097 apply (auto simp: field_simps) |
1098 apply (auto simp: field_simps) |
1098 done |
1099 done |
1099 then show "j < 2 ^ n" |
1100 then show "j < 2 ^ n" |
1100 by auto |
1101 by auto |
1101 show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n" |
1102 show "\<bar>real i / 2 ^ m - real j / 2 ^ n\<bar> < 1/2 ^ n" |