Step | Hyp | Ref
| Expression |
1 | | df-fib 30459 |
. . . 4
Fibci seqstr Word
|
2 | 1 | fveq1i 6192 |
. . 3
Fibci
seqstr Word
|
3 | 2 | a1i 11 |
. 2
Fibci seqstr Word
|
4 | | nn0ex 11298 |
. . . 4
|
5 | 4 | a1i 11 |
. . 3
|
6 | | 0nn0 11307 |
. . . . 5
|
7 | 6 | a1i 11 |
. . . 4
|
8 | | 1nn0 11308 |
. . . . 5
|
9 | 8 | a1i 11 |
. . . 4
|
10 | 7, 9 | s2cld 13616 |
. . 3
Word |
11 | | eqid 2622 |
. . 3
Word Word |
12 | | fiblem 30460 |
. . . 4
Word Word |
13 | 12 | a1i 11 |
. . 3
Word Word
|
14 | | eluzp1p1 11713 |
. . . . 5
|
15 | | nnuz 11723 |
. . . . 5
|
16 | 14, 15 | eleq2s 2719 |
. . . 4
|
17 | | s2len 13634 |
. . . . . 6
|
18 | | 1p1e2 11134 |
. . . . . 6
|
19 | 17, 18 | eqtr4i 2647 |
. . . . 5
|
20 | 19 | fveq2i 6194 |
. . . 4
|
21 | 16, 20 | syl6eleqr 2712 |
. . 3
|
22 | 5, 10, 11, 13, 21 | sseqp1 30457 |
. 2
seqstr Word
Word
seqstr Word
..^ |
23 | | id 22 |
. . . . . . 7
|
24 | | fveq2 6191 |
. . . . . . . 8
|
25 | 24 | oveq1d 6665 |
. . . . . . 7
|
26 | 23, 25 | fveq12d 6197 |
. . . . . 6
|
27 | 24 | oveq1d 6665 |
. . . . . . 7
|
28 | 23, 27 | fveq12d 6197 |
. . . . . 6
|
29 | 26, 28 | oveq12d 6668 |
. . . . 5
|
30 | 29 | cbvmptv 4750 |
. . . 4
Word Word
|
31 | 30 | a1i 11 |
. . 3
Word Word |
32 | | simpr 477 |
. . . . 5
seqstr Word
..^ seqstr Word
..^ |
33 | 1 | a1i 11 |
. . . . . 6
seqstr Word
..^ Fibci seqstr Word
|
34 | 33 | reseq1d 5395 |
. . . . 5
seqstr Word
..^ Fibci ..^ seqstr Word
..^ |
35 | 32, 34 | eqtr4d 2659 |
. . . 4
seqstr Word
..^ Fibci ..^ |
36 | | simpr 477 |
. . . . . . . . . . 11
Fibci ..^
Fibci ..^ |
37 | 36 | fveq2d 6195 |
. . . . . . . . . 10
Fibci ..^
Fibci ..^ |
38 | 5, 10, 11, 13 | sseqf 30454 |
. . . . . . . . . . . . 13
seqstr Word
|
39 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
Fibci seqstr Word
|
40 | 39 | feq1d 6030 |
. . . . . . . . . . . . 13
Fibci
seqstr Word
|
41 | 38, 40 | mpbird 247 |
. . . . . . . . . . . 12
Fibci |
42 | | nnnn0 11299 |
. . . . . . . . . . . . 13
|
43 | 42, 9 | nn0addcld 11355 |
. . . . . . . . . . . 12
|
44 | 5, 41, 43 | subiwrdlen 30448 |
. . . . . . . . . . 11
Fibci ..^ |
45 | 44 | adantr 481 |
. . . . . . . . . 10
Fibci ..^
Fibci ..^ |
46 | 37, 45 | eqtrd 2656 |
. . . . . . . . 9
Fibci ..^
|
47 | 46 | oveq1d 6665 |
. . . . . . . 8
Fibci ..^
|
48 | | nncn 11028 |
. . . . . . . . . . 11
|
49 | | 1cnd 10056 |
. . . . . . . . . . 11
|
50 | | 2cnd 11093 |
. . . . . . . . . . 11
|
51 | 48, 49, 50 | addsubassd 10412 |
. . . . . . . . . 10
|
52 | 48, 50, 49 | subsub2d 10421 |
. . . . . . . . . 10
|
53 | | 2m1e1 11135 |
. . . . . . . . . . . 12
|
54 | 53 | oveq2i 6661 |
. . . . . . . . . . 11
|
55 | 54 | a1i 11 |
. . . . . . . . . 10
|
56 | 51, 52, 55 | 3eqtr2d 2662 |
. . . . . . . . 9
|
57 | 56 | adantr 481 |
. . . . . . . 8
Fibci ..^
|
58 | 47, 57 | eqtrd 2656 |
. . . . . . 7
Fibci ..^
|
59 | 58 | fveq2d 6195 |
. . . . . 6
Fibci ..^
|
60 | 36 | fveq1d 6193 |
. . . . . 6
Fibci ..^
Fibci ..^
|
61 | | nnm1nn0 11334 |
. . . . . . . . 9
|
62 | | peano2nn 11032 |
. . . . . . . . 9
|
63 | | nnre 11027 |
. . . . . . . . . . 11
|
64 | | 2re 11090 |
. . . . . . . . . . . . 13
|
65 | 64 | a1i 11 |
. . . . . . . . . . . 12
|
66 | 63, 65 | readdcld 10069 |
. . . . . . . . . . 11
|
67 | | 1red 10055 |
. . . . . . . . . . 11
|
68 | | 2rp 11837 |
. . . . . . . . . . . . 13
|
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
|
70 | 63, 69 | ltaddrpd 11905 |
. . . . . . . . . . 11
|
71 | 63, 66, 67, 70 | ltsub1dd 10639 |
. . . . . . . . . 10
|
72 | 48, 50, 49 | addsubassd 10412 |
. . . . . . . . . . 11
|
73 | 53 | oveq2i 6661 |
. . . . . . . . . . 11
|
74 | 72, 73 | syl6eq 2672 |
. . . . . . . . . 10
|
75 | 71, 74 | breqtrd 4679 |
. . . . . . . . 9
|
76 | | elfzo0 12508 |
. . . . . . . . 9
..^
|
77 | 61, 62, 75, 76 | syl3anbrc 1246 |
. . . . . . . 8
..^ |
78 | 77 | adantr 481 |
. . . . . . 7
Fibci ..^
..^ |
79 | | fvres 6207 |
. . . . . . 7
..^
Fibci ..^ Fibci
|
80 | 78, 79 | syl 17 |
. . . . . 6
Fibci ..^
Fibci ..^ Fibci
|
81 | 59, 60, 80 | 3eqtrd 2660 |
. . . . 5
Fibci ..^
Fibci
|
82 | 46 | oveq1d 6665 |
. . . . . . . 8
Fibci ..^
|
83 | | simpl 473 |
. . . . . . . . . 10
Fibci ..^
|
84 | 83 | nncnd 11036 |
. . . . . . . . 9
Fibci ..^
|
85 | | 1cnd 10056 |
. . . . . . . . 9
Fibci ..^
|
86 | 84, 85 | pncand 10393 |
. . . . . . . 8
Fibci ..^
|
87 | 82, 86 | eqtrd 2656 |
. . . . . . 7
Fibci ..^
|
88 | 87 | fveq2d 6195 |
. . . . . 6
Fibci ..^
|
89 | 36 | fveq1d 6193 |
. . . . . 6
Fibci ..^
Fibci ..^ |
90 | | nn0fz0 12437 |
. . . . . . . . . 10
|
91 | 42, 90 | sylib 208 |
. . . . . . . . 9
|
92 | | nnz 11399 |
. . . . . . . . . 10
|
93 | | fzval3 12536 |
. . . . . . . . . 10
..^ |
94 | 92, 93 | syl 17 |
. . . . . . . . 9
..^ |
95 | 91, 94 | eleqtrd 2703 |
. . . . . . . 8
..^ |
96 | 95 | adantr 481 |
. . . . . . 7
Fibci ..^
..^ |
97 | | fvres 6207 |
. . . . . . 7
..^
Fibci ..^ Fibci |
98 | 96, 97 | syl 17 |
. . . . . 6
Fibci ..^
Fibci ..^ Fibci |
99 | 88, 89, 98 | 3eqtrd 2660 |
. . . . 5
Fibci ..^
Fibci |
100 | 81, 99 | oveq12d 6668 |
. . . 4
Fibci ..^
Fibci Fibci |
101 | 35, 100 | syldan 487 |
. . 3
seqstr Word
..^ Fibci Fibci |
102 | 39 | reseq1d 5395 |
. . . 4
Fibci ..^ seqstr Word
..^ |
103 | 5, 41, 43 | subiwrd 30447 |
. . . . 5
Fibci ..^ Word |
104 | | ovex 6678 |
. . . . . . . . 9
seqstr Word
|
105 | 1, 104 | eqeltri 2697 |
. . . . . . . 8
Fibci |
106 | 105 | resex 5443 |
. . . . . . 7
Fibci ..^ |
107 | 106 | a1i 11 |
. . . . . 6
Fibci ..^ |
108 | 18 | fveq2i 6194 |
. . . . . . . 8
|
109 | 16, 108 | syl6eleq 2711 |
. . . . . . 7
|
110 | 44, 109 | eqeltrd 2701 |
. . . . . 6
Fibci ..^ |
111 | | hashf 13125 |
. . . . . . 7
|
112 | | ffn 6045 |
. . . . . . 7
|
113 | | elpreima 6337 |
. . . . . . 7
Fibci ..^
Fibci ..^ Fibci ..^ |
114 | 111, 112,
113 | mp2b 10 |
. . . . . 6
Fibci ..^
Fibci ..^ Fibci ..^ |
115 | 107, 110,
114 | sylanbrc 698 |
. . . . 5
Fibci ..^ |
116 | 103, 115 | elind 3798 |
. . . 4
Fibci ..^ Word |
117 | 102, 116 | eqeltrrd 2702 |
. . 3
seqstr Word
..^ Word |
118 | | ovex 6678 |
. . . 4
Fibci Fibci |
119 | 118 | a1i 11 |
. . 3
Fibci Fibci |
120 | 31, 101, 117, 119 | fvmptd 6288 |
. 2
Word
seqstr Word
..^ Fibci Fibci |
121 | 3, 22, 120 | 3eqtrd 2660 |
1
Fibci Fibci Fibci |