defpred S1[ Nat] means for z being Tuple of $1, BOOLEAN st z /. $1 = TRUE holds
Absval z >= 2 to_power ($1 -' 1);
A1: for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[n + 1]
let z be Tuple of n + 1, BOOLEAN ; :: thesis: ( z /. (n + 1) = TRUE implies Absval z >= 2 to_power ((n + 1) -' 1) )
assume A2: z /. (n + 1) = TRUE ; :: thesis: Absval z >= 2 to_power ((n + 1) -' 1)
consider x being Element of n -tuples_on BOOLEAN, a being Element of BOOLEAN such that
A3: z = x ^ <*a*> by FINSEQ_2:117;
A4: n + 1 >= 1 by NAT_1:11;
then (n + 1) - 1 >= 1 - 1 by XREAL_1:9;
then A5: (n + 1) -' 1 = n by XREAL_0:def 2;
len z = n + 1 by CARD_1:def 7;
then A6: z /. (n + 1) = (x ^ <*a*>) . (n + 1) by A3, A4, FINSEQ_4:15
.= a by FINSEQ_2:116 ;
Absval z = (Absval x) + (IFEQ (a,FALSE,0,(2 to_power n))) by A3, BINARITH:20
.= (Absval x) + (2 to_power n) by A2, A6, FUNCOP_1:def 8 ;
hence Absval z >= 2 to_power ((n + 1) -' 1) by A5, NAT_1:11; :: thesis: verum
end;
A7: S1[1]
proof
let z be Tuple of 1, BOOLEAN ; :: thesis: ( z /. 1 = TRUE implies Absval z >= 2 to_power (1 -' 1) )
assume A8: z /. 1 = TRUE ; :: thesis: Absval z >= 2 to_power (1 -' 1)
A9: len z = 1 by CARD_1:def 7;
then z . 1 = z /. 1 by FINSEQ_4:15;
then z = <*TRUE*> by A8, A9, FINSEQ_1:40;
then A10: Absval z = 1 by BINARITH:16;
2 to_power (1 -' 1) = 2 to_power (1 - 1) by XREAL_0:def 2;
hence Absval z >= 2 to_power (1 -' 1) by A10, POWER:24; :: thesis: verum
end;
thus for n being non zero Nat holds S1[n] from NAT_1:sch 10(A7, A1); :: thesis: verum