Machine proof is one of the important research directions in the field of artificial intelligence, and it is an attempt by people to imitate human reasoning ability through machines. Formal verification techniques in machine proofs have been widely used in the fields of mathematics and computer science. With the help of the assistant proof Rocq, this paper constructs the axiom system of real numbers based on the Morse-Kelley axiomatic set theory, and completes the exponential operation of integers through the recursive theorem. This achievement not only improves the axiom system of real numbers, but also provides new ideas and methods for formal research in related fields. At the same time, all the formal definitions and theorems in this paper have been verified and run by Rocq.