Definition df-rmx

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

	Ref	Expression
Assertion	df-rmx	$$⊢X_{\mathrm{rm}}=\left(a\in {\mathbb{Z}}_{\ge 2},n\in \mathbb{Z}⟼1^{st}\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		crmx	$$class{X}_{\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		c1st	$$class{1}^{st}$$
8		vb	$$setvarb$$
9		cn0	$$class{\mathbb{N}}_0$$
10	9 6	cxp	$$class\left({\mathbb{N}}_0\times \mathbb{Z}\right)$$
11	8	cv	$$setvarb$$
12	11 7	cfv	$$class{1}^{st}\left(b\right)$$
13		caddc	$$class+$$
14		csqrt	$$class\surd$$
15	1	cv	$$setvara$$
16		cexp	$$class^$$
17	15 3 16	co	$$class{a}^2$$
18		cmin	$$class-$$
19		c1	$$class1$$
20	17 19 18	co	$$class\left(a^2-1\right)$$
21	20 14	cfv	$$class\sqrt{a^2-1}$$
22		cmul	$$class\times$$
23		c2nd	$$class{2}^{nd}$$
24	11 23	cfv	$$class{2}^{nd}\left(b\right)$$
25	21 24 22	co	$$class\sqrt{a^2-1}{2}^{nd}\left(b\right)$$
26	12 25 13	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	15 21 13	co	$$class\left(a+\sqrt{a^2-1}\right)$$
30	5	cv	$$setvarn$$
31	29 30 16	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{1}^{st}\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}⟼1^{st}\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{X}_{\mathrm{rm}}=\left(a\in {\mathbb{Z}}_{\ge 2},n\in \mathbb{Z}⟼1^{st}\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)$$