This looks guaranteed by the standard, we can start with section [expr.static.cast]p4 which says:
An expression e can be explicitly converted to a type T if there is an implicit conversion sequence from e to T ...
implicit conversion sequence is covered in [over.best.ics] and we have the following:
A well-formed implicit conversion sequence is one of the following forms:
- (3.1) a standard conversion sequence,
...
and standard conversion sequence is covered in [over.ics.scs] which says:
[ Note: As described in [conv], a standard conversion sequence is either the Identity conversion by itself (that is, no conversion) or consists of one to three conversions from the other four categories.
If there are two or more conversions in the sequence, the conversions are applied in the canonical order: Lvalue Transformation, Promotion or Conversion, Qualification Adjustment.
— end note ]
and we have the floating point promotion case we have here covered in [conv.fpprom]p1 which says:
A prvalue of type float can be converted to a prvalue of type double.
The value is unchanged.
Going the other way double to float would be a conversion and that is covered in [conv#double]p1:
A prvalue of floating-point type can be converted to a prvalue of another floating-point type.
If the source value can be exactly represented in the destination type, the result of the conversion is that exact representation.
If the source value is between two adjacent destination values, the result of the conversion is an implementation-defined choice of either of those values. Otherwise, the behavior is undefined.
This case depends on whether the source can be exactly represented by the destination which is not guaranteed.
The subquestion on floating point divide by zero is complicated and covered in my answer to The behaviour of floating point division by zero.