let m be Nat; :: thesis: for p being Prime st p > 5 holds
((p -' 1) !) + 1 <> p |^ m
let p be Prime; :: thesis: ( p > 5 implies ((p -' 1) !) + 1 <> p |^ m )
assume that
A1: p > 5 and
A2: ((p -' 1) !) + 1 = p |^ m ; :: thesis: contradiction
A3: p > 2 by A1, XXREAL_0:2;
then consider k being Nat such that
A4: p = (2 * k) + 1 by ABIAN:9, PEPIN:17;
A5: p > 1 by A1, XXREAL_0:2;
A6: ( p -' 2 = p - 2 & p -' 1 = p - 1 ) by A1, XXREAL_0:2, XREAL_1:233;
( 2 * k = p - 1 & p - 1 > 5 - 1 & 5 - 1 = 2 * 2 ) by A1, A4, XREAL_1:9;
then A7: k > 2 by XREAL_1:64;
A8: (p |^ m) - 1 = (p |^ m) -' 1 by NAT_1:14, XREAL_1:233;
A9: (p -' 1) * (p -' 1) divides (p -' 1) !

proof

A10: ((p -' 2) !) * ((p -' 2) + 1) = ((p -' 2) + 1) ! by NEWTON:15;
1 * k < p - 1 by A4, XREAL_1:68;
then k + 1 <= p - 1 by INT_1:7;
then k <= (p - 1) - 1 by XREAL_1:19;
then 2 * k divides (p -' 2) ! by A7, A6, NUMBER16:37;
hence (p -' 1) * (p -' 1) divides (p -' 1) ! by A4, A6, A10, INT_4:7; :: thesis: verum

end;

A11: m > 0

proof

assume m <= 0 ; :: thesis: contradiction
then m = 0 ;
then ((p -' 1) !) + 1 = 1 by A2, NEWTON:4;
then (p -' 1) ! = 0 ;
hence contradiction ; :: thesis: verum

end;

then A12: m -' 1 = m - 1 by NAT_1:14, XREAL_1:233;
consider t being Nat such that
A13: (p |^ m) -' 1 = (p -' 1) * t by A6, A8, NUMBER01:11, NAT_D:def 3;
A14: p -' 1 divides t by INT_4:7, A9, A13, A2;
A15: p -' 1 divides m

proof

deffunc H₁( Nat) -> set = (p |^ ($1 + 1)) - 1;
consider P being XFinSequence such that
A16: ( len P = m -' 1 & ( for n being Nat st n in m -' 1 holds
P . n = H₁(n) ) ) from AFINSQ_1:sch 2();
rng P c= INT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng P or y in INT )
assume y in rng P ; :: thesis: y in INT
then consider x being object such that
A17: ( x in dom P & y = P . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by A17;
( y = H₁(x) & H₁(x) in INT ) by A16, A17, INT_1:def 1;
hence y in INT ; :: thesis: verum

end;

then reconsider P = P as XFinSequence of INT by RELAT_1:def 19;
A18: for n being Nat st n in dom P holds
p -' 1 divides P . n

proof

let n be Nat; :: thesis: ( n in dom P implies p -' 1 divides P . n )
assume A19: n in dom P ; :: thesis: p -' 1 divides P . n
p -' 1 divides H₁(n) by A6, NUMBER01:11;
hence p -' 1 divides P . n by A19, A16; :: thesis: verum

end;

t = ((p |^ m) -' 1) div (p -' 1) by A13
.= (Sum P) + m by A12, A11, A16, A5, A6, A8, NUMBER01:12 ;
hence p -' 1 divides m by A14, A18, NUMERAL2:16, INT_2:1; :: thesis: verum

end;

p |^ m > ((p -' 1) !) + 1

proof

p -' 1 <= m by A15, A11, INT_2:27;
then A20: p to_power m >= p to_power (p -' 1) by A5, PRE_FF:8;
A21: p - 1 > 2 - 1 by A3, XREAL_1:14;
( p -' 1 < (p -' 1) + 1 & (p -' 1) + 1 = p ) by A6, NAT_1:13;
then p |^ (p -' 1) > (p -' 1) |^ (p -' 1) by A21, PREPOWER:10;
then A22: p |^ m > (p -' 1) |^ (p -' 1) by A20, XXREAL_0:2;
p -' 1 >= 1 + 1 by A21, A6, NAT_1:13;
then (p -' 1) |^ (p -' 1) > (p -' 1) ! by NEWTON02:122;
then (p -' 1) |^ (p -' 1) >= ((p -' 1) !) + 1 by NAT_1:13;
hence p |^ m > ((p -' 1) !) + 1 by A22, XXREAL_0:2; :: thesis: verum

end;

hence contradiction by A2; :: thesis: verum