let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n = 5 * m or n = (5 * m) + 1 or n = (5 * m) + 2 or n = (5 * m) + 3 or n = (5 * m) + 4 )
take n div 5 ; :: thesis: ( n = 5 * (n div 5) or n = (5 * (n div 5)) + 1 or n = (5 * (n div 5)) + 2 or n = (5 * (n div 5)) + 3 or n = (5 * (n div 5)) + 4 )
set l = n mod 5;
A1: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

proof

n mod 5 < 4 + 1 by NAT_D:1;
then A2: n mod 5 <= 3 + 1 by NAT_1:13;

now :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

per cases ( n mod 5 <= 3 or n mod 5 = 3 + 1 ) by A2, NAT_1:8;

suppose A3: n mod 5 <= 3 ; :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

now :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

per cases ( n mod 5 <= 2 or n mod 5 = 2 + 1 ) by A3, NAT_1:8;

suppose A4: n mod 5 <= 2 ; :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

now :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

per cases ( n mod 5 <= 1 or n mod 5 = 1 + 1 ) by A4, NAT_1:8;

suppose A5: n mod 5 <= 1 ; :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

now :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

per cases ( n mod 5 <= 0 or n mod 5 = 0 + 1 ) by A5, NAT_1:8;

suppose n mod 5 <= 0 ; :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) by NAT_1:2; :: thesis: verum

end;

suppose n mod 5 = 0 + 1 ; :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; :: thesis: verum

end;

suppose n mod 5 = 1 + 1 ; :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; :: thesis: verum

end;

suppose n mod 5 = 2 + 1 ; :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; :: thesis: verum

end;

suppose n mod 5 = 3 + 1 ; :: thesis: ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 )

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 5 = 0 or n mod 5 = 1 or n mod 5 = 2 or n mod 5 = 3 or n mod 5 = 4 ) ; :: thesis: verum

end;

n = (5 * (n div 5)) + (n mod 5) by NAT_D:2;
hence ( n = 5 * (n div 5) or n = (5 * (n div 5)) + 1 or n = (5 * (n div 5)) + 2 or n = (5 * (n div 5)) + 3 or n = (5 * (n div 5)) + 4 ) by A1; :: thesis: verum