2,1 are_coprime ;
then 2,(2 * 2) + 1 are_coprime by NUMBER04:64;
then 5,(5 * 1) + 2 are_coprime by NUMBER04:64;
then 7,(7 * 1) + 5 are_coprime by NUMBER04:64;
then 12,(12 * 1) + 7 are_coprime by NUMBER04:64;
then 19,(19 * 3) + 12 are_coprime by NUMBER04:64;
then 69,(69 * 1) + 19 are_coprime by NUMBER04:64;
then 88,(88 * 6) + 69 are_coprime by NUMBER04:64;
then 597,(597 * 1) + 88 are_coprime by NUMBER04:64;
then 685,(1 * 685) + 597 are_coprime by NUMBER04:64;
then 1282,(1282 * 5225) + 685 are_coprime by NUMBER04:64;
then (6699135 * 1) + 1282,6699135 are_coprime by NUMBER04:64;
then 6699135 + (6700417 * 410880),6700417 are_coprime by NUMBER04:64;
hence ((2 |^ 32) - 1) * 641,6700417 are_coprime by Th28; :: thesis: verum