Step | Hyp | Ref
| Expression |
1 | | df-fib 33037 |
. . . 4
β’ Fibci =
(β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) |
2 | 1 | fveq1i 6848 |
. . 3
β’
(Fibciβ(π +
1)) = ((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))))β(π + 1)) |
3 | 2 | a1i 11 |
. 2
β’ (π β β β
(Fibciβ(π + 1)) =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))))β(π + 1))) |
4 | | nn0ex 12426 |
. . . 4
β’
β0 β V |
5 | 4 | a1i 11 |
. . 3
β’ (π β β β
β0 β V) |
6 | | 0nn0 12435 |
. . . . 5
β’ 0 β
β0 |
7 | 6 | a1i 11 |
. . . 4
β’ (π β β β 0 β
β0) |
8 | | 1nn0 12436 |
. . . . 5
β’ 1 β
β0 |
9 | 8 | a1i 11 |
. . . 4
β’ (π β β β 1 β
β0) |
10 | 7, 9 | s2cld 14767 |
. . 3
β’ (π β β β
β¨β01ββ© β Word β0) |
11 | | eqid 2737 |
. . 3
β’ (Word
β0 β© (β‘β―
β
(β€β₯β(β―ββ¨β01ββ©)))) =
(Word β0 β© (β‘β― β
(β€β₯β(β―ββ¨β01ββ©)))) |
12 | | fiblem 33038 |
. . . 4
β’ (π€ β (Word
β0 β© (β‘β―
β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))):(Word β0
β© (β‘β― β
(β€β₯β(β―ββ¨β01ββ©))))βΆβ0 |
13 | 12 | a1i 11 |
. . 3
β’ (π β β β (π€ β (Word
β0 β© (β‘β―
β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))):(Word β0
β© (β‘β― β
(β€β₯β(β―ββ¨β01ββ©))))βΆβ0) |
14 | | eluzp1p1 12798 |
. . . . 5
β’ (π β
(β€β₯β1) β (π + 1) β
(β€β₯β(1 + 1))) |
15 | | nnuz 12813 |
. . . . 5
β’ β =
(β€β₯β1) |
16 | 14, 15 | eleq2s 2856 |
. . . 4
β’ (π β β β (π + 1) β
(β€β₯β(1 + 1))) |
17 | | s2len 14785 |
. . . . . 6
β’
(β―ββ¨β01ββ©) = 2 |
18 | | 1p1e2 12285 |
. . . . . 6
β’ (1 + 1) =
2 |
19 | 17, 18 | eqtr4i 2768 |
. . . . 5
β’
(β―ββ¨β01ββ©) = (1 + 1) |
20 | 19 | fveq2i 6850 |
. . . 4
β’
(β€β₯β(β―ββ¨β01ββ©))
= (β€β₯β(1 + 1)) |
21 | 16, 20 | eleqtrrdi 2849 |
. . 3
β’ (π β β β (π + 1) β
(β€β₯β(β―ββ¨β01ββ©))) |
22 | 5, 10, 11, 13, 21 | sseqp1 33035 |
. 2
β’ (π β β β
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))))β(π + 1)) = ((π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β
1))))β((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1))))) |
23 | | id 22 |
. . . . . . 7
β’ (π€ = π‘ β π€ = π‘) |
24 | | fveq2 6847 |
. . . . . . . 8
β’ (π€ = π‘ β (β―βπ€) = (β―βπ‘)) |
25 | 24 | oveq1d 7377 |
. . . . . . 7
β’ (π€ = π‘ β ((β―βπ€) β 2) = ((β―βπ‘) β 2)) |
26 | 23, 25 | fveq12d 6854 |
. . . . . 6
β’ (π€ = π‘ β (π€β((β―βπ€) β 2)) = (π‘β((β―βπ‘) β 2))) |
27 | 24 | oveq1d 7377 |
. . . . . . 7
β’ (π€ = π‘ β ((β―βπ€) β 1) = ((β―βπ‘) β 1)) |
28 | 23, 27 | fveq12d 6854 |
. . . . . 6
β’ (π€ = π‘ β (π€β((β―βπ€) β 1)) = (π‘β((β―βπ‘) β 1))) |
29 | 26, 28 | oveq12d 7380 |
. . . . 5
β’ (π€ = π‘ β ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))) = ((π‘β((β―βπ‘) β 2)) + (π‘β((β―βπ‘) β 1)))) |
30 | 29 | cbvmptv 5223 |
. . . 4
β’ (π€ β (Word
β0 β© (β‘β―
β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))) = (π‘ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π‘β((β―βπ‘) β 2)) + (π‘β((β―βπ‘) β 1)))) |
31 | 30 | a1i 11 |
. . 3
β’ (π β β β (π€ β (Word
β0 β© (β‘β―
β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))) = (π‘ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π‘β((β―βπ‘) β 2)) + (π‘β((β―βπ‘) β 1))))) |
32 | | simpr 486 |
. . . . 5
β’ ((π β β β§ π‘ =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) β π‘ =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) |
33 | 1 | a1i 11 |
. . . . . 6
β’ ((π β β β§ π‘ =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) β Fibci =
(β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))))) |
34 | 33 | reseq1d 5941 |
. . . . 5
β’ ((π β β β§ π‘ =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) β (Fibci βΎ
(0..^(π + 1))) =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) |
35 | 32, 34 | eqtr4d 2780 |
. . . 4
β’ ((π β β β§ π‘ =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) β π‘ = (Fibci βΎ (0..^(π + 1)))) |
36 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β π‘ = (Fibci βΎ (0..^(π + 1)))) |
37 | 36 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β
(β―βπ‘) =
(β―β(Fibci βΎ (0..^(π + 1))))) |
38 | 5, 10, 11, 13 | sseqf 33032 |
. . . . . . . . . . . . 13
β’ (π β β β
(β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β
1))))):β0βΆβ0) |
39 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β β β Fibci =
(β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1)))))) |
40 | 39 | feq1d 6658 |
. . . . . . . . . . . . 13
β’ (π β β β
(Fibci:β0βΆβ0 β
(β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β
1))))):β0βΆβ0)) |
41 | 38, 40 | mpbird 257 |
. . . . . . . . . . . 12
β’ (π β β β
Fibci:β0βΆβ0) |
42 | | nnnn0 12427 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β0) |
43 | 42, 9 | nn0addcld 12484 |
. . . . . . . . . . . 12
β’ (π β β β (π + 1) β
β0) |
44 | 5, 41, 43 | subiwrdlen 33026 |
. . . . . . . . . . 11
β’ (π β β β
(β―β(Fibci βΎ (0..^(π + 1)))) = (π + 1)) |
45 | 44 | adantr 482 |
. . . . . . . . . 10
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β
(β―β(Fibci βΎ (0..^(π + 1)))) = (π + 1)) |
46 | 37, 45 | eqtrd 2777 |
. . . . . . . . 9
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β
(β―βπ‘) = (π + 1)) |
47 | 46 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β
((β―βπ‘) β
2) = ((π + 1) β
2)) |
48 | | nncn 12168 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
49 | | 1cnd 11157 |
. . . . . . . . . . 11
β’ (π β β β 1 β
β) |
50 | | 2cnd 12238 |
. . . . . . . . . . 11
β’ (π β β β 2 β
β) |
51 | 48, 49, 50 | addsubassd 11539 |
. . . . . . . . . 10
β’ (π β β β ((π + 1) β 2) = (π + (1 β
2))) |
52 | 48, 50, 49 | subsub2d 11548 |
. . . . . . . . . 10
β’ (π β β β (π β (2 β 1)) = (π + (1 β
2))) |
53 | | 2m1e1 12286 |
. . . . . . . . . . . 12
β’ (2
β 1) = 1 |
54 | 53 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (π β (2 β 1)) = (π β 1) |
55 | 54 | a1i 11 |
. . . . . . . . . 10
β’ (π β β β (π β (2 β 1)) = (π β 1)) |
56 | 51, 52, 55 | 3eqtr2d 2783 |
. . . . . . . . 9
β’ (π β β β ((π + 1) β 2) = (π β 1)) |
57 | 56 | adantr 482 |
. . . . . . . 8
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β ((π + 1) β 2) = (π β 1)) |
58 | 47, 57 | eqtrd 2777 |
. . . . . . 7
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β
((β―βπ‘) β
2) = (π β
1)) |
59 | 58 | fveq2d 6851 |
. . . . . 6
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β (π‘β((β―βπ‘) β 2)) = (π‘β(π β 1))) |
60 | 36 | fveq1d 6849 |
. . . . . 6
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β (π‘β(π β 1)) = ((Fibci βΎ (0..^(π + 1)))β(π β 1))) |
61 | | nnm1nn0 12461 |
. . . . . . . . 9
β’ (π β β β (π β 1) β
β0) |
62 | | peano2nn 12172 |
. . . . . . . . 9
β’ (π β β β (π + 1) β
β) |
63 | | nnre 12167 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
64 | | 2re 12234 |
. . . . . . . . . . . . 13
β’ 2 β
β |
65 | 64 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β 2 β
β) |
66 | 63, 65 | readdcld 11191 |
. . . . . . . . . . 11
β’ (π β β β (π + 2) β
β) |
67 | | 1red 11163 |
. . . . . . . . . . 11
β’ (π β β β 1 β
β) |
68 | | 2rp 12927 |
. . . . . . . . . . . . 13
β’ 2 β
β+ |
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β 2 β
β+) |
70 | 63, 69 | ltaddrpd 12997 |
. . . . . . . . . . 11
β’ (π β β β π < (π + 2)) |
71 | 63, 66, 67, 70 | ltsub1dd 11774 |
. . . . . . . . . 10
β’ (π β β β (π β 1) < ((π + 2) β
1)) |
72 | 48, 50, 49 | addsubassd 11539 |
. . . . . . . . . . 11
β’ (π β β β ((π + 2) β 1) = (π + (2 β
1))) |
73 | 53 | oveq2i 7373 |
. . . . . . . . . . 11
β’ (π + (2 β 1)) = (π + 1) |
74 | 72, 73 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π β β β ((π + 2) β 1) = (π + 1)) |
75 | 71, 74 | breqtrd 5136 |
. . . . . . . . 9
β’ (π β β β (π β 1) < (π + 1)) |
76 | | elfzo0 13620 |
. . . . . . . . 9
β’ ((π β 1) β (0..^(π + 1)) β ((π β 1) β
β0 β§ (π + 1) β β β§ (π β 1) < (π + 1))) |
77 | 61, 62, 75, 76 | syl3anbrc 1344 |
. . . . . . . 8
β’ (π β β β (π β 1) β (0..^(π + 1))) |
78 | 77 | adantr 482 |
. . . . . . 7
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β (π β 1) β (0..^(π + 1))) |
79 | | fvres 6866 |
. . . . . . 7
β’ ((π β 1) β (0..^(π + 1)) β ((Fibci βΎ
(0..^(π + 1)))β(π β 1)) =
(Fibciβ(π β
1))) |
80 | 78, 79 | syl 17 |
. . . . . 6
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β ((Fibci βΎ
(0..^(π + 1)))β(π β 1)) =
(Fibciβ(π β
1))) |
81 | 59, 60, 80 | 3eqtrd 2781 |
. . . . 5
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β (π‘β((β―βπ‘) β 2)) =
(Fibciβ(π β
1))) |
82 | 46 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β
((β―βπ‘) β
1) = ((π + 1) β
1)) |
83 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β π β
β) |
84 | 83 | nncnd 12176 |
. . . . . . . . 9
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β π β
β) |
85 | | 1cnd 11157 |
. . . . . . . . 9
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β 1 β
β) |
86 | 84, 85 | pncand 11520 |
. . . . . . . 8
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β ((π + 1) β 1) = π) |
87 | 82, 86 | eqtrd 2777 |
. . . . . . 7
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β
((β―βπ‘) β
1) = π) |
88 | 87 | fveq2d 6851 |
. . . . . 6
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β (π‘β((β―βπ‘) β 1)) = (π‘βπ)) |
89 | 36 | fveq1d 6849 |
. . . . . 6
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β (π‘βπ) = ((Fibci βΎ (0..^(π + 1)))βπ)) |
90 | | nn0fz0 13546 |
. . . . . . . . . 10
β’ (π β β0
β π β (0...π)) |
91 | 42, 90 | sylib 217 |
. . . . . . . . 9
β’ (π β β β π β (0...π)) |
92 | | nnz 12527 |
. . . . . . . . . 10
β’ (π β β β π β
β€) |
93 | | fzval3 13648 |
. . . . . . . . . 10
β’ (π β β€ β
(0...π) = (0..^(π + 1))) |
94 | 92, 93 | syl 17 |
. . . . . . . . 9
β’ (π β β β
(0...π) = (0..^(π + 1))) |
95 | 91, 94 | eleqtrd 2840 |
. . . . . . . 8
β’ (π β β β π β (0..^(π + 1))) |
96 | 95 | adantr 482 |
. . . . . . 7
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β π β (0..^(π + 1))) |
97 | | fvres 6866 |
. . . . . . 7
β’ (π β (0..^(π + 1)) β ((Fibci βΎ (0..^(π + 1)))βπ) = (Fibciβπ)) |
98 | 96, 97 | syl 17 |
. . . . . 6
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β ((Fibci βΎ
(0..^(π + 1)))βπ) = (Fibciβπ)) |
99 | 88, 89, 98 | 3eqtrd 2781 |
. . . . 5
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β (π‘β((β―βπ‘) β 1)) =
(Fibciβπ)) |
100 | 81, 99 | oveq12d 7380 |
. . . 4
β’ ((π β β β§ π‘ = (Fibci βΎ (0..^(π + 1)))) β ((π‘β((β―βπ‘) β 2)) + (π‘β((β―βπ‘) β 1))) =
((Fibciβ(π β
1)) + (Fibciβπ))) |
101 | 35, 100 | syldan 592 |
. . 3
β’ ((π β β β§ π‘ =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) β ((π‘β((β―βπ‘) β 2)) + (π‘β((β―βπ‘) β 1))) =
((Fibciβ(π β
1)) + (Fibciβπ))) |
102 | 39 | reseq1d 5941 |
. . . 4
β’ (π β β β (Fibci
βΎ (0..^(π + 1))) =
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) |
103 | 5, 41, 43 | subiwrd 33025 |
. . . . 5
β’ (π β β β (Fibci
βΎ (0..^(π + 1)))
β Word β0) |
104 | | ovex 7395 |
. . . . . . . . 9
β’
(β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) β V |
105 | 1, 104 | eqeltri 2834 |
. . . . . . . 8
β’ Fibci
β V |
106 | 105 | resex 5990 |
. . . . . . 7
β’ (Fibci
βΎ (0..^(π + 1)))
β V |
107 | 106 | a1i 11 |
. . . . . 6
β’ (π β β β (Fibci
βΎ (0..^(π + 1)))
β V) |
108 | 18 | fveq2i 6850 |
. . . . . . . 8
β’
(β€β₯β(1 + 1)) =
(β€β₯β2) |
109 | 16, 108 | eleqtrdi 2848 |
. . . . . . 7
β’ (π β β β (π + 1) β
(β€β₯β2)) |
110 | 44, 109 | eqeltrd 2838 |
. . . . . 6
β’ (π β β β
(β―β(Fibci βΎ (0..^(π + 1)))) β
(β€β₯β2)) |
111 | | hashf 14245 |
. . . . . . 7
β’
β―:VβΆ(β0 βͺ {+β}) |
112 | | ffn 6673 |
. . . . . . 7
β’
(β―:VβΆ(β0 βͺ {+β}) β β―
Fn V) |
113 | | elpreima 7013 |
. . . . . . 7
β’ (β―
Fn V β ((Fibci βΎ (0..^(π + 1))) β (β‘β― β
(β€β₯β2)) β ((Fibci βΎ (0..^(π + 1))) β V β§
(β―β(Fibci βΎ (0..^(π + 1)))) β
(β€β₯β2)))) |
114 | 111, 112,
113 | mp2b 10 |
. . . . . 6
β’ ((Fibci
βΎ (0..^(π + 1)))
β (β‘β― β
(β€β₯β2)) β ((Fibci βΎ (0..^(π + 1))) β V β§
(β―β(Fibci βΎ (0..^(π + 1)))) β
(β€β₯β2))) |
115 | 107, 110,
114 | sylanbrc 584 |
. . . . 5
β’ (π β β β (Fibci
βΎ (0..^(π + 1)))
β (β‘β― β
(β€β₯β2))) |
116 | 103, 115 | elind 4159 |
. . . 4
β’ (π β β β (Fibci
βΎ (0..^(π + 1)))
β (Word β0 β© (β‘β― β
(β€β₯β2)))) |
117 | 102, 116 | eqeltrrd 2839 |
. . 3
β’ (π β β β
((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1))) β (Word
β0 β© (β‘β―
β (β€β₯β2)))) |
118 | | ovex 7395 |
. . . 4
β’
((Fibciβ(π
β 1)) + (Fibciβπ)) β V |
119 | 118 | a1i 11 |
. . 3
β’ (π β β β
((Fibciβ(π β
1)) + (Fibciβπ))
β V) |
120 | 31, 101, 117, 119 | fvmptd 6960 |
. 2
β’ (π β β β ((π€ β (Word
β0 β© (β‘β―
β (β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β
1))))β((β¨β01ββ©seqstr(π€ β (Word β0 β©
(β‘β― β
(β€β₯β2))) β¦ ((π€β((β―βπ€) β 2)) + (π€β((β―βπ€) β 1))))) βΎ (0..^(π + 1)))) = ((Fibciβ(π β 1)) +
(Fibciβπ))) |
121 | 3, 22, 120 | 3eqtrd 2781 |
1
β’ (π β β β
(Fibciβ(π + 1)) =
((Fibciβ(π β
1)) + (Fibciβπ))) |