equal
deleted
inserted
replaced
381 Goal "[| #0 < r; #0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))"; |
381 Goal "[| #0 < r; #0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))"; |
382 by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
382 by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
383 real_inverse_less_iff]) 1); |
383 real_inverse_less_iff]) 1); |
384 qed "real_inverse_le_iff"; |
384 qed "real_inverse_le_iff"; |
385 |
385 |
|
386 Goal "[| (#0::real) < d1; #0 < d2 |] ==> EX e. #0 < e & e < d1 & e < d2"; |
|
387 by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1); |
|
388 by (asm_simp_tac (simpset() addsimps [min_def]) 1); |
|
389 qed "real_lbound_gt_zero"; |