metamath/valid/mathd-algebra-181.mm

$(
  @{
    mathd-algebra-181.0 @e |- ( ph -> N e. RR ) $@
    mathd-algebra-181.1 @e |- ( ph -> N =/= 3 ) $@
    mathd-algebra-181.2 @e |- ( ph -> ( ( N + 5 ) / ( N - 3 ) ) = 2 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-181 @p |- ( ph -> N = ; 1 1 ) @=
      ? @.
  @}
$)