${
  $d U n $.
  $d V n $.
  $d k n $.
  $d k ph $.
  amc12a-2003-p1.0 $e |- ( ph -> U : NN --> NN ) $.
  amc12a-2003-p1.1 $e |- ( ph -> V : NN --> NN ) $.
  amc12a-2003-p1.2 $e |- ( ph -> A. n e. NN ( U ` n ) = ( 2 x. n ) ) $.
  amc12a-2003-p1.3 $e |- ( ph -> A. n e. NN ( V ` n ) = ( ( 2 x. n ) - 1 ) ) $.
  $( (Contributed by Kunhao Zheng, 22-Apr-2021.) $)
  amc12a-2003-p1 $p |- ( ph -> ( sum_ k e. ( 1 ... ; ; ; 2 0 0 3 ) ( U ` k ) - 
sum_ k e. ( 1 ... ; ; ; 2 0 0 3 ) ( V ` k ) ) = ; ; ; 2 0 0 3 ) $=
( c1 c2 cc0 co cfv cmin csu cmul wcel cn wceq cdc c3 cfz wral elfznn adantl cv 
wa adantr fveq2 oveq2 eqeq12d rspcv oveq1d mpan9 sylan2 oveq12d sumeq2dv sylc 
fzfid wf ffvelrnd nncnd fsumsub chash 2cnd mulcld 1cnd nncand cfn fzfi cc 
fsumconst sylancr cn0 2nn0 0nn0 deccl 3nn0 hashfz1 nn0cni mulid1i syl6eq mp1i 
3eqtrd 3eqtr3d ) AJKLUAZLUAZUBUAZUCMZCUGZBNZWKENZOMZCPWJKWKQMZWOJOMZOM 
ZCPZWJWLCPWJWMCPOMWIAWJWNWQCAWKWJRZUHZWLWOWMWPOWTWKSRZDUGZBNZKXBQMZTZDSUDZW 
LWOTZWSXAAWKWIUEZUFZAXFWSHUIXEXGDWKSXBWKTZXCWLXDWOXBWKBUJXBWKKQUKZULUMUSWSA 
XAWMWPTZXHAXBENZXDJOMZTZDSUDXAXLIXOXLDWKSXJXMWMXNWPXBWKEUJXJXDWOJOXKUNULUMU 
OUPUQURAWJWLWMCAJWIUTWTWLWTSSWKBASSBVAWSFUIXIVBVCWTWMWTSSWKEASSEVAWSGUIXIVB 
VCVDAWRWJJCPZWJVENZJQMZWIAWJWQJCWTWOJWTKWKWTVFWSWKVLRAWSWKXHVCUFVGWTVHVIURA 
WJVJRJVLRXPXRTJWIVKAVHWJJCVMVNAXRWIJQMWIAXQWIJQWIVORXQWITAWHUBWGLKLVPVQVRVQ 
VRVSVRZWIVTWDUNWIWIXSWAWBWCWEWF $.
$}