metamath/valid/numbertheory-2dvd4expn.mm

${
  numbertheory-2dvd4expn.0 $e |- ( ph -> N e. NN ) $.
  $( (Contributed by Kunhao Zheng, 29-Mar-2021.) $)
  numbertheory-2dvd4expn $p |- ( ph -> 2 || ( 4 ^ N ) ) $=
( c2 c4 cdvds wbr cexp co cmul cz wcel dvdsmul2 mp2an 2t2e4 eqcomi breqtrri 2z 
wa cn adantr simpr wi 4z dvdspw mp3an12 sylc ex mpi ) ADEFGZDEBHIFGZDDDJ 
IZEFDKLZUMDULFGRRDDMNULEOPQAUJUKAUJSBTLZUJUKAUNUJCUAAUJUBUMEKLUNUJUKUCRUDDE 
BUEUFUGUHUI $. 
$}