(def-theorem ()"forall(x:kk, not(x=o_kk) implies #(inv(x)))"(theory fields) (usages d-r-convergence) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem multiplicative-inverse-for-fields ("x")) )))

(def-overloading + (h-o-real-arithmetic +) (fields +_kk))

(def-overloading * (h-o-real-arithmetic *) (fields *_kk))

(def-overloading - (h-o-real-arithmetic -) (fields -_kk))

(def-theorem ()"forall(x:kk,o_kk+x=x)"(theory fields) (proof ( (apply-macete-with-minor-premises commutative-law-for-addition-for-fields) (apply-macete-with-minor-premises additive-identity-for-fields) )))

(def-theorem ()"forall(x:kk,-x+x=o_kk)"(theory fields) (proof ( (apply-macete-with-minor-premises commutative-law-for-addition-for-fields) (apply-macete-with-minor-premises additive-inverse-for-fields) )))

(def-translation groups-to-additive-kk (fixed-theories h-o-real-arithmetic) (source abelian-groups) (target fields) (sort-pairs (gg kk)) (constant-pairs (inv -_kk) (mul +_kk) (e o_kk)))

(def-theorem o_kk-times-is-o_kk"forall(x:kk, x*o_kk=o_kk)"(theory fields) (proof ( direct-inference (cut-with-single-formula"x*o_kk=x*o_kk+x*o_kk") (incorporate-antecedent"with(x:kk,x*o_kk=x*o_kk+x*o_kk);") (apply-macete-with-minor-premises tr%right-trivial-cancellation-law-left) simplify (cut-with-single-formula"o_kk=o_kk+o_kk") (backchain"o_kk=o_kk+o_kk;") (apply-macete-with-minor-premises left-distributive-law-for-fields) (apply-macete-with-minor-premises additive-identity-for-fields) )))

(def-constant sub_kk"lambda(x,y:kk,x+(-y))"(theory fields))

(def-constant /_kk"lambda(x,y:kk, if(y=o_kk,?kk,inv(y)*x))"(theory fields))

(def-overloading sub (h-o-real-arithmetic sub) (fields sub_kk))

(def-overloading / (h-o-real-arithmetic /) (fields /_kk))

(def-theorem ()"forall(y,x:kk,x-y=x+-y)"(proof ( unfold-defined-constants simplify )) (theory fields))

(def-theorem ()"total_q{sub_kk,[kk,kk,kk]}"(theory fields) (proof ( unfold-defined-constants insistent-direct-inference-strategy beta-reduce-repeatedly )) (usages d-r-convergence))

(def-theorem division-characterization-fields"forall(a,b:kk, not(b=o_kk) implies b*(a/b)=a)"(theory fields) (proof ( (unfold-single-defined-constant (0) /_kk) simplify (force-substitution"b*(inv(b)*a)""(b*inv(b))*a"(0)) (apply-macete-with-minor-premises multiplicative-inverse-for-fields) (apply-macete-with-minor-premises multiplicative-identity-for-fields) (apply-macete-with-minor-premises associative-law-for-multiplication-for-fields) )))

(def-theorem non-o_kk-is-closed-under-inv"forall(x:kk, not(x=o_kk) implies not(inv(x)=o_kk))"(theory fields) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"i_kk=x*inv(x)") (contrapose"with(x:kk,not(x=o_kk));") (contrapose"with(x:kk,i_kk=x*inv(x));") (backchain"with(x:kk,inv(x)=o_kk);") (apply-macete-with-minor-premises o_kk-times-is-o_kk) (contrapose"with(x:kk,not(x=o_kk));") (apply-macete-with-minor-premises multiplicative-inverse-for-fields) )))

(def-theorem non-o_kk-is-closed-under-*_kk"forall(x,y:kk, not(x=o_kk) and not(y=o_kk) implies not(x*y=o_kk))"(theory fields) (proof ( direct-and-antecedent-inference-strategy (contrapose"with(x:kk,not(x=o_kk));") (cut-with-single-formula"x=x*y*inv(y)") (backchain"with(y,x:kk,x=x*y*inv(y));") (backchain"with(y,x:kk,x*y=o_kk);") (apply-macete-with-minor-premises commutative-law-for-multiplication-for-fields) (apply-macete-with-minor-premises o_kk-times-is-o_kk) (apply-macete-with-minor-premises associative-law-for-multiplication-for-fields) (apply-macete-with-minor-premises multiplicative-inverse-for-fields) (apply-macete-with-minor-premises commutative-law-for-multiplication-for-fields) (apply-macete-with-minor-premises multiplicative-identity-for-fields) )))

(def-theorem ()"forsome(x:kk,not(x=o_kk))"lemma (theory fields) (proof ( (instantiate-existential ("i_kk")) simplify )))

(def-theorem ()"forall(x,y:kk, not(x=o_kk) implies y=o_kk or not(x*y=o_kk))"lemma (theory fields) (proof ( (apply-macete-with-minor-premises non-o_kk-is-closed-under-*_kk) simplify )))

(def-theorem ()"forall(x:kk,not(x=o_kk) implies inv(x)*x=i_kk)"lemma (theory fields) (proof ( (apply-macete-with-minor-premises commutative-law-for-multiplication-for-fields) (apply-macete-with-minor-premises multiplicative-inverse-for-fields) )))

(def-theorem ()"forall(x,y,z:kk, not(x=o_kk) and not(y=o_kk) and not(z=o_kk) implies not(x *_kk y=o_kk) and (not(y *_kk z=o_kk) and x *_kk y *_kk z=x *_kk (y *_kk z)))"lemma (theory fields) (proof ( (apply-macete-with-minor-premises non-o_kk-is-closed-under-*_kk) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises associative-law-for-multiplication-for-fields) )))

(def-theorem ()"forall(x,y:kk,not(x=o_kk) and not(y=o_kk) implies x*y=y*x)"lemma (theory fields) (proof ( direct-and-antecedent-inference-strategy (assume-theorem commutative-law-for-multiplication-for-fields) (backchain"forall(y,x:kk,x*y=y*x);") )))

(def-theorem ()"forall(x:kk,not(x=o_kk) implies x*i_kk=x)"lemma (theory fields) (proof ( (apply-macete-with-minor-premises commutative-law-for-multiplication-for-fields) (apply-macete-with-minor-premises multiplicative-identity-for-fields) )))

(def-theorem ()"forall(x:kk, not(x=o_kk) implies not(inv(x)=o_kk) and inv(x) *_kk x=i_kk)"lemma (theory fields) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises non-o_kk-is-closed-under-inv) (apply-macete-with-minor-premises commutative-law-for-multiplication-for-fields) (apply-macete-with-minor-premises multiplicative-inverse-for-fields) )))

(def-theorem ()"forall(x:kk, not(x=o_kk) implies not(inv(x)=o_kk) and x *_kk inv(x)=i_kk)"lemma (theory fields) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises non-o_kk-is-closed-under-inv) (apply-macete-with-minor-premises multiplicative-inverse-for-fields) )))

(def-theorem ()"forall(x:kk,x=o_kk or not(inv(x)=o_kk))"lemma (theory fields) (proof ( (apply-macete-with-minor-premises non-o_kk-is-closed-under-inv) direct-and-antecedent-inference-strategy )))

(def-translation groups-to-multiplicative-kk force-under-quick-load (source abelian-groups) (target fields) (fixed-theories h-o-real-arithmetic) (sort-pairs (gg (pred"lambda(x:kk, not(x=o_kk))"))) (constant-pairs (e i_kk) (inv"lambda(x:kk, if(x=o_kk,?kk,inv(x)))") (mul"lambda(x,y:kk,if(x=o_kk or y=o_kk,?kk,x*y))")) (theory-interpretation-check using-simplification))

(def-transported-symbols (multiple) (renamer groups-multiplicative-kk-renamer) (translation groups-to-multiplicative-kk) )

(def-constant ^_kk"lambda(x:kk,n:zz, if(not(x=o_kk),pexp(n,x),0<n,o_kk,?kk))"(theory fields))

(def-overloading ^ (h-o-real-arithmetic ^) (fields ^_kk))

(def-theorem ()"forall(y,x:kk, x/y==x*y^[-1])"(theory fields) (proof ( (unfold-single-defined-constant (0) /_kk) direct-and-antecedent-inference-strategy (case-split ("y=o_kk")) simplify (unfold-single-defined-constant (0) ^_kk) simplify simplify (assume-theorem commutative-law-for-multiplication-for-fields) (backchain"forall(y,x:kk,x*y=y*x);") (cut-with-single-formula"inv(y)=y^[-1]") (unfold-single-defined-constant (0) ^_kk) simplify (instantiate-transported-theorem multiple-commutes-with-negation-corollary groups-to-multiplicative-kk ("y")) simplify )))

(def-theorem o_kk-exponent"forall(m:zz, #(o_kk^m,kk) implies o_kk^m=o_kk)"(theory fields) (proof ( unfold-defined-constants simplify )))

(def-theorem ()"forall(n:zz, #(i_kk^n,kk) implies i_kk^n=i_kk)"(theory fields) (proof ( unfold-defined-constants simplify direct-and-antecedent-inference-strategy (instantiate-transported-theorem multiple-of-group-identity groups-to-multiplicative-kk ("n")) )))

(def-theorem ()"forall(x:kk,#(x^0,kk) implies x^0=i_kk)"(theory fields) (proof ( unfold-defined-constants simplify direct-inference direct-and-antecedent-inference-strategy (instantiate-transported-theorem 0-multiple-is-group-identity groups-to-multiplicative-kk ("x")) )))

(def-theorem ()"forall(x:kk,x^1=x)"(theory fields) (proof ( (unfold-single-defined-constant (0) ^_kk) direct-inference (case-split ("x=o_kk")) simplify simplify (instantiate-transported-theorem 1-multiple-is-element groups-to-multiplicative-kk ("x")) )))

(def-theorem ()"forall(n,m:zz, x:kk ,#((x^m)^n,kk) implies (x^m)^n=x^(m*n))"(theory fields) (proof ( direct-inference (case-split ("x=o_kk")) (block (script-comment"`case-split' at (1)") (backchain-repeatedly ("with(x:kk,x=o_kk);")) direct-inference (cut-with-single-formula"0<m and 0<n and 0<m*n") (block (script-comment"`cut-with-single-formula' at (0)") (apply-macete-with-minor-premises o_kk-exponent) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (apply-macete-with-minor-premises o_kk-exponent) (unfold-single-defined-constant (0) ^_kk) simplify ) (block (script-comment"`apply-macete-with-minor-premises' at (1)") (unfold-single-defined-constant (0) ^_kk) simplify ) ) (block (script-comment"`cut-with-single-formula' at (1)") (cut-with-single-formula"#(o_kk^m) and o_kk^m=o_kk") (block (script-comment"`cut-with-single-formula' at (0)") (contrapose"with(k:kk,#(k,kk));") (backchain"with(p:prop,p and p);") (contrapose"with(p:prop,p or p or p);") (antecedent-inference"with(p:prop,p and p);") (incorporate-antecedent"with(k:kk,#(k));") (incorporate-antecedent"with(k:kk,#(k,kk));") (unfold-single-defined-constant (0 1) ^_kk) simplify ) (apply-macete-with-minor-premises o_kk-exponent) ) ) (block (script-comment"`case-split' at (2)") (cut-with-single-formula"not(pexp(m,x)=o_kk)") (block (script-comment"`cut-with-single-formula' at (0)") (apply-macete-with-minor-premises commutative-law-for-multiplication) (move-to-ancestor 1) unfold-defined-constants simplify beta-reduce-with-minor-premises (block (script-comment"`beta-reduce-with-minor-premises' at (0)") simplify (instantiate-transported-theorem multiple-is-homogenuous groups-to-multiplicative-kk ("n""m""x") ) direct-inference (apply-macete-with-minor-premises commutative-law-for-multiplication) ) (instantiate-transported-theorem multiple-totality groups-to-multiplicative-kk ("m""x") ) ) (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("x""m") ) ) )))

(def-theorem ()"forall(n,m:zz, x:kk ,((#(x^m,kk) and #(x^n,kk)) iff #((x^m)^n,kk)))"(theory fields) (proof ( direct-inference unfold-defined-constants (case-split ("x=o_kk")) simplify (block (script-comment"`case-split' at (2)") simplify (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("x""m")) (cut-with-single-formula"not pexp(m,x)=o_kk") simplify (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("pexp(m,x)""n")) direct-and-antecedent-inference-strategy (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("x""n"))) )))

(def-theorem ()"forall(m:zz ,y,x:kk,(#(x^m*y^m,kk) or #((x*y)^m,kk)) implies x^m*y^m=(x*y)^m)"(theory fields) (proof ( direct-inference (case-split ("x=o_kk")) (block (script-comment"`case-split' at (1)") simplify (apply-macete-with-minor-premises commutative-law-for-multiplication-for-fields) (apply-macete-with-minor-premises o_kk-times-is-o_kk) (unfold-single-defined-constant (1 2) ^_kk) simplify direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises o_kk-times-is-o_kk) (unfold-single-defined-constant (0) ^_kk) (case-split ("y=o_kk")) simplify (block (script-comment"`case-split' at (2)") simplify (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("y""m")))) (block (script-comment"`case-split' at (2)") (case-split ("y=o_kk")) (block (script-comment"`case-split' at (1)") simplify (apply-macete-with-minor-premises o_kk-times-is-o_kk) (unfold-single-defined-constant (1 2) ^_kk) simplify direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises o_kk-times-is-o_kk) (unfold-single-defined-constant (0) ^_kk) simplify (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("x""m"))) (block (script-comment"`case-split' at (2)") direct-inference (unfold-single-defined-constant-globally ^_kk) (cut-with-single-formula"not(x*y=o_kk)") (block (script-comment"`cut-with-single-formula' at (0)") simplify (instantiate-transported-theorem multiple-is-additive-in-group groups-to-multiplicative-kk ("m""x""y")) (contrapose"with(k:kk,k=k);") (cut-with-single-formula"not pexp(m,x)=o_kk and not pexp(m,y)=o_kk") (block (script-comment"`cut-with-single-formula' at (0)") simplify beta-reduce-with-minor-premises simplify (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("y""m")) (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("x""m"))) (block (script-comment"`cut-with-single-formula' at (1)") (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("x""m")) direct-inference (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("y""m")))) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises non-o_kk-is-closed-under-*_kk) direct-inference))) )))

(def-theorem ()"forall(n,m:zz, x:kk,#(x^m*x^n,kk) implies x^(m+n)=x^m*x^n)"(theory fields) (proof ( direct-inference (case-split ("x=o_kk")) unfold-defined-constants simplify (apply-macete-with-minor-premises o_kk-times-is-o_kk) unfold-defined-constants simplify (instantiate-transported-theorem multiple-is-additive groups-to-multiplicative-kk ("m""n""x")) (cut-with-single-formula"not(pexp(m,x)=o_kk) and not(pexp(n,x)=o_kk)") (simplify-antecedent"with(x,y:kk, x=y)") (weaken (0)) direct-inference (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("x""m")) (instantiate-transported-theorem multiple-totality-with-range groups-to-multiplicative-kk ("x""n")) )))

(def-algebraic-processor field-algebraic-processor (language fields) (base ((operations (+ +_kk) (* *_kk) (- -_kk) (^ ^_kk) (sub sub_kk) (zero o_kk) (unit i_kk)) commutes)) (exponent rr-algebraic-processor))

(def-theory-processors fields (algebraic-simplifier (field-algebraic-processor ^_kk sub_kk *_kk +_kk -_kk)) (algebraic-term-comparator field-algebraic-processor))

(def-theorem ()"forall(x:kk,y:zz,(0<y or not(x=o_kk)) implies #(x^y))"(proof ( direct-and-antecedent-inference-strategy unfold-defined-constants simplify unfold-defined-constants simplify )) (theory fields) (usages d-r-convergence))

(def-theorem ()"forall(x:kk, y:zz, x=o_kk and not(0<y) implies not(#(x^y)))"(proof ( direct-and-antecedent-inference-strategy unfold-defined-constants simplify )) (theory fields) (usages d-r-convergence))

(def-transported-symbols (multiple) (renamer groups-additive-kk-renamer) (translation groups-to-additive-kk) )

(def-overloading * (fields *_ext))

(def-theorem *_ext-totality"total_q{*_ext,[zz,kk,kk]}"(proof ( (apply-macete-with-minor-premises tr%multiple-totality) )) (theory fields) (usages d-r-convergence))

(def-recursive-constant sum_kk"lambda(sigma:[zz,zz,[zz,kk],kk],lambda(m,n:zz,f:[zz,kk], if(m<=n,sigma(m,n-1,f)+f(n),o_kk)))"(definition-name sum_kk) (theory fields))

(def-recursive-constant prod_kk"lambda(pi:[zz,zz,[zz,kk],kk],lambda(m,n:zz,f:[zz,kk], if(m<=n,pi(m,n-1,f)*f(n),i_kk)))"(definition-name prod_kk) (theory fields))

(def-overloading sum (h-o-real-arithmetic sum) (fields sum_kk))

(def-overloading prod (h-o-real-arithmetic prod) (fields prod_kk))

(def-theorem sum_kk-definedness"forall(m,n:zz,f:[zz,kk],forall(k:zz,m<=k and k<=n implies #(f(k))) implies #(sum(m,n,f)))"(theory fields) (proof ( direct-inference (case-split ("m<=n")) (induction integer-inductor ()) direct-and-antecedent-inference-strategy (prove-by-logic-and-simplification 3) (prove-by-logic-and-simplification 3) (unfold-single-defined-constant (0) sum_kk) simplify )) (usages d-r-convergence))

(def-translation monoids-to-additive-kk (fixed-theories h-o-real-arithmetic) (source commutative-monoid-theory) (target fields) (sort-pairs (uu kk)) (constant-pairs (** +_kk) (e o_kk)) (theory-interpretation-check using-simplification))

(def-theorem external-multiplication-conversion"forall(m:zz,x:kk,m*x=m*i_kk*x)"(theory fields) (proof ( direct-inference (case-split ("0<=m")) (induction integer-inductor ("m")) (unfold-single-defined-constant (0 1) *_ext) simplify (cut-with-single-formula"forall(m:zz,x:kk,0<=m implies m*x=m*i_kk*x);") (backchain-backwards"forall(m:zz,x:kk,0<=m implies m*x=m*i_kk*x);") simplify (weaken (0)) direct-and-antecedent-inference-strategy)))

(def-theorem ()"forall(x:kk,m,n:zz, (m+n)*x=m*x+n*x)"(theory fields) (usages rewrite) (proof ( (apply-macete-with-minor-premises tr%multiple-is-additive) simplify )))

(def-theorem ()"forall(x:kk,0*x=o_kk)"(theory fields) (usages rewrite) (proof ( unfold-defined-constants simplify )))

(def-theorem ()"forall(x:kk,1*x=x)"(theory fields) (usages rewrite) (proof ( unfold-defined-constants simplify )))

(def-theorem uniqueness-of-exponentiation"forall(f:[kk,zz,kk], (forall(x:kk, n:zz, not(x=o_kk) and 0<=n implies f(x,n+1)=f(x,n)*x) and forall(x:kk, not(x=o_kk) implies f(x,0)=i_kk) and forall(x:kk, n:zz, not(x=o_kk) and 0<=n implies f(x,-n)=(f(x,n))^[-1]) and forall(n:zz,1<=n implies f(o_kk,n)=o_kk) and forall(n:zz, n<=0 implies not(#(f(o_kk,n))))) iff f=^_kk)"lemma (theory fields) (proof ( direct-inference direct-inference (antecedent-inference-strategy (0)) extensionality direct-and-antecedent-inference-strategy (case-split ("1<=x_1")) (induction trivial-integer-inductor ("x_1")) beta-reduce-repeatedly (instantiate-universal-antecedent"with(f:[kk,zz,kk], forall(x:kk,n:zz, not(x=o_kk) and 0<=n implies f(x,n+1)=f(x,n)*x));"("x_0""0")) simplify (simplify-antecedent"not(0<=0);") (incorporate-antecedent"with(x_0:kk,f:[kk,zz,kk],f(x_0,0+1)=f(x_0,0)*x_0);") simplify (case-split ("x_0=o_kk")) simplify simplify (case-split ("x_0=o_kk")) simplify (instantiate-universal-antecedent"with(f:[kk,zz,kk], forall(x:kk,n:zz, not(x=o_kk) and 0<=n implies f(x,n+1)=f(x,n)*x));"("x_0""t")) (simplify-antecedent"with(t:zz,not(0<=t));") (incorporate-antecedent"with(t:zz,x_0:kk,f:[kk,zz,kk],f(x_0,t+1)=f(x_0,t)*x_0);") simplify (case-split ("x_0=o_kk")) simplify (case-split ("x_1=0")) simplify (force-substitution"x_1""-(-x_1)"(0)) (backchain"with(f:[kk,zz,kk], forall(x:kk,n:zz, not(x=o_kk) and 0<=n implies f(x,-n)=f(x,n)^[-1]));") direct-and-antecedent-inference-strategy simplify (cut-with-single-formula"forall(x_1:zz, 1<=x_1 implies f(x_0,x_1)==x_0^x_1)") (backchain"with(x_0:kk,f:[kk,zz,kk], forall(x_1:zz,1<=x_1 implies f(x_0,x_1)==x_0^x_1));") simplify simplify simplify )))

(def-theorem uniqueness-of-exponentiation-corollary"forall(f:[kk,zz,kk], (forall(x:kk, n:zz, not(x=o_kk) and 0<=n implies f(x,n+1)=f(x,n)*x) and forall(x:kk, not(x=o_kk) implies f(x,0)=i_kk) and forall(x:kk, n:zz, not(x=o_kk) and 0<=n implies f(x,-n)*f(x,n)=i_kk) and forall(n:zz,1<=n implies f(o_kk,n)=o_kk) and forall(n:zz, n<=0 implies not(#(f(o_kk,n))))) implies f=^_kk)"lemma (theory fields) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem uniqueness-of-exponentiation ("f")) (contrapose"with(n:zz,x:kk,f:[kk,zz,kk],not(f(x,-n)=f(x,n)^[-1]));") (instantiate-universal-antecedent"with(f:[kk,zz,kk], forall(x:kk,n:zz, not(x=o_kk) and 0<=n implies f(x,-n)*f(x,n)=i_kk));"("x""n")) (cut-with-single-formula"not(f(x,n)=o_kk) and #(f(x,n)) and #(f(x,-n))") (force-substitution"f(x,n)^[-1]""f(x,n)^[-1]*(f(x,-n)*f(x,n))"(0)) (weaken (1)) simplify simplify direct-and-antecedent-inference-strategy (contrapose"with(n:zz,x:kk,f:[kk,zz,kk],f(x,-n)*f(x,n)=i_kk);") (case-split ("#(f(x,-n))")) simplify (contrapose"with(n:zz,x:kk,f:[kk,zz,kk],not(#(f(x,-n))));") )))