A1: 2 |^ 2 = 2 |^ (1 + 1)
.= (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 ;
A2: 2 |^ (2 + 2) = 4 * 4 by A1, NEWTON:8;
A3: 2 |^ (4 + 4) = 16 * 16 by A2, NEWTON:8;
A4: 2 |^ (8 + 1) = (2 |^ 8) * (2 |^ 1) by NEWTON:8
.= 256 * 2 by A3 ;
A5: 23 = (2 * 11) + 1 ;
11777 = (23 * (2 |^ 9)) + 1 by A4;
hence 11777 is Proth by A4, A5; :: thesis: verum