let a, b, c, n be Nat; ( a >= b & (c |^ n) - (b |^ n) = a |^ n implies ( (c - b) gcd (a |^ n) = c - b & (c - a) gcd (b |^ n) = c - a ) )
assume A1:
( a >= b & (c |^ n) - (b |^ n) = a |^ n )
; ( (c - b) gcd (a |^ n) = c - b & (c - a) gcd (b |^ n) = c - a )
A1a:
c |^ n = (b |^ n) + (a |^ n)
by A1;
then A1c:
c - b >= a - b
by Th6, XREAL_1:9;
a - b >= b - b
by A1, XREAL_1:9;
then A1f:
c - b in NAT
by A1c, INT_1:3;
c - a >= a - a
by A1a, Th6, XREAL_1:9;
then A1i:
c - a in NAT
by INT_1:3;
c - a divides (c |^ n) - (a |^ n)
by Th32;
hence
( (c - b) gcd (a |^ n) = c - b & (c - a) gcd (b |^ n) = c - a )
by A1, A1i, A1f, Th32, NEWTON:49; verum