metamath/valid/mathd-algebra-482.mm

$(
  @{
    mathd-algebra-482.0 @e |- ( ph -> K e. RR ) $@
    mathd-algebra-482.1 @e |- ( ph -> M e. Prime ) $@
    mathd-algebra-482.2 @e |- ( ph -> N e. Prime ) $@
    mathd-algebra-482.3 @e |- F = ( x e. RR |-> ( ( ( x ^ 2 ) - ( ; 1 2 x. x ) ) + K ) ) $@
    mathd-algebra-482.4 @e |- ( ph -> ( F ` M ) = 0 ) $@
    mathd-algebra-482.5 @e |- ( ph -> ( F ` N ) = 0 ) $@
    mathd-algebra-482.6 @e |- ( ph -> M =/= N ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    mathd-algebra-482 @p |- ( ph -> K = ; 3 5 ) @=
      ? @.
  @}
$)