Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rmyluc Unicode version

Theorem rmyluc 26932
 Description: The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 26924 and rmy1 26925. Part 3 of equation 2.12 of [JonesMatijasevic] p. 695. JonesMatijasevic uses this theorem to redefine the X and Y sequences to have domain , which simplifies some later theorems. It may shorten the derivation to use this as our initial definition. Incidentally, the X sequence satisfies the exact same recurrence. (Contributed by Stefan O'Rear, 1-Oct-2014.)
Assertion
Ref Expression
rmyluc Yrm Yrm Yrm

Proof of Theorem rmyluc
StepHypRef Expression
1 peano2z 10302 . . . 4
2 frmy 26909 . . . . 5 Yrm
32fovcl 6161 . . . 4 Yrm
41, 3sylan2 461 . . 3 Yrm
54zcnd 10360 . 2 Yrm
6 2cn 10054 . . . 4
72fovcl 6161 . . . . . 6 Yrm
87zcnd 10360 . . . . 5 Yrm
9 eluzelre 10481 . . . . . . 7
109recnd 9098 . . . . . 6
1110adantr 452 . . . . 5
128, 11mulcld 9092 . . . 4 Yrm
13 mulcl 9058 . . . 4 Yrm Yrm
146, 12, 13sylancr 645 . . 3 Yrm
15 peano2zm 10304 . . . . 5
162fovcl 6161 . . . . 5 Yrm
1715, 16sylan2 461 . . . 4 Yrm
1817zcnd 10360 . . 3 Yrm
1914, 18subcld 9395 . 2 Yrm Yrm
20 rmyp1 26928 . . . 4 Yrm Yrm Xrm
21 rmym1 26930 . . . 4 Yrm Yrm Xrm
2220, 21oveq12d 6085 . . 3 Yrm Yrm Yrm Xrm Yrm Xrm
23 frmx 26908 . . . . . 6 Xrm
2423fovcl 6161 . . . . 5 Xrm
2524nn0cnd 10260 . . . 4 Xrm
2612, 25, 12ppncand 9435 . . 3 Yrm Xrm Yrm Xrm Yrm Yrm
2714, 18npcand 9399 . . . 4 Yrm Yrm Yrm Yrm
28122timesd 10194 . . . 4 Yrm Yrm Yrm
2927, 28eqtr2d 2463 . . 3 Yrm Yrm Yrm Yrm Yrm
3022, 26, 293eqtrd 2466 . 2 Yrm Yrm Yrm Yrm Yrm