let a be odd Nat; ( a > 1 implies for s being Nat st s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 holds
( (a |^ s) + 1 > s & (a |^ s) + 1 is double_odd & (a |^ ((a |^ s) + 1)) + 1 is double_odd & (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1 ) )
assume A1:
a > 1
; for s being Nat st s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 holds
( (a |^ s) + 1 > s & (a |^ s) + 1 is double_odd & (a |^ ((a |^ s) + 1)) + 1 is double_odd & (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1 )
let s be Nat; ( s is double_odd & (a |^ s) + 1 is double_odd & s divides (a |^ s) + 1 implies ( (a |^ s) + 1 > s & (a |^ s) + 1 is double_odd & (a |^ ((a |^ s) + 1)) + 1 is double_odd & (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1 ) )
assume that
A2:
s is double_odd
and
A3:
(a |^ s) + 1 is double_odd
and
A4:
s divides (a |^ s) + 1
; ( (a |^ s) + 1 > s & (a |^ s) + 1 is double_odd & (a |^ ((a |^ s) + 1)) + 1 is double_odd & (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1 )
consider j1 being odd Nat such that
A5:
s = 2 * j1
by A2;
consider j2 being odd Nat such that
A6:
(a |^ s) + 1 = 2 * j2
by A3;
consider j3 being Nat such that
A7:
j1 = (2 * j3) + 1
by ABIAN:9;
consider m being Nat such that
A8:
(a |^ s) + 1 = s * m
by A4, NAT_D:def 3;
(a |^ s) + 1 = (2 * j1) * m
by A5, A8;
then
j2 = j1 * m
by A6;
then
m is odd
;
then consider z being Nat such that
A9:
m = (2 * z) + 1
by ABIAN:9;
set s1 = (a |^ s) + 1;
1 + 1 <= a
by A1, NAT_1:13;
then A10:
a |^ s > s
by NEWTON:86;
(a |^ s) + 0 < (a |^ s) + 1
by XREAL_1:8;
hence
(a |^ s) + 1 > s
by A10, XXREAL_0:2; ( (a |^ s) + 1 is double_odd & (a |^ ((a |^ s) + 1)) + 1 is double_odd & (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1 )
thus
(a |^ s) + 1 is double_odd
by A3; ( (a |^ ((a |^ s) + 1)) + 1 is double_odd & (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1 )
set q = ((((4 * j3) * z) + (2 * z)) + (2 * j3)) + 1;
a |^ (2 * (((((4 * j3) * z) + (2 * z)) + (2 * j3)) + 1)) = (a |^ (((((4 * j3) * z) + (2 * z)) + (2 * j3)) + 1)) |^ 2
by NEWTON:9;
hence
(a |^ ((a |^ s) + 1)) + 1 is double_odd
by A5, A7, A8, A9; (a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1
(a |^ s) + 1 divides ((a |^ s) |^ ((2 * z) + 1)) + (1 |^ ((2 * z) + 1))
by NEWTON01:35;
hence
(a |^ s) + 1 divides (a |^ ((a |^ s) + 1)) + 1
by A8, A9, NEWTON:9; verum