deffunc H1( Nat) -> Subset of NAT = divisors ($1,4,1);
deffunc H2( Nat) -> Subset of NAT = divisors ($1,4,3);
set A = { n where n is Nat : card H1(3 |^ ((2 * n) + 1)) = card H2(3 |^ ((2 * n) + 1)) } ;
set X = { n where n is Nat : card H1(n) = card H2(n) } ;
set n = 3 |^ ((2 * 0) + 1);
A1: card H1(3 |^ ((2 * 0) + 1)) = 1 by Th29;
card H2(3 |^ ((2 * 0) + 1)) = 1 by Th30;
then A2: 3 |^ ((2 * 0) + 1) in { n where n is Nat : card H1(n) = card H2(n) } by A1;
A3: { 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) } )
take b = 3 |^ ((2 * a) + 1); :: thesis: ( b > a & b in { n where n is Nat : card H1(n) = card H2(n) } )
1 * a <= 2 * a by XREAL_1:64;
then A4: a + 0 < (2 * a) + 1 by XREAL_1:8;
b > (2 * a) + 1 by NEWTON:86;
hence b > a by A4, XXREAL_0:2; :: thesis: b in { n where n is Nat : card H1(n) = card H2(n) }
A5: card H1(b) = a + 1 by Th29;
card H2(b) = a + 1 by Th30;
hence b in { n where n is Nat : card H1(n) = card H2(n) } by A5; :: thesis: verum
end;
hence { n where n is Nat : card (divisors (n,4,1)) = card (divisors (n,4,3)) } is infinite by A2, A3, NUMBER04:1; :: thesis: verum