We propose a definition of equivariant (with respect to an Iwahori subgroup) K-theory of the formal power series model Q(G) of semi-infinite flag manifolds, and we prove the Pieri-Chevalley formula, which describes the product, in the K-theory of Q(G), of the structure sheaf of a semi-infinite Schubert variety with a line bundle (associated to a dominant integral weight) over Q(G). In order to achieve this, we provide a number of fundamental results on Q(G) and its Schubert subvarieties including the Borel-Weil-Bott theory, whose precise shape was conjectured by Braverman and Finkelberg in 2014. One more ingredient of this article besides the geometric results above is (a combinatorial version of) standard monomial theory for level-zero extremal weight modules over quantum affine algebras, which is described in terms of semi-infinite Lakshmibai-Seshadri paths. In fact, in our Pieri-Chevalley formula, the positivity of structure coefficients is proved by giving an explicit representation-theoretic meaning through semi-infinite Lakshmibai-Seshadri paths.