\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{FLD001-0.ax} Ordered field axioms (axiom formulation glxx)






$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y)\mbox{ and }\mbox{defined}(z) ) \ \Rightarrow \ x + ( y + z ){=}( x + y ) + z\qquad\mbox{cnf}(\mbox{associativity\_addition},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ 0 + x{=}x\qquad\mbox{cnf}(\mbox{existence\_of\_identity\_addition},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ x + -x{=}0\qquad\mbox{cnf}(\mbox{existence\_of\_inverse\_addition},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ x + y{=}y + x\qquad\mbox{cnf}(\mbox{commutativity\_addition},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y)\mbox{ and }\mbox{defined}(z) ) \ \Rightarrow \ x\cdot ( y\cdot z ){=}( x\cdot y )\cdot z\qquad\mbox{cnf}(\mbox{associativity\_multiplication},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ 1\cdot x{=}x\qquad\mbox{cnf}(\mbox{existence\_of\_identity\_multiplication},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ ( x\cdot x^{-1}{=}1\mbox{ or }x{=}0 )\qquad\mbox{cnf}(\mbox{existence\_of\_inverse\_multiplication},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ x\cdot y{=}y\cdot x\qquad\mbox{cnf}(\mbox{commutativity\_multiplication},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y)\mbox{ and }\mbox{defined}(z) ) \ \Rightarrow \ x\cdot z + y\cdot z{=}( x + y )\cdot z\qquad\mbox{cnf}(\mbox{distributivity},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ \mbox{defined}(x + y)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_addition},\mbox{axiom})$

$\mbox{defined}(0)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_additive\_identity},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ \mbox{defined}(-x)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_additive\_inverse},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ \mbox{defined}(x\cdot y)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_multiplication},\mbox{axiom})$

$\mbox{defined}(1)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_multiplicative\_identity},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ ( \mbox{defined}(x^{-1})\mbox{ or }x{=}0 )\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_multiplicative\_inverse},\mbox{axiom})$

$( x \leq y\mbox{ and }y \leq x ) \ \Rightarrow \ x{=}y\qquad\mbox{cnf}(\mbox{antisymmetry\_of\_order\_relation},\mbox{axiom})$

$( x \leq y\mbox{ and }y \leq z ) \ \Rightarrow \ x \leq z\qquad\mbox{cnf}(\mbox{transitivity\_of\_order\_relation},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ ( x \leq y\mbox{ or }y \leq x )\qquad\mbox{cnf}(\mbox{totality\_of\_order\_relation},\mbox{axiom})$

$( \mbox{defined}(z)\mbox{ and }x \leq y ) \ \Rightarrow \ x + z \leq y + z\qquad\mbox{cnf}(\mbox{compatibility\_of\_order\_relation\_and\_addition},\mbox{axiom})$

$( 0 \leq y\mbox{ and }0 \leq z ) \ \Rightarrow \ 0 \leq y\cdot z\qquad\mbox{cnf}(\mbox{compatibility\_of\_order\_relation\_and\_multiplication},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ x{=}x\qquad\mbox{cnf}(\mbox{reflexivity\_of\_equality},\mbox{axiom})$

$y{=}x \ \Rightarrow \ x{=}y\qquad\mbox{cnf}(\mbox{symmetry\_of\_equality},\mbox{axiom})$

$( x{=}y\mbox{ and }y{=}z ) \ \Rightarrow \ x{=}z\qquad\mbox{cnf}(\mbox{transitivity\_of\_equality},\mbox{axiom})$

$( \mbox{defined}(z)\mbox{ and }x{=}y ) \ \Rightarrow \ x + z{=}y + z\qquad\mbox{cnf}(\mbox{compatibility\_of\_equality\_and\_addition},\mbox{axiom})$

$( \mbox{defined}(z)\mbox{ and }x{=}y ) \ \Rightarrow \ x\cdot z{=}y\cdot z\qquad\mbox{cnf}(\mbox{compatibility\_of\_equality\_and\_multiplication},\mbox{axiom})$

$( x \leq z\mbox{ and }x{=}y ) \ \Rightarrow \ y \leq z\qquad\mbox{cnf}(\mbox{compatibility\_of\_equality\_and\_order\_relation},\mbox{axiom})$

$\neg\,0{=}1\qquad\mbox{cnf}(\mbox{different\_identities},\mbox{axiom})$

\medskip\textbf{FLD002-0.ax} Ordered field axioms (axiom formulation re)






$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }u + z{=}w ) \ \Rightarrow \ x + v{=}w\qquad\mbox{cnf}(\mbox{associativity\_addition}_1,\mbox{axiom})$

$( x + y{=}u\mbox{ and }y + z{=}v\mbox{ and }x + v{=}w ) \ \Rightarrow \ u + z{=}w\qquad\mbox{cnf}(\mbox{associativity\_addition}_2,\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ 0 + x{=}x\qquad\mbox{cnf}(\mbox{existence\_of\_identity\_addition},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ -x + x{=}0\qquad\mbox{cnf}(\mbox{existence\_of\_inverse\_addition},\mbox{axiom})$

$x + y{=}z \ \Rightarrow \ y + x{=}z\qquad\mbox{cnf}(\mbox{commutativity\_addition},\mbox{axiom})$

$( x\cdot y{=}u\mbox{ and }y\cdot z{=}v\mbox{ and }u\cdot z{=}w ) \ \Rightarrow \ x\cdot v{=}w\qquad\mbox{cnf}(\mbox{associativity\_multiplication}_1,\mbox{axiom})$

$( x\cdot y{=}u\mbox{ and }y\cdot z{=}v\mbox{ and }x\cdot v{=}w ) \ \Rightarrow \ u\cdot z{=}w\qquad\mbox{cnf}(\mbox{associativity\_multiplication}_2,\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ 1\cdot x{=}x\qquad\mbox{cnf}(\mbox{existence\_of\_identity\_multiplication},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ ( x^{-1}\cdot x{=}1\mbox{ or }0 + x{=}0 )\qquad\mbox{cnf}(\mbox{existence\_of\_inverse\_multiplication},\mbox{axiom})$

$x\cdot y{=}z \ \Rightarrow \ y\cdot x{=}z\qquad\mbox{cnf}(\mbox{commutativity\_multiplication},\mbox{axiom})$

$( x + y{=}a\mbox{ and }a\cdot z{=}b\mbox{ and }x\cdot z{=}c\mbox{ and }y\cdot z{=}d ) \ \Rightarrow \ c + d{=}b\qquad\mbox{cnf}(\mbox{distributivity}_1,\mbox{axiom})$

$( x + y{=}a\mbox{ and }x\cdot z{=}c\mbox{ and }y\cdot z{=}d\mbox{ and }c + d{=}b ) \ \Rightarrow \ a\cdot z{=}b\qquad\mbox{cnf}(\mbox{distributivity}_2,\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ \mbox{defined}(x + y)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_addition},\mbox{axiom})$

$\mbox{defined}(0)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_additive\_identity},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ \mbox{defined}(-x)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_additive\_inverse},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ \mbox{defined}(x\cdot y)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_multiplication},\mbox{axiom})$

$\mbox{defined}(1)\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_multiplicative\_identity},\mbox{axiom})$

$\mbox{defined}(x) \ \Rightarrow \ ( \mbox{defined}(x^{-1})\mbox{ or }0 + x{=}0 )\qquad\mbox{cnf}(\mbox{well\_definedness\_of\_multiplicative\_inverse},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ x + y{=}x + y\qquad\mbox{cnf}(\mbox{totality\_of\_addition},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ x\cdot y{=}x\cdot y\qquad\mbox{cnf}(\mbox{totality\_of\_multiplication},\mbox{axiom})$

$( x \leq y\mbox{ and }y \leq x ) \ \Rightarrow \ 0 + x{=}y\qquad\mbox{cnf}(\mbox{antisymmetry\_of\_order\_relation},\mbox{axiom})$

$( x \leq y\mbox{ and }y \leq z ) \ \Rightarrow \ x \leq z\qquad\mbox{cnf}(\mbox{transitivity\_of\_order\_relation},\mbox{axiom})$

$( \mbox{defined}(x)\mbox{ and }\mbox{defined}(y) ) \ \Rightarrow \ ( x \leq y\mbox{ or }y \leq x )\qquad\mbox{cnf}(\mbox{totality\_of\_order\_relation},\mbox{axiom})$

$( x \leq y\mbox{ and }x + z{=}u\mbox{ and }y + z{=}v ) \ \Rightarrow \ u \leq v\qquad\mbox{cnf}(\mbox{compatibility\_of\_order\_relation\_and\_addition},\mbox{axiom})$

$( 0 \leq x\mbox{ and }0 \leq y\mbox{ and }x\cdot y{=}z ) \ \Rightarrow \ 0 \leq z\qquad\mbox{cnf}(\mbox{compatibility\_of\_order\_relation\_and\_multiplication},\mbox{axiom})$

$\neg\,0 + 0{=}1\qquad\mbox{cnf}(\mbox{different\_identities},\mbox{axiom})$

\medskip\textbf{FLD009-3.p} Linear equations in the multiplicative group have a solution






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,a\cdot x{=}b\qquad\mbox{cnf}(\mbox{not\_product}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD070-1.p} One-sided addition of two order relations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,0 \leq a + b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD030-4.p} Compatibility of multiplication and equality relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{product}_5,\mbox{negated\_conjecture})$

$1\cdot a{=}d\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$\neg\,d\cdot b{=}c\qquad\mbox{cnf}(\mbox{not\_product}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD031-3.p} If a is one, then the multiplicative inverse of a is also one






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$1\cdot a{=}1\qquad\mbox{cnf}(\mbox{product}_2,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,1\cdot a^{-1}{=}1\qquad\mbox{cnf}(\mbox{not\_product}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD050-1.p} Fraction calculation, part 4






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$a\cdot d{=}b\cdot c\qquad\mbox{cnf}(\mbox{multiply\_equals\_multiply}_7,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1}{=}c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_multiply}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD067-1.p} Side change in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,0 \leq b + -a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD054-1.p} Fraction calculation, part 8






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$\neg\,a^{-1} + b^{-1}{=}( a + b )\cdot ( a\cdot b )^{-1}\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_multiply}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD025-4.p} The resulting equation of a multiplication of two equations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$1\cdot a{=}b\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$1\cdot c{=}d\qquad\mbox{cnf}(\mbox{product}_7,\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_8,\mbox{negated\_conjecture})$

$\neg\,d\cdot b{=}u\qquad\mbox{cnf}(\mbox{not\_product}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD094-3.p} One-sided Elimination of a multiplicative inverse, part 4






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$a^{-1} \leq -1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,-1 \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD072-2.p} One-sided multiplication of two order relations, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_6,\mbox{negated\_conjecture})$

$\neg\,u \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD063-3.p} Elimination of additive inverses in an order relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$-b \leq -a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD045-2.p} Compatibility of multiplication and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$( -a )\cdot ( -b ){=}c\qquad\mbox{cnf}(\mbox{multiply\_equals\_c}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}d\qquad\mbox{cnf}(\mbox{multiply\_equals\_d}_6,\mbox{negated\_conjecture})$

$\neg\,c{=}d\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_d}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD023-1.p} Side Change of a term in an equation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a{=}b\qquad\mbox{cnf}(\mbox{a\_equals\_b}_3,\mbox{negated\_conjecture})$

$\neg\,0{=}b + -a\qquad\mbox{cnf}(\mbox{additive\_identity\_not\_equal\_to\_add}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD035-1.p} Elimination of a multiplication in an equation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a\cdot c{=}b\cdot c\qquad\mbox{cnf}(\mbox{multiply\_equals\_multiply}_4,\mbox{negated\_conjecture})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,a{=}b\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_b}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD064-3.p} Side change of a term in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$\neg\,-a \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD037-3.p} Side change of a term in an equation by multiplication, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$1\cdot a{=}b\qquad\mbox{cnf}(\mbox{product}_4,\mbox{negated\_conjecture})$

$\neg\,b\cdot a^{-1}{=}1\qquad\mbox{cnf}(\mbox{not\_product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD032-1.p} If the multiplicative inverse of a is one, then a is one itself






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$a^{-1}{=}1\qquad\mbox{cnf}(\mbox{multiplicative\_inverses\_equal},\mbox{negated\_conjecture})$

$\neg\,a{=}1\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_multiplicative\_identity}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD026-1.p} Compatibility of multiplicative inverses with equality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$a{=}b\qquad\mbox{cnf}(\mbox{a\_equals\_b}_4,\mbox{negated\_conjecture})$

$\neg\,a^{-1}{=}b^{-1}\qquad\mbox{cnf}(\mbox{multiplicative\_inverses\_not\_equal},\mbox{negated\_conjecture})$

\medskip\textbf{FLD098-4.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$1 + -a{=}u\qquad\mbox{cnf}(\mbox{sum}_{10},\mbox{negated\_conjecture})$

$1 + -b{=}v\qquad\mbox{cnf}(\mbox{sum}_{11},\mbox{negated\_conjecture})$

$u\cdot v{=}w\qquad\mbox{cnf}(\mbox{product}_{12},\mbox{negated\_conjecture})$

$a + b{=}s\qquad\mbox{cnf}(\mbox{sum}_{13},\mbox{negated\_conjecture})$

$1 + -s{=}t\qquad\mbox{cnf}(\mbox{sum}_{14},\mbox{negated\_conjecture})$

$\neg\,t \leq w\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{FLD016-5.p} Solutions of linear equations in the additive group are unique






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(q)\qquad\mbox{cnf}(\mbox{q\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(r)\qquad\mbox{cnf}(\mbox{r\_is\_defined},\mbox{hypothesis})$

$a + u{=}q\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$a + v{=}r\qquad\mbox{cnf}(\mbox{sum}_7,\mbox{negated\_conjecture})$

$0 + q{=}r\qquad\mbox{cnf}(\mbox{sum}_8,\mbox{negated\_conjecture})$

$\neg\,0 + u{=}v\qquad\mbox{cnf}(\mbox{not\_sum}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD012-1.p} Compatibility of operation and inverse in multiplicative group






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$\neg\,( a\cdot b )^{-1}{=}a^{-1}\cdot b^{-1}\qquad\mbox{cnf}(\mbox{multiplicative\_inverse\_not\_equal\_to\_multiply}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD077-3.p} Elimination of a product in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$c \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot c \leq b\cdot c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,b \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD027-3.p} Elimination of multiplicative inverses in an equation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$1\cdot a^{-1}{=}b^{-1}\qquad\mbox{cnf}(\mbox{product}_5,\mbox{negated\_conjecture})$

$\neg\,1\cdot a{=}b\qquad\mbox{cnf}(\mbox{not\_product}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD066-3.p} Elimination of a summation in an order relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a + c{=}u\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$b + c{=}v\qquad\mbox{cnf}(\mbox{sum}_7,\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD052-2.p} Fraction calculation, part 6






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(p)\qquad\mbox{cnf}(\mbox{p\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(q)\qquad\mbox{cnf}(\mbox{q\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_{13},\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_{14},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{multiply\_equals\_s}_{15},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}t\qquad\mbox{cnf}(\mbox{multiply\_equals\_t}_{16},\mbox{negated\_conjecture})$

$s + t{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_{17},\mbox{negated\_conjecture})$

$a\cdot d{=}p\qquad\mbox{cnf}(\mbox{multiply\_equals\_p}_{18},\mbox{negated\_conjecture})$

$b\cdot c{=}q\qquad\mbox{cnf}(\mbox{multiply\_equals\_q}_{19},\mbox{negated\_conjecture})$

$p + q{=}k\qquad\mbox{cnf}(\mbox{add\_equals\_k}_{20},\mbox{negated\_conjecture})$

$b\cdot d{=}l\qquad\mbox{cnf}(\mbox{multiply\_equals\_l}_{21},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_u}_{22},\mbox{negated\_conjecture})$

\medskip\textbf{FLD031-5.p} If a is one, then the multiplicative inverse of a is also one






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$1\cdot a{=}1\qquad\mbox{cnf}(\mbox{product}_2,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,1\cdot 1{=}a^{-1}\qquad\mbox{cnf}(\mbox{not\_product}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD097-3.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,1 + ( a + b ) \leq ( 1 + a )\cdot ( 1 + b )\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD008-3.p} Compatibility of operation and inverse in the additive group






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + -( a + b ){=}-a + -b\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD084-1.p} Elimination of multiplicative inverses in an order, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$b^{-1} \leq a^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$0 \leq b^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD076-3.p} Two-sided multiplication in an order relation, part 3






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot c \leq b\cdot c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD064-1.p} Side change of a term in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$\neg\,-a \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD039-3.p} In a field with two or more elements, 1 and 0 must be different






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_1,\mbox{negated\_conjecture})$

$0 + 1{=}0\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD087-3.p} Elimination of a multiplicative inverse in an order, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$0 \leq a^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,0 \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD090-1.p} A characterization of 1 with help of the order relation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$m\cdot x \leq x\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$\neg\,m{=}1\qquad\mbox{cnf}(\mbox{m\_not\_equal\_to\_multiplicative\_identity}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD077-1.p} Elimination of a product in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$c \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot c \leq b\cdot c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,b \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD013-2.p} The resulting equation of the summation of two equations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a{=}b\qquad\mbox{cnf}(\mbox{a\_equals\_b}_6,\mbox{negated\_conjecture})$

$c{=}d\qquad\mbox{cnf}(\mbox{c\_equals\_d}_7,\mbox{negated\_conjecture})$

$a + c{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_8,\mbox{negated\_conjecture})$

$\neg\,d + b{=}u\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_u}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD078-2.p} Side change in an order relation, multiplicative part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_7,\mbox{negated\_conjecture})$

$\neg\,u \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD030-3.p} Compatibility of multiplication and equality relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$1\cdot a{=}d\qquad\mbox{cnf}(\mbox{product}_4,\mbox{negated\_conjecture})$

$\neg\,d\cdot b{=}a\cdot b\qquad\mbox{cnf}(\mbox{not\_product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD034-3.p} Every element equal one is a multiplicative identity






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$1\cdot m{=}1\qquad\mbox{cnf}(\mbox{product}_3,\mbox{negated\_conjecture})$

$\neg\,m\cdot a{=}a\qquad\mbox{cnf}(\mbox{not\_product}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD067-4.p} Side change in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$b + -a{=}u\qquad\mbox{cnf}(\mbox{sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD081-4.p} Two-sided multiplication of two order relations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$c \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{10},\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_{11},\mbox{negated\_conjecture})$

$d\cdot b{=}v\qquad\mbox{cnf}(\mbox{product}_{12},\mbox{negated\_conjecture})$

$\neg\,u \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{13},\mbox{negated\_conjecture})$

\medskip\textbf{FLD070-3.p} One-sided addition of two order relations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,0 \leq a + b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD022-3.p} Elimination of a summation in an equation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a + c{=}u\qquad\mbox{cnf}(\mbox{sum}_5,\mbox{negated\_conjecture})$

$b + c{=}u\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}b\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD024-3.p} Side Change of a term in an equation, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$b + -a{=}0\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}b\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD036-3.p} Only a multiplication by zero can make elements equal






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_5,\mbox{negated\_conjecture})$

$b\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$\neg\,1\cdot a{=}b\qquad\mbox{cnf}(\mbox{not\_product}_7,\mbox{negated\_conjecture})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD041-1.p} If a,b are not 0, the the product of a and b is not 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$a\cdot b{=}0\qquad\mbox{cnf}(\mbox{multiply\_equals\_additive\_identity}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD074-1.p} Two-sided multiplication in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a\cdot c \leq b\cdot c\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD082-1.p} Compatibility of order and multiplicative inverses, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,b^{-1} \leq a^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD048-1.p} Fraction calculation, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$\neg\,( a\cdot b^{-1} )\cdot ( c\cdot d^{-1} ){=}( a\cdot c )\cdot ( b\cdot d )^{-1}\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_multiply}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD093-1.p} One-sided Elimination of a multiplicative inverse, part 3






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$1 \leq a^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD017-1.p} Substitution of an element in additive equations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(x)\qquad\mbox{cnf}(\mbox{x\_is\_defined},\mbox{hypothesis})$

$a{=}x\qquad\mbox{cnf}(\mbox{a\_equals\_x}_5,\mbox{negated\_conjecture})$

$a + b{=}c\qquad\mbox{cnf}(\mbox{add\_equals\_c}_6,\mbox{negated\_conjecture})$

$\neg\,x + b{=}c\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_c}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD051-2.p} Fraction calculation, part 5






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_{10},\mbox{negated\_conjecture})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_{11},\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_{12},\mbox{negated\_conjecture})$

$s\cdot t^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_{13},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{multiply\_equals\_s}_{14},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}t\qquad\mbox{cnf}(\mbox{multiply\_equals\_t}_{15},\mbox{negated\_conjecture})$

$a\cdot d{=}k\qquad\mbox{cnf}(\mbox{multiply\_equals\_k}_{16},\mbox{negated\_conjecture})$

$b\cdot c{=}l\qquad\mbox{cnf}(\mbox{multiply\_equals\_l}_{17},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_u}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{FLD050-4.p} Fraction calculation, part 4






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{product}_9,\mbox{negated\_conjecture})$

$a\cdot d{=}k\qquad\mbox{cnf}(\mbox{product}_{10},\mbox{negated\_conjecture})$

$b\cdot c{=}k\qquad\mbox{cnf}(\mbox{product}_{11},\mbox{negated\_conjecture})$

$\neg\,c\cdot d^{-1}{=}s\qquad\mbox{cnf}(\mbox{not\_product}_{12},\mbox{negated\_conjecture})$

\medskip\textbf{FLD025-5.p} The resulting equation of a multiplication of two equations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$1\cdot a{=}b\qquad\mbox{cnf}(\mbox{product}_7,\mbox{negated\_conjecture})$

$1\cdot c{=}d\qquad\mbox{cnf}(\mbox{product}_8,\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_9,\mbox{negated\_conjecture})$

$d\cdot b{=}v\qquad\mbox{cnf}(\mbox{product}_{10},\mbox{negated\_conjecture})$

$\neg\,1\cdot u{=}v\qquad\mbox{cnf}(\mbox{not\_product}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD008-1.p} Compatibility of operation and inverse in the additive group






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,-( a + b ){=}-a + -b\qquad\mbox{cnf}(\mbox{additive\_inverse\_not\_equal\_to\_add}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD050-3.p} Fraction calculation, part 4






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$a\cdot d{=}b\cdot c\qquad\mbox{cnf}(\mbox{product}_7,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1}{=}c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{not\_product}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD077-4.p} Elimination of a product in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$c \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_8,\mbox{negated\_conjecture})$

$b\cdot c{=}v\qquad\mbox{cnf}(\mbox{product}_9,\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{10},\mbox{negated\_conjecture})$

$\neg\,b \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD094-1.p} One-sided Elimination of a multiplicative inverse, part 4






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$a^{-1} \leq -1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,-1 \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD040-1.p} If a is not 0, then the multiplicative inverse of a is not 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$a^{-1}{=}0\qquad\mbox{cnf}(\mbox{multiplicative\_inverse\_equals\_additive\_identity}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD054-4.p} Fraction calculation, part 8






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

$a^{-1} + b^{-1}{=}u\qquad\mbox{cnf}(\mbox{sum}_8,\mbox{negated\_conjecture})$

$a + b{=}k\qquad\mbox{cnf}(\mbox{sum}_9,\mbox{negated\_conjecture})$

$a\cdot b{=}l\qquad\mbox{cnf}(\mbox{product}_{10},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{not\_product}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD071-2.p} One-sided multiplication of two order relations, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_6,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD035-3.p} Elimination of a multiplication in an equation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_5,\mbox{negated\_conjecture})$

$b\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

$\neg\,1\cdot a{=}b\qquad\mbox{cnf}(\mbox{not\_product}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD013-4.p} The resulting equation of the summation of two equations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$0 + a{=}b\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$0 + c{=}d\qquad\mbox{cnf}(\mbox{sum}_7,\mbox{negated\_conjecture})$

$a + c{=}u\qquad\mbox{cnf}(\mbox{sum}_8,\mbox{negated\_conjecture})$

$\neg\,d + b{=}u\qquad\mbox{cnf}(\mbox{not\_sum}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD072-4.p} One-sided multiplication of two order relations, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$\neg\,u \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD038-3.p} Side change of a term in an equation by multiplication, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$b\cdot a^{-1}{=}1\qquad\mbox{cnf}(\mbox{product}_4,\mbox{negated\_conjecture})$

$\neg\,1\cdot a{=}b\qquad\mbox{cnf}(\mbox{not\_product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD051-4.p} Fraction calculation, part 5






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{10},\mbox{negated\_conjecture})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{11},\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{12},\mbox{negated\_conjecture})$

$s\cdot t^{-1}{=}u\qquad\mbox{cnf}(\mbox{product}_{13},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{product}_{14},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}t\qquad\mbox{cnf}(\mbox{product}_{15},\mbox{negated\_conjecture})$

$a\cdot d{=}k\qquad\mbox{cnf}(\mbox{product}_{16},\mbox{negated\_conjecture})$

$b\cdot c{=}l\qquad\mbox{cnf}(\mbox{product}_{17},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{not\_product}_{18},\mbox{negated\_conjecture})$

\medskip\textbf{FLD041-2.p} If a,b are not 0, the the product of a and b is not 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{multiply\_equals\_c}_6,\mbox{negated\_conjecture})$

$c{=}0\qquad\mbox{cnf}(\mbox{c\_equals\_additive\_identity}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD030-2.p} Compatibility of multiplication and equality relation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{multiply\_equals\_c}_5,\mbox{negated\_conjecture})$

$a{=}d\qquad\mbox{cnf}(\mbox{a\_equals\_d}_6,\mbox{negated\_conjecture})$

$\neg\,d\cdot b{=}c\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_c}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD015-1.p} Compatibility of additive inverses with the equality, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$-a{=}-b\qquad\mbox{cnf}(\mbox{additive\_inverse\_equals\_additive\_inverse}_3,\mbox{negated\_conjecture})$

$\neg\,a{=}b\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_b}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD068-3.p} Side change of a term in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq b + -a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD085-3.p} Elimination of multiplicative inverses in an order, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$b^{-1} \leq a^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a^{-1} \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD067-3.p} Side change in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,0 \leq b + -a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD058-1.p} If a greater 0 and b greater or equal a the b greater 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$b{=}0\qquad\mbox{cnf}(\mbox{b\_equals\_additive\_identity}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD077-2.p} Elimination of a product in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$c \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_8,\mbox{negated\_conjecture})$

$b\cdot c{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_9,\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{10},\mbox{negated\_conjecture})$

$\neg\,b \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD062-1.p} Compatibility of the order relation and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,-b \leq -a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD044-4.p} Compatibility of multiplication and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{product}_4,\mbox{negated\_conjecture})$

$\neg\,( -a )\cdot b{=}-u\qquad\mbox{cnf}(\mbox{not\_product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD059-4.p} If a greater or equal 0, then 2a greater or equal 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$a + a{=}u\qquad\mbox{cnf}(\mbox{sum}_4,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD078-3.p} Side change in an order relation, multiplicative part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1} \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD007-3.p} The additive inverse fulfills the involution property






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + -( -a ){=}a\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD022-1.p} Elimination of a summation in an equation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a + c{=}b + c\qquad\mbox{cnf}(\mbox{add\_equals\_add}_4,\mbox{negated\_conjecture})$

$\neg\,a{=}b\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_b}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD050-2.p} Fraction calculation, part 4






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_7,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{multiply\_equals\_s}_9,\mbox{negated\_conjecture})$

$a\cdot d{=}k\qquad\mbox{cnf}(\mbox{multiply\_equals\_k}_{10},\mbox{negated\_conjecture})$

$b\cdot c{=}k\qquad\mbox{cnf}(\mbox{multiply\_equals\_k}_{11},\mbox{negated\_conjecture})$

$\neg\,c\cdot d^{-1}{=}s\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_s}_{12},\mbox{negated\_conjecture})$

\medskip\textbf{FLD086-1.p} Compatibility of order and multiplicative inverses, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,0 \leq a^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD059-3.p} If a greater or equal 0, then 2a greater or equal 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$\neg\,0 \leq a + a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD079-1.p} Side change in an order relation, multiplicative part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a\cdot b^{-1} \leq 1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD053-2.p} Fraction calculation, part 7






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(p)\qquad\mbox{cnf}(\mbox{p\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(q)\qquad\mbox{cnf}(\mbox{q\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_{12},\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_{13},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{multiply\_equals\_s}_{14},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}t\qquad\mbox{cnf}(\mbox{multiply\_equals\_t}_{15},\mbox{negated\_conjecture})$

$s + -t{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_{16},\mbox{negated\_conjecture})$

$a\cdot d{=}p\qquad\mbox{cnf}(\mbox{multiply\_equals\_p}_{17},\mbox{negated\_conjecture})$

$b\cdot c{=}q\qquad\mbox{cnf}(\mbox{multiply\_equals\_q}_{18},\mbox{negated\_conjecture})$

$p + -q{=}k\qquad\mbox{cnf}(\mbox{add\_equals\_k}_{19},\mbox{negated\_conjecture})$

$b\cdot d{=}l\qquad\mbox{cnf}(\mbox{multiply\_equals\_l}_{20},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_u}_{21},\mbox{negated\_conjecture})$

\medskip\textbf{FLD049-4.p} Fraction calculation, part 3






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{product}_9,\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}s\qquad\mbox{cnf}(\mbox{product}_{10},\mbox{negated\_conjecture})$

$a\cdot d{=}k\qquad\mbox{cnf}(\mbox{product}_{11},\mbox{negated\_conjecture})$

$\neg\,b\cdot c{=}k\qquad\mbox{cnf}(\mbox{not\_product}_{12},\mbox{negated\_conjecture})$

\medskip\textbf{FLD080-3.p} The square of an element is always greater or equal 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 \leq a\cdot a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD102-1.p} Ordered field axioms (axiom formulation re)






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

\medskip\textbf{FLD005-1.p} Every linear equation in the additive group has a solution






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a + x{=}b\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_b}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD030-1.p} Compatibility of multiplication and equality relation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a{=}d\qquad\mbox{cnf}(\mbox{a\_equals\_d}_4,\mbox{negated\_conjecture})$

$\neg\,d\cdot b{=}a\cdot b\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_multiply}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD025-1.p} The resulting equation of a multiplication of two equations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a{=}b\qquad\mbox{cnf}(\mbox{a\_equals\_b}_5,\mbox{negated\_conjecture})$

$c{=}d\qquad\mbox{cnf}(\mbox{c\_equals\_d}_6,\mbox{negated\_conjecture})$

$\neg\,a\cdot c{=}d\cdot b\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_multiply}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD060-1.p} If b greater or equal b, then 2b greater or equal 2a






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a + a \leq b + b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD033-3.p} The multiplicative identity is unique






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$m\cdot a{=}a\qquad\mbox{cnf}(\mbox{product}_4,\mbox{negated\_conjecture})$

$\neg\,1\cdot m{=}1\qquad\mbox{cnf}(\mbox{not\_product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD052-4.p} Fraction calculation, part 6






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(p)\qquad\mbox{cnf}(\mbox{p\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(q)\qquad\mbox{cnf}(\mbox{q\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{13},\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{14},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{product}_{15},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}t\qquad\mbox{cnf}(\mbox{product}_{16},\mbox{negated\_conjecture})$

$s + t{=}u\qquad\mbox{cnf}(\mbox{sum}_{17},\mbox{negated\_conjecture})$

$a\cdot d{=}p\qquad\mbox{cnf}(\mbox{product}_{18},\mbox{negated\_conjecture})$

$b\cdot c{=}q\qquad\mbox{cnf}(\mbox{product}_{19},\mbox{negated\_conjecture})$

$p + q{=}k\qquad\mbox{cnf}(\mbox{sum}_{20},\mbox{negated\_conjecture})$

$b\cdot d{=}l\qquad\mbox{cnf}(\mbox{product}_{21},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{not\_product}_{22},\mbox{negated\_conjecture})$

\medskip\textbf{FLD013-1.p} The resulting equation of the summation of two equations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a{=}b\qquad\mbox{cnf}(\mbox{a\_equals\_b}_5,\mbox{negated\_conjecture})$

$c{=}d\qquad\mbox{cnf}(\mbox{c\_equals\_d}_6,\mbox{negated\_conjecture})$

$\neg\,a + c{=}d + b\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_add}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD029-3.p} The solution of a multiplicative linear equation is unique






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$a\cdot u{=}b\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$a\cdot v{=}b\qquad\mbox{cnf}(\mbox{product}_7,\mbox{negated\_conjecture})$

$\neg\,1\cdot u{=}v\qquad\mbox{cnf}(\mbox{not\_product}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD078-4.p} Side change in an order relation, multiplicative part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{product}_7,\mbox{negated\_conjecture})$

$\neg\,u \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD013-3.p} The resulting equation of the summation of two equations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$0 + a{=}b\qquad\mbox{cnf}(\mbox{sum}_5,\mbox{negated\_conjecture})$

$0 + c{=}d\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$\neg\,a + c{=}d + b\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD095-4.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{10},\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{11},\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{12},\mbox{negated\_conjecture})$

$0 \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{13},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{product}_{14},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}v\qquad\mbox{cnf}(\mbox{product}_{15},\mbox{negated\_conjecture})$

$a + c{=}s\qquad\mbox{cnf}(\mbox{sum}_{16},\mbox{negated\_conjecture})$

$b + d{=}t\qquad\mbox{cnf}(\mbox{sum}_{17},\mbox{negated\_conjecture})$

$s\cdot t^{-1}{=}w\qquad\mbox{cnf}(\mbox{product}_{18},\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{19},\mbox{negated\_conjecture})$

$\neg\,u \leq w\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{20},\mbox{negated\_conjecture})$

\medskip\textbf{FLD071-4.p} One-sided multiplication of two order relations, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD048-3.p} Fraction calculation, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$\neg\,( a\cdot b^{-1} )\cdot ( c\cdot d^{-1} ){=}( a\cdot c )\cdot ( b\cdot d )^{-1}\qquad\mbox{cnf}(\mbox{not\_product}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD056-1.p} Reflexivity of the order relation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD049-1.p} Fraction calculation, part 3






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{multiply\_equals\_multiply}_7,\mbox{negated\_conjecture})$

$\neg\,a\cdot d{=}b\cdot c\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_multiply}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD049-2.p} Fraction calculation, part 3






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_7,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{multiply\_equals\_s}_9,\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}s\qquad\mbox{cnf}(\mbox{multiply\_equals\_s}_{10},\mbox{negated\_conjecture})$

$a\cdot d{=}k\qquad\mbox{cnf}(\mbox{multiply\_equals\_k}_{11},\mbox{negated\_conjecture})$

$\neg\,b\cdot c{=}k\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_k}_{12},\mbox{negated\_conjecture})$

\medskip\textbf{FLD076-4.p} Two-sided multiplication in an order relation, part 3






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_8,\mbox{negated\_conjecture})$

$b\cdot c{=}v\qquad\mbox{cnf}(\mbox{product}_9,\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{10},\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD096-4.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{10},\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{11},\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{12},\mbox{negated\_conjecture})$

$0 \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{13},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{product}_{14},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}v\qquad\mbox{cnf}(\mbox{product}_{15},\mbox{negated\_conjecture})$

$a + c{=}s\qquad\mbox{cnf}(\mbox{sum}_{16},\mbox{negated\_conjecture})$

$b + d{=}t\qquad\mbox{cnf}(\mbox{sum}_{17},\mbox{negated\_conjecture})$

$s\cdot t^{-1}{=}w\qquad\mbox{cnf}(\mbox{product}_{18},\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{19},\mbox{negated\_conjecture})$

$\neg\,w \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{20},\mbox{negated\_conjecture})$

\medskip\textbf{FLD096-3.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$0 \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1} \leq c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$\neg\,( a + c )\cdot ( b + d )^{-1} \leq c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{10},\mbox{negated\_conjecture})$

\medskip\textbf{FLD079-4.p} Side change in an order relation, multiplicative part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$u \leq 1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD010-1.p} In the multiplicative group inverse(identity)=identity






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\neg\,1^{-1}{=}1\qquad\mbox{cnf}(\mbox{multiplicative\_inv\_not\_equal\_to\_multiplicative\_id}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD065-1.p} Side change of a term in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$-a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$\neg\,0 \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD037-1.p} Side change of a term in an equation by multiplication, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$a{=}b\qquad\mbox{cnf}(\mbox{a\_equals\_b}_4,\mbox{negated\_conjecture})$

$\neg\,1{=}b\cdot a^{-1}\qquad\mbox{cnf}(\mbox{multiplicative\_identity\_not\_equal\_to\_multiply}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD054-3.p} Fraction calculation, part 8






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$\neg\,a^{-1} + b^{-1}{=}( a + b )\cdot ( a\cdot b )^{-1}\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD100-4.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$1 + a{=}u\qquad\mbox{cnf}(\mbox{sum}_{10},\mbox{negated\_conjecture})$

$1 + b{=}v\qquad\mbox{cnf}(\mbox{sum}_{11},\mbox{negated\_conjecture})$

$u\cdot v{=}w\qquad\mbox{cnf}(\mbox{product}_{12},\mbox{negated\_conjecture})$

$a + b{=}s\qquad\mbox{cnf}(\mbox{sum}_{13},\mbox{negated\_conjecture})$

$1 + s{=}t\qquad\mbox{cnf}(\mbox{sum}_{14},\mbox{negated\_conjecture})$

$\neg\,t \leq w\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{FLD056-3.p} Reflexivity of the order relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD049-3.p} Fraction calculation, part 3






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{product}_7,\mbox{negated\_conjecture})$

$\neg\,a\cdot d{=}b\cdot c\qquad\mbox{cnf}(\mbox{not\_product}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD011-3.p} The multiplicative inverse fulfills the involution property






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$\neg\,1\cdot ( a^{-1} )^{-1}{=}a\qquad\mbox{cnf}(\mbox{not\_product}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD075-2.p} Two-sided multiplication in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_6,\mbox{negated\_conjecture})$

$b\cdot c{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_7,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$c \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$\neg\,v \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{10},\mbox{negated\_conjecture})$

\medskip\textbf{FLD029-1.p} The solution of a multiplicative linear equation is unique






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$a\cdot u{=}b\qquad\mbox{cnf}(\mbox{multiply\_equals\_b}_6,\mbox{negated\_conjecture})$

$a\cdot v{=}b\qquad\mbox{cnf}(\mbox{multiply\_equals\_b}_7,\mbox{negated\_conjecture})$

$\neg\,u{=}v\qquad\mbox{cnf}(\mbox{u\_not\_equal\_to\_v}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD079-3.p} Side change in an order relation, multiplicative part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a\cdot b^{-1} \leq 1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD011-1.p} The multiplicative inverse fulfills the involution property






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$\neg\,( a^{-1} )^{-1}{=}a\qquad\mbox{cnf}(\mbox{multiplicative\_inverse\_not\_equal\_to\_a}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD074-2.p} Two-sided multiplication in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_6,\mbox{negated\_conjecture})$

$b\cdot c{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_7,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$\neg\,u \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{10},\mbox{negated\_conjecture})$

\medskip\textbf{FLD059-1.p} If a greater or equal 0, then 2a greater or equal 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$\neg\,0 \leq a + a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD086-3.p} Compatibility of order and multiplicative inverses, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,0 \leq a^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD046-1.p} Compatibility of the additive and the multiplicative inverse






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$\neg\,( -a )^{-1}{=}-a^{-1}\qquad\mbox{cnf}(\mbox{mult\_inverse\_not\_equal\_to\_additive\_inverse}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD073-4.p} One-sided multiplication of two order relations, part 3






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD019-3.p} If the additive inverse of a is zero, a itself is zero






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$0 + -a{=}0\qquad\mbox{cnf}(\mbox{sum}_2,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD039-1.p} In a field with two or more elements, 1 and 0 must be different






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_1,\mbox{negated\_conjecture})$

$1{=}0\qquad\mbox{cnf}(\mbox{multiplicative\_identity\_equals\_additive\_identity}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD008-2.p} Compatibility of operation and inverse in the additive group






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a + b{=}c\qquad\mbox{cnf}(\mbox{add\_equals\_c}_5,\mbox{negated\_conjecture})$

$-a + -b{=}d\qquad\mbox{cnf}(\mbox{add\_equals\_d}_6,\mbox{negated\_conjecture})$

$\neg\,-c{=}d\qquad\mbox{cnf}(\mbox{additive\_inverse\_not\_equal\_to\_d}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD057-3.p} 0 is less than 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\neg\,0 \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_1,\mbox{negated\_conjecture})$

\medskip\textbf{FLD074-4.p} Two-sided multiplication in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_8,\mbox{negated\_conjecture})$

$b\cdot c{=}v\qquad\mbox{cnf}(\mbox{product}_9,\mbox{negated\_conjecture})$

$\neg\,u \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{10},\mbox{negated\_conjecture})$

\medskip\textbf{FLD065-3.p} Side change of a term in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$-a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$\neg\,0 \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD063-1.p} Elimination of additive inverses in an order relation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$-b \leq -a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD073-3.p} One-sided multiplication of two order relations, part 3






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,0 \leq a\cdot b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD092-3.p} One-sided Elimination of a multiplicative inverse, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$a \leq -1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,-1 \leq a^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD093-3.p} One-sided Elimination of a multiplicative inverse, part 3






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$1 \leq a^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD003-1.p} Elimination of an additive term/inverse term - pair






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a + ( b + -b ){=}a\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_a}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD041-4.p} If a,b are not 0, the the product of a and b is not 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}c\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$0 + c{=}0\qquad\mbox{cnf}(\mbox{sum}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD005-3.p} Every linear equation in the additive group has a solution






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a + x{=}b\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD036-1.p} Only a multiplication by zero can make elements equal






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a\cdot c{=}b\cdot c\qquad\mbox{cnf}(\mbox{multiply\_equals\_multiply}_4,\mbox{negated\_conjecture})$

$\neg\,a{=}b\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_b}_5,\mbox{negated\_conjecture})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD044-2.p} Compatibility of multiplication and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$( -a )\cdot b{=}c\qquad\mbox{cnf}(\mbox{multiply\_equals\_c}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}d\qquad\mbox{cnf}(\mbox{multiply\_equals\_d}_6,\mbox{negated\_conjecture})$

$\neg\,c{=}-d\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_inverse}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD020-3.p} The additive identity is unique






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$m + a{=}a\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + m{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD006-3.p} In the additive group it holds: inverse(identity)=identity






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\neg\,0 + -0{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_1,\mbox{negated\_conjecture})$

\medskip\textbf{FLD069-1.p} If b $>$ 0 and a $>$= 0, then a + b not 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$a + b{=}0\qquad\mbox{cnf}(\mbox{add\_equals\_additive\_identity}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD012-4.p} Compatibility of operation and inverse in multiplicative group






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{product}_7,\mbox{negated\_conjecture})$

$a^{-1}\cdot b^{-1}{=}v\qquad\mbox{cnf}(\mbox{product}_8,\mbox{negated\_conjecture})$

$\neg\,1\cdot u^{-1}{=}v\qquad\mbox{cnf}(\mbox{not\_product}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD021-1.p} Every element equal to zero is an additive identity






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$m{=}0\qquad\mbox{cnf}(\mbox{m\_equals\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,m + a{=}a\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_a}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD028-1.p} The solution of a multiplicative linear equation is unique






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$a\cdot u{=}b\qquad\mbox{cnf}(\mbox{multiply\_equals\_b}_6,\mbox{negated\_conjecture})$

$a\cdot v{=}b\qquad\mbox{cnf}(\mbox{multiply\_equals\_b}_7,\mbox{negated\_conjecture})$

$\neg\,u{=}v\qquad\mbox{cnf}(\mbox{u\_not\_equal\_to\_v}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD068-1.p} Side change of a term in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq b + -a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD055-1.p} Compatibility of order and equality relation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$b{=}c\qquad\mbox{cnf}(\mbox{b\_equals\_c}_5,\mbox{negated\_conjecture})$

$\neg\,a \leq c\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD047-1.p} Fraction calculation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1}{=}( a\cdot c )\cdot ( b\cdot c )^{-1}\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_multiply}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD012-2.p} Compatibility of operation and inverse in multiplicative group






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_7,\mbox{negated\_conjecture})$

$a^{-1}\cdot b^{-1}{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_8,\mbox{negated\_conjecture})$

$\neg\,u^{-1}{=}v\qquad\mbox{cnf}(\mbox{multiplicative\_inverse\_not\_equal\_to\_v}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD052-3.p} Fraction calculation, part 6






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1} + c\cdot d^{-1}{=}( a\cdot d + b\cdot c )\cdot ( b\cdot d )^{-1}\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD073-1.p} One-sided multiplication of two order relations, part 3






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,0 \leq a\cdot b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD060-4.p} If b greater or equal b, then 2b greater or equal 2a






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a + a{=}u\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$b + b{=}v\qquad\mbox{cnf}(\mbox{sum}_7,\mbox{negated\_conjecture})$

$\neg\,u \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD080-1.p} The square of an element is always greater or equal 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 \leq a\cdot a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD047-4.p} Fraction calculation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{product}_9,\mbox{negated\_conjecture})$

$a\cdot c{=}s\qquad\mbox{cnf}(\mbox{product}_{10},\mbox{negated\_conjecture})$

$b\cdot c{=}t\qquad\mbox{cnf}(\mbox{product}_{11},\mbox{negated\_conjecture})$

$\neg\,s\cdot t^{-1}{=}u\qquad\mbox{cnf}(\mbox{not\_product}_{12},\mbox{negated\_conjecture})$

\medskip\textbf{FLD028-3.p} The solution of a multiplicative linear equation is unique






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$a\cdot u{=}b\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$a\cdot v{=}b\qquad\mbox{cnf}(\mbox{product}_7,\mbox{negated\_conjecture})$

$\neg\,1\cdot u{=}v\qquad\mbox{cnf}(\mbox{not\_product}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD060-2.p} If b greater or equal b, then 2b greater or equal 2a






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a + a{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_5,\mbox{negated\_conjecture})$

$b + b{=}v\qquad\mbox{cnf}(\mbox{add\_equals\_v}_6,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$\neg\,u \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD032-3.p} If the multiplicative inverse of a is one, then a is one itself






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$1\cdot a^{-1}{=}1\qquad\mbox{cnf}(\mbox{product}_3,\mbox{negated\_conjecture})$

$\neg\,1\cdot a{=}1\qquad\mbox{cnf}(\mbox{not\_product}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD020-1.p} The additive identity is unique






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$m + a{=}a\qquad\mbox{cnf}(\mbox{add\_equals\_a}_3,\mbox{negated\_conjecture})$

$\neg\,m{=}0\qquad\mbox{cnf}(\mbox{m\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD033-1.p} The multiplicative identity is unique






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$m\cdot a{=}a\qquad\mbox{cnf}(\mbox{multiply\_equals\_a}_4,\mbox{negated\_conjecture})$

$\neg\,m{=}1\qquad\mbox{cnf}(\mbox{m\_not\_equal\_to\_multiplicative\_identity}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD090-3.p} A characterization of 1 with help of the order relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$m\cdot x{=}y \ \Rightarrow \ y \leq x\qquad\mbox{cnf}(\mbox{less\_or\_equal\_or\_not\_product}_2,\mbox{negated\_conjecture})$

$\neg\,0 + m{=}1\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD006-1.p} In the additive group it holds: inverse(identity)=identity






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\neg\,-0{=}0\qquad\mbox{cnf}(\mbox{additive\_inverse\_not\_equal\_to\_additive\_identity}_1,\mbox{negated\_conjecture})$

\medskip\textbf{FLD053-4.p} Fraction calculation, part 7






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(p)\qquad\mbox{cnf}(\mbox{p\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(q)\qquad\mbox{cnf}(\mbox{q\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{12},\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{13},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{product}_{14},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}t\qquad\mbox{cnf}(\mbox{product}_{15},\mbox{negated\_conjecture})$

$s + -t{=}u\qquad\mbox{cnf}(\mbox{sum}_{16},\mbox{negated\_conjecture})$

$a\cdot d{=}p\qquad\mbox{cnf}(\mbox{product}_{17},\mbox{negated\_conjecture})$

$b\cdot c{=}q\qquad\mbox{cnf}(\mbox{product}_{18},\mbox{negated\_conjecture})$

$p + -q{=}k\qquad\mbox{cnf}(\mbox{sum}_{19},\mbox{negated\_conjecture})$

$b\cdot d{=}l\qquad\mbox{cnf}(\mbox{product}_{20},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{not\_product}_{21},\mbox{negated\_conjecture})$

\medskip\textbf{FLD060-3.p} If b greater or equal b, then 2b greater or equal 2a






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a + a \leq b + b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD092-1.p} One-sided Elimination of a multiplicative inverse, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$a \leq -1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,-1 \leq a^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD071-1.p} One-sided multiplication of two order relations, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,0 \leq a\cdot b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD069-3.p} If b $>$ 0 and a $>$= 0, then a + b not 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$a + b{=}0\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD040-3.p} If a is not 0, then the multiplicative inverse of a is not 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$0 + 0{=}a^{-1}\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD097-1.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,1 + ( a + b ) \leq ( 1 + a )\cdot ( 1 + b )\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD002-3.p} Transformation multiplicative relation -$\to$ additive relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$1\cdot a{=}b\qquad\mbox{cnf}(\mbox{product}_3,\mbox{hypothesis})$

$\neg\,0 + a{=}b\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD052-1.p} Fraction calculation, part 6






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1} + c\cdot d^{-1}{=}( a\cdot d + b\cdot c )\cdot ( b\cdot d )^{-1}\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_multiply}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD018-3.p} If a is zero, the additive inverse of a is also zero






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$0 + a{=}0\qquad\mbox{cnf}(\mbox{sum}_2,\mbox{negated\_conjecture})$

$\neg\,0 + -a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD024-1.p} Side Change of a term in an equation, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0{=}b + -a\qquad\mbox{cnf}(\mbox{additive\_identity\_equals\_add}_3,\mbox{negated\_conjecture})$

$\neg\,a{=}b\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_b}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD089-3.p} Elimination of a multiplicative inverse in an order, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$a^{-1} \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD014-1.p} Compatibility of additive inverses with the equality, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a{=}b\qquad\mbox{cnf}(\mbox{a\_equals\_b}_3,\mbox{negated\_conjecture})$

$\neg\,-a{=}-b\qquad\mbox{cnf}(\mbox{additive\_inverse\_not\_equal\_to\_additive\_inverse}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD025-3.p} The resulting equation of a multiplication of two equations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$1\cdot a{=}b\qquad\mbox{cnf}(\mbox{product}_5,\mbox{negated\_conjecture})$

$1\cdot c{=}d\qquad\mbox{cnf}(\mbox{product}_6,\mbox{negated\_conjecture})$

$\neg\,d\cdot b{=}a\cdot c\qquad\mbox{cnf}(\mbox{not\_product}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD076-1.p} Two-sided multiplication in an order relation, part 3






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot c \leq b\cdot c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD099-2.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a \leq 1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a{=}1\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_multiplicative\_identity}_6,\mbox{negated\_conjecture})$

$1 + a{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_7,\mbox{negated\_conjecture})$

$1 + -a{=}v\qquad\mbox{cnf}(\mbox{add\_equals\_v}_8,\mbox{negated\_conjecture})$

$\neg\,u \leq v^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD059-2.p} If a greater or equal 0, then 2a greater or equal 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$a + a{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_4,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD016-3.p} Solutions of linear equations in the additive group are unique






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a + u{=}b\qquad\mbox{cnf}(\mbox{sum}_5,\mbox{negated\_conjecture})$

$a + v{=}b\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$\neg\,0 + u{=}v\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD023-3.p} Side Change of a term in an equation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 + a{=}b\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

$\neg\,b + -a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD075-1.p} Two-sided multiplication in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$c \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,b\cdot c \leq a\cdot c\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD055-3.p} Compatibility of order and equality relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$0 + b{=}c\qquad\mbox{cnf}(\mbox{sum}_5,\mbox{negated\_conjecture})$

$\neg\,a \leq c\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD089-1.p} Elimination of a multiplicative inverse in an order, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$a^{-1} \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD082-3.p} Compatibility of order and multiplicative inverses, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,b^{-1} \leq a^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD047-3.p} Fraction calculation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1}{=}( a\cdot c )\cdot ( b\cdot c )^{-1}\qquad\mbox{cnf}(\mbox{not\_product}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD025-2.p} The resulting equation of a multiplication of two equations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a{=}b\qquad\mbox{cnf}(\mbox{a\_equals\_b}_7,\mbox{negated\_conjecture})$

$c{=}d\qquad\mbox{cnf}(\mbox{c\_equals\_d}_8,\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_9,\mbox{negated\_conjecture})$

$d\cdot b{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_{10},\mbox{negated\_conjecture})$

$\neg\,v{=}u\qquad\mbox{cnf}(\mbox{v\_not\_equal\_to\_u}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD040-5.p} If a is not 0, then the multiplicative inverse of a is not 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$0 + a^{-1}{=}0\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD026-3.p} Compatibility of multiplicative inverses with equality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$1\cdot a{=}b\qquad\mbox{cnf}(\mbox{product}_4,\mbox{negated\_conjecture})$

$\neg\,1\cdot a^{-1}{=}b^{-1}\qquad\mbox{cnf}(\mbox{not\_product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD070-4.p} One-sided addition of two order relations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a + b{=}c\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$\neg\,0 \leq c\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD010-3.p} In the multiplicative group inverse(identity)=identity






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\neg\,0 + 1{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_1,\mbox{negated\_conjecture})$

$\neg\,1\cdot 1^{-1}{=}1\qquad\mbox{cnf}(\mbox{not\_product}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD010-5.p} In the multiplicative group inverse(identity)=identity






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\neg\,0 + 1{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_1,\mbox{negated\_conjecture})$

$\neg\,0 + 1^{-1}{=}1\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD012-3.p} Compatibility of operation and inverse in multiplicative group






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$\neg\,1\cdot ( a\cdot b )^{-1}{=}a^{-1}\cdot b^{-1}\qquad\mbox{cnf}(\mbox{not\_product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD083-3.p} Compatibility of order and multiplicative inverses, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,b^{-1} \leq a^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD062-3.p} Compatibility of the order relation and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,-b \leq -a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD061-1.p} The resulting inequality of a summation of two inequalities






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$c \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,a + c \leq d + b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD053-1.p} Fraction calculation, part 7






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1} + -c\cdot d^{-1}{=}( a\cdot d + -b\cdot c )\cdot ( b\cdot d )^{-1}\qquad\mbox{cnf}(\mbox{add\_not\_equal\_to\_multiply}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD044-3.p} Compatibility of multiplication and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,( -a )\cdot b{=}-a\cdot b\qquad\mbox{cnf}(\mbox{not\_product}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD087-1.p} Elimination of a multiplicative inverse in an order, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$0 \leq a^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,0 \leq a\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD057-1.p} 0 is less than 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\neg\,0 \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_1,\mbox{negated\_conjecture})$

\medskip\textbf{FLD045-3.p} Compatibility of multiplication and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a\cdot b{=}( -a )\cdot ( -b )\qquad\mbox{cnf}(\mbox{not\_product}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD091-3.p} One-sided Elimination of a multiplicative inverse, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$1 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a^{-1} \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD014-3.p} Compatibility of additive inverses with the equality, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 + a{=}b\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + -a{=}-b\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD081-3.p} Two-sided multiplication of two order relations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$c \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$\neg\,a\cdot c \leq d\cdot b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD095-2.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_{10},\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_{11},\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{12},\mbox{negated\_conjecture})$

$0 \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{13},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_{14},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_{15},\mbox{negated\_conjecture})$

$a + c{=}s\qquad\mbox{cnf}(\mbox{add\_equals\_s}_{16},\mbox{negated\_conjecture})$

$b + d{=}t\qquad\mbox{cnf}(\mbox{add\_equals\_t}_{17},\mbox{negated\_conjecture})$

$s\cdot t^{-1}{=}w\qquad\mbox{cnf}(\mbox{multiply\_equals\_w}_{18},\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{19},\mbox{negated\_conjecture})$

$\neg\,u \leq w\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{20},\mbox{negated\_conjecture})$

\medskip\textbf{FLD098-3.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,1 + -( a + b ) \leq ( 1 + -a )\cdot ( 1 + -b )\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD076-2.p} Two-sided multiplication in an order relation, part 3






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_6,\mbox{negated\_conjecture})$

$b\cdot c{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_7,\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_9,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{10},\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD027-1.p} Elimination of multiplicative inverses in an equation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$a^{-1}{=}b^{-1}\qquad\mbox{cnf}(\mbox{multiplicative\_inverses\_equal},\mbox{negated\_conjecture})$

$\neg\,a{=}b\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_b}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD054-2.p} Fraction calculation, part 8






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_7,\mbox{negated\_conjecture})$

$a^{-1} + b^{-1}{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_8,\mbox{negated\_conjecture})$

$a + b{=}k\qquad\mbox{cnf}(\mbox{add\_equals\_k}_9,\mbox{negated\_conjecture})$

$a\cdot b{=}l\qquad\mbox{cnf}(\mbox{multiply\_equals\_l}_{10},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_u}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD068-4.p} Side change of a term in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$b + -a{=}u\qquad\mbox{cnf}(\mbox{sum}_4,\mbox{negated\_conjecture})$

$0 \leq u\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD041-3.p} If a,b are not 0, the the product of a and b is not 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$a\cdot b{=}0\qquad\mbox{cnf}(\mbox{product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD074-3.p} Two-sided multiplication in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a\cdot c \leq b\cdot c\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD067-2.p} Side change in an order relation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$b + -a{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_5,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD088-3.p} Compatibility of order and multiplicative inverses, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a^{-1} \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD045-4.p} Compatibility of multiplication and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$( -a )\cdot ( -b ){=}u\qquad\mbox{cnf}(\mbox{product}_4,\mbox{negated\_conjecture})$

$\neg\,a\cdot b{=}u\qquad\mbox{cnf}(\mbox{not\_product}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD058-3.p} If a greater 0 and b greater or equal a the b greater 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$0 + b{=}0\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD043-1.p} The multiplication with 0 yields 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0\cdot a{=}0\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD016-1.p} Solutions of linear equations in the additive group are unique






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a + u{=}b\qquad\mbox{cnf}(\mbox{add\_equals\_b}_5,\mbox{negated\_conjecture})$

$a + v{=}b\qquad\mbox{cnf}(\mbox{add\_equals\_b}_6,\mbox{negated\_conjecture})$

$\neg\,u{=}v\qquad\mbox{cnf}(\mbox{u\_not\_equal\_to\_v}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD078-1.p} Side change in an order relation, multiplicative part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1} \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD009-1.p} Linear equations in the multiplicative group have a solution






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,a\cdot x{=}b\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_b}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD088-1.p} Compatibility of order and multiplicative inverses, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a^{-1} \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD081-2.p} Two-sided multiplication of two order relations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$c \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{10},\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_{11},\mbox{negated\_conjecture})$

$d\cdot b{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_{12},\mbox{negated\_conjecture})$

$\neg\,u \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{13},\mbox{negated\_conjecture})$

\medskip\textbf{FLD019-1.p} If the additive inverse of a is zero, a itself is zero






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$-a{=}0\qquad\mbox{cnf}(\mbox{additive\_inverse\_equals\_additive\_identity}_2,\mbox{negated\_conjecture})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD084-3.p} Elimination of multiplicative inverses in an order, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$b^{-1} \leq a^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$0 \leq b^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD072-3.p} One-sided multiplication of two order relations, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,a\cdot b \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD100-2.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$1 + a{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_{10},\mbox{negated\_conjecture})$

$1 + b{=}v\qquad\mbox{cnf}(\mbox{add\_equals\_v}_{11},\mbox{negated\_conjecture})$

$u\cdot v{=}w\qquad\mbox{cnf}(\mbox{multiply\_equals\_w}_{12},\mbox{negated\_conjecture})$

$a + b{=}s\qquad\mbox{cnf}(\mbox{add\_equals\_s}_{13},\mbox{negated\_conjecture})$

$1 + s{=}t\qquad\mbox{cnf}(\mbox{add\_equals\_t}_{14},\mbox{negated\_conjecture})$

$\neg\,t \leq w\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{FLD013-5.p} The resulting equation of the summation of two equations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$0 + a{=}b\qquad\mbox{cnf}(\mbox{sum}_7,\mbox{negated\_conjecture})$

$0 + c{=}d\qquad\mbox{cnf}(\mbox{sum}_8,\mbox{negated\_conjecture})$

$a + c{=}u\qquad\mbox{cnf}(\mbox{sum}_9,\mbox{negated\_conjecture})$

$d + b{=}v\qquad\mbox{cnf}(\mbox{sum}_{10},\mbox{negated\_conjecture})$

$\neg\,0 + u{=}v\qquad\mbox{cnf}(\mbox{not\_sum}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD071-3.p} One-sided multiplication of two order relations, part 1






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,0 \leq a\cdot b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD075-4.p} Two-sided multiplication in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$c \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$a\cdot c{=}u\qquad\mbox{cnf}(\mbox{product}_8,\mbox{negated\_conjecture})$

$b\cdot c{=}v\qquad\mbox{cnf}(\mbox{product}_9,\mbox{negated\_conjecture})$

$\neg\,v \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{10},\mbox{negated\_conjecture})$

\medskip\textbf{FLD045-1.p} Compatibility of multiplication and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,( -a )\cdot ( -b ){=}a\cdot b\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_multiply}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD083-1.p} Compatibility of order and multiplicative inverses, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,b^{-1} \leq a^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD099-1.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$a \leq 1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a{=}1\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_multiplicative\_identity}_4,\mbox{negated\_conjecture})$

$\neg\,1 + a \leq ( 1 + -a )^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD098-2.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$1 + -a{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_{10},\mbox{negated\_conjecture})$

$1 + -b{=}v\qquad\mbox{cnf}(\mbox{add\_equals\_v}_{11},\mbox{negated\_conjecture})$

$u\cdot v{=}w\qquad\mbox{cnf}(\mbox{multiply\_equals\_w}_{12},\mbox{negated\_conjecture})$

$a + b{=}s\qquad\mbox{cnf}(\mbox{add\_equals\_s}_{13},\mbox{negated\_conjecture})$

$1 + -s{=}t\qquad\mbox{cnf}(\mbox{add\_equals\_t}_{14},\mbox{negated\_conjecture})$

$\neg\,t \leq w\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{FLD031-1.p} If a is one, then the multiplicative inverse of a is also one






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$a{=}1\qquad\mbox{cnf}(\mbox{a\_equals\_multiplicative\_identity}_2,\mbox{negated\_conjecture})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,a^{-1}{=}1\qquad\mbox{cnf}(\mbox{multiplicative\_inverses\_not\_equal},\mbox{negated\_conjecture})$

\medskip\textbf{FLD061-3.p} The resulting inequality of a summation of two inequalities






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$c \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,a + c \leq d + b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD100-1.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,1 + ( a + b ) \leq ( 1 + a )\cdot ( 1 + b )\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD007-1.p} The additive inverse fulfills the involution property






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,-( -a ){=}a\qquad\mbox{cnf}(\mbox{additive\_inverse\_not\_equal\_to\_a}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD046-3.p} Compatibility of the additive and the multiplicative inverse






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + a{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_2,\mbox{negated\_conjecture})$

$\neg\,0 + ( -a )^{-1}{=}-a^{-1}\qquad\mbox{cnf}(\mbox{not\_sum}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD043-5.p} The multiplication with 0 yields 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,0\cdot a{=}0\qquad\mbox{cnf}(\mbox{not\_product}_2,\mbox{negated\_conjecture})$

\medskip\textbf{FLD017-3.p} Substitution of an element in additive equations






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(x)\qquad\mbox{cnf}(\mbox{x\_is\_defined},\mbox{hypothesis})$

$0 + a{=}x\qquad\mbox{cnf}(\mbox{sum}_5,\mbox{negated\_conjecture})$

$a + b{=}c\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$\neg\,x + b{=}c\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD095-1.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$0 \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1} \leq c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1} \leq ( a + c )\cdot ( b + d )^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{10},\mbox{negated\_conjecture})$

\medskip\textbf{FLD075-3.p} Two-sided multiplication in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$c \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,b\cdot c \leq a\cdot c\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD015-3.p} Compatibility of additive inverses with the equality, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 + -a{=}-b\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}b\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD096-1.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$0 \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1} \leq c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$\neg\,( a + c )\cdot ( b + d )^{-1} \leq c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{10},\mbox{negated\_conjecture})$

\medskip\textbf{FLD097-4.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$1 + a{=}u\qquad\mbox{cnf}(\mbox{sum}_{10},\mbox{negated\_conjecture})$

$1 + b{=}v\qquad\mbox{cnf}(\mbox{sum}_{11},\mbox{negated\_conjecture})$

$u\cdot v{=}w\qquad\mbox{cnf}(\mbox{product}_{12},\mbox{negated\_conjecture})$

$a + b{=}s\qquad\mbox{cnf}(\mbox{sum}_{13},\mbox{negated\_conjecture})$

$1 + s{=}t\qquad\mbox{cnf}(\mbox{sum}_{14},\mbox{negated\_conjecture})$

$\neg\,t \leq w\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{FLD038-1.p} Side change of a term in an equation by multiplication, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$1{=}b\cdot a^{-1}\qquad\mbox{cnf}(\mbox{multiplicative\_identity\_equals\_multiply}_4,\mbox{negated\_conjecture})$

$\neg\,a{=}b\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_b}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD048-2.p} Fraction calculation, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_{10},\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_{11},\mbox{negated\_conjecture})$

$s\cdot t{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_{12},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{multiply\_equals\_s}_{13},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}t\qquad\mbox{cnf}(\mbox{multiply\_equals\_t}_{14},\mbox{negated\_conjecture})$

$a\cdot c{=}k\qquad\mbox{cnf}(\mbox{multiply\_equals\_k}_{15},\mbox{negated\_conjecture})$

$b\cdot d{=}l\qquad\mbox{cnf}(\mbox{multiply\_equals\_l}_{16},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_u}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{FLD080-2.p} The square of an element is always greater or equal 0






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a\cdot a{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_3,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD004-1.p} Elimination of an multiplicative term/inverse term - pair






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,a\cdot ( b\cdot b^{-1} ){=}a\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_a}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD044-1.p} Compatibility of multiplication and additive inverses






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,( -a )\cdot b{=}-a\cdot b\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_additive\_inverse}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD061-2.p} The resulting inequality of a summation of two inequalities






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a + c{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_7,\mbox{negated\_conjecture})$

$d + b{=}v\qquad\mbox{cnf}(\mbox{add\_equals\_v}_8,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$c \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{10},\mbox{negated\_conjecture})$

$\neg\,u \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD051-1.p} Fraction calculation, part 5






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_5,\mbox{negated\_conjecture})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_6,\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_7,\mbox{negated\_conjecture})$

$\neg\,( a\cdot b^{-1} )\cdot ( c\cdot d^{-1} )^{-1}{=}( a\cdot d )\cdot ( b\cdot c )^{-1}\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_multiply}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD061-4.p} The resulting inequality of a summation of two inequalities






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$c \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$a + c{=}u\qquad\mbox{cnf}(\mbox{sum}_9,\mbox{negated\_conjecture})$

$d + b{=}v\qquad\mbox{cnf}(\mbox{sum}_{10},\mbox{negated\_conjecture})$

$\neg\,u \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{11},\mbox{negated\_conjecture})$

\medskip\textbf{FLD034-1.p} Every element equal one is a multiplicative identity






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$m{=}1\qquad\mbox{cnf}(\mbox{m\_equals\_multiplicative\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,m\cdot a{=}a\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_a}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD048-4.p} Fraction calculation, part 2






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(k)\qquad\mbox{cnf}(\mbox{k\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(l)\qquad\mbox{cnf}(\mbox{l\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{10},\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_{11},\mbox{negated\_conjecture})$

$s\cdot t{=}u\qquad\mbox{cnf}(\mbox{product}_{12},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}s\qquad\mbox{cnf}(\mbox{product}_{13},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}t\qquad\mbox{cnf}(\mbox{product}_{14},\mbox{negated\_conjecture})$

$a\cdot c{=}k\qquad\mbox{cnf}(\mbox{product}_{15},\mbox{negated\_conjecture})$

$b\cdot d{=}l\qquad\mbox{cnf}(\mbox{product}_{16},\mbox{negated\_conjecture})$

$\neg\,k\cdot l^{-1}{=}u\qquad\mbox{cnf}(\mbox{not\_product}_{17},\mbox{negated\_conjecture})$

\medskip\textbf{FLD081-1.p} Two-sided multiplication of two order relations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$0 \leq c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$c \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$\neg\,a\cdot c \leq d\cdot b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD073-2.p} One-sided multiplication of two order relations, part 3






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot b{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_6,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD097-2.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$1 + a{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_{10},\mbox{negated\_conjecture})$

$1 + b{=}v\qquad\mbox{cnf}(\mbox{add\_equals\_v}_{11},\mbox{negated\_conjecture})$

$u\cdot v{=}w\qquad\mbox{cnf}(\mbox{multiply\_equals\_w}_{12},\mbox{negated\_conjecture})$

$a + b{=}s\qquad\mbox{cnf}(\mbox{add\_equals\_s}_{13},\mbox{negated\_conjecture})$

$1 + s{=}t\qquad\mbox{cnf}(\mbox{add\_equals\_t}_{14},\mbox{negated\_conjecture})$

$\neg\,t \leq w\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{15},\mbox{negated\_conjecture})$

\medskip\textbf{FLD099-4.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$a \leq 1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}1\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$1 + a{=}u\qquad\mbox{cnf}(\mbox{sum}_7,\mbox{negated\_conjecture})$

$1 + -a{=}v\qquad\mbox{cnf}(\mbox{sum}_8,\mbox{negated\_conjecture})$

$\neg\,u \leq v^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_9,\mbox{negated\_conjecture})$

\medskip\textbf{FLD098-1.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,1 + -( a + b ) \leq ( 1 + -a )\cdot ( 1 + -b )\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD096-2.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(v)\qquad\mbox{cnf}(\mbox{v\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(w)\qquad\mbox{cnf}(\mbox{w\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_{10},\mbox{negated\_conjecture})$

$\neg\,d{=}0\qquad\mbox{cnf}(\mbox{d\_not\_equal\_to\_additive\_identity}_{11},\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{12},\mbox{negated\_conjecture})$

$0 \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{13},\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_{14},\mbox{negated\_conjecture})$

$c\cdot d^{-1}{=}v\qquad\mbox{cnf}(\mbox{multiply\_equals\_v}_{15},\mbox{negated\_conjecture})$

$a + c{=}s\qquad\mbox{cnf}(\mbox{add\_equals\_s}_{16},\mbox{negated\_conjecture})$

$b + d{=}t\qquad\mbox{cnf}(\mbox{add\_equals\_t}_{17},\mbox{negated\_conjecture})$

$s\cdot t^{-1}{=}w\qquad\mbox{cnf}(\mbox{multiply\_equals\_w}_{18},\mbox{negated\_conjecture})$

$u \leq v\qquad\mbox{cnf}(\mbox{less\_or\_equal}_{19},\mbox{negated\_conjecture})$

$\neg\,w \leq v\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{20},\mbox{negated\_conjecture})$

\medskip\textbf{FLD095-3.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$0 \leq d\qquad\mbox{cnf}(\mbox{less\_or\_equal}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1} \leq c\cdot d^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_9,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1} \leq ( a + c )\cdot ( b + d )^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_{10},\mbox{negated\_conjecture})$

\medskip\textbf{FLD101-1.p} Ordered field axioms (axiom formulation glxx)






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

\medskip\textbf{FLD099-3.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_2,\mbox{negated\_conjecture})$

$a \leq 1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,0 + a{=}1\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

$\neg\,1 + a \leq ( 1 + -a )^{-1}\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD018-1.p} If a is zero, the additive inverse of a is also zero






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$a{=}0\qquad\mbox{cnf}(\mbox{a\_equals\_additive\_identity}_2,\mbox{negated\_conjecture})$

$\neg\,-a{=}0\qquad\mbox{cnf}(\mbox{additive\_inverse\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

\medskip\textbf{FLD066-1.p} Elimination of a summation in an order relation






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a + c \leq b + c\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD051-3.p} Fraction calculation, part 5






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + c{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

$\neg\,( a\cdot b^{-1} )\cdot ( c\cdot d^{-1} )^{-1}{=}( a\cdot d )\cdot ( b\cdot c )^{-1}\qquad\mbox{cnf}(\mbox{not\_product}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD068-2.p} Side change of a term in an order relation, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$b + -a{=}u\qquad\mbox{cnf}(\mbox{add\_equals\_u}_4,\mbox{negated\_conjecture})$

$0 \leq u\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_6,\mbox{negated\_conjecture})$

\medskip\textbf{FLD053-3.p} Fraction calculation, part 7






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_5,\mbox{negated\_conjecture})$

$\neg\,0 + d{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_6,\mbox{negated\_conjecture})$

$\neg\,a\cdot b^{-1} + -c\cdot d^{-1}{=}( a\cdot d + -b\cdot c )\cdot ( b\cdot d )^{-1}\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD091-1.p} One-sided Elimination of a multiplicative inverse, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_2,\mbox{negated\_conjecture})$

$1 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$\neg\,a^{-1} \leq 1\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD043-3.p} The multiplication with 0 yields 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0\cdot a{=}b\qquad\mbox{cnf}(\mbox{product}_3,\mbox{negated\_conjecture})$

$\neg\,0 + b{=}0\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD079-2.p} Side change in an order relation, multiplicative part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_6,\mbox{negated\_conjecture})$

$u \leq 1\qquad\mbox{cnf}(\mbox{less\_or\_equal}_7,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_8,\mbox{negated\_conjecture})$

\medskip\textbf{FLD072-1.p} One-sided multiplication of two order relations, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,a\cdot b \leq 0\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD001-3.p} Transformation additive relation -$\to$ multiplicative relation






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$0 + a{=}b\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{hypothesis})$

$\neg\,1\cdot a{=}b\qquad\mbox{cnf}(\mbox{not\_product}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD080-4.p} The square of an element is always greater or equal 0






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$a\cdot a{=}u\qquad\mbox{cnf}(\mbox{product}_3,\mbox{negated\_conjecture})$

$\neg\,0 \leq u\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD085-1.p} Elimination of multiplicative inverses in an order, part 2






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\neg\,a{=}0\qquad\mbox{cnf}(\mbox{a\_not\_equal\_to\_additive\_identity}_3,\mbox{negated\_conjecture})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_4,\mbox{negated\_conjecture})$

$b^{-1} \leq a^{-1}\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$a^{-1} \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,a \leq b\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD070-2.p} One-sided addition of two order relations






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$a + b{=}c\qquad\mbox{cnf}(\mbox{add\_equals\_c}_4,\mbox{negated\_conjecture})$

$0 \leq a\qquad\mbox{cnf}(\mbox{less\_or\_equal}_5,\mbox{negated\_conjecture})$

$0 \leq b\qquad\mbox{cnf}(\mbox{less\_or\_equal}_6,\mbox{negated\_conjecture})$

$\neg\,0 \leq c\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_7,\mbox{negated\_conjecture})$

\medskip\textbf{FLD021-3.p} Every element equal to zero is an additive identity






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(m)\qquad\mbox{cnf}(\mbox{m\_is\_defined},\mbox{hypothesis})$

$0 + m{=}0\qquad\mbox{cnf}(\mbox{sum}_3,\mbox{negated\_conjecture})$

$\neg\,m + a{=}a\qquad\mbox{cnf}(\mbox{not\_sum}_4,\mbox{negated\_conjecture})$

\medskip\textbf{FLD047-2.p} Fraction calculation, part 1






$\mbox{include}(\mbox{'Axioms/FLD001-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(u)\qquad\mbox{cnf}(\mbox{u\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(s)\qquad\mbox{cnf}(\mbox{s\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(t)\qquad\mbox{cnf}(\mbox{t\_is\_defined},\mbox{hypothesis})$

$\neg\,b{=}0\qquad\mbox{cnf}(\mbox{b\_not\_equal\_to\_additive\_identity}_7,\mbox{negated\_conjecture})$

$\neg\,c{=}0\qquad\mbox{cnf}(\mbox{c\_not\_equal\_to\_additive\_identity}_8,\mbox{negated\_conjecture})$

$a\cdot b^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_equals\_u}_9,\mbox{negated\_conjecture})$

$a\cdot c{=}s\qquad\mbox{cnf}(\mbox{multiply\_equals\_s}_{10},\mbox{negated\_conjecture})$

$b\cdot c{=}t\qquad\mbox{cnf}(\mbox{multiply\_equals\_t}_{11},\mbox{negated\_conjecture})$

$\neg\,s\cdot t^{-1}{=}u\qquad\mbox{cnf}(\mbox{multiply\_not\_equal\_to\_u}_{12},\mbox{negated\_conjecture})$

\medskip\textbf{FLD100-3.p} Difficult inequality






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$a \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_3,\mbox{negated\_conjecture})$

$b \leq 0\qquad\mbox{cnf}(\mbox{less\_or\_equal}_4,\mbox{negated\_conjecture})$

$\neg\,1 + ( a + b ) \leq ( 1 + a )\cdot ( 1 + b )\qquad\mbox{cnf}(\mbox{not\_less\_or\_equal}_5,\mbox{negated\_conjecture})$

\medskip\textbf{FLD008-4.p} Compatibility of operation and inverse in the additive group






$\mbox{include}(\mbox{'Axioms/FLD002-0.ax'})$

$\mbox{defined}(a)\qquad\mbox{cnf}(\mbox{a\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(b)\qquad\mbox{cnf}(\mbox{b\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(c)\qquad\mbox{cnf}(\mbox{c\_is\_defined},\mbox{hypothesis})$

$\mbox{defined}(d)\qquad\mbox{cnf}(\mbox{d\_is\_defined},\mbox{hypothesis})$

$a + b{=}c\qquad\mbox{cnf}(\mbox{sum}_5,\mbox{negated\_conjecture})$

$-a + -b{=}d\qquad\mbox{cnf}(\mbox{sum}_6,\mbox{negated\_conjecture})$

$\neg\,0 + -c{=}d\qquad\mbox{cnf}(\mbox{not\_sum}_7,\mbox{negated\_conjecture})$

\medskip
\end{document}