let a be Nat; :: thesis: ( 10 divides (a |^ 10) + 1 iff ex k being Nat st
( a = (10 * k) + 3 or a = (10 * k) + 7 ) )
thus ( 10 divides (a |^ 10) + 1 implies ex k being Nat st
( a = (10 * k) + 3 or a = (10 * k) + 7 ) ) :: thesis: ( ex k being Nat st
( a = (10 * k) + 3 or a = (10 * k) + 7 ) implies 10 divides (a |^ 10) + 1 )

proof

assume 10 divides (a |^ 10) + 1 ; :: thesis: ex k being Nat st
( a = (10 * k) + 3 or a = (10 * k) + 7 )
then consider r, k being Nat such that
A1: a = (10 * k) + r and
A2: 10 divides (r |^ 10) + 1 and
A3: not not r = 0 & ... & not r = 9 by Th30;
take k ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

per cases ( r = 0 or r = 1 or r = 2 or r = 3 or r = 4 or r = 5 or r = 6 or r = 7 or r = 8 or r = 9 ) by A3;

suppose r = 0 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A2, INT_2:27; :: thesis: verum

end;

suppose r = 1 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A2, INT_2:27; :: thesis: verum

end;

suppose r = 2 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A2, Lm25; :: thesis: verum

end;

suppose r = 3 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A1; :: thesis: verum

end;

suppose r = 4 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A2, Lm26, Th5; :: thesis: verum

end;

suppose r = 5 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A2, Lm27, Th6; :: thesis: verum

end;

suppose r = 6 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A2, Lm28, Th7; :: thesis: verum

end;

suppose r = 7 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A1; :: thesis: verum

end;

suppose r = 8 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A2, Lm29, Th9; :: thesis: verum

end;

suppose r = 9 ; :: thesis: ( a = (10 * k) + 3 or a = (10 * k) + 7 )

hence ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A2, Lm30, Th10; :: thesis: verum

end;

end;

end;

given k being Nat such that A4: ( a = (10 * k) + 3 or a = (10 * k) + 7 ) ; :: thesis: 10 divides (a |^ 10) + 1

per cases ( a = (10 * k) + 3 or a = (10 * k) + 7 ) by A4;

suppose A5: a = (10 * k) + 3 ; :: thesis: 10 divides (a |^ 10) + 1

not not 3 = 0 & ... & not 3 = 9 ;
hence 10 divides (a |^ 10) + 1 by A5, Th4, INT_1:def 3, Th30; :: thesis: verum

end;

suppose A6: a = (10 * k) + 7 ; :: thesis: 10 divides (a |^ 10) + 1

not not 7 = 0 & ... & not 7 = 9 ;
hence 10 divides (a |^ 10) + 1 by A6, Th8, INT_1:def 3, Th30; :: thesis: verum

end;

end;