:: FIB_NUM2 semantic presentation

Show IDV graph for whole article

theorem :: FIB_NUM2:1

Show IDV graph

for n being non empty Nat holds (n -' 1) + 2 = n + 1

proof end;

theorem Th2: :: FIB_NUM2:2

Show IDV graph

for n being odd Integer
for m being non empty real number holds (- m) to_power n = - (m to_power n)

proof end;

theorem Th3: :: FIB_NUM2:3

Show IDV graph

for n being odd Integer holds (- 1) to_power n = - 1

proof end;

theorem Th4: :: FIB_NUM2:4

Show IDV graph

for n being even Integer
for m being non empty real number holds (- m) to_power n = m to_power n

proof end;

theorem Th5: :: FIB_NUM2:5

Show IDV graph

for n being even Integer holds (- 1) to_power n = 1

proof end;

theorem Th6: :: FIB_NUM2:6

Show IDV graph

for m being non empty real number
for n being Integer holds ((- 1) * m) to_power n = ((- 1) to_power n) * (m to_power n)

proof end;

theorem Th7: :: FIB_NUM2:7

Show IDV graph

for k, m being Nat
for a being non empty real number holds a to_power (k + m) = (a to_power k) * (a to_power m)

proof end;

theorem Th8: :: FIB_NUM2:8

Show IDV graph

for n being Nat
for k being non empty real number
for m being odd Integer holds (k to_power m) to_power n = k to_power (m * n)

proof end;

theorem Th9: :: FIB_NUM2:9

Show IDV graph

for n being Nat holds ((- 1) to_power (- n)) ^2 = 1

proof end;

theorem Th10: :: FIB_NUM2:10

Show IDV graph

for k, m being Nat
for a being non empty real number holds (a to_power (- k)) * (a to_power (- m)) = a to_power ((- k) - m)

proof end;

theorem Th11: :: FIB_NUM2:11

Show IDV graph

for n being Nat holds (- 1) to_power (- (2 * n)) = 1

proof end;

theorem Th12: :: FIB_NUM2:12

Show IDV graph

for k being Nat
for a being non empty real number holds (a to_power k) * (a to_power (- k)) = 1

proof end;

registration

let n be odd Integer;
cluster - n -> odd ;
coherence

proof end;

end;

registration

let n be even Integer;
cluster - n -> even ;
coherence

proof end;

end;

theorem Th13: :: FIB_NUM2:13

Show IDV graph

for n being Nat holds (- 1) to_power (- n) = (- 1) to_power n

proof end;

theorem Th14: :: FIB_NUM2:14

Show IDV graph

for n, k, m, m1, n1 being Nat st k divides m & k divides n holds
k divides (m * m1) + (n * n1)

proof end;

registration

cluster non empty finite natural-membered with_non-empty_elements set ;
existence

proof end;

end;

registration

let f be Function of NAT , NAT ;
let A be finite natural-membered with_non-empty_elements set ;
cluster f | A -> FinSubsequence-like ;
coherence

proof end;

end;

theorem Th15: :: FIB_NUM2:15

Show IDV graph

for p being FinSubsequence holds rng (Seq p) c= rng p

proof end;

definition

let f be Function of NAT , NAT ;
let A be finite natural-membered with_non-empty_elements set ;
func Prefix f,A -> FinSequence of NAT equals :: FIB_NUM2:def 1
Seq (f | A);
coherence

proof end;

end;

:: deftheorem defines Prefix FIB_NUM2:def 1 :

theorem Th16: :: FIB_NUM2:16

Show IDV graph

for m, n, k being Nat st k <> 0 & k + m <= n holds
m < n

proof end;

registration

cluster omega -> bounded_below ;
coherence

proof end;

end;

registration

cluster K417(1,2,3) -> natural-membered with_non-empty_elements ;
coherence

proof end;

end;

registration

cluster K418(1,2,3,4) -> natural-membered with_non-empty_elements ;
coherence

proof end;

end;

theorem Th17: :: FIB_NUM2:17

Show IDV graph

for i, j being Nat
for x, y being set st 0 < i & i < j holds
{[i,x],[j,y]} is FinSubsequence

proof end;

theorem Th18: :: FIB_NUM2:18

Show IDV graph

for i, j being Nat
for x, y being set
for q being FinSubsequence st i < j & q = {[i,x],[j,y]} holds
Seq q = <*x,y*>

proof end;

registration

let n be Nat;
cluster Seg n -> with_non-empty_elements ;
coherence

proof end;

end;

registration

let A be with_non-empty_elements set ;
cluster -> with_non-empty_elements Element of K40(A);
coherence

proof end;

end;

registration

let A be with_non-empty_elements set ;
let B be set ;
cluster A /\ B -> with_non-empty_elements ;
coherence

proof end;

cluster B /\ A -> with_non-empty_elements ;
coherence ;

end;

theorem Th19: :: FIB_NUM2:19

Show IDV graph

for k being Nat
for a being set st k >= 1 holds
{[k,a]} is FinSubsequence

proof end;

theorem Th20: :: FIB_NUM2:20

Show IDV graph

for i being Nat
for y being set
for f being FinSubsequence st f = {[1,y]} holds
i Shift f = {[(1 + i),y]}

proof end;

theorem Th21: :: FIB_NUM2:21

Show IDV graph

for q being FinSubsequence
for k, n being Nat st dom q c= Seg k & n > k holds
ex p being FinSequence st
( q c= p & dom p = Seg n )

proof end;

theorem Th22: :: FIB_NUM2:22

Show IDV graph

for q being FinSubsequence ex p being FinSequence st q c= p

proof end;

scheme :: FIB_NUM2:sch 1
FibInd1{ P₁[ Nat] } :

for k being non empty Nat holds P₁[k]

provided

A1: P₁[1] and
A2: P₁[2] and
A3: for k being non empty Nat st P₁[k] & P₁[k + 1] holds
P₁[k + 2]

proof end;

scheme :: FIB_NUM2:sch 2
FibInd2{ P₁[ Nat] } :

for k being non trivial Nat holds P₁[k]

provided

A1: P₁[2] and
A2: P₁[3] and
A3: for k being non trivial Nat st P₁[k] & P₁[k + 1] holds
P₁[k + 2]

proof end;

theorem Th23: :: FIB_NUM2:23

Show IDV graph

Fib 2 = 1

proof end;

theorem Th24: :: FIB_NUM2:24

Show IDV graph

Fib 3 = 2

proof end;

theorem Th25: :: FIB_NUM2:25

Show IDV graph

Fib 4 = 3

proof end;

theorem Th26: :: FIB_NUM2:26

Show IDV graph

for n being Nat holds Fib (n + 2) = (Fib n) + (Fib (n + 1))

proof end;

theorem Th27: :: FIB_NUM2:27

Show IDV graph

for n being Nat holds Fib (n + 3) = (Fib (n + 2)) + (Fib (n + 1))

proof end;

theorem Th28: :: FIB_NUM2:28

Show IDV graph

for n being Nat holds Fib (n + 4) = (Fib (n + 2)) + (Fib (n + 3))

proof end;

theorem Th29: :: FIB_NUM2:29

Show IDV graph

for n being Nat holds Fib (n + 5) = (Fib (n + 3)) + (Fib (n + 4))

proof end;

Lm1: for k being Nat holds Fib ((2 * (k + 2)) + 1) = (Fib ((2 * k) + 3)) + (Fib ((2 * k) + 4))

proof end;

theorem Th30: :: FIB_NUM2:30

Show IDV graph

for n being Nat holds Fib (n + 2) = (Fib (n + 3)) - (Fib (n + 1))

proof end;

theorem Th31: :: FIB_NUM2:31

Show IDV graph

for n being Nat holds Fib (n + 1) = (Fib (n + 2)) - (Fib n)

proof end;

theorem Th32: :: FIB_NUM2:32

Show IDV graph

for n being Nat holds Fib n = (Fib (n + 2)) - (Fib (n + 1))

proof end;

theorem Th33: :: FIB_NUM2:33

Show IDV graph

for n being Nat holds ((Fib n) * (Fib (n + 2))) - ((Fib (n + 1)) ^2 ) = (- 1) |^ (n + 1)

proof end;

theorem :: FIB_NUM2:34

Show IDV graph

for n being non empty Nat holds ((Fib (n -' 1)) * (Fib (n + 1))) - ((Fib n) ^2 ) = (- 1) |^ n

proof end;

theorem Th35: :: FIB_NUM2:35

Show IDV graph

tau > 0

proof end;

theorem Th36: :: FIB_NUM2:36

Show IDV graph

tau_bar = (- tau ) to_power (- 1)

proof end;

theorem Th37: :: FIB_NUM2:37

Show IDV graph

for n being Nat holds (- tau ) to_power ((- 1) * n) = ((- tau ) to_power (- 1)) to_power n

proof end;

theorem Th38: :: FIB_NUM2:38

Show IDV graph

- (1 / tau ) = tau_bar

proof end;

theorem Th39: :: FIB_NUM2:39

Show IDV graph

for r being Nat holds (((tau to_power r) ^2 ) - (2 * ((- 1) to_power r))) + ((tau to_power (- r)) ^2 ) = ((tau to_power r) - (tau_bar to_power r)) ^2

proof end;

theorem :: FIB_NUM2:40

Show IDV graph

for n, r being non empty Nat st r <= n holds
((Fib n) ^2 ) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2 )

proof end;

theorem :: FIB_NUM2:41

Show IDV graph

for n being Nat holds ((Fib n) ^2 ) + ((Fib (n + 1)) ^2 ) = Fib ((2 * n) + 1)

proof end;

theorem Th42: :: FIB_NUM2:42

Show IDV graph

for n being Nat
for k being non empty Nat holds Fib (n + k) = ((Fib k) * (Fib (n + 1))) + ((Fib (k -' 1)) * (Fib n))

proof end;

theorem Th43: :: FIB_NUM2:43

Show IDV graph

for k being Nat
for n being non empty Nat holds Fib n divides Fib (n * k)

proof end;

theorem Th44: :: FIB_NUM2:44

Show IDV graph

for n being Nat
for k being non empty Nat st k divides n holds
Fib k divides Fib n

proof end;

theorem Th45: :: FIB_NUM2:45

Show IDV graph

for n being Nat holds Fib n <= Fib (n + 1)

proof end;

theorem Th46: :: FIB_NUM2:46

Show IDV graph

for n being Nat st n > 1 holds
Fib n < Fib (n + 1)

proof end;

theorem :: FIB_NUM2:47

Show IDV graph

for m, n being Nat st m >= n holds
Fib m >= Fib n

proof end;

theorem Th48: :: FIB_NUM2:48

Show IDV graph

for n, k being Nat st k > 1 & k < n holds
Fib k < Fib n

proof end;

theorem Th49: :: FIB_NUM2:49

Show IDV graph

for k being Nat holds
( Fib k = 1 iff ( k = 1 or k = 2 ) )

proof end;

theorem Th50: :: FIB_NUM2:50

Show IDV graph

for k, n being Nat st n > 1 & k <> 0 & k <> 1 & ( ( k <> 1 & n <> 2 ) or ( k <> 2 & n <> 1 ) ) holds
( Fib k = Fib n iff k = n )

proof end;

theorem Th51: :: FIB_NUM2:51

Show IDV graph

for n being Nat st n > 1 & n <> 4 & not n is prime holds
ex k being non empty Nat st
( k <> 1 & k <> 2 & k <> n & k divides n )

proof end;

theorem :: FIB_NUM2:52

Show IDV graph

for n being Nat st n > 1 & n <> 4 & Fib n is prime holds
n is prime

proof end;

definition

func FIB -> Function of NAT , NAT means :Def2: :: FIB_NUM2:def 2
for k being Nat holds it . k = Fib k;
existence

proof end;

proof end;

end;

:: deftheorem Def2 defines FIB FIB_NUM2:def 2 :

definition

func EvenNAT -> Subset of NAT equals :: FIB_NUM2:def 3
{ (2 * k) where k is Nat : verum } ;
coherence

proof end;

func OddNAT -> Subset of NAT equals :: FIB_NUM2:def 4
{ ((2 * k) + 1) where k is Nat : verum } ;
coherence

proof end;

end;

:: deftheorem defines EvenNAT FIB_NUM2:def 3 :

:: deftheorem defines OddNAT FIB_NUM2:def 4 :

theorem Th53: :: FIB_NUM2:53

Show IDV graph

for k being Nat holds
( 2 * k in EvenNAT & not (2 * k) + 1 in EvenNAT )

proof end;

theorem Th54: :: FIB_NUM2:54

Show IDV graph

for k being Nat holds
( (2 * k) + 1 in OddNAT & not 2 * k in OddNAT )

proof end;

definition

let n be Nat;
func EvenFibs n -> FinSequence of NAT equals :: FIB_NUM2:def 5
Prefix FIB ,(EvenNAT /\ (Seg n));
coherence ;
func OddFibs n -> FinSequence of NAT equals :: FIB_NUM2:def 6
Prefix FIB ,(OddNAT /\ (Seg n));
coherence ;

end;

:: deftheorem defines EvenFibs FIB_NUM2:def 5 :

:: deftheorem defines OddFibs FIB_NUM2:def 6 :

theorem Th55: :: FIB_NUM2:55

Show IDV graph

EvenFibs 0 = {}

proof end;

theorem :: FIB_NUM2:56

Show IDV graph

Seq (FIB | {2}) = <*1*>

proof end;

theorem Th57: :: FIB_NUM2:57

Show IDV graph

EvenFibs 2 = <*1*>

proof end;

theorem :: FIB_NUM2:58

Show IDV graph

EvenFibs 4 = <*1,3*>

proof end;

theorem Th59: :: FIB_NUM2:59

Show IDV graph

for k being Nat holds (EvenNAT /\ (Seg ((2 * k) + 2))) \/ {((2 * k) + 4)} = EvenNAT /\ (Seg ((2 * k) + 4))

proof end;

theorem Th60: :: FIB_NUM2:60

Show IDV graph

for k being Nat holds (FIB | (EvenNAT /\ (Seg ((2 * k) + 2)))) \/ {[((2 * k) + 4),(FIB . ((2 * k) + 4))]} = FIB | (EvenNAT /\ (Seg ((2 * k) + 4)))

proof end;

theorem Th61: :: FIB_NUM2:61

Show IDV graph

for n being Nat holds EvenFibs ((2 * n) + 2) = (EvenFibs (2 * n)) ^ <*(Fib ((2 * n) + 2))*>

proof end;

theorem Th62: :: FIB_NUM2:62

Show IDV graph

OddFibs 1 = <*1*>

proof end;

theorem Th63: :: FIB_NUM2:63

Show IDV graph

OddFibs 3 = <*1,2*>

proof end;

theorem Th64: :: FIB_NUM2:64

Show IDV graph

for k being Nat holds (OddNAT /\ (Seg ((2 * k) + 3))) \/ {((2 * k) + 5)} = OddNAT /\ (Seg ((2 * k) + 5))

proof end;

theorem Th65: :: FIB_NUM2:65

Show IDV graph

for k being Nat holds (FIB | (OddNAT /\ (Seg ((2 * k) + 3)))) \/ {[((2 * k) + 5),(FIB . ((2 * k) + 5))]} = FIB | (OddNAT /\ (Seg ((2 * k) + 5)))

proof end;

theorem Th66: :: FIB_NUM2:66

Show IDV graph

for n being Nat holds OddFibs ((2 * n) + 3) = (OddFibs ((2 * n) + 1)) ^ <*(Fib ((2 * n) + 3))*>

proof end;

theorem :: FIB_NUM2:67

Show IDV graph

for n being Nat holds Sum (EvenFibs ((2 * n) + 2)) = (Fib ((2 * n) + 3)) - 1

proof end;

theorem :: FIB_NUM2:68

Show IDV graph

for n being Nat holds Sum (OddFibs ((2 * n) + 1)) = Fib ((2 * n) + 2)

proof end;

theorem Th69: :: FIB_NUM2:69

Show IDV graph

for n being Nat holds Fib n, Fib (n + 1) are_relative_prime

proof end;

theorem Th70: :: FIB_NUM2:70

Show IDV graph

for n being non empty Nat
for m being Nat st m <> 1 & m divides Fib n holds
not m divides Fib (n -' 1)

proof end;

theorem :: FIB_NUM2:71

Show IDV graph

for m being Nat
for n being non empty Nat st m is prime & n is prime & m divides Fib n holds
for r being Nat st r < n & r <> 0 holds
not m divides Fib r

proof end;

theorem :: FIB_NUM2:72

Show IDV graph

for n being non empty Nat holds {((Fib n) * (Fib (n + 3))),((2 * (Fib (n + 1))) * (Fib (n + 2))),(((Fib (n + 1)) ^2 ) + ((Fib (n + 2)) ^2 ))} is Pythagorean_triple

proof end;