equal
deleted
inserted
replaced
60 hence "x = - (- y)"; by (rule real_add_minus_eq_minus); |
60 hence "x = - (- y)"; by (rule real_add_minus_eq_minus); |
61 also; have "... = y"; by simp; |
61 also; have "... = y"; by simp; |
62 finally; show "?thesis"; .; |
62 finally; show "?thesis"; .; |
63 qed; |
63 qed; |
64 |
64 |
65 lemma rabs_minus_one: "rabs (- 1r) = 1r"; |
65 lemma abs_minus_one: "abs (- 1r) = 1r"; |
66 proof -; |
66 proof -; |
67 have "-1r < 0r"; |
67 have "-1r < 0r"; |
68 by (rule real_minus_zero_less_iff[RS iffD1], simp, |
68 by (rule real_minus_zero_less_iff[RS iffD1], simp, |
69 rule real_zero_less_one); |
69 rule real_zero_less_one); |
70 hence "rabs (- 1r) = - (- 1r)"; |
70 hence "abs (- 1r) = - (- 1r)"; |
71 by (rule rabs_minus_eqI2); |
71 by (rule abs_minus_eqI2); |
72 also; have "... = 1r"; by simp; |
72 also; have "... = 1r"; by simp; |
73 finally; show ?thesis; .; |
73 finally; show ?thesis; .; |
74 qed; |
74 qed; |
75 |
75 |
76 lemma real_mult_le_le_mono2: |
76 lemma real_mult_le_le_mono2: |