metamath/valid/amc12a-2002-p12.mm

$(
  @{
    amc12a-2002-p12.0 @e |- ( ph -> F : RR --> RR ) $@
    amc12a-2002-p12.1 @e |- ( ph -> k e. RR ) $@
    amc12a-2002-p12.2 @e |- ( ph -> A. x e. RR ( F ` x ) = ( ( ( x ^ 2 ) - ( ; 6 3 x. x ) ) + k ) ) $@
    amc12a-2002-p12.3 @e |- ( ph -> ( `' F " { 0 } ) C_ Prime ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    amc12a-2002-p12 @p |- ( ph -> k = ; ; 1 2 2 ) @=
      ? @.
  @}
$)