metamath/valid/amc12a-2010-p10.mm

$(
  @{
    amc12a-2010-p10.0 @e |- ( ph -> A : NN --> RR ) $@
    amc12a-2010-p10.1 @e |- ( ph -> P e. RR ) $@
    amc12a-2010-p10.2 @e |- ( ph -> Q e. RR ) $@
    amc12a-2010-p10.3 @e |- ( ( ph /\ n e. NN ) -> ( ( A ` ( n + 2 ) ) - ( A ` ( n + 1 ) ) ) = ( ( A ` ( n + 1 ) ) - ( A ` n ) ) ) $@
    amc12a-2010-p10.4 @e |- ( ph -> ( A ` 1 ) = P ) $@
    amc12a-2010-p10.5 @e |- ( ph -> ( A ` 2 ) = 9 ) $@
    amc12a-2010-p10.6 @e |- ( ph -> ( A ` 3 ) = ( ( 3 x. P ) - Q ) ) $@
    amc12a-2010-p10.7 @e |- ( ph -> ( A ` 4 ) = ( ( 3 x. P ) + Q ) ) $@
    @( (Contributed by Kunhao Zheng, 9-Aug-2021.) @)
    amc12a-2010-p10 @p |- ( ph -> ( A ` ; ; ; 2 0 1 0 ) = ; ; ; 8 0 4 1 ) @=
      ? @.
  @}
$)