((3 * 1) + 1) mod 3 = 1 by NUMBER02:16;
then A1: 1 = 3 gcd (4 mod 3) by NEWTON:51
.= 4 gcd 3 by NAT_D:30 ;
(5 * 3) gcd (5 * 4) = 5 * (3 gcd 4) by PYTHTRIP:8;
hence not 15,20 are_coprime by A1; :: thesis: ( (15 |^ 2) + (20 |^ 2) = 5 |^ 4 & not 7 divides 15 * 20 )
A2: ( 15 |^ 2 = 15 * 15 & 20 |^ 2 = 20 * 20 ) by WSIERP_1:1;
5 |^ 4 = ((5 * 5) * 5) * 5 by POLYEQ_5:3;
hence (15 |^ 2) + (20 |^ 2) = 5 |^ 4 by A2; :: thesis: not 7 divides 15 * 20
15 * 20 = (7 * 42) + 6 ;
then (15 * 20) mod 7 = 6 by NUMBER02:16;
hence not 7 divides 15 * 20 by PEPIN:6; :: thesis: verum