let n be Nat; :: thesis: ( 5 divides n + 1 or 5 divides n + 7 or 5 divides n + 9 or 5 divides n + 13 or 5 divides n + 15 )
assume that
A1: not 5 divides n + 1 and
A2: not 5 divides n + 7 and
A3: not 5 divides n + 9 and
A4: not 5 divides n + 13 ; :: thesis: 5 divides n + 15
A5: 1 mod 5 = 1 by NAT_D:24;
A6: 2 mod 5 = 2 by NAT_D:24;
A7: 3 mod 5 = 3 by NAT_D:24;
A8: 4 mod 5 = 4 by NAT_D:24;
A9: ((5 * 1) + 2) mod 5 = 2 mod 5 by NAT_D:21;
A10: ((5 * 2) + 3) mod 5 = 3 mod 5 by NAT_D:21;
A11: ((5 * 1) + 4) mod 5 = 4 mod 5 by NAT_D:21;
A12: (5 * 3) mod 5 = 0 by NAT_D:13;
A13: ((n + 1) - 1) mod 5 = (((n + 1) mod 5) - (1 mod 5)) mod 5 by INT_6:7;
A14: (n + 15) mod 5 = ((n mod 5) + (15 mod 5)) mod 5 by NAT_D:66;

per cases ( (n + 1) mod 5 = 1 or (n + 1) mod 5 = 2 or (n + 1) mod 5 = 3 or (n + 1) mod 5 = 4 ) by A1, Lm18;

suppose (n + 1) mod 5 = 1 ; :: thesis: 5 divides n + 15

hence 5 divides n + 15 by A12, A13, A14, INT_1:62; :: thesis: verum

end;

suppose (n + 1) mod 5 = 2 ; :: thesis: 5 divides n + 15

then (n + 9) mod 5 = ((2 - 1) + 4) mod 5 by A13, A5, A8, A11, NAT_D:66
.= 0 by NAT_D:25 ;
hence 5 divides n + 15 by A3, INT_1:62; :: thesis: verum

end;

suppose (n + 1) mod 5 = 3 ; :: thesis: 5 divides n + 15

then (n + 13) mod 5 = ((3 - 1) + 3) mod 5 by A5, A6, A13, A10, NAT_D:66
.= 0 by NAT_D:25 ;
hence 5 divides n + 15 by A4, INT_1:62; :: thesis: verum

end;

suppose (n + 1) mod 5 = 4 ; :: thesis: 5 divides n + 15

then (n + 7) mod 5 = ((4 - 1) + 2) mod 5 by A5, A9, A6, A7, A13, NAT_D:66
.= 0 by NAT_D:25 ;
hence 5 divides n + 15 by A2, INT_1:62; :: thesis: verum

end;

end;