environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, ZFMISC_1, MCART_1, NAT_1, FUNCT_1, CARD_1, ARYTM_3, INT_1, XXREAL_0, ARYTM_1, RELAT_1, POWER, NEWTON, FINSEQ_1, ORDINAL4, PARTFUN1, PRE_FF, REAL_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, INT_1, NAT_D, MCART_1, DOMAIN_1, POWER, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, NEWTON, FINSEQ_1, FINSEQ_2;
definitions ;
theorems TARSKI, AXIOMS, NAT_1, INT_1, POWER, NEWTON, FINSEQ_1, FINSEQ_4, FINSEQ_3, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, CARD_1, SUBSET_1, ZFMISC_1;
schemes NAT_1, RECDEF_1;
registrations SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, XCMPLX_0, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, XXREAL_0, REAL_1, NAT_1, NAT_D, MEMBERED, PARTFUN1, NEWTON, POWER, RELSET_1, FINSEQ_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions ;
definition
let n be
Nat;
existence
ex b1 being Element of NAT ex fib being sequence of [:NAT,NAT:] st
( b1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) )
uniqueness
for b1, b2 being Element of NAT st ex fib being sequence of [:NAT,NAT:] st
( b1 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) & ex fib being sequence of [:NAT,NAT:] st
( b2 = (fib . n) `1 & fib . 0 = [0,1] & ( for n being Nat holds fib . (n + 1) = [((fib . n) `2),(((fib . n) `1) + ((fib . n) `2))] ) ) holds
b1 = b2
end;
defpred S1[ Nat, FinSequence of NAT , set ] means ( ( for k being Nat st $1 + 2 = 2 * k holds
$3 = $2 ^ <*($2 /. k)*> ) & ( for k being Nat st $1 + 2 = (2 * k) + 1 holds
$3 = $2 ^ <*(($2 /. k) + ($2 /. (k + 1)))*> ) );
Lm1:
for n being Nat
for x being Element of NAT * ex y being Element of NAT * st S1[n,x,y]
defpred S2[ Nat, FinSequence of NAT , set ] means ( ( for k being Element of NAT st $1 + 2 = 2 * k holds
$3 = $2 ^ <*($2 /. k)*> ) & ( for k being Element of NAT st $1 + 2 = (2 * k) + 1 holds
$3 = $2 ^ <*(($2 /. k) + ($2 /. (k + 1)))*> ) );
Lm2:
for n being Nat
for x, y1, y2 being Element of NAT * st S2[n,x,y1] & S2[n,x,y2] holds
y1 = y2
reconsider single1 = <*1*> as Element of NAT * by FINSEQ_1:def 11;
consider fusc being sequence of (NAT *) such that
Lm3:
fusc . 0 = single1
and
Lm4:
for n being Nat holds S1[n,fusc . n,fusc . (n + 1)]
from RECDEF_1:sch 2(Lm1);
Lm5:
for n being Nat holds S1[n,fusc . n,fusc . (n + 1)]
by Lm4;
theorem
for
n being
Nat st
n <> 0 holds
n < 2
* n
theorem
for
n being
Nat holds
n < (2 * n) + 1