The extremal function for K9 minors

We prove that every (simple) graph on n⩾9 vertices and at least 7n-27 edges either has a K9 minor, or is isomorphic to K2,2,2,3,3, or is isomorphic to a graph obtained from disjoint copies of K1,2,2,2,2,2 by identifying cliques of size six. The proof of one of our lemmas is computer-assisted.