metamath/valid/mathd-algebra-437.mm

$(
  @{
    mathd-algebra-437.0 @e |- ( ph -> N e. ZZ ) $@
    mathd-algebra-437.1 @e |- ( ph -> X e. RR ) $@
    mathd-algebra-437.2 @e |- ( ph -> Y e. RR ) $@
    mathd-algebra-437.3 @e |- ( ph -> ( X ^ 3 ) = -u ; 4 5 ) $@
    mathd-algebra-437.4 @e |- ( ph -> ( Y ^ 3 ) = -u ; ; 1 0 1 ) $@
    mathd-algebra-437.5 @e |- ( ph -> X < N ) $@
    mathd-algebra-437.6 @e |- ( ph -> N < Y ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    mathd-algebra-437 @p |- ( ph -> N = -u 4 ) @=
      ? @.
  @}
$)