let n be Nat; :: thesis: card { k where k is Nat : k divides 5 |^ n } = n + 1
deffunc H₁( Nat) -> set = 5 |^ $1;
A1: H₁( 0 ) = 1 by NEWTON:4;
deffunc H₂( Nat) -> set = { m where m is Nat : m divides H₁($1) } ;
defpred S₁[ Nat] means card H₂($1) = $1 + 1;
A2: S₁[ 0 ]

proof

H₂( 0 ) = {1}

proof

thus H₂( 0 ) c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= H₂( 0 )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₂( 0 ) or x in {1} )
assume x in H₂( 0 ) ; :: thesis: x in {1}
then consider m being Nat such that
A3: x = m and
A4: m divides H₁( 0 ) ;
A5: m mod 4 = 1 by A4, Th34;
0 mod 4 = 0 ;
then m = 1 by A1, A5, A4, NAT_D:7, NAT_1:25;
hence x in {1} by A3, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in H₂( 0 ) )
assume x in {1} ; :: thesis: x in H₂( 0 )
then x = 1 by TARSKI:def 1;
hence x in H₂( 0 ) by A1; :: thesis: verum

end;

hence S₁[ 0 ] by CARD_1:30; :: thesis: verum

end;

A6: for a being Nat st S₁[a] holds
S₁[a + 1]

proof

let a be Nat; :: thesis: ( S₁[a] implies S₁[a + 1] )
assume A7: S₁[a] ; :: thesis: S₁[a + 1]
set b = a + 1;
set K = H₁(a + 1);
reconsider An = H₂(a) as finite set by Lm9;

A8: now :: thesis: not H₁(a + 1) in An

assume H₁(a + 1) in An ; :: thesis: contradiction
then A9: ex m being Nat st
( H₁(a + 1) = m & m divides H₁(a) ) ;
a < a + 1 by NAT_1:16;
hence contradiction by A9, NAT_D:7, PEPIN:66; :: thesis: verum

end;

H₂(a + 1) = H₂(a) \/ {H₁(a + 1)}

proof

thus H₂(a + 1) c= H₂(a) \/ {H₁(a + 1)} :: according to XBOOLE_0:def 10 :: thesis: H₂(a) \/ {H₁(a + 1)} c= H₂(a + 1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₂(a + 1) or x in H₂(a) \/ {H₁(a + 1)} )
assume x in H₂(a + 1) ; :: thesis: x in H₂(a) \/ {H₁(a + 1)}
then consider m being Nat such that
A10: x = m and
A11: m divides H₁(a + 1) ;
consider t being Element of NAT such that
A12: m = H₁(t) and
A13: t <= a + 1 by A11, PEPIN:34, PEPIN:59;

per cases ( t <= a or t = a + 1 ) by A13, NAT_1:8;

suppose t <= a ; :: thesis: x in H₂(a) \/ {H₁(a + 1)}

then H₁(t) divides H₁(a) by NEWTON:89;
then x in H₂(a) by A10, A12;
hence x in H₂(a) \/ {H₁(a + 1)} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose t = a + 1 ; :: thesis: x in H₂(a) \/ {H₁(a + 1)}

then x in {H₁(a + 1)} by A10, A12, TARSKI:def 1;
hence x in H₂(a) \/ {H₁(a + 1)} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H₂(a) \/ {H₁(a + 1)} or x in H₂(a + 1) )
assume x in H₂(a) \/ {H₁(a + 1)} ; :: thesis: x in H₂(a + 1)

per cases then ( x in H₂(a) or x in {H₁(a + 1)} ) by XBOOLE_0:def 3;

suppose x in H₂(a) ; :: thesis: x in H₂(a + 1)

then consider m being Nat such that
A14: ( x = m & m divides H₁(a) ) ;
a <= a + 1 by NAT_1:16;
then H₁(a) divides H₁(a + 1) by NEWTON:89;
then ex m being Nat st
( x = m & m divides H₁(a + 1) ) by A14, INT_2:9;
hence x in H₂(a + 1) ; :: thesis: verum

end;

suppose x in {H₁(a + 1)} ; :: thesis: x in H₂(a + 1)

then x = H₁(a + 1) by TARSKI:def 1;
hence x in H₂(a + 1) ; :: thesis: verum

end;

end;

end;

hence S₁[a + 1] by A7, A8, CARD_2:41; :: thesis: verum

end;

for a being Nat holds S₁[a] from NAT_1:sch 2(A2, A6);
hence card { k where k is Nat : k divides 5 |^ n } = n + 1 ; :: thesis: verum