A1: PrimeDivisors 75 = PrimeDivisors (3 * 25)
.= (PrimeDivisors 3) \/ (PrimeDivisors (5 * 5)) by DivisorsMulti
.= ((PrimeDivisors 3) \/ (PrimeDivisors 3)) \/ (PrimeDivisors 5) by DivSquare
.= (PrimeDivisors 3) \/ ((PrimeDivisors 3) \/ (PrimeDivisors 5)) by XBOOLE_1:4
.= (PrimeDivisors (5 * 3)) \/ (PrimeDivisors 3) by DivisorsMulti
.= (PrimeDivisors (5 * 3)) \/ (PrimeDivisors (3 * 3)) by DivSquare
.= (PrimeDivisors (5 * 3)) \/ (PrimeDivisors (9 * 9)) by DivSquare
.= PrimeDivisors ((5 * 3) * (9 * 9)) by DivisorsMulti
.= PrimeDivisors 1215 ;
PrimeDivisors (75 + 1) = PrimeDivisors ((2 * 2) * 19)
.= (PrimeDivisors (2 * 2)) \/ (PrimeDivisors 19) by DivisorsMulti
.= ((PrimeDivisors 2) \/ (PrimeDivisors 2)) \/ (PrimeDivisors 19) by DivisorsMulti
.= ((PrimeDivisors (2 * 2)) \/ (PrimeDivisors 2)) \/ (PrimeDivisors 19) by DivSquare
.= (PrimeDivisors 19) \/ (PrimeDivisors ((2 * 2) * 2)) by DivisorsMulti
.= (PrimeDivisors 19) \/ (PrimeDivisors (8 * 8)) by DivSquare
.= PrimeDivisors (19 * (8 * 8)) by DivisorsMulti
.= PrimeDivisors (1215 + 1) ;
hence ( PrimeDivisors 75 = PrimeDivisors 1215 & PrimeDivisors (75 + 1) = PrimeDivisors (1215 + 1) ) by A1; :: thesis: verum