Definition df-rmy

Description: Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy and rmxyval for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014)

	Ref	Expression
Assertion	df-rmy	$$⊢Y_{\mathrm{rm}}=\left(a\in {\mathbb{Z}}_{\ge 2},n\in \mathbb{Z}⟼2^{nd}\left({\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)}^{-1}\left({\left(a+\sqrt{a^2-1}\right)}^n\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crmy	$$class{Y}_{\mathrm{rm}}$$
1		va	$$setvara$$
2		cuz	$$class{\mathbb{Z}}_{\ge }$$
3		c2	$$class2$$
4	3 2	cfv	$$class{\mathbb{Z}}_{\ge 2}$$
5		vn	$$setvarn$$
6		cz	$$class\mathbb{Z}$$
7		c2nd	$$class{2}^{nd}$$
8		vb	$$setvarb$$
9		cn0	$$class{\mathbb{N}}_0$$
10	9 6	cxp	$$class\left({\mathbb{N}}_0\times \mathbb{Z}\right)$$
11		c1st	$$class{1}^{st}$$
12	8	cv	$$setvarb$$
13	12 11	cfv	$$class{1}^{st}\left(b\right)$$
14		caddc	$$class+$$
15		csqrt	$$class\surd$$
16	1	cv	$$setvara$$
17		cexp	$$class^$$
18	16 3 17	co	$$class{a}^2$$
19		cmin	$$class-$$
20		c1	$$class1$$
21	18 20 19	co	$$class\left(a^2-1\right)$$
22	21 15	cfv	$$class\sqrt{a^2-1}$$
23		cmul	$$class\times$$
24	12 7	cfv	$$class{2}^{nd}\left(b\right)$$
25	22 24 23	co	$$class\sqrt{a^2-1}{2}^{nd}\left(b\right)$$
26	13 25 14	co	$$class\left(1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)$$
27	8 10 26	cmpt	$$class\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)$$
28	27	ccnv	$$class{\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)}^{-1}$$
29	16 22 14	co	$$class\left(a+\sqrt{a^2-1}\right)$$
30	5	cv	$$setvarn$$
31	29 30 17	co	$$class{\left(a+\sqrt{a^2-1}\right)}^n$$
32	31 28	cfv	$$class{\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)}^{-1}\left({\left(a+\sqrt{a^2-1}\right)}^n\right)$$
33	32 7	cfv	$$class{2}^{nd}\left({\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)}^{-1}\left({\left(a+\sqrt{a^2-1}\right)}^n\right)\right)$$
34	1 5 4 6 33	cmpo	$$class\left(a\in {\mathbb{Z}}_{\ge 2},n\in \mathbb{Z}⟼2^{nd}\left({\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)}^{-1}\left({\left(a+\sqrt{a^2-1}\right)}^n\right)\right)\right)$$
35	0 34	wceq	$$wff{Y}_{\mathrm{rm}}=\left(a\in {\mathbb{Z}}_{\ge 2},n\in \mathbb{Z}⟼2^{nd}\left({\left(b\in \left({\mathbb{N}}_0\times \mathbb{Z}\right)⟼1^{st}\left(b\right)+\sqrt{a^2-1}{2}^{nd}\left(b\right)\right)}^{-1}\left({\left(a+\sqrt{a^2-1}\right)}^n\right)\right)\right)$$