Definition df-rmx 43751

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

Assertion

Ref	Expression
df-rmx	⊢ Xrm = (𝑎 ∈ (ℤ≥‘2), 𝑛 ∈ ℤ ↦ (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))))

Distinct variable group:   𝑛,𝑎,𝑏

Detailed syntax breakdown of Definition df-rmx

Step	Hyp	Ref	Expression
1		crmx 43749	. 2 class Xrm
2		va	. . 3 setvar 𝑎
3		vn	. . 3 setvar 𝑛
4		c2 12323	. . . 4 class 2
5		cuz 12891	. . . 4 class ℤ≥
6	4, 5	cfv 6537	. . 3 class (ℤ≥‘2)
7		cz 12619	. . 3 class ℤ
8	2	cv 1569	. . . . . . 7 class 𝑎
9		cexp 14129	. . . . . . . . . 10 class ↑
10	8, 4, 9	co 7417	. . . . . . . . 9 class (𝑎↑2)
11		c1 11129	. . . . . . . . 9 class 1
12		cmin 11469	. . . . . . . . 9 class −
13	10, 11, 12	co 7417	. . . . . . . 8 class ((𝑎↑2) − 1)
14		csqrt 15324	. . . . . . . 8 class √
15	13, 14	cfv 6537	. . . . . . 7 class (√‘((𝑎↑2) − 1))
16		caddc 11131	. . . . . . 7 class +
17	8, 15, 16	co 7417	. . . . . 6 class (𝑎 + (√‘((𝑎↑2) − 1)))
18	3	cv 1569	. . . . . 6 class 𝑛
19	17, 18, 9	co 7417	. . . . 5 class ((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)
20		vb	. . . . . . 7 setvar 𝑏
21		cn0 12532	. . . . . . . 8 class ℕ0
22	21, 7	cxp 5657	. . . . . . 7 class (ℕ0 × ℤ)
23	20	cv 1569	. . . . . . . . 9 class 𝑏
24		c1st 7988	. . . . . . . . 9 class 1st
25	23, 24	cfv 6537	. . . . . . . 8 class (1st ‘𝑏)
26		c2nd 7989	. . . . . . . . . 10 class 2nd
27	23, 26	cfv 6537	. . . . . . . . 9 class (2nd ‘𝑏)
28		cmul 11133	. . . . . . . . 9 class ·
29	15, 27, 28	co 7417	. . . . . . . 8 class ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))
30	25, 29, 16	co 7417	. . . . . . 7 class ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏)))
31	20, 22, 30	cmpt 5190	. . . . . 6 class (𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))
32	31	ccnv 5658	. . . . 5 class ◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))
33	19, 32	cfv 6537	. . . 4 class (◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))
34	33, 24	cfv 6537	. . 3 class (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)))
35	2, 3, 6, 7, 34	cmpo 7419	. 2 class (𝑎 ∈ (ℤ≥‘2), 𝑛 ∈ ℤ ↦ (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))))
36	1, 35	wceq 1570	1 wff Xrm = (𝑎 ∈ (ℤ≥‘2), 𝑛 ∈ ℤ ↦ (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))))

This definition is used by:  rmxfval  43753  frmx  43762