metamath/valid/imo-1966-p5.mm

$(
  @{
    imo-1966-p5.0 @e |- ( ph -> A : ( 1 ... 4 ) --> RR ) $@
    imo-1966-p5.1 @e |- ( ph -> X : ( 1 ... 4 ) --> RR ) $@
    imo-1966-p5.2 @e |- ( ph -> ( A ` 1 ) =/= ( A ` 2 ) ) $@
    imo-1966-p5.3 @e |- ( ph -> ( A ` 1 ) =/= ( A ` 3 ) ) $@
    imo-1966-p5.4 @e |- ( ph -> ( A ` 1 ) =/= ( A ` 4 ) ) $@
    imo-1966-p5.5 @e |- ( ph -> ( A ` 2 ) =/= ( A ` 3 ) ) $@
    imo-1966-p5.6 @e |- ( ph -> ( A ` 2 ) =/= ( A ` 4 ) ) $@
    imo-1966-p5.7 @e |- ( ph -> ( A ` 3 ) =/= ( A ` 4 ) ) $@
    imo-1966-p5.8 @e |- ( ph -> ( ( ( ( abs ` ( ( A ` 1 ) - ( A ` 2 ) ) ) x. ( X ` 2 ) ) + ( ( abs ` ( ( A ` 1 ) - ( A ` 3 ) ) ) x. ( X ` 3 ) ) ) + ( ( abs ` ( ( A ` 1 ) - ( A ` 4 ) ) ) x. ( X ` 4 ) ) ) = 1 ) $@
    imo-1966-p5.9 @e |- ( ph -> ( ( ( ( abs ` ( ( A ` 2 ) - ( A ` 1 ) ) ) x. ( X ` 1 ) ) + ( ( abs ` ( ( A ` 2 ) - ( A ` 3 ) ) ) x. ( X ` 3 ) ) ) + ( ( abs ` ( ( A ` 2 ) - ( A ` 4 ) ) ) x. ( X ` 4 ) ) ) = 1 ) $@
    imo-1966-p5.10 @e |- ( ph -> ( ( ( ( abs ` ( ( A ` 3 ) - ( A ` 1 ) ) ) x. ( X ` 1 ) ) + ( ( abs ` ( ( A ` 3 ) - ( A ` 2 ) ) ) x. ( X ` 2 ) ) ) + ( ( abs ` ( ( A ` 3 ) - ( A ` 4 ) ) ) x. ( X ` 4 ) ) ) = 1 ) $@
    imo-1966-p5.11 @e |- ( ph -> ( ( ( ( abs ` ( ( A ` 4 ) - ( A ` 1 ) ) ) x. ( X ` 1 ) ) + ( ( abs ` ( ( A ` 4 ) - ( A ` 2 ) ) ) x. ( X ` 2 ) ) ) + ( ( abs ` ( ( A ` 4 ) - ( A ` 3 ) ) ) x. ( X ` 3 ) ) ) = 1 ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    imo-1966-p5 @p |- ( ph -> ( ( ( X ` 2 ) = 0 /\ ( X ` 3 ) = 0 ) /\ ( ( X ` 1 ) = ( 1 / ( abs ` ( ( A ` 1 ) - ( A ` 4 ) ) ) ) /\ ( X ` 4 ) = ( 1 / ( abs ` ( ( A ` 1 ) - ( A ` 4 ) ) ) ) ) ) ) @=
      ? @.
  @}
$)