Non-NaN results for conventional IEEE directed arithmetic

Directed dyadic rounding may produce a finite value or an infinity, but never a NaN. Consequently, directed addition, subtraction, multiplication, and nonzero-denominator division preserve the non-NaN classification when both operands are finite. These facts are shared by the IEEE interval soundness proofs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_addDown_eq_false_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.addDown y).isNaN = false

Directed-down addition is non-NaN on finite operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_addUp_eq_false_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.addUp y).isNaN = false

Directed-up addition is non-NaN on finite operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_mulDown_eq_false_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.mulDown y).isNaN = false

Directed-down multiplication is non-NaN on finite operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_mulUp_eq_false_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.mulUp y).isNaN = false

Directed-up multiplication is non-NaN on finite operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_divDown_eq_false_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) : (x.divDown y).isNaN = false

Directed-down division is non-NaN on finite operands with a nonzero divisor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_divUp_eq_false_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) : (x.divUp y).isNaN = false

Directed-up division is non-NaN on finite operands with a nonzero divisor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_subDown_eq_false_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.subDown y).isNaN = false

Directed-down subtraction is non-NaN on finite operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isNaN_subUp_eq_false_of_isFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.subUp y).isNaN = false

Directed-up subtraction is non-NaN on finite operands.