environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, INT_2, ARYTM_3, RELAT_1, NAT_1, CARD_1, XXREAL_0, PRE_FF, FUNCT_3, SQUARE_1, ARYTM_1, COMPLEX1, POWER, NEWTON, SEQ_1, VALUED_0, VALUED_1, FUNCT_1, SEQ_2, ORDINAL2, XXREAL_2, FIB_NUM, REAL_1;
notations HIDDEN, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, NAT_D, INT_2, VALUED_0, VALUED_1, SEQ_1, XXREAL_0, COMPLEX1, PRE_FF, COMSEQ_2, SEQ_2, QUIN_1, NEWTON, POWER;
definitions ;
theorems NAT_1, PRE_FF, INT_2, SQUARE_1, WSIERP_1, EULER_1, PYTHTRIP, QUIN_1, ABSVALUE, POWER, NEWTON, SEQM_3, SEQ_1, SEQ_2, SEQ_4, PREPOWER, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, FUNCT_2, ORDINAL1, NAT_D, VALUED_1, VALUED_0, XREAL_0, TARSKI;
schemes NAT_1, SEQ_1;
registrations RELSET_1, XREAL_0, SQUARE_1, MEMBERED, QUIN_1, NEWTON, INT_1, VALUED_0, VALUED_1, FUNCT_2, NUMBERS, SEQ_4, NAT_1, SEQ_2, ORDINAL1, FDIFF_1;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, NAT_D, QUIN_1, SEQ_2, SEQM_3, LIMFUNC1, NEWTON, POWER, PRE_FF, VALUED_1, PARTFUN1, SETFAM_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, NUMBERS;
requirements HIDDEN, SUBSET, NUMERALS, REAL, ARITHM, BOOLE;
equalities SQUARE_1, VALUED_1, XCMPLX_0;
expansions ;
scheme
FibInd{
P1[
set ] } :
for
k being
Nat holds
P1[
k]
provided
A1:
P1[
0 ]
and A2:
P1[1]
and A3:
for
k being
Nat st
P1[
k] &
P1[
k + 1] holds
P1[
k + 2]
(0 + 1) + 1 = 2
;
then Lm1:
Fib 2 = 1
by PRE_FF:1;
Lm2:
(1 + 1) + 1 = 3
;
Lm3:
for k being Nat holds Fib (k + 1) >= k
Lm4:
for m being Nat holds Fib (m + 1) >= Fib m
Lm5:
for m, n being Element of NAT st m >= n holds
Fib m >= Fib n
Lm6:
for m being Element of NAT holds Fib (m + 1) <> 0
Lm7:
for n being Nat holds (Fib n) gcd (Fib (n + 1)) = 1
Lm8:
( tau ^2 = tau + 1 & tau_bar ^2 = tau_bar + 1 )
Lm9:
2 < sqrt 5
by SQUARE_1:20, SQUARE_1:27;
Lm10:
sqrt 5 <> 0
by SQUARE_1:20, SQUARE_1:27;
Lm11:
sqrt 5 < 3
1 < tau
then Lm12:
0 < tau
;
Lm13:
tau_bar < 0
Lm14:
|.tau_bar.| < 1
Lm15:
for n being Element of NAT
for x being Real st |.x.| <= 1 holds
|.(x |^ n).| <= 1
Lm16:
for n being Element of NAT holds |.((tau_bar to_power n) / (sqrt 5)).| < 1