metamath/valid/aimeI-2001-p3.mm

$(
  @{
    aimeI-2001-p3.0 @e |- ( ph -> X : NN --> ZZ ) $@
    aimeI-2001-p3.1 @e |- ( ph -> ( X ` 1 ) = ; ; 2 1 1 ) $@
    aimeI-2001-p3.2 @e |- ( ph -> ( X ` 2 ) = ; ; 3 7 5 ) $@
    aimeI-2001-p3.3 @e |- ( ph -> ( X ` 3 ) = ; ; 4 2 0 ) $@
    aimeI-2001-p3.4 @e |- ( ph -> ( X ` 4 ) = ; ; 5 2 3 ) $@
    aimeI-2001-p3.5 @e |- ( ph -> N e. NN ) $@
    aimeI-2001-p3.6 @e |- ( ph -> 5 <_ N ) $@
    aimeI-2001-p3.7 @e |- ( ph -> ( X ` N ) = ( ( ( ( X ` ( N - 1 ) ) - ( X ` ( N - 2 ) ) ) + ( X ` ( N - 3 ) ) ) - ( X ` ( N - 4 ) ) ) ) $@
    @( (Contributed by Kunhao Zheng, 12-Aug-2021.) @)
    aimeI-2001-p3 @p |- ( ph -> ( ( ( X ` ; ; 5 3 1 ) + ( X ` ; ; 7 5 3 ) ) + ( X ` ; ; 9 7 5 ) ) = ; ; 8 9 8 ) @=
      ? @.
  @}
$)