Verification For Difference And Difference Quotient In MIZAR

Nowadays, with the progress of the times. In order to release from various mental labor, scientists who devote to learn how to solve complicated problems with high technology are more and more unsatisfied with the laggared scientific technology. Under such a situation, to prove mathematics problems with computers has been a hot field for mathematics from an parts of the world. With the development of the computer technology, people have set up many kinds of machine languages to program in formalized way. Some program is especially for mathematics, and it can give the model construction and the machine verification of relevant mathematical problems.This article introduces the realization of difference and difference quotient in Mizar system, and it give the relevant verification of different problems of difference and difference quotient with Mizar system. The main work is as follow.Firstly, we introduce the formalized mathematics, the history of the Mizar system and its current situation. Secondly, we explain how to complete the composing and verification of a Mizar article simply. In Mizar system, we give the proof of the difference and difference quotient of special function and partial property of difference and difference quotient. Finally, we give the definition of 0_order difference and high_order difference and the proof of their property.These results have been verified by the Mizar, and relevant content has been published in Formalized Mathematics.