It is known that rational approximations of elementary analytic functions (exp, log, trigonometric and hyperbolic functions, and their inverse functions) are computable in the complexity class TC^0. In this talk, we will show how to formalize their construction and basic properties in the correspoding arithmetical theory VTC^0, working with completions of fraction fields of models of VTC^0. As a consequence, we will show that every countable model of VTC^0 is an exponential integer part of a real-closed exponential field, using a recursive saturation argument.