TreeView Knowledge Base Browser - NegativeRealNumber

appearance as argument number 1

(documentation NegativeRealNumber ChineseLanguage "这是一个小于零的 RealNumber。")	chinese_format.kif 1747-1747
(documentation NegativeRealNumber EnglishLanguage "A RealNumber that is less than zero.")	Merge.kif 1853-1854
(externalImage NegativeRealNumber "http://upload.wikimedia.org/wikipedia/ commons/ 0/ 09/ Number-line.gif")	pictureList.kif 10166-10166
(subclass NegativeRealNumber RealNumber)	Merge.kif 1851-1851	Negative real number is a subclass of real number

appearance as argument number 2

(partition RealNumber NegativeRealNumber NonnegativeRealNumber)	Merge.kif 1800-1800	Real number is exhaustively partitioned into negative real number and nonnegative real number
(subclass NegativeInteger NegativeRealNumber)	Merge.kif 1894-1894	Negative integer is a subclass of negative real number
(termFormat ChineseLanguage NegativeRealNumber "负实数")	chinese_format.kif 865-865
(termFormat EnglishLanguage NegativeRealNumber "negative real number")	english_format.kif 937-937

antecedent

(<=> (instance ?NUMBER NegativeRealNumber) (and (lessThan ?NUMBER 0) (instance ?NUMBER RealNumber)))	Merge.kif 1856-1860	A quantity is an instance of negative real number if and only if the quantity is less than 0 and the quantity is an instance of real number
(=> (instance ?NUMBER NegativeRealNumber) (equal (SignumFn ?NUMBER) -1))	Merge.kif 4923-4925	If a real number is an instance of negative real number, then the sign of the real number is equal to -1

consequent

(<=>
    (and
        (equal
            (AbsoluteValueFn ?NUMBER1) ?NUMBER2)
        (instance ?NUMBER1 RealNumber)
        (instance ?NUMBER2 RealNumber))
    (or
        (and
            (instance ?NUMBER1 NonnegativeRealNumber)
            (equal ?NUMBER1 ?NUMBER2))
        (and
            (instance ?NUMBER1 NegativeRealNumber)
            (equal ?NUMBER2
                (SubtractionFn 0 ?NUMBER1)))))

Merge.kif 4547-4558