metamath/valid/induction-divisibility-9div10tonm1.mm

${
  $d N x $.
  $d ph x y $.
  induction-divisibility-9div10tonm1.0 $e |- ( ph -> N e. NN0 ) $.
  $( (Contributed by Stanislas Polu, 8-Oct-2020.) $)
  induction-divisibility-9div10tonm1 $p |- ( ph -> 9 || ( ( ; 1 0 ^ N ) - 1 ) ) 
$=
( wcel c9 c1 cc0 cexp co cmin cdvds wbr caddc wceq oveq2 oveq1d breq2d cmul a1i 
breqtrd vx vy cn0 id cv 9nn0 nn0zi dvds0 ax-mp 1m1e0 breqtrri 1nn0 0nn0 cdc cz 
deccl nn0cni exp0i oveq1i wa simpr simplr zexpcl sylancr dvdsmultr1d iddvds 
mpan 1zzd zsubcld adantl adantr zmulcld dvds2addd cc 9cn expcld 1cnd mulcld 
eqcomd mulid2d oveq2d adddird 9p1e10b expp1d mulcomd nn0indd syl2anc addsubassd 
eqtr4d ) AABUCDEFGUNZBHIZFJIZKLZAUDCAEWJUAUEZHIZFJIZKLEWJGHIZFJI 
ZKLZEWJUBUEZHIZFJIZKLZEWJWTFMIZHIZFJIZKLWMUAUBBWNGNZWPWREKXGWOWQFJWNGWJHOPQ 
WNWTNZWPXBEKXHWOXAFJWNWTWJHOPQWNXDNZWPXFEKXIWOXEFJWNXDWJHOPQWNBNZWPWLEKXJWO 
WKFJWNBWJHOPQWSAEFFJIZWRKEGXKKEUODZEGKLEUFUGZEUHUIUJUKWQFFJWJWJFGULUMUPZUQZ 
URUSUKSAWTUCDZUTZXCUTZEWJXARIZFJIZXFKXREEFMIZXARIZFJIZXTKXREEXARIZFXARIZMIZ 
FJIZYCKXREYDXAMIZFJIZYGKXREYDXBMIZYIKXREYDXBXLXRXMSZXQXCVAXREEXAYKYKXRWJUOD 
ZXPXAUODZWJXNUGZAXPXCVBWJWTVCZVDZEEKLZXRXLYQXMEVFUISVEXQXBUODZXCXPYRAXPXAFY 
LXPYMYNYOVGXPVHVIVJVKXREXAYKYPVLVMXRYIYJXRYDXAFXQYDVNDXCXQEXAEVNDZXQVOSXQWJ 
WTWJVNDZXQXOSZAXPVAZVPZVRVKXQXAVNDXCUUCVKZXRVQZWHVSTXRYHYFFJXRXAYEYDMXRYEXA 
XRXAUUDVTVSWAPTXRYFYBFJXRYBYFXREFXAYSXRVOSUUEUUDWBVSPTXRYBXSFJXRYAWJXARYAWJ 
NXRWCSPPTXRXSXEFJXRXEXSXRXEXAWJRIZXSXQXEUUFNXCXQWJWTUUAUUBWDVKXRWJXAYTXRXOS 
UUDWEWIVSPTWFWG $. 
$}