let p be Safe Prime; :: thesis: ( p <> 7 implies p mod 6 = 5 )
assume A1: p <> 7 ; :: thesis: p mod 6 = 5
A2: (4 * p) mod 6 = (2 * (2 * p)) mod (2 * 3)
.= 2 * ((2 * p) mod 3) by INT_4:20
.= 2 * (((2 mod 3) * (p mod 3)) mod 3) by NAT_D:67
.= 2 * ((2 * (p mod 3)) mod 3) by NAT_D:24
.= 2 * ((2 * 2) mod 3) by A1, Th4
.= 2 * ((1 + (3 * 1)) mod 3)
.= 2 * (1 mod 3) by NAT_D:61
.= 2 * 1 by PEPIN:5 ;
A3: (3 * p) mod 6 = (3 * p) mod (3 * 2)
.= 3 * (p mod 2) by INT_4:20
.= 3 * 1 by Th3 ;
p mod 6 = (p + (6 * p)) mod 6 by NAT_D:61
.= ((3 * p) + (4 * p)) mod 6
.= ((3 * 1) + (2 * 1)) mod 6 by A3, A2, NAT_D:66
.= 5 by NAT_D:24 ;
hence p mod 6 = 5 ; :: thesis: verum