Metamath Proof Explorer


Theorem rmyluc2

Description: Lucas sequence property of Y with better output ordering. (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion rmyluc2 ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ( ๐‘ + 1 ) ) = ( ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐‘ ) ) โˆ’ ( ๐ด Yrm ( ๐‘ โˆ’ 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 rmyluc โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ( ๐‘ + 1 ) ) = ( ( 2 ยท ( ( ๐ด Yrm ๐‘ ) ยท ๐ด ) ) โˆ’ ( ๐ด Yrm ( ๐‘ โˆ’ 1 ) ) ) )
2 frmy โŠข Yrm : ( ( โ„คโ‰ฅ โ€˜ 2 ) ร— โ„ค ) โŸถ โ„ค
3 2 fovcl โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ๐‘ ) โˆˆ โ„ค )
4 3 zcnd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ๐‘ ) โˆˆ โ„‚ )
5 eluzelcn โŠข ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐ด โˆˆ โ„‚ )
6 5 adantr โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐ด โˆˆ โ„‚ )
7 4 6 mulcomd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐ด Yrm ๐‘ ) ยท ๐ด ) = ( ๐ด ยท ( ๐ด Yrm ๐‘ ) ) )
8 7 oveq2d โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( 2 ยท ( ( ๐ด Yrm ๐‘ ) ยท ๐ด ) ) = ( 2 ยท ( ๐ด ยท ( ๐ด Yrm ๐‘ ) ) ) )
9 2cnd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ 2 โˆˆ โ„‚ )
10 9 6 4 mulassd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐‘ ) ) = ( 2 ยท ( ๐ด ยท ( ๐ด Yrm ๐‘ ) ) ) )
11 8 10 eqtr4d โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( 2 ยท ( ( ๐ด Yrm ๐‘ ) ยท ๐ด ) ) = ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐‘ ) ) )
12 11 oveq1d โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( 2 ยท ( ( ๐ด Yrm ๐‘ ) ยท ๐ด ) ) โˆ’ ( ๐ด Yrm ( ๐‘ โˆ’ 1 ) ) ) = ( ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐‘ ) ) โˆ’ ( ๐ด Yrm ( ๐‘ โˆ’ 1 ) ) ) )
13 1 12 eqtrd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ( ๐‘ + 1 ) ) = ( ( ( 2 ยท ๐ด ) ยท ( ๐ด Yrm ๐‘ ) ) โˆ’ ( ๐ด Yrm ( ๐‘ โˆ’ 1 ) ) ) )