deffunc H1( Nat) -> Subset of NAT = divisors ((5 |^ $1),4,1);
deffunc H2( Nat) -> Subset of NAT = divisors ((5 |^ $1),4,3);
set X = { n where n is Nat : card H1(n) > card H2(n) } ;
{ k where k is Nat : k divides 5 |^ 0 } = H1( 0 ) by Th36;
then card H1( 0 ) = 0 + 1 by Th37;
then card H1( 0 ) > card H2( 0 ) by Th38, CARD_1:27;
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 { a where a is Nat : a divides 5 |^ (n + 1) } = (n + 1) + 1 by Th37;
then card H1(n + 1) = (n + 1) + 1 by Th36;
then card H1(n + 1) > card H2(n + 1) by Th38, CARD_1:27;
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 ((5 |^ n),4,1)) > card (divisors ((5 |^ n),4,3)) } is infinite by A1, A2, NUMBER04:1; :: thesis: verum