Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fibp1 Structured version   Visualization version   GIF version

Theorem fibp1 33041
Description: Value of the Fibonacci sequence at higher indices. (Contributed by Thierry Arnoux, 25-Apr-2019.)
Assertion
Ref Expression
fibp1 (𝑁 ∈ β„• β†’ (Fibciβ€˜(𝑁 + 1)) = ((Fibciβ€˜(𝑁 βˆ’ 1)) + (Fibciβ€˜π‘)))

Proof of Theorem fibp1
Dummy variables 𝑀 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-fib 33037 . . . 4 Fibci = (βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1)))))
21fveq1i 6848 . . 3 (Fibciβ€˜(𝑁 + 1)) = ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1)))))β€˜(𝑁 + 1))
32a1i 11 . 2 (𝑁 ∈ β„• β†’ (Fibciβ€˜(𝑁 + 1)) = ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1)))))β€˜(𝑁 + 1)))
4 nn0ex 12426 . . . 4 β„•0 ∈ V
54a1i 11 . . 3 (𝑁 ∈ β„• β†’ β„•0 ∈ V)
6 0nn0 12435 . . . . 5 0 ∈ β„•0
76a1i 11 . . . 4 (𝑁 ∈ β„• β†’ 0 ∈ β„•0)
8 1nn0 12436 . . . . 5 1 ∈ β„•0
98a1i 11 . . . 4 (𝑁 ∈ β„• β†’ 1 ∈ β„•0)
107, 9s2cld 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
1312a1i 11 . . 3 (𝑁 ∈ β„• β†’ (𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1)))):(Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜(β™―β€˜βŸ¨β€œ01β€βŸ©))))βŸΆβ„•0)
14 eluzp1p1 12798 . . . . 5 (𝑁 ∈ (β„€β‰₯β€˜1) β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜(1 + 1)))
15 nnuz 12813 . . . . 5 β„• = (β„€β‰₯β€˜1)
1614, 15eleq2s 2856 . . . 4 (𝑁 ∈ β„• β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜(1 + 1)))
17 s2len 14785 . . . . . 6 (β™―β€˜βŸ¨β€œ01β€βŸ©) = 2
18 1p1e2 12285 . . . . . 6 (1 + 1) = 2
1917, 18eqtr4i 2768 . . . . 5 (β™―β€˜βŸ¨β€œ01β€βŸ©) = (1 + 1)
2019fveq2i 6850 . . . 4 (β„€β‰₯β€˜(β™―β€˜βŸ¨β€œ01β€βŸ©)) = (β„€β‰₯β€˜(1 + 1))
2116, 20eleqtrrdi 2849 . . 3 (𝑁 ∈ β„• β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜(β™―β€˜βŸ¨β€œ01β€βŸ©)))
225, 10, 11, 13, 21sseqp1 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 (𝑀 = 𝑑 β†’ (β™―β€˜π‘€) = (β™―β€˜π‘‘))
2524oveq1d 7377 . . . . . . 7 (𝑀 = 𝑑 β†’ ((β™―β€˜π‘€) βˆ’ 2) = ((β™―β€˜π‘‘) βˆ’ 2))
2623, 25fveq12d 6854 . . . . . 6 (𝑀 = 𝑑 β†’ (π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) = (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 2)))
2724oveq1d 7377 . . . . . . 7 (𝑀 = 𝑑 β†’ ((β™―β€˜π‘€) βˆ’ 1) = ((β™―β€˜π‘‘) βˆ’ 1))
2823, 27fveq12d 6854 . . . . . 6 (𝑀 = 𝑑 β†’ (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1)) = (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 1)))
2926, 28oveq12d 7380 . . . . 5 (𝑀 = 𝑑 β†’ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))) = ((π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 2)) + (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 1))))
3029cbvmptv 5223 . . . 4 (𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1)))) = (𝑑 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 2)) + (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 1))))
3130a1i 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))))
331a1i 11 . . . . . 6 ((𝑁 ∈ β„• ∧ 𝑑 = ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) β†Ύ (0..^(𝑁 + 1)))) β†’ Fibci = (βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))))
3433reseq1d 5941 . . . . 5 ((𝑁 ∈ β„• ∧ 𝑑 = ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) β†Ύ (0..^(𝑁 + 1)))) β†’ (Fibci β†Ύ (0..^(𝑁 + 1))) = ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) β†Ύ (0..^(𝑁 + 1))))
3532, 34eqtr4d 2780 . . . 4 ((𝑁 ∈ β„• ∧ 𝑑 = ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) β†Ύ (0..^(𝑁 + 1)))) β†’ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1))))
36 simpr 486 . . . . . . . . . . 11 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1))))
3736fveq2d 6851 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (β™―β€˜π‘‘) = (β™―β€˜(Fibci β†Ύ (0..^(𝑁 + 1)))))
385, 10, 11, 13sseqf 33032 . . . . . . . . . . . . 13 (𝑁 ∈ β„• β†’ (βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))):β„•0βŸΆβ„•0)
391a1i 11 . . . . . . . . . . . . . 14 (𝑁 ∈ β„• β†’ Fibci = (βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))))
4039feq1d 6658 . . . . . . . . . . . . 13 (𝑁 ∈ β„• β†’ (Fibci:β„•0βŸΆβ„•0 ↔ (βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))):β„•0βŸΆβ„•0))
4138, 40mpbird 257 . . . . . . . . . . . 12 (𝑁 ∈ β„• β†’ Fibci:β„•0βŸΆβ„•0)
42 nnnn0 12427 . . . . . . . . . . . . 13 (𝑁 ∈ β„• β†’ 𝑁 ∈ β„•0)
4342, 9nn0addcld 12484 . . . . . . . . . . . 12 (𝑁 ∈ β„• β†’ (𝑁 + 1) ∈ β„•0)
445, 41, 43subiwrdlen 33026 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ (β™―β€˜(Fibci β†Ύ (0..^(𝑁 + 1)))) = (𝑁 + 1))
4544adantr 482 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (β™―β€˜(Fibci β†Ύ (0..^(𝑁 + 1)))) = (𝑁 + 1))
4637, 45eqtrd 2777 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (β™―β€˜π‘‘) = (𝑁 + 1))
4746oveq1d 7377 . . . . . . . 8 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((β™―β€˜π‘‘) βˆ’ 2) = ((𝑁 + 1) βˆ’ 2))
48 nncn 12168 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ 𝑁 ∈ β„‚)
49 1cnd 11157 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ 1 ∈ β„‚)
50 2cnd 12238 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ 2 ∈ β„‚)
5148, 49, 50addsubassd 11539 . . . . . . . . . 10 (𝑁 ∈ β„• β†’ ((𝑁 + 1) βˆ’ 2) = (𝑁 + (1 βˆ’ 2)))
5248, 50, 49subsub2d 11548 . . . . . . . . . 10 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ (2 βˆ’ 1)) = (𝑁 + (1 βˆ’ 2)))
53 2m1e1 12286 . . . . . . . . . . . 12 (2 βˆ’ 1) = 1
5453oveq2i 7373 . . . . . . . . . . 11 (𝑁 βˆ’ (2 βˆ’ 1)) = (𝑁 βˆ’ 1)
5554a1i 11 . . . . . . . . . 10 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ (2 βˆ’ 1)) = (𝑁 βˆ’ 1))
5651, 52, 553eqtr2d 2783 . . . . . . . . 9 (𝑁 ∈ β„• β†’ ((𝑁 + 1) βˆ’ 2) = (𝑁 βˆ’ 1))
5756adantr 482 . . . . . . . 8 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((𝑁 + 1) βˆ’ 2) = (𝑁 βˆ’ 1))
5847, 57eqtrd 2777 . . . . . . 7 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((β™―β€˜π‘‘) βˆ’ 2) = (𝑁 βˆ’ 1))
5958fveq2d 6851 . . . . . 6 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 2)) = (π‘‘β€˜(𝑁 βˆ’ 1)))
6036fveq1d 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 ∈ ℝ
6564a1i 11 . . . . . . . . . . . 12 (𝑁 ∈ β„• β†’ 2 ∈ ℝ)
6663, 65readdcld 11191 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ (𝑁 + 2) ∈ ℝ)
67 1red 11163 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ 1 ∈ ℝ)
68 2rp 12927 . . . . . . . . . . . . 13 2 ∈ ℝ+
6968a1i 11 . . . . . . . . . . . 12 (𝑁 ∈ β„• β†’ 2 ∈ ℝ+)
7063, 69ltaddrpd 12997 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ 𝑁 < (𝑁 + 2))
7163, 66, 67, 70ltsub1dd 11774 . . . . . . . . . 10 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ 1) < ((𝑁 + 2) βˆ’ 1))
7248, 50, 49addsubassd 11539 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ ((𝑁 + 2) βˆ’ 1) = (𝑁 + (2 βˆ’ 1)))
7353oveq2i 7373 . . . . . . . . . . 11 (𝑁 + (2 βˆ’ 1)) = (𝑁 + 1)
7472, 73eqtrdi 2793 . . . . . . . . . 10 (𝑁 ∈ β„• β†’ ((𝑁 + 2) βˆ’ 1) = (𝑁 + 1))
7571, 74breqtrd 5136 . . . . . . . . 9 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ 1) < (𝑁 + 1))
76 elfzo0 13620 . . . . . . . . 9 ((𝑁 βˆ’ 1) ∈ (0..^(𝑁 + 1)) ↔ ((𝑁 βˆ’ 1) ∈ β„•0 ∧ (𝑁 + 1) ∈ β„• ∧ (𝑁 βˆ’ 1) < (𝑁 + 1)))
7761, 62, 75, 76syl3anbrc 1344 . . . . . . . 8 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ 1) ∈ (0..^(𝑁 + 1)))
7877adantr 482 . . . . . . 7 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (𝑁 βˆ’ 1) ∈ (0..^(𝑁 + 1)))
79 fvres 6866 . . . . . . 7 ((𝑁 βˆ’ 1) ∈ (0..^(𝑁 + 1)) β†’ ((Fibci β†Ύ (0..^(𝑁 + 1)))β€˜(𝑁 βˆ’ 1)) = (Fibciβ€˜(𝑁 βˆ’ 1)))
8078, 79syl 17 . . . . . 6 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((Fibci β†Ύ (0..^(𝑁 + 1)))β€˜(𝑁 βˆ’ 1)) = (Fibciβ€˜(𝑁 βˆ’ 1)))
8159, 60, 803eqtrd 2781 . . . . 5 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 2)) = (Fibciβ€˜(𝑁 βˆ’ 1)))
8246oveq1d 7377 . . . . . . . 8 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((β™―β€˜π‘‘) βˆ’ 1) = ((𝑁 + 1) βˆ’ 1))
83 simpl 484 . . . . . . . . . 10 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ 𝑁 ∈ β„•)
8483nncnd 12176 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ 𝑁 ∈ β„‚)
85 1cnd 11157 . . . . . . . . 9 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ 1 ∈ β„‚)
8684, 85pncand 11520 . . . . . . . 8 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
8782, 86eqtrd 2777 . . . . . . 7 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((β™―β€˜π‘‘) βˆ’ 1) = 𝑁)
8887fveq2d 6851 . . . . . 6 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 1)) = (π‘‘β€˜π‘))
8936fveq1d 6849 . . . . . 6 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (π‘‘β€˜π‘) = ((Fibci β†Ύ (0..^(𝑁 + 1)))β€˜π‘))
90 nn0fz0 13546 . . . . . . . . . 10 (𝑁 ∈ β„•0 ↔ 𝑁 ∈ (0...𝑁))
9142, 90sylib 217 . . . . . . . . 9 (𝑁 ∈ β„• β†’ 𝑁 ∈ (0...𝑁))
92 nnz 12527 . . . . . . . . . 10 (𝑁 ∈ β„• β†’ 𝑁 ∈ β„€)
93 fzval3 13648 . . . . . . . . . 10 (𝑁 ∈ β„€ β†’ (0...𝑁) = (0..^(𝑁 + 1)))
9492, 93syl 17 . . . . . . . . 9 (𝑁 ∈ β„• β†’ (0...𝑁) = (0..^(𝑁 + 1)))
9591, 94eleqtrd 2840 . . . . . . . 8 (𝑁 ∈ β„• β†’ 𝑁 ∈ (0..^(𝑁 + 1)))
9695adantr 482 . . . . . . 7 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ 𝑁 ∈ (0..^(𝑁 + 1)))
97 fvres 6866 . . . . . . 7 (𝑁 ∈ (0..^(𝑁 + 1)) β†’ ((Fibci β†Ύ (0..^(𝑁 + 1)))β€˜π‘) = (Fibciβ€˜π‘))
9896, 97syl 17 . . . . . 6 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((Fibci β†Ύ (0..^(𝑁 + 1)))β€˜π‘) = (Fibciβ€˜π‘))
9988, 89, 983eqtrd 2781 . . . . 5 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 1)) = (Fibciβ€˜π‘))
10081, 99oveq12d 7380 . . . 4 ((𝑁 ∈ β„• ∧ 𝑑 = (Fibci β†Ύ (0..^(𝑁 + 1)))) β†’ ((π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 2)) + (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 1))) = ((Fibciβ€˜(𝑁 βˆ’ 1)) + (Fibciβ€˜π‘)))
10135, 100syldan 592 . . 3 ((𝑁 ∈ β„• ∧ 𝑑 = ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) β†Ύ (0..^(𝑁 + 1)))) β†’ ((π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 2)) + (π‘‘β€˜((β™―β€˜π‘‘) βˆ’ 1))) = ((Fibciβ€˜(𝑁 βˆ’ 1)) + (Fibciβ€˜π‘)))
10239reseq1d 5941 . . . 4 (𝑁 ∈ β„• β†’ (Fibci β†Ύ (0..^(𝑁 + 1))) = ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) β†Ύ (0..^(𝑁 + 1))))
1035, 41, 43subiwrd 33025 . . . . 5 (𝑁 ∈ β„• β†’ (Fibci β†Ύ (0..^(𝑁 + 1))) ∈ Word β„•0)
104 ovex 7395 . . . . . . . . 9 (βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) ∈ V
1051, 104eqeltri 2834 . . . . . . . 8 Fibci ∈ V
106105resex 5990 . . . . . . 7 (Fibci β†Ύ (0..^(𝑁 + 1))) ∈ V
107106a1i 11 . . . . . 6 (𝑁 ∈ β„• β†’ (Fibci β†Ύ (0..^(𝑁 + 1))) ∈ V)
10818fveq2i 6850 . . . . . . . 8 (β„€β‰₯β€˜(1 + 1)) = (β„€β‰₯β€˜2)
10916, 108eleqtrdi 2848 . . . . . . 7 (𝑁 ∈ β„• β†’ (𝑁 + 1) ∈ (β„€β‰₯β€˜2))
11044, 109eqeltrd 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))))
114111, 112, 113mp2b 10 . . . . . 6 ((Fibci β†Ύ (0..^(𝑁 + 1))) ∈ (β—‘β™― β€œ (β„€β‰₯β€˜2)) ↔ ((Fibci β†Ύ (0..^(𝑁 + 1))) ∈ V ∧ (β™―β€˜(Fibci β†Ύ (0..^(𝑁 + 1)))) ∈ (β„€β‰₯β€˜2)))
115107, 110, 114sylanbrc 584 . . . . 5 (𝑁 ∈ β„• β†’ (Fibci β†Ύ (0..^(𝑁 + 1))) ∈ (β—‘β™― β€œ (β„€β‰₯β€˜2)))
116103, 115elind 4159 . . . 4 (𝑁 ∈ β„• β†’ (Fibci β†Ύ (0..^(𝑁 + 1))) ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))))
117102, 116eqeltrrd 2839 . . 3 (𝑁 ∈ β„• β†’ ((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) β†Ύ (0..^(𝑁 + 1))) ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))))
118 ovex 7395 . . . 4 ((Fibciβ€˜(𝑁 βˆ’ 1)) + (Fibciβ€˜π‘)) ∈ V
119118a1i 11 . . 3 (𝑁 ∈ β„• β†’ ((Fibciβ€˜(𝑁 βˆ’ 1)) + (Fibciβ€˜π‘)) ∈ V)
12031, 101, 117, 119fvmptd 6960 . 2 (𝑁 ∈ β„• β†’ ((𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))β€˜((βŸ¨β€œ01β€βŸ©seqstr(𝑀 ∈ (Word β„•0 ∩ (β—‘β™― β€œ (β„€β‰₯β€˜2))) ↦ ((π‘€β€˜((β™―β€˜π‘€) βˆ’ 2)) + (π‘€β€˜((β™―β€˜π‘€) βˆ’ 1))))) β†Ύ (0..^(𝑁 + 1)))) = ((Fibciβ€˜(𝑁 βˆ’ 1)) + (Fibciβ€˜π‘)))
1213, 22, 1203eqtrd 2781 1 (𝑁 ∈ β„• β†’ (Fibciβ€˜(𝑁 + 1)) = ((Fibciβ€˜(𝑁 βˆ’ 1)) + (Fibciβ€˜π‘)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3448   βˆͺ cun 3913   ∩ cin 3914  {csn 4591   class class class wbr 5110   ↦ cmpt 5193  β—‘ccnv 5637   β†Ύ cres 5640   β€œ cima 5641   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061  +∞cpnf 11193   < clt 11196   βˆ’ cmin 11392  β„•cn 12160  2c2 12215  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  ...cfz 13431  ..^cfzo 13574  β™―chash 14237  Word cword 14409  βŸ¨β€œcs2 14737  seqstrcsseq 33023  Fibcicfib 33036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fzo 13575  df-seq 13914  df-hash 14238  df-word 14410  df-lsw 14458  df-concat 14466  df-s1 14491  df-substr 14536  df-pfx 14566  df-s2 14744  df-sseq 33024  df-fib 33037
This theorem is referenced by:  fib2  33042  fib3  33043  fib4  33044  fib5  33045  fib6  33046
  Copyright terms: Public domain W3C validator