theorem Th30: :: NUMBER03:30

for a being Nat holds
( 10 divides (a |^ 10) + 1 iff ex r, k being Nat st
( a = (10 * k) + r & 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 ) )