begin
tt1:
for m, n being natural number holds - m <= m * ((- 1) to_power n)
tt2:
for m, n being natural number holds - (m * ((- 1) to_power n)) >= - m
theorem JakPower36:
theorem JakPower32:
theorem pomoc1:
theorem pomoc2:
albet3:
tau * tau_bar = - 1
albet2:
tau_bar / tau = ((sqrt 5) - 3) / 2
albet4:
tau / tau_bar = ((- 3) - (sqrt 5)) / 2
alfa2:
tau to_power 2 = (3 + (sqrt 5)) / 2
beta2:
tau_bar to_power 2 = (3 - (sqrt 5)) / 2
beta3:
tau_bar to_power 3 = 2 - (sqrt 5)
beta6:
tau_bar to_power 6 = 9 - (4 * (sqrt 5))
theorem hop3:
hop2:
for n being natural number holds ((abs tau_bar ) to_power n) * (1 / (sqrt 5)) > 0
hop4:
for n being natural number holds ((abs tau_bar ) to_power n) * (1 / (sqrt 5)) < 1 / 2
theorem pom1:
theorem pom2:
theorem hop8:
theorem
theorem hopp9:
theorem hopp10:
theorem luc1:
C2:
tau_bar ^2 = (3 - (sqrt 5)) / 2
by beta2, POWER:53;
d3:
sqrt 5 > 0
by SQUARE_1:93;
then
(sqrt 5) + 3 > (- (sqrt 5)) + 3
by XREAL_1:8;
then
((sqrt 5) + 3) / 2 > ((- (sqrt 5)) + 3) / 2
by XREAL_1:76;
then B0:
tau ^2 > tau_bar ^2
by alfa2, C2, POWER:53;
sqrt 5 < sqrt (3 ^2 )
by SQUARE_1:95;
then
sqrt 5 < 3
by SQUARE_1:def 4;
then
(sqrt 5) - 3 < 3 - 3
by XREAL_1:11;
then D2:
((sqrt 5) - 3) / 2 < 0
;
theorem
theorem hop9:
theorem mag1:
theorem mag2:
theorem Lemat11:
begin
theorem
theorem
set s5 = sqrt 5;
d0:
1 < sqrt 5
by SQUARE_1:83, SQUARE_1:95;
1 - (sqrt 5) <> 0
by SQUARE_1:83, SQUARE_1:95;
then
(1 - (sqrt 5)) ^2 > 0
by SQUARE_1:74;
then d1:
(1 - (sqrt 5)) to_power 2 > 0
by POWER:53;
d3:
sqrt 5 > 0
by SQUARE_1:93;
2 * 1 < 2 * (sqrt 5)
by d0, XREAL_1:70;
then
- (2 * (sqrt 5)) < - 2
by XREAL_1:26;
then
(- (2 * (sqrt 5))) + 6 < (- 2) + 6
by XREAL_1:10;
then
(1 - (2 * (sqrt 5))) + 5 < 4
;
then
((1 ^2 ) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2 ) < 4
by SQUARE_1:def 4;
then
(1 - (sqrt 5)) ^2 < 2 ^2
;
then
(1 - (sqrt 5)) ^2 < 2 to_power 2
by POWER:53;
then xx:
(1 - (sqrt 5)) to_power 2 < 2 to_power 2
by POWER:53;
theorem
theorem
theorem Tw13a:
theorem Tw13b:
theorem Wn14:
theorem
theorem
theorem
B2:
sqrt 5 > 0
by SQUARE_1:93;
D1: (sqrt 5) / (((sqrt 5) - 5) * tau ) =
(sqrt 5) / (((sqrt 5) - ((sqrt 5) ^2 )) * tau )
by SQUARE_1:def 4
.=
(sqrt 5) / ((sqrt 5) * ((1 - (sqrt 5)) * tau ))
.=
((sqrt 5) / (sqrt 5)) / ((1 - (sqrt 5)) * tau )
by XCMPLX_1:79
.=
1 / (((1 - (sqrt 5)) * (1 + (sqrt 5))) / 2)
by B2, FIB_NUM:def 1, XCMPLX_1:60
.=
(1 * 2) / ((1 - (sqrt 5)) * (1 + (sqrt 5)))
by XCMPLX_1:78
.=
2 / ((1 ^2 ) - ((sqrt 5) ^2 ))
.=
2 / ((1 ^2 ) - 5)
by SQUARE_1:def 4
.=
- (1 / 2)
;
theorem
tt:
sqrt 5 > 1
by SQUARE_1:83, SQUARE_1:95;
then y2:
( (sqrt 5) - 1 > 1 - 1 & sqrt 5 > 0 )
by XREAL_1:11;
sqrt 5 > 2
by SQUARE_1:85, SQUARE_1:95;
then
- (sqrt 5) < - 2
by XREAL_1:26;
then
(- (sqrt 5)) + 5 < (- 2) + 5
by XREAL_1:8;
then
(- (sqrt 5)) + ((sqrt 5) ^2 ) < 3
by SQUARE_1:def 4;
then
((sqrt 5) * ((sqrt 5) - 1)) / 5 < 3 / 5
by XREAL_1:76;
then
((sqrt 5) - 1) * ((sqrt 5) / 5) < 6 / 10
;
then
((sqrt 5) - 1) * ((sqrt 5) / ((sqrt 5) ^2 )) < 6 / 10
by SQUARE_1:def 4;
then
( ((sqrt 5) - 1) * ((1 * (sqrt 5)) / ((sqrt 5) * (sqrt 5))) < 6 / 10 & sqrt 5 > 0 )
by SQUARE_1:93;
then
((sqrt 5) - 1) * (1 / (sqrt 5)) < 6 / 10
by XCMPLX_1:92;
then Y3:
((sqrt 5) - 1) / (sqrt 5) < 6 / 10
by XCMPLX_1:100;
sqrt ((3 / 2) ^2 ) <= sqrt 5
by SQUARE_1:94;
then
3 / 2 <= sqrt 5
by SQUARE_1:def 4;
then
(3 / 2) * 2 <= (sqrt 5) * 2
by XREAL_1:66;
then g8:
3 / 4 <= (2 * (sqrt 5)) / (2 * 2)
by XREAL_1:74;
r2:
( (sqrt 5) - 1 > 1 - 1 & sqrt 5 > 0 )
by tt, XREAL_1:11;
( (- 1) + (sqrt 5) < 0 + (sqrt 5) & sqrt 5 > 0 )
by SQUARE_1:93, XREAL_1:8;
then
( ((sqrt 5) - 1) / (sqrt 5) < (sqrt 5) / (sqrt 5) & sqrt 5 > 0 )
by XREAL_1:76;
then R3:
((sqrt 5) - 1) / (sqrt 5) < 1
by XCMPLX_1:60;
sqrt 5 < sqrt (3 ^2 )
by SQUARE_1:95;
then
sqrt 5 < 3
by SQUARE_1:def 4;
then
- (sqrt 5) > - 3
by XREAL_1:26;
then rt:
(- (sqrt 5)) + 3 > (- 3) + 3
by XREAL_1:8;
- (sqrt 5) < - 1
by tt, XREAL_1:26;
then
(- (sqrt 5)) + 3 < (- 1) + 3
by XREAL_1:8;
then xx:
(3 - (sqrt 5)) / 2 < 2 / 2
by XREAL_1:76;
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem