let f, k be positive Nat; :: thesis: ( f = k ! iff ex j, h, w being Nat ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) ) )
set k2 = 2 * k;
A1: k >= 1 by NAT_1:14;
then A2: ( 2 * k >= 1 * 2 & 2 * k >= 1 * 1 ) by XREAL_1:66;
thus ( f = k ! implies ex j, h, w being Nat ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) ) ) :: thesis: ( ex j, h, w being Nat ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) ) implies f = k ! )

proof

assume A3: f = k ! ; :: thesis: ex j, h, w being Nat ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) )
consider n, i being Nat such that
A4: ( 10 divides n + 1 & ((((2 * k) ^2) * ((2 * k) * ((2 * k) + 2))) * ((n + 1) ^2)) + 1 = i ^2 ) by A2, Th6;
set p = (n + 1) |^ k;
set q = (((n + 1) |^ k) + 1) |^ n;
set z = ((n + 1) |^ k) |^ (k + 1);
set w = ((((n + 1) |^ k) + 1) |^ n) div (((n + 1) |^ k) |^ (k + 1));
A5: (2 * k) |^ k <= n

proof

A6: (2 * k) -' 2 = (2 * k) - 2 by A2, XREAL_1:233;
A7: ((2 * k) - 1) + ((2 * k) |^ ((2 * k) -' 2)) <= n by A2, A4, Th5;

per cases ( k = 1 or k > 1 ) by A1, XXREAL_0:1;

suppose k = 1 ; :: thesis: (2 * k) |^ k <= n

then ( (2 * k) |^ ((2 * k) -' 2) = 1 & (2 * k) |^ k = 2 * k ) by NEWTON:4, A6;
hence (2 * k) |^ k <= n by A7; :: thesis: verum

end;

suppose k > 1 ; :: thesis: (2 * k) |^ k <= n

then k >= 1 + 1 by NAT_1:13;
then k + k >= k + 2 by XREAL_1:6;
then (2 * k) |^ ((2 * k) -' 2) >= (2 * k) |^ k by NAT_6:1, A6, XREAL_1:19;
then ((2 * k) |^ ((2 * k) -' 2)) + ((2 * k) - 1) >= ((2 * k) |^ k) + 0 by XREAL_1:7;
hence (2 * k) |^ k <= n by A7, XXREAL_0:2; :: thesis: verum

end;

end;

end;

n > 0

proof

assume n <= 0 ; :: thesis: contradiction
then n = 0 ;
hence contradiction by A4, INT_2:13; :: thesis: verum

end;

then reconsider n = n as positive Nat ;
n < n + 1 by NAT_1:13;
then A8: n |^ k < (n + 1) |^ k by PREPOWER:10, NAT_1:14;
A9: ((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1)) > 0 by A8, A5, Th11;
((n + 1) |^ k) * (((n + 1) |^ k) |^ k) = ((n + 1) |^ k) |^ (k + 1) by NEWTON:6;
then ( k ! < (((n + 1) |^ k) |^ (k + 1)) / (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1))) & (((n + 1) |^ k) |^ (k + 1)) / (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1))) < (k !) + 1 ) by A8, A5, Th11;
then A10: ( f * (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1))) < ((n + 1) |^ k) |^ (k + 1) & ((n + 1) |^ k) |^ (k + 1) < (f + 1) * (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1))) ) by A3, A9, XREAL_1:77, XREAL_1:79;
then reconsider h = (((n + 1) |^ k) |^ (k + 1)) - (f * (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1)))) as Element of NAT by NAT_1:21;
reconsider h = h as positive Nat by A10, XREAL_1:50;
set j = (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1))) - h;
0 < ((f + 1) * (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1)))) - (((n + 1) |^ k) |^ (k + 1)) by A10, XREAL_1:50;
then reconsider j = (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1))) - h as positive Nat ;
A11: ((2 * k) - 1) + ((2 * k) |^ ((2 * k) -' 2)) > (2 * k) - 1 by XREAL_1:29;
((((n + 1) |^ k) + 1) |^ n) div (((n + 1) |^ k) |^ (k + 1)) > 0

proof

A12: (n + 1) |^ k >= 1 by NAT_1:14;
((2 * k) - 1) + ((2 * k) |^ ((2 * k) -' 2)) <= n by A2, A4, Th5;
then (2 * k) - 1 < n by A11, XXREAL_0:2;
then ((2 * k) - 1) + 1 <= n by INT_1:7;
then ( 1 + k <= k + k & k + k <= n ) by A1, XREAL_1:7;
then ( 1 + k <= n & (n + 1) |^ k < ((n + 1) |^ k) + 1 ) by XXREAL_0:2, NAT_1:13;
then ( ((n + 1) |^ k) to_power (k + 1) <= ((n + 1) |^ k) to_power n & ((n + 1) |^ k) to_power n < (((n + 1) |^ k) + 1) to_power n ) by A12, PRE_FF:8, POWER:37;
then A13: ((n + 1) |^ k) |^ (k + 1) < (((n + 1) |^ k) + 1) |^ n by XXREAL_0:2;
assume ((((n + 1) |^ k) + 1) |^ n) div (((n + 1) |^ k) |^ (k + 1)) <= 0 ; :: thesis: contradiction
then ((((n + 1) |^ k) + 1) |^ n) div (((n + 1) |^ k) |^ (k + 1)) = 0 ;
hence contradiction by A13, NAT_2:12; :: thesis: verum

end;

then reconsider w = ((((n + 1) |^ k) + 1) |^ n) div (((n + 1) |^ k) |^ (k + 1)) as positive Nat ;
take j ; :: thesis: ex h, w being Nat ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) )
take h ; :: thesis: ex w being Nat ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) )
take w ; :: thesis: ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) )
take n ; :: thesis: ex p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) )
take (n + 1) |^ k ; :: thesis: ex q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & (n + 1) |^ k = (n + 1) |^ k & q = (((n + 1) |^ k) + 1) |^ n & z = ((n + 1) |^ k) |^ (k + 1) )
take (((n + 1) |^ k) + 1) |^ n ; :: thesis: ex z being positive Nat st
( (((n + 1) |^ k) + 1) |^ n = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & (n + 1) |^ k = (n + 1) |^ k & (((n + 1) |^ k) + 1) |^ n = (((n + 1) |^ k) + 1) |^ n & z = ((n + 1) |^ k) |^ (k + 1) )
take ((n + 1) |^ k) |^ (k + 1) ; :: thesis: ( (((n + 1) |^ k) + 1) |^ n = ((w * (((n + 1) |^ k) |^ (k + 1))) + h) + j & ((n + 1) |^ k) |^ (k + 1) = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & (n + 1) |^ k = (n + 1) |^ k & (((n + 1) |^ k) + 1) |^ n = (((n + 1) |^ k) + 1) |^ n & ((n + 1) |^ k) |^ (k + 1) = ((n + 1) |^ k) |^ (k + 1) )
(((((2 * k) ^2) * (2 * k)) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square by A4, NEWTON:81;
then (((((2 * k) |^ 2) * (2 * k)) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square by NEWTON:81;
then A14: ((((2 * k) |^ (2 + 1)) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square by NEWTON:6;
(((n + 1) |^ k) + 1) |^ n = ((((((n + 1) |^ k) + 1) |^ n) div (((n + 1) |^ k) |^ (k + 1))) * (((n + 1) |^ k) |^ (k + 1))) + (((((n + 1) |^ k) + 1) |^ n) mod (((n + 1) |^ k) |^ (k + 1))) by NAT_D:2;
then (((n + 1) |^ k) + 1) |^ n = ((w * (((n + 1) |^ k) |^ (k + 1))) + h) + j ;
hence ( (((n + 1) |^ k) + 1) |^ n = ((w * (((n + 1) |^ k) |^ (k + 1))) + h) + j & ((n + 1) |^ k) |^ (k + 1) = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & (n + 1) |^ k = (n + 1) |^ k & (((n + 1) |^ k) + 1) |^ n = (((n + 1) |^ k) + 1) |^ n & ((n + 1) |^ k) |^ (k + 1) = ((n + 1) |^ k) |^ (k + 1) ) by A14; :: thesis: verum

end;

given j, h, w being Nat, n, p, q, z being positive Nat such that A15: q = ((w * z) + h) + j and
A16: z = (f * (h + j)) + h and
A17: ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square and
A18: p = (n + 1) |^ k and
A19: q = (p + 1) |^ n and
A20: z = p |^ (k + 1) ; :: thesis: f = k !
A21: (2 * k) |^ k <= n

proof

A22: (2 * k) -' 2 = (2 * k) - 2 by A2, XREAL_1:233;
((((2 * k) |^ (2 + 1)) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 = (((((2 * k) |^ 2) * (2 * k)) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 by NEWTON:6
.= (((((2 * k) ^2) * (2 * k)) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 by NEWTON:81
.= (((((2 * k) ^2) * (2 * k)) * ((2 * k) + 2)) * ((n + 1) ^2)) + 1 by NEWTON:81 ;
then ex i being Nat st ((((2 * k) ^2) * ((2 * k) * ((2 * k) + 2))) * ((n + 1) ^2)) + 1 = i ^2 by A17, PYTHTRIP:def 3;
then A23: ((2 * k) - 1) + ((2 * k) |^ ((2 * k) -' 2)) <= n by A2, Th5;

per cases ( k = 1 or k > 1 ) by A1, XXREAL_0:1;

suppose k = 1 ; :: thesis: (2 * k) |^ k <= n

then ( (2 * k) |^ ((2 * k) -' 2) = 1 & (2 * k) |^ k = 2 * k ) by NEWTON:4, A22;
hence (2 * k) |^ k <= n by A23; :: thesis: verum

end;

suppose k > 1 ; :: thesis: (2 * k) |^ k <= n

then k >= 1 + 1 by NAT_1:13;
then k + k >= k + 2 by XREAL_1:6;
then (2 * k) |^ ((2 * k) -' 2) >= (2 * k) |^ k by A22, NAT_6:1, XREAL_1:19;
then ((2 * k) |^ ((2 * k) -' 2)) + ((2 * k) - 1) >= ((2 * k) |^ k) + 0 by XREAL_1:7;
hence (2 * k) |^ k <= n by A23, XXREAL_0:2; :: thesis: verum

end;

end;

end;

( j <= h + j & 1 * (h + j) <= f * (h + j) ) by XREAL_1:64, NAT_1:11, NAT_1:14;
then j <= f * (h + j) by XXREAL_0:2;
then A24: h + j <= z by A16, XREAL_1:6;
n < n + 1 by NAT_1:13;
then A25: n |^ k < p by PREPOWER:10, NAT_1:14, A18;
A26: p * (p |^ k) = z by NEWTON:6, A20;
h + j <> z

proof

assume h + j = z ; :: thesis: contradiction
then q = z * (w + 1) by A15;
then q mod z = 0 by NAT_D:13;
hence contradiction by A25, A21, Th11, A19, A20; :: thesis: verum

end;

then A27: h + j < z by A24, XXREAL_0:1;
A28: (w * z) mod z = 0 by NAT_D:13;
( q = (w * z) + (h + j) & z <> 0 ) by A15;
then q mod z = h + j by A27, A28, NAT_D:16;
then A29: ( k ! < z / (h + j) & z / (h + j) < (k !) + 1 ) by A26, A25, A21, Th11, A18, A19, A20;
z <= z + j by NAT_1:11;
then A30: z <= (f + 1) * (h + j) by A16;
( h + j = 0 or h + j > 0 ) ;
then z / (h + j) <= f + 1 by XREAL_1:79, A30;
then k ! < f + 1 by A29, XXREAL_0:2;
then A31: k ! <= f by NAT_1:13;
h + j <> 0 by A16;
then f <= z / (h + j) by XREAL_1:77, A16, NAT_1:11;
then f < (k !) + 1 by A29, XXREAL_0:2;
then f <= k ! by NAT_1:13;
hence f = k ! by A31, XXREAL_0:1; :: thesis: verum