dp: 2 is prime by INT_2:28;
tp: 13 is prime by NAT_4:28;
then 2,13 are_coprime by dp, INT_2:30;
then ( (2 |^ (Euler 13)) mod 13 = 1 & 12 = 13 - 1 ) by EULER_2:18;
then (2 |^ 12) mod 13 = 1 by EULER_1:20, tp;
then 2 |^ 12,1 are_congruent_mod 13 by NAT_6:10;
then (2 |^ 12) |^ 5,1 |^ 5 are_congruent_mod 13 by GR_CY_3:34;
then 2 |^ (12 * 5),1 |^ 5 are_congruent_mod 13 by NEWTON:9;
then ds: 2 |^ 60,1 are_congruent_mod 13 by NEWTON:10;
2 |^ 1 = 2 by NEWTON:5;
then 2 |^ (1 + 1) = 2 * 2 by NEWTON:6;
then 2 |^ (2 + 1) = 2 * 4 by NEWTON:6;
then 2 |^ (3 + 1) = 2 * 8 by NEWTON:6;
then 2 |^ (4 + 1) = 2 * 16 by NEWTON:6;
then (2 |^ 5) - 6 = 13 * 2 ;
then 2 |^ 5,6 are_congruent_mod 13 by INT_1:def 5;
then (2 |^ 5) |^ 2,6 |^ 2 are_congruent_mod 13 by GR_CY_3:34;
then 2 |^ (5 * 2),6 |^ 2 are_congruent_mod 13 by NEWTON:9;
then ts: 2 |^ (5 * 2),6 * 6 are_congruent_mod 13 by WSIERP_1:1;
36 - (- 3) = 13 * 3 ;
then 36, - 3 are_congruent_mod 13 by INT_1:def 5;
then 2 |^ 10, - 3 are_congruent_mod 13 by ts, INT_1:15;
then (2 |^ 60) * (2 |^ 10),1 * (- 3) are_congruent_mod 13 by ds, INT_1:18;
then dsi: 2 |^ (60 + 10), - 3 are_congruent_mod 13 by NEWTON:8;
3 |^ (2 + 1) = (3 |^ 2) * 3 by NEWTON:6
.= (3 * 3) * 3 by WSIERP_1:1
.= (2 * 13) + 1 ;
then (3 |^ 3) - 1 = 2 * 13 ;
then 3 |^ 3,1 are_congruent_mod 13 by INT_1:def 5;
then (3 |^ 3) |^ 23,1 |^ 23 are_congruent_mod 13 by GR_CY_3:34;
then 3 |^ (3 * 23),1 |^ 23 are_congruent_mod 13 by NEWTON:9;
then ( 3 |^ 69,1 are_congruent_mod 13 & 3,3 are_congruent_mod 13 ) by NEWTON:10, INT_1:11;
then (3 |^ 69) * 3,1 * 3 are_congruent_mod 13 by INT_1:18;
then 3 |^ (69 + 1),1 * 3 are_congruent_mod 13 by NEWTON:6;
then (2 |^ 70) + (3 |^ 70),(- 3) + 3 are_congruent_mod 13 by dsi, INT_1:16;
then 13 divides ((2 |^ 70) + (3 |^ 70)) - 0 by INT_1:def 4;
hence 13 divides (2 |^ 70) + (3 |^ 70) ; :: thesis: verum