let n be Nat; :: thesis: card { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } = n + 1
deffunc H1( Nat) -> set = 3 |^ $1;
A1: H1( 0 ) = 1 by NEWTON:4;
deffunc H2( Nat) -> set = { H1(m) where m is Nat : ( m is even & m <= (2 * $1) + 1 ) } ;
defpred S1[ Nat] means card H2($1) = $1 + 1;
A2: S1[ 0 ]
proof
H2( 0 ) = {1}
proof
thus H2( 0 ) c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= H2( 0 )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H2( 0 ) or x in {1} )
assume x in H2( 0 ) ; :: thesis: x in {1}
then consider m being Nat such that
A3: x = H1(m) and
A4: m is even and
A5: m <= (2 * 0) + 1 ;
m = 0 by A4, A5, NAT_1:25;
hence x in {1} by A1, A3, TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in H2( 0 ) )
assume x in {1} ; :: thesis: x in H2( 0 )
then x = 1 by TARSKI:def 1;
hence x in H2( 0 ) by A1; :: thesis: verum
end;
hence S1[ 0 ] by CARD_1:30; :: thesis: verum
end;
A6: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; :: thesis: ( S1[a] implies S1[a + 1] )
assume A7: S1[a] ; :: thesis: S1[a + 1]
set K = H1((2 * a) + 2);
defpred S2[ Nat] means $1 is even ;
set X = { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) } ;
A8: { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) } is finite from FINSEQ_1:sch 6();
 { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) } = H2(a)
proof
thus { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) } c= H2(a) :: according to XBOOLE_0:def 10 :: thesis: H2(a) c= { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) } or x in H2(a) )
assume x in { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) } ; :: thesis: x in H2(a)
then ex i being Nat st
( x = H1(i) & i <= (2 * a) + 1 & S2[i] ) ;
hence x in H2(a) ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H2(a) or x in { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) } )
assume x in H2(a) ; :: thesis: x in { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) }
then ex i being Nat st
( x = H1(i) & S2[i] & i <= (2 * a) + 1 ) ;
hence x in { H1(i) where i is Nat : ( i <= (2 * a) + 1 & S2[i] ) } ; :: thesis: verum
end;
then reconsider An = H2(a) as finite set by A8;
A9: now :: thesis: not H1((2 * a) + 2) in An
assume H1((2 * a) + 2) in An ; :: thesis: contradiction
then consider m being Nat such that
A10: H1((2 * a) + 2) = H1(m) and
m is even and
A11: m <= (2 * a) + 1 ;
(2 * a) + 1 < ((2 * a) + 1) + 1 by NAT_1:16;
hence contradiction by A10, A11, PEPIN:30; :: thesis: verum
end;
set b = a + 1;
H2(a + 1) = H2(a) \/ {H1((2 * a) + 2)}
proof
thus H2(a + 1) c= H2(a) \/ {H1((2 * a) + 2)} :: according to XBOOLE_0:def 10 :: thesis: H2(a) \/ {H1((2 * a) + 2)} c= H2(a + 1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H2(a + 1) or x in H2(a) \/ {H1((2 * a) + 2)} )
assume x in H2(a + 1) ; :: thesis: x in H2(a) \/ {H1((2 * a) + 2)}
then consider m being Nat such that
A12: x = H1(m) and
A13: m is even and
A14: m <= (2 * (a + 1)) + 1 ;
per cases ( m <= (2 * a) + 1 or m > (2 * a) + 1 ) ;
suppose m <= (2 * a) + 1 ; :: thesis: x in H2(a) \/ {H1((2 * a) + 2)}
then x in H2(a) by A12, A13;
hence x in H2(a) \/ {H1((2 * a) + 2)} by XBOOLE_0:def 3; :: thesis: verum
end;
suppose m > (2 * a) + 1 ; :: thesis: x in H2(a) \/ {H1((2 * a) + 2)}
then m >= ((2 * a) + 1) + 1 by NAT_1:13;
then not not m = ((2 * a) + 2) + 0 & ... & not m = ((2 * a) + 2) + 1 by A14, NAT_1:62;
then x in {H1((2 * a) + 2)} by A12, A13, TARSKI:def 1;
hence x in H2(a) \/ {H1((2 * a) + 2)} by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H2(a) \/ {H1((2 * a) + 2)} or x in H2(a + 1) )
assume x in H2(a) \/ {H1((2 * a) + 2)} ; :: thesis: x in H2(a + 1)
per cases then ( x in H2(a) or x in {H1((2 * a) + 2)} ) by XBOOLE_0:def 3;
suppose x in H2(a) ; :: thesis: x in H2(a + 1)
then consider m being Nat such that
A15: x = H1(m) and
A16: m is even and
A17: m <= (2 * a) + 1 ;
a <= a + 1 by NAT_1:16;
then 2 * a <= 2 * (a + 1) by XREAL_1:64;
then (2 * a) + 1 <= (2 * (a + 1)) + 1 by XREAL_1:6;
then m <= (2 * (a + 1)) + 1 by A17, XXREAL_0:2;
hence x in H2(a + 1) by A15, A16; :: thesis: verum
end;
suppose x in {H1((2 * a) + 2)} ; :: thesis: x in H2(a + 1)
then A18: x = H1((2 * a) + 2) by TARSKI:def 1;
(2 * a) + 2 <= (2 * (a + 1)) + 1 by NAT_1:16;
hence x in H2(a + 1) by A18; :: thesis: verum
end;
end;
end;
hence S1[a + 1] by A7, A9, CARD_2:41; :: thesis: verum
end;
for a being Nat holds S1[a] from NAT_1:sch 2(A2, A6);
 hence card { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) } = n + 1 ; :: thesis: verum