equal
deleted
inserted
replaced
436 assume "norm (h - 0) < norm x" |
436 assume "norm (h - 0) < norm x" |
437 hence "h \<noteq> -x" by clarsimp |
437 hence "h \<noteq> -x" by clarsimp |
438 hence 2: "x + h \<noteq> 0" |
438 hence 2: "x + h \<noteq> 0" |
439 apply (rule contrapos_nn) |
439 apply (rule contrapos_nn) |
440 apply (rule sym) |
440 apply (rule sym) |
441 apply (erule equals_zero_I) |
441 apply (erule minus_unique) |
442 done |
442 done |
443 show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h |
443 show "norm (?inv (x + h) - ?inv x - - (?inv x * h * ?inv x)) / norm h |
444 = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h" |
444 = norm ((?inv (x + h) - ?inv x) * h * ?inv x) / norm h" |
445 apply (subst inverse_diff_inverse [OF 2 x]) |
445 apply (subst inverse_diff_inverse [OF 2 x]) |
446 apply (subst minus_diff_minus) |
446 apply (subst minus_diff_minus) |