```(def-language field-language
(base-types kk)
(constants
(o_kk kk)
(i_kk kk)
(-_kk (kk kk))
(+_kk (kk kk kk))
(*_kk (kk kk kk))
(inv (kk kk))))
```

```
(def-theory fields
(component-theories h-o-real-arithmetic)
(language field-language)
(distinct-constants (i_kk o_kk))
(axioms
(associative-law-for-multiplication-for-fields
"forall(z,y,x:kk,(x *_kk y) *_kk z=x *_kk (y *_kk z))")
(left-distributive-law-for-fields
"forall(z,y,x:kk,x *_kk (y +_kk z)=x *_kk y +_kk x *_kk z)")
(multiplicative-identity-for-fields
"forall(x:kk,i_kk  *_kk x = x)" rewrite)
"forall(x:kk,x +_kk o_kk = x)" rewrite)
"forall(x:kk,x +_kk (-_kk x) = o_kk)" rewrite)
(commutative-law-for-multiplication-for-fields
"forall(y,x:kk,x *_kk y=y *_kk x)")
"forall(z,y,x:kk,(x +_kk y) +_kk z=x +_kk (y +_kk z))")
"forall(y,x:kk,x +_kk y=y +_kk x)")
(multiplicative-inverse-for-fields
"forall(x:kk,not(x = o_kk) implies x *_kk inv(x)=i_kk)" )))
```

```
(def-theorem field-zero-is-not-field-one
"not(o_kk = i_kk)"
(theory fields)
(proof
(
simplify
)))
```

```(def-theorem ()
"total_q(+_kk,[kk,kk,kk])"
(theory fields)
(usages d-r-convergence)
(proof
(
insistent-direct-inference
)))
```

```(def-theorem ()
"total_q(*_kk,[kk,kk,kk])"
(theory fields)
(usages d-r-convergence)
(proof
(
insistent-direct-inference
(assume-theorem commutative-law-for-multiplication-for-fields)
)))
```

```(def-theorem ()
"total_q(-_kk,[kk,kk])"
(theory fields)
(usages d-r-convergence)
(proof
(
insistent-direct-inference
)))

```

```
(def-translation fields-to-rr
(source fields)
(target h-o-real-arithmetic)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(kk rr))
(constant-pairs
(o_kk 0)
(i_kk 1)
(-_kk -)
(+_kk +)
(*_kk *)
(inv "lambda(x:rr,1/x)"))
(theory-interpretation-check using-simplification))
```