metamath/valid/mathd-algebra-144.mm

$(
  @{
    mathd-algebra-144.0 @e |- ( ph -> A e. NN ) $@
    mathd-algebra-144.1 @e |- ( ph -> B e. NN ) $@
    mathd-algebra-144.2 @e |- ( ph -> C e. NN ) $@
    mathd-algebra-144.3 @e |- ( ph -> D e. NN ) $@
    mathd-algebra-144.4 @e |- ( ph -> ( C - B ) = D ) $@
    mathd-algebra-144.5 @e |- ( ph -> ( B - A ) = D ) $@
    mathd-algebra-144.6 @e |- ( ph -> ( ( A + B ) + C ) = ; 6 0 ) $@
    mathd-algebra-144.7 @e |- ( ph -> ( A + B ) > C ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-144 @p |- ( ph -> D < ; 1 0 ) @=
      ? @.
  @}
$)