Ordered Field Axioms

Following (lines 1 through 5) are the axioms for an ordered field (f,+,0,*1)


Field axioms

Where:
_x  = the additive inverse of x 
1/x = the multiplicative inverse of x

1	Set(f)
	& ALL(a):ALL(b):[a  f & b  f => a+b  f]
	& ALL(a):ALL(b):ALL(c):[a  f & b  f & c  f => a+b+c=a+(b+c)]
	& ALL(a):ALL(b):[a  r & b  f => a+b=b+a]
	& 0  f
	& ALL(a):[a  f => a+0=a]
	& ALL(a):[a  f => _a  f]
	& ALL(a):[a  f => a+_a=0]
	& ALL(a):ALL(b):[a  f & b  f => a*b  f]
	& ALL(a):ALL(b):ALL(c):[a  f & b  f & c  f => a*b*c=a*(b*c)]
	& ALL(a):ALL(b):[a  f & b  f => a*b=b*a]
	& ALL(a):ALL(b):ALL(c):[a  f & b  f & c  f => a*(b+c)=a*b+a*c]
	& 1  f
	& ~0=1
	& ALL(a):[a  f => a*1=a]
	& ALL(a):[a  f & ~a=0 => 1/a  f]
	& ALL(a):[a  f => a*(1/a)=1]
	Premise

Trichotomy for <

2	ALL(a):ALL(b):[a  f & b  f
	=> [a<b | b<a | a=b]
	& ~[a<b & b<a]
	& ~[a<b & a=b]
	& ~[b<a & a=b]]
	Premise

Associativity of <

3	ALL(a):ALL(b):ALL(c):[a  f & b  f & c  f & a<b & b<c => a<c]
	Premise

Additivity of <

4	ALL(a):ALL(b):[a  f & b  f & a<b => ALL(c):[c  f => a+c<b+c]]
	Premise

Multiplicativity of <

5	ALL(a):ALL(b):[a  f & b  f & a<b
	=> ALL(c):[c  f & 0<c => a*c<b*c]
	& ALL(c):[c  f & c<0 => b*c<a*c]]
	Premise