We propose a definition of equivariant (with respect to an Iwahori subgroup) $K$-theory of the formal power series model $mathbf{Q}_{G}$ of semi-infinite flag manifold and prove the Pieri-Chevalley formula, which describes the product, in the $K$-theory of $mathbf{Q}_{G}$, of the structure sheaf of a semi-infinite Schubert variety with a line bundle (associated to a dominant integral weight) over $mathbf{Q}_{G}$. In order to achieve this, we provide a number of fundamental results on $mathbf{Q}_{G}$ and its Schubert subvarieties including the Borel-Weil-Bott theory, whose special case is conjectured in [A. Braverman and M. Finkelberg, Weyl modules and $q$-Whittaker functions, Math. Ann. 359 (2014), 45--59]. One more ingredient of this paper 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.