prove
(`!n. ~((n EXP 2 + n + 1) MOD 5 = 0)`,
GEN_TAC THEN
MP_TAC (MP(SPECL[`n:num`;`5`]DIVISION)(ARITH_RULE`~(5=0)`)) THEN
STRIP_TAC THEN
FIRST_X_ASSUM SUBST1_TAC THEN
MAP_EVERY ABBREV_TAC [`q = n DIV 5`;`r = n MOD 5`] THEN
SIMP_TAC [NUM_RING `(q * 5 + r) EXP 2 + (q * 5 + r) + 1 = ( 5 * q EXP 2 +2 * q * r + q) * 5 + r EXP 2 + r + 1`;MOD_MULT_ADD] THEN
MP_TAC (UNDISCH(ARITH_RULE`r<5==>r=0 \/ r=1 \/ r=2 \/ r=3 \/ r=4`)) THEN
STRIP_TAC THEN
POP_ASSUM SUBST1_TAC THEN ARITH_TAC);;
val it : thm = |- !n. ~((n EXP 2 + n + 1) MOD 5 = 0)
# g `!n. ~((n EXP 2 + n + 1) MOD 5 = 0)` ;;
val it : goalstack = 1 subgoal (1 total)
`!n. ~((n EXP 2 + n + 1) MOD 5 = 0)`
# e( GEN_TAC );;
val it : goalstack = 1 subgoal (1 total)
`~((n EXP 2 + n + 1) MOD 5 = 0)`
# e( MP_TAC (MP(SPECL[`n:num`;`5`]DIVISION)(ARITH_RULE`~(5=0)`)) THEN STRIP_TAC
);;
val it : goalstack = 1 subgoal (1 total)
0 [`n = n DIV 5 * 5 + n MOD 5`]
1 [`n MOD 5 < 5`]
`~((n EXP 2 + n + 1) MOD 5 = 0)`
# e( FIRST_X_ASSUM SUBST1_TAC );;
val it : goalstack = 1 subgoal (1 total)
0 [`n MOD 5 < 5`]
`~(((n DIV 5 * 5 + n MOD 5) EXP 2 + (n DIV 5 * 5 + n MOD 5) + 1) MOD 5 = 0)`
# e( MAP_EVERY ABBREV_TAC [`q = n DIV 5`;`r = n MOD 5`] );;
val it : goalstack = 1 subgoal (1 total)
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
`~(((q * 5 + r) EXP 2 + (q * 5 + r) + 1) MOD 5 = 0)`
# e( SIMP_TAC [NUM_RING `(q * 5 + r) EXP 2 + (q * 5 + r) + 1 = ( 5 * q EXP 2 +2
* q * r + q) * 5 + r EXP 2 + r + 1`;MOD_MULT_ADD] );;
val it : goalstack = 1 subgoal (1 total)
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
# e( MP_TAC (UNDISCH(ARITH_RULE`r<5==>r=0 \/ r=1 \/ r=2 \/ r=3 \/ r=4`)) THEN ST
RIP_TAC );;
val it : goalstack = 5 subgoals (5 total)
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 4`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 3`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 2`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 1`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 0`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
# e( POP_ASSUM SUBST1_TAC THEN ARITH_TAC );;
val it : goalstack = 1 subgoal (4 total)
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 1`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
# e( POP_ASSUM SUBST1_TAC THEN ARITH_TAC );;
val it : goalstack = 1 subgoal (3 total)
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 2`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
# e( POP_ASSUM SUBST1_TAC THEN ARITH_TAC );;
val it : goalstack = 1 subgoal (2 total)
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 3`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
# e( POP_ASSUM SUBST1_TAC THEN ARITH_TAC );;
val it : goalstack = 1 subgoal (1 total)
0 [`r < 5`]
1 [`n DIV 5 = q`]
2 [`n MOD 5 = r`]
3 [`r = 4`]
`~((r EXP 2 + r + 1) MOD 5 = 0)`
# e( POP_ASSUM SUBST1_TAC THEN ARITH_TAC );;
val it : goalstack = No subgoals
