deffunc H1( Nat) -> Subset of NAT = divisors ((3 |^ ((2 * $1) + 1)),4,1);
deffunc H2( Nat) -> Subset of NAT = divisors ((3 |^ ((2 * $1) + 1)),4,3);
set X = { n where n is Nat : card H1(n) = card H2(n) } ;
card H1( 0 ) = card H2( 0 ) by Th31;
then A1: 0 in { n where n is Nat : card H1(n) = card H2(n) } ;
A2: { n where n is Nat : card H1(n) = card H2(n) } is natural-membered
proof
let x be object ; :: according to MEMBERED:def 6 :: thesis: ( not x in { n where n is Nat : card H1(n) = card H2(n) } or x is natural )
assume x in { n where n is Nat : card H1(n) = card H2(n) } ; :: thesis: x is natural
then ex n being Nat st
( x = n & card H1(n) = card H2(n) ) ;
hence x is natural ; :: thesis: verum
end;
for a being Nat st a in { n where n is Nat : card H1(n) = card H2(n) } holds
ex b being Nat st
( b > a & b in { n where n is Nat : card H1(n) = card H2(n) } )
proof
let a be Nat; :: thesis: ( a in { n where n is Nat : card H1(n) = card H2(n) } implies ex b being Nat st
( b > a & b in { n where n is Nat : card H1(n) = card H2(n) } ) )
assume a in { n where n is Nat : card H1(n) = card H2(n) } ; :: thesis: ex b being Nat st
( b > a & b in { n where n is Nat : card H1(n) = card H2(n) } )
then consider n being Nat such that
A3: a = n and
card H1(n) = card H2(n) ;
take n + 1 ; :: thesis: ( n + 1 > a & n + 1 in { n where n is Nat : card H1(n) = card H2(n) } )
thus n + 1 > a by A3, NAT_1:16; :: thesis: n + 1 in { n where n is Nat : card H1(n) = card H2(n) }
card H1(n + 1) = card H2(n + 1) by Th31;
hence n + 1 in { n where n is Nat : card H1(n) = card H2(n) } ; :: thesis: verum
end;
hence { n where n is Nat : card (divisors ((3 |^ ((2 * n) + 1)),4,1)) = card (divisors ((3 |^ ((2 * n) + 1)),4,3)) } is infinite by A1, A2, NUMBER04:1; :: thesis: verum