let n be Nat; :: thesis: divisors ((3 |^ ((2 * n) + 1)),4,1) = { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) }
set A = divisors ((3 |^ ((2 * n) + 1)),4,1);
set B = { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } ;
thus divisors ((3 |^ ((2 * n) + 1)),4,1) c= { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } :: according to XBOOLE_0:def 10 :: thesis: { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } c= divisors ((3 |^ ((2 * n) + 1)),4,1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in divisors ((3 |^ ((2 * n) + 1)),4,1) or x in { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } )
assume x in divisors ((3 |^ ((2 * n) + 1)),4,1) ; :: thesis: x in { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) }
then consider k being Nat such that
A1: x = k and
A2: k mod 4 = 1 and
A3: k divides 3 |^ ((2 * n) + 1) ;
consider t being Element of NAT such that
A4: k = 3 |^ t and
A5: t <= (2 * n) + 1 by A3, PEPIN:34, PEPIN:41;
t is even by A2, A4, Th24;
hence x in { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } by A1, A4, A5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } or x in divisors ((3 |^ ((2 * n) + 1)),4,1) )
assume x in { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } ; :: thesis: x in divisors ((3 |^ ((2 * n) + 1)),4,1)
then consider m being Nat such that
A6: x = 3 |^ m and
A7: m is even and
A8: m <= (2 * n) + 1 ;
A9: (3 |^ m) mod 4 = 1 by A7, Th23;
3 |^ m divides 3 |^ ((2 * n) + 1) by A8, NEWTON:89;
hence x in divisors ((3 |^ ((2 * n) + 1)),4,1) by A6, A9; :: thesis: verum