let n be non zero Nat; :: thesis: ex x being non zero Nat st
for i being Nat holds n divides (x |^|^ (i + 1)) + 1
A1: ( n divides 2 * n & 2 divides 2 * n ) ;
set x = (2 * n) - 1;
reconsider x = (2 * n) - 1 as non zero odd Nat ;
take x ; :: thesis: for i being Nat holds n divides (x |^|^ (i + 1)) + 1
let i be Nat; :: thesis: n divides (x |^|^ (i + 1)) + 1
A3: x |^|^ (i + 1) = x |^|^ (Segm (i + 1))
.= x |^|^ (succ (Segm i)) by NAT_1:38
.= exp (x,(x |^|^ i)) by ORDINAL5:14
.= x |^ (x |^|^ i) ;
2 * n divides x - (- 1) ;
then x |^ (x |^|^ i),(- 1) |^ (x |^|^ i) are_congruent_mod 2 * n by GR_CY_3:34, INT_1:def 4;
then x |^|^ (i + 1), - 1 are_congruent_mod 2 * n by A3;
hence n divides (x |^|^ (i + 1)) + 1 by A1, INT_2:9; :: thesis: verum