metamath/valid/mathd-algebra-73.mm

$(
  @{
    mathd-algebra-73.0 @e |- ( ph -> P e. CC ) $@
    mathd-algebra-73.1 @e |- ( ph -> Q e. CC ) $@
    mathd-algebra-73.2 @e |- ( ph -> R e. CC ) $@
    mathd-algebra-73.3 @e |- ( ph -> X e. CC ) $@
    mathd-algebra-73.4 @e |- ( ph -> ( ( X - P ) x. ( X - Q ) ) = ( ( R - P ) x. ( R - Q ) ) ) $@
    mathd-algebra-73.5 @e |- ( ph -> X =/= R ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-73 @p |- ( ph -> X = ( ( P + Q ) - R ) ) @=
      ? @.
  @}
$)